no goals
n₁ n₂ : Int
d₁ d₂ : Nat
⊢ mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂)
if z₁ : d₁ = 0 then simp [z₁] else if z₂ : d₂ = 0 then simp [z₂] else
rw [← normalize_eq_mkRat z₁, ← normalize_eq_mkRat z₂, normalize_mul_normalize, normalize_eq_mkRat]
no goals
n₁ n₂ : Int
d₁ d₂ : Nat
z₁ : d₁ = 0
⊢ mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂)
simp [z₁]
no goals
n₁ n₂ : Int
d₁ d₂ : Nat
z₁ : ¬d₁ = 0
⊢ mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂)
if z₂ : d₂ = 0 then simp [z₂] else
rw [← normalize_eq_mkRat z₁, ← normalize_eq_mkRat z₂, normalize_mul_normalize, normalize_eq_mkRat]
no goals
n₁ n₂ : Int
d₁ d₂ : Nat
z₁ : ¬d₁ = 0
z₂ : d₂ = 0
⊢ mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂)
simp [z₂]
no goals
n₁ n₂ : Int
d₁ d₂ : Nat
z₁ : ¬d₁ = 0
z₂ : ¬d₂ = 0
⊢ mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂)
rw [← normalize_eq_mkRat z₁, ← normalize_eq_mkRat z₂, normalize_mul_normalize, normalize_eq_mkRat]