-- Mathlib/Algebra/Order/Interval/Basic.lean
theorem mul_eq_one_iff : s * t = 1 ↔ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1

Proof state:
case refine_2
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
⊢ (∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1) → s * t = 1

Tactic:
rintro ⟨b, c, rfl, rfl, h⟩

Result:
case refine_2.intro.intro.intro.intro
α : Type u_2
inst✝ : OrderedCommGroup α
b c : α
h : b * c = 1
⊢ pure b * pure c = 1

Proof state:
case refine_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
⊢ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1

Tactic:
have := (mul_le_mul_iff_of_ge s.fst_le_snd t.fst_le_snd).1 (h.2.trans h.1.symm).le

Result:
case refine_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
⊢ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1

Proof state:
case refine_2.intro.intro.intro.intro
α : Type u_2
inst✝ : OrderedCommGroup α
b c : α
h : b * c = 1
⊢ pure b * pure c = 1

Tactic:
rw [pure_mul_pure, h, pure_one]

Result:
no goals

Proof state:
case refine_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
⊢ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1

Tactic:
refine ⟨s.fst, t.fst, ?_, ?_, h.1⟩ <;> apply NonemptyInterval.ext <;> dsimp [pure]

Result:
case refine_1.refine_1.toProd
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
⊢ s.toProd = (s.toProd.1, s.toProd.1)

case refine_1.refine_2.toProd
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
⊢ t.toProd = (t.toProd.1, t.toProd.1)

Proof state:
case refine_1.refine_2.toProd
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
⊢ t.toProd = (t.toProd.1, t.toProd.1)

Tactic:
nth_rw 2 [this.2]

Result:
no goals

Proof state:
case refine_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : s * t = 1
⊢ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1

Tactic:
rw [NonemptyInterval.ext_iff, Prod.ext_iff] at h

Result:
case refine_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
⊢ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1

Proof state:
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
⊢ s * t = 1 ↔ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1

Tactic:
refine ⟨fun h => ?_, ?_⟩

Result:
case refine_1
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : s * t = 1
⊢ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1

case refine_2
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
⊢ (∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1) → s * t = 1

Proof state:
case refine_1.refine_1.toProd
α : Type u_2
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).toProd.1 = (toProd 1).1 ∧ (s * t).toProd.2 = (toProd 1).2
this : s.toProd.1 = s.toProd.2 ∧ t.toProd.1 = t.toProd.2
⊢ s.toProd = (s.toProd.1, s.toProd.1)

Tactic:
nth_rw 2 [this.1]

Result:
no goals