Theorem: Lean4Axiomatic.Rational.Impl.Fraction.Naive.eqv_trans_nonzero_denom (Lean4Axiomatic/Rational/Impl/Fraction/Naive.lean)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q r : Fraction ℤ
⊢ q.denominator ≄ 0 → p ≃ q → q ≃ r → p ≃ r
Tactic:
revert p
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, q.denominator ≄ 0 → p ≃ q → q ≃ r → p ≃ r

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, q.denominator ≄ 0 → p ≃ q → q ≃ r → p ≃ r
Tactic:
intro (pn//pd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
pn pd : ℤ
⊢ q.denominator ≄ 0 → pn//pd ≃ q → q ≃ r → pn//pd ≃ r

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
pn pd : ℤ
⊢ q.denominator ≄ 0 → pn//pd ≃ q → q ≃ r → pn//pd ≃ r
Tactic:
revert q
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
⊢ ∀ {q : Fraction ℤ}, q.denominator ≄ 0 → pn//pd ≃ q → q ≃ r → pn//pd ≃ r

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
⊢ ∀ {q : Fraction ℤ}, q.denominator ≄ 0 → pn//pd ≃ q → q ≃ r → pn//pd ≃ r
Tactic:
intro (qn//qd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd qn qd : ℤ
⊢ (qn//qd).denominator ≄ 0 → pn//pd ≃ qn//qd → qn//qd ≃ r → pn//pd ≃ r

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd qn qd : ℤ
⊢ (qn//qd).denominator ≄ 0 → pn//pd ≃ qn//qd → qn//qd ≃ r → pn//pd ≃ r
Tactic:
revert r
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
⊢ ∀ {r : Fraction ℤ}, (qn//qd).denominator ≄ 0 → pn//pd ≃ qn//qd → qn//qd ≃ r → pn//pd ≃ r

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd : ℤ
⊢ ∀ {r : Fraction ℤ}, (qn//qd).denominator ≄ 0 → pn//pd ≃ qn//qd → qn//qd ≃ r → pn//pd ≃ r
Tactic:
intro (rn//rd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
⊢ (qn//qd).denominator ≄ 0 → pn//pd ≃ qn//qd → qn//qd ≃ rn//rd → pn//pd ≃ rn//rd

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
⊢ (qn//qd).denominator ≄ 0 → pn//pd ≃ qn//qd → qn//qd ≃ rn//rd → pn//pd ≃ rn//rd
Tactic:
intro (_ : qd ≄ 0) (_ : pn//pd ≃ qn//qd) (_ : qn//qd ≃ rn//rd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝² : qd ≄ 0
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
⊢ pn//pd ≃ rn//rd

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝² : qd ≄ 0
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
⊢ pn//pd ≃ rn//rd
Tactic:
have : (pn * rd) * qd ≃ (rn * pd) * qd := calc
  (pn * rd) * qd ≃ _ := AA.substL AA.comm
  (rd * pn) * qd ≃ _ := AA.assoc
  rd * (pn * qd) ≃ _ := AA.substR ‹pn * qd ≃ qn * pd›
  rd * (qn * pd) ≃ _ := Rel.symm AA.assoc
  (rd * qn) * pd ≃ _ := AA.substL AA.comm
  (qn * rd) * pd ≃ _ := AA.substL ‹qn * rd ≃ rn * qd›
  (rn * qd) * pd ≃ _ := AA.assoc
  rn * (qd * pd) ≃ _ := AA.substR AA.comm
  rn * (pd * qd) ≃ _ := Rel.symm AA.assoc
  (rn * pd) * qd ≃ _ := Rel.refl
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝² : qd ≄ 0
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this : pn * rd * qd ≃ rn * pd * qd
⊢ pn//pd ≃ rn//rd

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝² : qd ≄ 0
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this : pn * rd * qd ≃ rn * pd * qd
⊢ pn//pd ≃ rn//rd
Tactic:
have : pn * rd ≃ rn * pd :=
  Integer.mul_cancelR ‹qd ≄ 0› ‹(pn * rd) * qd ≃ (rn * pd) * qd›
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝² : qd ≄ 0
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝ : pn * rd * qd ≃ rn * pd * qd
this : pn * rd ≃ rn * pd
⊢ pn//pd ≃ rn//rd

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd qn qd rn rd : ℤ
x✝² : qd ≄ 0
x✝¹ : pn//pd ≃ qn//qd
x✝ : qn//qd ≃ rn//rd
this✝ : pn * rd * qd ≃ rn * pd * qd
this : pn * rd ≃ rn * pd
⊢ pn//pd ≃ rn//rd
Tactic:
exact this
State after:
no goals