F : Type ?u.37416
ι : Type ?u.37419
α : Type u_1
β : Type ?u.37425
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
this : ↑n⁻¹.den ∣ n.num
⊢ ↑(m / n) = ↑m / ↑n
F : Type ?u.37416
ι : Type ?u.37419
α : Type u_1
β : Type ?u.37425
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
have : (n⁻¹.den : ℤ) ∣ n.num := by
  conv in n⁻¹.den => rw [← @num_den n, inv_def']
  apply den_dvd
F : Type ?u.37416
ι : Type ?u.37419
α : Type u_1
β : Type ?u.37425
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
this✝ : ↑n⁻¹.den ∣ n.num
this : ↑n⁻¹.den = 0 → ↑n.num = 0
⊢ ↑(m / n) = ↑m / ↑n
F : Type ?u.37416
ι : Type ?u.37419
α : Type u_1
β : Type ?u.37425
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
this : ↑n⁻¹.den ∣ n.num
⊢ ↑(m / n) = ↑m / ↑n
have : (n⁻¹.den : α) = 0 → (n.num : α) = 0 := fun h => by
  let ⟨k, e⟩ := this
  have := congr_arg ((↑) : ℤ → α) e ; rwa [Int.cast_mul, Int.cast_ofNat, h, zero_mul] at this
no goals
F : Type ?u.37416
ι : Type ?u.37419
α : Type u_1
β : Type ?u.37425
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
this✝ : ↑n⁻¹.den ∣ n.num
this : ↑n⁻¹.den = 0 → ↑n.num = 0
⊢ ↑(m / n) = ↑m / ↑n
rw [division_def, cast_mul_of_ne_zero md (mt this nn), cast_inv_of_ne_zero nn nd, division_def]
F : Type ?u.37416
ι : Type ?u.37419
α : Type u_1
β : Type ?u.37425
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
⊢ ↑(↑n.den /. n.num).den ∣ n.num
F : Type ?u.37416
ι : Type ?u.37419
α : Type u_1
β : Type ?u.37425
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
⊢ ↑n⁻¹.den ∣ n.num
conv in n⁻¹.den => rw [← @num_den n, inv_def']
no goals
F : Type ?u.37416
ι : Type ?u.37419
α : Type u_1
β : Type ?u.37425
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
⊢ ↑(↑n.den /. n.num).den ∣ n.num
apply den_dvd
F : Type ?u.37416
ι : Type ?u.37419
α : Type u_1
β : Type ?u.37425
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
this : ↑n⁻¹.den ∣ n.num
h : ↑n⁻¹.den = 0
k : ℤ
e : n.num = ↑n⁻¹.den * k
⊢ ↑n.num = 0
F : Type ?u.37416
ι : Type ?u.37419
α : Type u_1
β : Type ?u.37425
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
this : ↑n⁻¹.den ∣ n.num
h : ↑n⁻¹.den = 0
⊢ ↑n.num = 0
let ⟨k, e⟩ := this
F : Type ?u.37416
ι : Type ?u.37419
α : Type u_1
β : Type ?u.37425
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
this✝ : ↑n⁻¹.den ∣ n.num
h : ↑n⁻¹.den = 0
k : ℤ
e : n.num = ↑n⁻¹.den * k
this : ↑n.num = ↑(↑n⁻¹.den * k)
⊢ ↑n.num = 0
F : Type ?u.37416
ι : Type ?u.37419
α : Type u_1
β : Type ?u.37425
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
this : ↑n⁻¹.den ∣ n.num
h : ↑n⁻¹.den = 0
k : ℤ
e : n.num = ↑n⁻¹.den * k
⊢ ↑n.num = 0
have := congr_arg ((↑) : ℤ → α) e
no goals
F : Type ?u.37416
ι : Type ?u.37419
α : Type u_1
β : Type ?u.37425
inst✝ : DivisionRing α
m n : ℚ
md : ↑m.den ≠ 0
nn : ↑n.num ≠ 0
nd : ↑n.den ≠ 0
this✝ : ↑n⁻¹.den ∣ n.num
h : ↑n⁻¹.den = 0
k : ℤ
e : n.num = ↑n⁻¹.den * k
this : ↑n.num = ↑(↑n⁻¹.den * k)
⊢ ↑n.num = 0
rwa [Int.cast_mul, Int.cast_ofNat, h, zero_mul] at this