F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
⊢ ↑(mk' n₁ d₁ * mk' n₂ d₂) = ↑(mk' n₁ d₁) * ↑(mk' n₂ d₂)
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
⊢ ↑(mk' n₁ d₁ * mk' n₂ d₂) = ↑(mk' n₁ d₁) * ↑(mk' n₂ d₂)
have d₁0' : (d₁ : ℤ) ≠ 0 :=
  Int.coe_nat_ne_zero.2 fun e => by rw [e] at d₁0 ; exact d₁0 Nat.cast_zero
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
⊢ ↑(mk' n₁ d₁ * mk' n₂ d₂) = ↑(mk' n₁ d₁) * ↑(mk' n₂ d₂)
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
⊢ ↑(mk' n₁ d₁ * mk' n₂ d₂) = ↑(mk' n₁ d₁) * ↑(mk' n₂ d₂)
have d₂0' : (d₂ : ℤ) ≠ 0 :=
  Int.coe_nat_ne_zero.2 fun e => by rw [e] at d₂0 ; exact d₂0 Nat.cast_zero
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
⊢ ↑(n₁ * n₂ /. (↑d₁ * ↑d₂)) = ↑(n₁ /. ↑d₁) * ↑(n₂ /. ↑d₂)
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
⊢ ↑(mk' n₁ d₁ * mk' n₂ d₂) = ↑(mk' n₁ d₁) * ↑(mk' n₂ d₂)
rw [num_den', num_den', mul_def' d₁0' d₂0']
no goals
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
⊢ ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
rw [(d₁.commute_cast (_ : α)).inv_right₀.eq]
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑0 ≠ 0
d₂0 : ↑d₂ ≠ 0
e : d₁ = 0
⊢ False
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
e : d₁ = 0
⊢ False
rw [e] at d₁0
no goals
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑0 ≠ 0
d₂0 : ↑d₂ ≠ 0
e : d₁ = 0
⊢ False
exact d₁0 Nat.cast_zero
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑0 ≠ 0
d₁0' : ↑d₁ ≠ 0
e : d₂ = 0
⊢ False
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
e : d₂ = 0
⊢ False
rw [e] at d₂0
no goals
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑0 ≠ 0
d₁0' : ↑d₁ ≠ 0
e : d₂ = 0
⊢ False
exact d₂0 Nat.cast_zero
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑(n₁ * n₂) / ↑(↑d₁ * ↑d₂) = ↑n₁ / ↑↑d₁ * (↑n₂ / ↑↑d₂)

case b0
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑↑d₂ ≠ 0

case b0
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑↑d₁ ≠ 0

case b0
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑(↑d₁ * ↑d₂) ≠ 0
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑(n₁ * n₂ /. (↑d₁ * ↑d₂)) = ↑(n₁ /. ↑d₁) * ↑(n₂ /. ↑d₂)
rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero, cast_mk_of_ne_zero]
no goals
case b0
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑↑d₂ ≠ 0

case b0
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑↑d₁ ≠ 0

case b0
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑(↑d₁ * ↑d₂) ≠ 0
all_goals simp [d₁0, d₂0]
no goals
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑(n₁ * n₂) / ↑(↑d₁ * ↑d₂) = ↑n₁ / ↑↑d₁ * (↑n₂ / ↑↑d₂)
simpa [division_def, mul_inv_rev, d₁0, d₂0, mul_assoc]
no goals
case b0
F : Type ?u.23959
ι : Type ?u.23962
α : Type u_1
β : Type ?u.23968
inst✝ : DivisionRing α
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : Nat.coprime (Int.natAbs n₁) d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : Nat.coprime (Int.natAbs n₂) d₂
d₁0 : ↑d₁ ≠ 0
d₂0 : ↑d₂ ≠ 0
d₁0' : ↑d₁ ≠ 0
d₂0' : ↑d₂ ≠ 0
this : ↑n₁ * (↑n₂ * (↑d₂)⁻¹ * (↑d₁)⁻¹) = ↑n₁ * ((↑d₁)⁻¹ * (↑n₂ * (↑d₂)⁻¹))
⊢ ↑(↑d₁ * ↑d₂) ≠ 0
simp [d₁0, d₂0]