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

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ (a//0 + b//0).to_prod ≃ (0//0).to_prod
Tactic:
show ((a * 0 + 0 * b)//(0 * 0)).to_prod ≃ (0//0).to_prod
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ ((a * 0 + 0 * b)//(0 * 0)).to_prod ≃ (0//0).to_prod

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ ((a * 0 + 0 * b)//(0 * 0)).to_prod ≃ (0//0).to_prod
Tactic:
show (a * 0 + 0 * b, 0 * 0) ≃ (0, 0)
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ (a * 0 + 0 * b, 0 * 0) ≃ (0, 0)

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ (a * 0 + 0 * b, 0 * 0) ≃ (0, 0)
Tactic:
apply Relation.Equivalence.Impl.Prod.eqv_defn.mpr
State after:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a * 0 + 0 * b ≃ 0 ∧ 0 * 0 ≃ 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a * 0 + 0 * b ≃ 0 ∧ 0 * 0 ≃ 0
Tactic:
apply And.intro
State after:
case left
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a * 0 + 0 * b ≃ 0

case right
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ 0 * 0 ≃ 0

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a * 0 + 0 * b ≃ 0
Tactic:
case left =>
  show a * 0 + 0 * b ≃ 0
  calc
    a * 0 + 0 * b ≃ _ := AA.substL AA.absorbR
    0 + 0 * b     ≃ _ := AA.identL
    0 * b         ≃ _ := AA.absorbL
    0             ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ 0 * 0 ≃ 0
Tactic:
case right =>
  show 0 * 0 ≃ 0
  exact AA.absorbL
State after:
no goals

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ a * 0 + 0 * b ≃ 0
Tactic:
calc
  a * 0 + 0 * b ≃ _ := AA.substL AA.absorbR
  0 + 0 * b     ≃ _ := AA.identL
  0 * b         ≃ _ := AA.absorbL
  0             ≃ _ := Rel.refl
State after:
no goals

State before:
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
⊢ 0 * 0 ≃ 0
Tactic:
exact AA.absorbL
State after:
no goals