Theorem: Lean4Axiomatic.Rational.Impl.Fraction.add_assoc (Lean4Axiomatic/Rational/Impl/Fraction/Addition.lean)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p q r : Fraction ℤ
⊢ p + q + r ≃ p + (q + r)
Tactic:
revert p
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p + q + r ≃ p + (q + r)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
⊢ ∀ {p : Fraction ℤ}, p + q + r ≃ p + (q + r)
Tactic:
intro (pn//pd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : Logic.AP (Positive pd)
⊢ pn//pd + q + r ≃ pn//pd + (q + r)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
q r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : Logic.AP (Positive pd)
⊢ pn//pd + q + r ≃ pn//pd + (q + r)
Tactic:
revert q
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : Logic.AP (Positive pd)
⊢ ∀ {q : Fraction ℤ}, pn//pd + q + r ≃ pn//pd + (q + r)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝ : Logic.AP (Positive pd)
⊢ ∀ {q : Fraction ℤ}, pn//pd + q + r ≃ pn//pd + (q + r)
Tactic:
intro (qn//qd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝¹ : Logic.AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
⊢ pn//pd + qn//qd + r ≃ pn//pd + (qn//qd + r)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
r : Fraction ℤ
pn pd : ℤ
denominator_positive✝¹ : Logic.AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
⊢ pn//pd + qn//qd + r ≃ pn//pd + (qn//qd + r)
Tactic:
revert r
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝¹ : Logic.AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
⊢ ∀ {r : Fraction ℤ}, pn//pd + qn//qd + r ≃ pn//pd + (qn//qd + r)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝¹ : Logic.AP (Positive pd)
qn qd : ℤ
denominator_positive✝ : Logic.AP (Positive qd)
⊢ ∀ {r : Fraction ℤ}, pn//pd + qn//qd + r ≃ pn//pd + (qn//qd + r)
Tactic:
intro (rn//rd)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝² : Logic.AP (Positive pd)
qn qd : ℤ
denominator_positive✝¹ : Logic.AP (Positive qd)
rn rd : ℤ
denominator_positive✝ : Logic.AP (Positive rd)
⊢ pn//pd + qn//qd + rn//rd ≃ pn//pd + (qn//qd + rn//rd)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝² : Logic.AP (Positive pd)
qn qd : ℤ
denominator_positive✝¹ : Logic.AP (Positive qd)
rn rd : ℤ
denominator_positive✝ : Logic.AP (Positive rd)
⊢ pn//pd + qn//qd + rn//rd ≃ pn//pd + (qn//qd + rn//rd)
Tactic:
calc
  (pn//pd + qn//qd) + rn//rd
    ≃ _ := eqv_refl
  (pn * qd + pd * qn)//(pd * qd) + rn//rd
    ≃ _ := eqv_refl
  ((pn * qd + pd * qn) * rd + (pd * qd) * rn)//((pd * qd) * rd)
    ≃ _ := substN (AA.substL AA.distribR)
  (((pn * qd) * rd + (pd * qn) * rd) + (pd * qd) * rn)//((pd * qd) * rd)
    ≃ _ := substN (AA.substL (AA.substL AA.assoc))
  ((pn * (qd * rd) + (pd * qn) * rd) + (pd * qd) * rn)//((pd * qd) * rd)
    ≃ _ := substN (AA.substL (AA.substR AA.assoc))
  ((pn * (qd * rd) + pd * (qn * rd)) + (pd * qd) * rn)//((pd * qd) * rd)
    ≃ _ := substN (AA.substR AA.assoc)
  ((pn * (qd * rd) + pd * (qn * rd)) + pd * (qd * rn))//((pd * qd) * rd)
    ≃ _ := substN AA.assoc
  (pn * (qd * rd) + (pd * (qn * rd) + pd * (qd * rn)))//((pd * qd) * rd)
    ≃ _ := substN (AA.substR (Rel.symm AA.distribL))
  (pn * (qd * rd) + pd * (qn * rd + qd * rn))//((pd * qd) * rd)
    ≃ _ := substD AA.assoc
  (pn * (qd * rd) + pd * (qn * rd + qd * rn))//(pd * (qd * rd))
    ≃ _ := eqv_refl
  pn//pd + (qn * rd + qd * rn)//(qd * rd)
    ≃ _ := eqv_refl
  pn//pd + (qn//qd + rn//rd)
    ≃ _ := eqv_refl
State after:
no goals