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

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

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

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

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

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