-- Mathlib/Tactic/CancelDenoms/Core.lean
theorem cancel_factors_eq {α} [Field α] {a b ad bd a' b' gcd : α} (ha : ad * a = a')
    (hb : bd * b = b') (had : ad ≠ 0) (hbd : bd ≠ 0) (hgcd : gcd ≠ 0) :
    (a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b'))

Proof state:
case a.mpr
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * (ad * bd * a) = 1 / gcd * (ad * bd * b)
⊢ a = b

Tactic:
simp only [← mul_assoc] at h

Result:
case a.mpr
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ a = b

Proof state:
case a.mpr.refine_1.ha.ha
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
case a.mpr.refine_1
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ 1 / gcd * ad ≠ 0

case a.mpr.refine_2
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ bd ≠ 0

Tactic:
on_goal 1 => apply mul_ne_zero

Result:
case a.mpr.refine_1.ha
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ 1 / gcd ≠ 0

case a.mpr.refine_1.hb
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ ad ≠ 0

case a.mpr.refine_2
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ bd ≠ 0

Proof state:
case a.mpr
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ 1 / gcd * (ad * bd * a) = 1 / gcd * (ad * bd * b) → a = b

Tactic:
intro h

Result:
case a.mpr
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * (ad * bd * a) = 1 / gcd * (ad * bd * b)
⊢ a = b

Proof state:
case a
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ a = b ↔ 1 / gcd * (ad * bd * a) = 1 / gcd * (ad * bd * b)

Tactic:
constructor

Result:
case a.mp
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ a = b → 1 / gcd * (ad * bd * a) = 1 / gcd * (ad * bd * b)

case a.mpr
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ 1 / gcd * (ad * bd * a) = 1 / gcd * (ad * bd * b) → a = b

Proof state:
case a.mpr.refine_2
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ bd ≠ 0

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ (a = b) = (1 / gcd * (bd * a') = 1 / gcd * (ad * b'))

Tactic:
rw [← ha, ← hb, ← mul_assoc bd, ← mul_assoc ad, mul_comm bd]

Result:
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ (a = b) = (1 / gcd * (ad * bd * a) = 1 / gcd * (ad * bd * b))

Proof state:
case a.mp
α : Type u_1
inst✝ : Field α
a ad bd a' b' gcd : α
ha : ad * a = a'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
hb : bd * a = b'
⊢ 1 / gcd * (ad * bd * a) = 1 / gcd * (ad * bd * a)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ (a = b) = (1 / gcd * (ad * bd * a) = 1 / gcd * (ad * bd * b))

Tactic:
ext

Result:
case a
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ a = b ↔ 1 / gcd * (ad * bd * a) = 1 / gcd * (ad * bd * b)

Proof state:
case a.mpr.refine_1.ha.hb
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ gcd ≠ 0

case a.mpr.refine_1.hb
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ ad ≠ 0

case a.mpr.refine_2
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ bd ≠ 0

Tactic:
all_goals assumption

Result:
no goals

Proof state:
case a.mpr
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ a = b

Tactic:
refine mul_left_cancel₀ (mul_ne_zero ?_ ?_) h

Result:
case a.mpr.refine_1
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ 1 / gcd * ad ≠ 0

case a.mpr.refine_2
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ bd ≠ 0

Proof state:
case a.mp
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
⊢ a = b → 1 / gcd * (ad * bd * a) = 1 / gcd * (ad * bd * b)

Tactic:
rintro rfl

Result:
case a.mp
α : Type u_1
inst✝ : Field α
a ad bd a' b' gcd : α
ha : ad * a = a'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
hb : bd * a = b'
⊢ 1 / gcd * (ad * bd * a) = 1 / gcd * (ad * bd * a)

Proof state:
case a.mpr.refine_1
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ 1 / gcd * ad ≠ 0

Tactic:
apply mul_ne_zero

Result:
case a.mpr.refine_1.ha
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ 1 / gcd ≠ 0

case a.mpr.refine_1.hb
α : Type u_1
inst✝ : Field α
a b ad bd a' b' gcd : α
ha : ad * a = a'
hb : bd * b = b'
had : ad ≠ 0
hbd : bd ≠ 0
hgcd : gcd ≠ 0
h : 1 / gcd * ad * bd * a = 1 / gcd * ad * bd * b
⊢ ad ≠ 0