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

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

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

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
⊢ 0//0 ≃ pn//pd
Tactic:
show 0 * pd ≃ pn * 0
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
⊢ 0 * pd ≃ pn * 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
pn pd : ℤ
⊢ 0 * pd ≃ pn * 0
Tactic:
calc
  0 * pd ≃ _ := AA.absorbL
  0      ≃ _ := Rel.symm AA.absorbR
  pn * 0 ≃ _ := Rel.refl
State after:
no goals