-- Mathlib/GroupTheory/ArchimedeanDensely.lean
lemma denselyOrdered_units_iff {G₀ : Type*} [LinearOrderedCommGroupWithZero G₀] [Nontrivial G₀ˣ] :
    DenselyOrdered G₀ˣ ↔ DenselyOrdered G₀

Proof state:
case mp.inr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
x y : G₀
h : x < y
hx : 0 < x
⊢ ∃ a, x < a ∧ a < y

Tactic:
obtain ⟨z, hz, hz'⟩ := H.dense (Units.mk0 x hx.ne') (Units.mk0 y (hx.trans h).ne')
  (by simp [← Units.val_lt_val, h])

Result:
case mp.inr.intro.intro
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
x y : G₀
h : x < y
hx : 0 < x
z : G₀ˣ
hz : Units.mk0 x ⋯ < z
hz' : z < Units.mk0 y ⋯
⊢ ∃ a, x < a ∧ a < y

Proof state:
case mp
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
x y : G₀
h : x < y
⊢ ∃ a, x < a ∧ a < y

Tactic:
rcases (zero_le' (a := x)).eq_or_lt with rfl|hx

Result:
case mp.inl
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
y : G₀
h : 0 < y
⊢ ∃ a, 0 < a ∧ a < y

case mp.inr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
x y : G₀
h : x < y
hx : 0 < x
⊢ ∃ a, x < a ∧ a < y

Proof state:
case mp.inl.intro.intro.refine_2
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
y : G₀ˣ
h : 0 < ↑y
z : G₀ˣ
hz : z ≠ 1
⊢ ↑(y * (mabs z)⁻¹) < ↑y

Tactic:
rw [Units.val_lt_val]

Result:
case mp.inl.intro.intro.refine_2
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
y : G₀ˣ
h : 0 < ↑y
z : G₀ˣ
hz : z ≠ 1
⊢ y * (mabs z)⁻¹ < y

Proof state:
case mp
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
⊢ DenselyOrdered G₀

Tactic:
refine ⟨fun x y h ↦ ?_⟩

Result:
case mp
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
x y : G₀
h : x < y
⊢ ∃ a, x < a ∧ a < y

Proof state:
case mpr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀
x y : G₀ˣ
h : x < y
⊢ ∃ a, x < a ∧ a < y

Tactic:
obtain ⟨z, hz⟩ := exists_between (Units.val_lt_val.mpr h)

Result:
case mpr.intro
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀
x y : G₀ˣ
h : x < y
z : G₀
hz : ↑x < z ∧ z < ↑y
⊢ ∃ a, x < a ∧ a < y

Proof state:
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
⊢ DenselyOrdered G₀ˣ ↔ DenselyOrdered G₀

Tactic:
constructor

Result:
case mp
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
⊢ DenselyOrdered G₀ˣ → DenselyOrdered G₀

case mpr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
⊢ DenselyOrdered G₀ → DenselyOrdered G₀ˣ

Proof state:
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
x y : G₀
h : x < y
hx : 0 < x
⊢ Units.mk0 x ⋯ < Units.mk0 y ⋯

Tactic:
simp [← Units.val_lt_val, h]

Result:
no goals

Proof state:
case mp.inl.intro.intro.refine_1
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
y : G₀ˣ
h : 0 < ↑y
z : G₀ˣ
hz : z ≠ 1
⊢ 0 < ↑(y * (mabs z)⁻¹)

Tactic:
simp [zero_lt_iff]

Result:
no goals

Proof state:
case mp.inl.intro.intro.refine_2
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
y : G₀ˣ
h : 0 < ↑y
z : G₀ˣ
hz : z ≠ 1
⊢ y * (mabs z)⁻¹ < y

Tactic:
simp [hz]

Result:
no goals

Proof state:
case mp.inl.intro
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
y : G₀ˣ
h : 0 < ↑y
⊢ ∃ a, 0 < a ∧ a < ↑y

Tactic:
obtain ⟨z, hz⟩ := exists_ne (1 : G₀ˣ)

Result:
case mp.inl.intro.intro
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
y : G₀ˣ
h : 0 < ↑y
z : G₀ˣ
hz : z ≠ 1
⊢ ∃ a, 0 < a ∧ a < ↑y

Proof state:
case mp.inl
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
y : G₀
h : 0 < y
⊢ ∃ a, 0 < a ∧ a < y

Tactic:
lift y to G₀ˣ using h.ne'.isUnit

Result:
case mp.inl.intro
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
y : G₀ˣ
h : 0 < ↑y
⊢ ∃ a, 0 < a ∧ a < ↑y

Proof state:
case mpr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀
⊢ DenselyOrdered G₀ˣ

Tactic:
refine ⟨fun x y h ↦ ?_⟩

Result:
case mpr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀
x y : G₀ˣ
h : x < y
⊢ ∃ a, x < a ∧ a < y

Proof state:
case mp
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
⊢ DenselyOrdered G₀ˣ → DenselyOrdered G₀

Tactic:
intro H

Result:
case mp
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
⊢ DenselyOrdered G₀

Proof state:
case mpr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
⊢ DenselyOrdered G₀ → DenselyOrdered G₀ˣ

Tactic:
intro H

Result:
case mpr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀
⊢ DenselyOrdered G₀ˣ

Proof state:
case mpr.intro.inr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀
x y : G₀ˣ
h : x < y
z : G₀
hz : ↑x < z ∧ z < ↑y
hz' : 0 < z
⊢ ∃ a, x < a ∧ a < y

Tactic:
refine ⟨Units.mk0 z hz'.ne', ?_⟩

Result:
case mpr.intro.inr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀
x y : G₀ˣ
h : x < y
z : G₀
hz : ↑x < z ∧ z < ↑y
hz' : 0 < z
⊢ x < Units.mk0 z ⋯ ∧ Units.mk0 z ⋯ < y

Proof state:
case mp.inl.intro.intro
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
y : G₀ˣ
h : 0 < ↑y
z : G₀ˣ
hz : z ≠ 1
⊢ ∃ a, 0 < a ∧ a < ↑y

Tactic:
refine ⟨(y * |z|ₘ⁻¹ : G₀ˣ), ?_, ?_⟩

Result:
case mp.inl.intro.intro.refine_1
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
y : G₀ˣ
h : 0 < ↑y
z : G₀ˣ
hz : z ≠ 1
⊢ 0 < ↑(y * (mabs z)⁻¹)

case mp.inl.intro.intro.refine_2
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
y : G₀ˣ
h : 0 < ↑y
z : G₀ˣ
hz : z ≠ 1
⊢ ↑(y * (mabs z)⁻¹) < ↑y

Proof state:
case mpr.intro.inr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀
x y : G₀ˣ
h : x < y
z : G₀
hz : ↑x < z ∧ z < ↑y
hz' : 0 < z
⊢ x < Units.mk0 z ⋯ ∧ Units.mk0 z ⋯ < y

Tactic:
simp [← Units.val_lt_val, hz]

Result:
no goals

Proof state:
case mp.inr.intro.intro
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀ˣ
x y : G₀
h : x < y
hx : 0 < x
z : G₀ˣ
hz : Units.mk0 x ⋯ < z
hz' : z < Units.mk0 y ⋯
⊢ ∃ a, x < a ∧ a < y

Tactic:
refine ⟨z, ?_, ?_⟩ <;>
simpa [← Units.val_lt_val]

Result:
no goals

Proof state:
case mpr.intro
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀
x y : G₀ˣ
h : x < y
z : G₀
hz : ↑x < z ∧ z < ↑y
⊢ ∃ a, x < a ∧ a < y

Tactic:
rcases (zero_le' (a := z)).eq_or_lt with rfl|hz'

Result:
case mpr.intro.inl
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀
x y : G₀ˣ
h : x < y
hz : ↑x < 0 ∧ 0 < ↑y
⊢ ∃ a, x < a ∧ a < y

case mpr.intro.inr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
H : DenselyOrdered G₀
x y : G₀ˣ
h : x < y
z : G₀
hz : ↑x < z ∧ z < ↑y
hz' : 0 < z
⊢ ∃ a, x < a ∧ a < y