case refine'_1
ι : Type ?u.338842
α : Type u_1
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.338842
α : Type u_1
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
⊢ (∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1) → s * t = 1
ι : Type ?u.338842
α : Type u_1
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
⊢ s * t = 1 ↔ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1
refine' ⟨fun h => _, _⟩
case refine'_1
ι : Type ?u.338842
α : Type u_1
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).fst = 1.fst ∧ (s * t).snd = 1.snd
⊢ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1
case refine'_1
ι : Type ?u.338842
α : Type u_1
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : s * t = 1
⊢ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1
rw [ext_iff, Prod.ext_iff] at h
case refine'_1
ι : Type ?u.338842
α : Type u_1
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).fst = 1.fst ∧ (s * t).snd = 1.snd
this : s.fst = s.snd ∧ t.fst = t.snd
⊢ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1
case refine'_1
ι : Type ?u.338842
α : Type u_1
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).fst = 1.fst ∧ (s * t).snd = 1.snd
⊢ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1
have := (mul_le_mul_iff_of_ge s.fst_le_snd t.fst_le_snd).1 (h.2.trans h.1.symm).le
case refine'_1.refine'_1.h
ι : Type ?u.338842
α : Type u_1
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).fst = 1.fst ∧ (s * t).snd = 1.snd
this : s.fst = s.snd ∧ t.fst = t.snd
⊢ s.toProd = (s.fst, s.fst)

case refine'_1.refine'_2.h
ι : Type ?u.338842
α : Type u_1
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).fst = 1.fst ∧ (s * t).snd = 1.snd
this : s.fst = s.snd ∧ t.fst = t.snd
⊢ t.toProd = (t.fst, t.fst)
case refine'_1
ι : Type ?u.338842
α : Type u_1
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).fst = 1.fst ∧ (s * t).snd = 1.snd
this : s.fst = s.snd ∧ t.fst = t.snd
⊢ ∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1
refine' ⟨s.fst, t.fst, _, _, h.1⟩ <;> apply NonemptyInterval.ext <;> dsimp [pure]
no goals
case refine'_1.refine'_1.h
ι : Type ?u.338842
α : Type u_1
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).fst = 1.fst ∧ (s * t).snd = 1.snd
this : s.fst = s.snd ∧ t.fst = t.snd
⊢ s.toProd = (s.fst, s.fst)
nth_rw 2 [this.1]
no goals
case refine'_1.refine'_2.h
ι : Type ?u.338842
α : Type u_1
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
h : (s * t).fst = 1.fst ∧ (s * t).snd = 1.snd
this : s.fst = s.snd ∧ t.fst = t.snd
⊢ t.toProd = (t.fst, t.fst)
nth_rw 2 [this.2]
case refine'_2.intro.intro.intro.intro
ι : Type ?u.338842
α : Type u_1
inst✝ : OrderedCommGroup α
b c : α
h : b * c = 1
⊢ pure b * pure c = 1
case refine'_2
ι : Type ?u.338842
α : Type u_1
inst✝ : OrderedCommGroup α
s t : NonemptyInterval α
⊢ (∃ a b, s = pure a ∧ t = pure b ∧ a * b = 1) → s * t = 1
rintro ⟨b, c, rfl, rfl, h⟩
no goals
case refine'_2.intro.intro.intro.intro
ι : Type ?u.338842
α : Type u_1
inst✝ : OrderedCommGroup α
b c : α
h : b * c = 1
⊢ pure b * pure c = 1
rw [pure_mul_pure, h, pure_one]