-- Mathlib/GroupTheory/ArchimedeanDensely.lean
/-- Any nontrivial (has other than 0 and 1) linearly ordered mul-archimedean group with zero is
either isomorphic (and order-isomorphic) to `ℤₘ₀`, or is densely ordered. -/
lemma LinearOrderedCommGroupWithZero.discrete_or_denselyOrdered (G : Type*)
    [LinearOrderedCommGroupWithZero G] [Nontrivial Gˣ] [MulArchimedean G] :
    Nonempty (G ≃*o ℤₘ₀) ∨ DenselyOrdered G

Proof state:
case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ : G
⊢ ∀ {b : G}, ((if h : a✝ = 0 then 0 else ↑(Units.mk0 a✝ h)) ≤ if h : b = 0 then 0 else ↑(Units.mk0 b h)) ↔ a✝ ≤ b

Tactic:
split_ifs <;>
simp_all [← Units.val_le_val]

Result:
no goals

Proof state:
case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
⊢ ∀ {a b : G}, WithZero.withZeroUnitsEquiv.symm.toFun a ≤ WithZero.withZeroUnitsEquiv.symm.toFun b ↔ a ≤ b

Tactic:
intro

Result:
case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ : G
⊢ ∀ {b : G}, WithZero.withZeroUnitsEquiv.symm.toFun a✝ ≤ WithZero.withZeroUnitsEquiv.symm.toFun b ↔ a✝ ≤ b

Proof state:
case refine_2
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
⊢ ∀ {a b : WithZero Gˣ}, f.withZero.toFun a ≤ f.withZero.toFun b ↔ a ≤ b

Tactic:
intro a b

Result:
case refine_2
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a b : WithZero Gˣ
⊢ f.withZero.toFun a ≤ f.withZero.toFun b ↔ a ≤ b

Proof state:
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ Nonempty (G ≃*o ℤₘ₀) ∨ DenselyOrdered G

Tactic:
rw [← denselyOrdered_units_iff]

Result:
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ Nonempty (G ≃*o ℤₘ₀) ∨ DenselyOrdered Gˣ

Proof state:
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ Nonempty (Gˣ ≃*o Multiplicative ℤ) → Nonempty (G ≃*o ℤₘ₀)

Tactic:
intro ⟨f⟩

Result:
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
⊢ Nonempty (G ≃*o ℤₘ₀)

Proof state:
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ Nonempty (G ≃*o ℤₘ₀) ∨ DenselyOrdered Gˣ

Tactic:
refine (LinearOrderedCommGroup.discrete_or_denselyOrdered Gˣ).imp_left ?_

Result:
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
⊢ Nonempty (Gˣ ≃*o Multiplicative ℤ) → Nonempty (G ≃*o ℤₘ₀)

Proof state:
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
⊢ Nonempty (G ≃*o ℤₘ₀)

Tactic:
refine ⟨OrderMonoidIso.trans
  ⟨WithZero.withZeroUnitsEquiv.symm, ?_⟩ ⟨f.withZero, ?_⟩⟩

Result:
case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
⊢ ∀ {a b : G}, WithZero.withZeroUnitsEquiv.symm.toFun a ≤ WithZero.withZeroUnitsEquiv.symm.toFun b ↔ a ≤ b

case refine_2
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
⊢ ∀ {a b : WithZero Gˣ}, f.withZero.toFun a ≤ f.withZero.toFun b ↔ a ≤ b

Proof state:
case refine_2
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a b : WithZero Gˣ
⊢ f.withZero.toFun a ≤ f.withZero.toFun b ↔ a ≤ b

Tactic:
induction a <;> induction b <;>
simp [MulEquiv.withZero]

Result:
no goals

Proof state:
case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ : G
⊢ ∀ {b : G}, WithZero.withZeroUnitsEquiv.symm.toFun a✝ ≤ WithZero.withZeroUnitsEquiv.symm.toFun b ↔ a✝ ≤ b

Tactic:
simp only [WithZero.withZeroUnitsEquiv, MulEquiv.symm_mk,
  MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe, MulEquiv.coe_mk,
  Equiv.coe_fn_symm_mk ]

Result:
case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ : G
⊢ ∀ {b : G}, ((if h : a✝ = 0 then 0 else ↑(Units.mk0 a✝ h)) ≤ if h : b = 0 then 0 else ↑(Units.mk0 b h)) ↔ a✝ ≤ b