feat(GroupWithZero/WithZero): injectivity and monotonicity of WithZero.map' (leanprover-community#25660)

factored out of leanprover-community#22420




Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Author: 2 people

Mathlib/Algebra/Group/WithOne/Defs.lean

@@ -89,6 +89,12 @@ def coe : α → WithOne α :=
 instance instCoeTC : CoeTC α (WithOne α) :=
   ⟨coe⟩
 
+@[to_additive]
+lemma «forall» {p : WithZero α → Prop} : (∀ x, p x) ↔ p 0 ∧ ∀ a : α, p a := Option.forall
+
+@[to_additive]
+lemma «exists» {p : WithZero α → Prop} : (∃ x, p x) ↔ p 0 ∨ ∃ a : α, p a := Option.exists
+
 /-- Recursor for `WithZero` using the preferred forms `0` and `↑a`. -/
 @[elab_as_elim, induction_eliminator, cases_eliminator]
 def _root_.WithZero.recZeroCoe {motive : WithZero α → Sort*} (zero : motive 0)

Mathlib/Algebra/GroupWithZero/WithZero.lean

@@ -22,6 +22,8 @@ This file proves that one can adjoin a new zero element to a group and get a gro
   a monoid homomorphism `f : α →* β`.
 -/
 
+open Function
+
 assert_not_exists DenselyOrdered Ring
 
 namespace WithZero
@@ -139,6 +141,11 @@ lemma map'_map'  (f : α →* β) (g : β →* γ) (x) : map' g (map' f x) = map
 lemma map'_comp (f : α →* β) (g : β →* γ) : map' (g.comp f) = (map' g).comp (map' f) :=
   MonoidWithZeroHom.ext fun x => (map'_map' f g x).symm
 
+lemma map'_injective_iff {f : α →* β} : Injective (map' f) ↔ Injective f := by
+  simp [Injective, WithZero.forall]
+
+alias ⟨_, map'_injective⟩ := map'_injective_iff
+
 end MulOneClass
 
 section Pow

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

@@ -26,7 +26,7 @@ whereas it is a very common target for valuations.
 The solutions is to use a typeclass, and that is exactly what we do in this file.
 -/
 
-variable {α : Type*}
+variable {α β : Type*}
 
 /-- A linearly ordered commutative monoid with a zero element. -/
 class LinearOrderedCommMonoidWithZero (α : Type*) extends CommMonoidWithZero α, LinearOrder α,
@@ -250,14 +250,16 @@ instance [LinearOrderedAddCommGroupWithTop α] :
 
 namespace WithZero
 section Preorder
-variable [Preorder α] {a b : α}
+variable [Preorder α] [Preorder β] {x : WithZero α} {a b : α}
 
 instance instPreorder : Preorder (WithZero α) := WithBot.preorder
 instance instOrderBot : OrderBot (WithZero α) := WithBot.orderBot
 
-lemma zero_le (a : WithZero α) : 0 ≤ a := bot_le
+@[simp] lemma zero_le (a : WithZero α) : 0 ≤ a := bot_le
 
-lemma zero_lt_coe (a : α) : (0 : WithZero α) < a := WithBot.bot_lt_coe a
+@[simp] lemma zero_lt_coe (a : α) : (0 : WithZero α) < a := WithBot.bot_lt_coe a
+@[simp] lemma not_coe_le_zero : ¬ a ≤ (0 : WithZero α) := WithBot.not_coe_le_bot a
+@[simp] lemma not_lt_zero : ¬ x < (0 : WithZero α) := WithBot.not_lt_bot _
 
 lemma zero_eq_bot : (0 : WithZero α) = ⊥ := rfl
 
@@ -318,6 +320,12 @@ instance instExistsAddOfLE [Add α] [ExistsAddOfLE α] : ExistsAddOfLE (WithZero
     obtain ⟨c, rfl⟩ := exists_add_of_le (WithZero.coe_le_coe.1 h)
     exact ⟨c, rfl⟩⟩
 
+lemma map'_mono [MulOneClass α] [MulOneClass β] {f : α →* β} (hf : Monotone f) :
+    Monotone (map' f) := by simpa [Monotone, WithZero.forall]
+
+lemma map'_strictMono [MulOneClass α] [MulOneClass β] {f : α →* β} (hf : StrictMono f) :
+    StrictMono (map' f) := by simpa [StrictMono, WithZero.forall]
+
 end Preorder
 
 section PartialOrder