F : Type ?u.21767
ι : Type ?u.21770
α : Type u_1
β : Type ?u.21776
inst✝ : DivisionRing α
m n : ℚ
m0 : ↑m.den ≠ 0
n0 : ↑n.den ≠ 0
this : ↑(-n).den ≠ 0
⊢ ↑(m - n) = ↑m - ↑n
F : Type ?u.21767
ι : Type ?u.21770
α : Type u_1
β : Type ?u.21776
inst✝ : DivisionRing α
m n : ℚ
m0 : ↑m.den ≠ 0
n0 : ↑n.den ≠ 0
⊢ ↑(m - n) = ↑m - ↑n
have : ((-n).den : α) ≠ 0 := by cases n ; exact n0
no goals
F : Type ?u.21767
ι : Type ?u.21770
α : Type u_1
β : Type ?u.21776
inst✝ : DivisionRing α
m n : ℚ
m0 : ↑m.den ≠ 0
n0 : ↑n.den ≠ 0
this : ↑(-n).den ≠ 0
⊢ ↑(m - n) = ↑m - ↑n
simp [sub_eq_add_neg, cast_add_of_ne_zero m0 this]
case mk'
F : Type ?u.21767
ι : Type ?u.21770
α : Type u_1
β : Type ?u.21776
inst✝ : DivisionRing α
m : ℚ
m0 : ↑m.den ≠ 0
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
n0 : ↑(mk' num✝ den✝).den ≠ 0
⊢ ↑(-mk' num✝ den✝).den ≠ 0
F : Type ?u.21767
ι : Type ?u.21770
α : Type u_1
β : Type ?u.21776
inst✝ : DivisionRing α
m n : ℚ
m0 : ↑m.den ≠ 0
n0 : ↑n.den ≠ 0
⊢ ↑(-n).den ≠ 0
cases n
no goals
case mk'
F : Type ?u.21767
ι : Type ?u.21770
α : Type u_1
β : Type ?u.21776
inst✝ : DivisionRing α
m : ℚ
m0 : ↑m.den ≠ 0
num✝ : ℤ
den✝ : ℕ
den_nz✝ : den✝ ≠ 0
reduced✝ : Nat.coprime (Int.natAbs num✝) den✝
n0 : ↑(mk' num✝ den✝).den ≠ 0
⊢ ↑(-mk' num✝ den✝).den ≠ 0
exact n0