-- 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, exclusively -/
lemma LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered (G : Type*)
    [LinearOrderedCommGroupWithZero G] [Nontrivial Gˣ] [MulArchimedean G] :
    Nonempty (G ≃*o ℤₘ₀) ↔ ¬ DenselyOrdered G

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

Tactic:
refine ⟨withZeroUnitsEquiv.symm.trans (MulEquiv.withZero f), ?_⟩

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

Proof state:
case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : G ≃*o ℤₘ₀
⊢ ∀ {a b : Gˣ}, (withZeroUnitsEquiv.trans ↑f).unzero.toFun a ≤ (withZeroUnitsEquiv.trans ↑f).unzero.toFun b ↔ a ≤ b

Tactic:
intros

Result:
case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : G ≃*o ℤₘ₀
a✝ b✝ : Gˣ
⊢ (withZeroUnitsEquiv.trans ↑f).unzero.toFun a✝ ≤ (withZeroUnitsEquiv.trans ↑f).unzero.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✝ : G
⊢ (map' ↑↑f) (if h : a✝ = 0 then 0 else ↑(Units.mk0 a✝ h)) ≤ (map' ↑↑f) (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 ℤₘ₀
⊢ Gˣ ≃*o Multiplicative ℤ

Tactic:
refine ⟨MulEquiv.unzero (withZeroUnitsEquiv.trans f), ?_⟩

Result:
case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : G ≃*o ℤₘ₀
⊢ ∀ {a b : Gˣ}, (withZeroUnitsEquiv.trans ↑f).unzero.toFun a ≤ (withZeroUnitsEquiv.trans ↑f).unzero.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✝ : G
⊢ (withZeroUnitsEquiv.symm.trans (↑f).withZero).toFun a✝ ≤ (withZeroUnitsEquiv.symm.trans (↑f).withZero).toFun b✝ ↔
    a✝ ≤ b✝

Tactic:
simp only [withZeroUnitsEquiv, MulEquiv.symm_mk, MulEquiv.withZero,
  MulEquiv.toMonoidHom_eq_coe, MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe,
  MulEquiv.trans_apply, MulEquiv.coe_mk, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk]

Result:
case refine_2
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
a✝ b✝ : G
⊢ (map' ↑↑f) (if h : a✝ = 0 then 0 else ↑(Units.mk0 a✝ h)) ≤ (map' ↑↑f) (if h : b✝ = 0 then 0 else ↑(Units.mk0 b✝ h)) ↔
    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,
    ← LinearOrderedCommGroup.discrete_iff_not_denselyOrdered]

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

Proof state:
case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : G ≃*o ℤₘ₀
a✝ b✝ : Gˣ
⊢ unzero ⋯ ≤ unzero ⋯ ↔ a✝ ≤ b✝

Tactic:
rw [← Units.val_le_val, ← map_le_map_iff f, ← coe_le_coe, coe_unzero, coe_unzero]

Result:
no goals

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

Tactic:
intros

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

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

Tactic:
refine Nonempty.congr ?_ ?_ <;> intro f

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

case refine_2
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : Gˣ ≃*o Multiplicative ℤ
⊢ G ≃*o ℤₘ₀

Proof state:
case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : G ≃*o ℤₘ₀
a✝ b✝ : Gˣ
⊢ (withZeroUnitsEquiv.trans ↑f).unzero.toFun a✝ ≤ (withZeroUnitsEquiv.trans ↑f).unzero.toFun b✝ ↔ a✝ ≤ b✝

Tactic:
simp only [MulEquiv.unzero, withZeroUnitsEquiv, MulEquiv.trans_apply,
  MulEquiv.coe_mk, Equiv.coe_fn_mk, recZeroCoe_coe, OrderMonoidIso.coe_mulEquiv,
  MulEquiv.symm_trans_apply, MulEquiv.symm_mk, Equiv.coe_fn_symm_mk, map_eq_zero, coe_ne_zero,
  ↓reduceDIte, unzero_coe, MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe]

Result:
case refine_1
G : Type u_2
inst✝² : LinearOrderedCommGroupWithZero G
inst✝¹ : Nontrivial Gˣ
inst✝ : MulArchimedean G
f : G ≃*o ℤₘ₀
a✝ b✝ : Gˣ
⊢ unzero ⋯ ≤ unzero ⋯ ↔ a✝ ≤ b✝