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

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

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

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : Logic.AP (Positive pd)
⊢ 0 + pn//pd ≃ pn//pd
Tactic:
show 0//1 + pn//pd ≃ pn//pd
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
denominator_positive✝ : Logic.AP (Positive pd)
⊢ 0//1 + pn//pd ≃ pn//pd

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