F : Type ?u.35260
ι : Type ?u.35263
α : Type u_1
β : Type ?u.35269
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑d ≠ 0
x✝ : n ≠ 0
⊢ ↑(mk' n d)⁻¹ = (↑(mk' n d))⁻¹
F : Type ?u.35260
ι : Type ?u.35263
α : Type u_1
β : Type ?u.35269
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑d ≠ 0
⊢ ↑(mk' n d)⁻¹ = (↑(mk' n d))⁻¹
have _ : (n : ℤ) ≠ 0 := fun e => by rw [e] at n0 ; exact n0 Int.cast_zero
F : Type ?u.35260
ι : Type ?u.35263
α : Type u_1
β : Type ?u.35269
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑d ≠ 0
x✝¹ : n ≠ 0
x✝ : ↑d ≠ 0
⊢ ↑(mk' n d)⁻¹ = (↑(mk' n d))⁻¹
F : Type ?u.35260
ι : Type ?u.35263
α : Type u_1
β : Type ?u.35269
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑d ≠ 0
x✝ : n ≠ 0
⊢ ↑(mk' n d)⁻¹ = (↑(mk' n d))⁻¹
have _ : (d : ℤ) ≠ 0 :=
  Int.coe_nat_ne_zero.2 fun e => by rw [e] at d0 ; exact d0 Nat.cast_zero
F : Type ?u.35260
ι : Type ?u.35263
α : Type u_1
β : Type ?u.35269
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑d ≠ 0
x✝¹ : n ≠ 0
x✝ : ↑d ≠ 0
⊢ ↑(↑d /. n) = (↑(n /. ↑d))⁻¹
F : Type ?u.35260
ι : Type ?u.35263
α : Type u_1
β : Type ?u.35269
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑d ≠ 0
x✝¹ : n ≠ 0
x✝ : ↑d ≠ 0
⊢ ↑(mk' n d)⁻¹ = (↑(mk' n d))⁻¹
rw [num_den', inv_def']
no goals
F : Type ?u.35260
ι : Type ?u.35263
α : Type u_1
β : Type ?u.35269
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑d ≠ 0
x✝¹ : n ≠ 0
x✝ : ↑d ≠ 0
⊢ ↑(↑d /. n) = (↑(n /. ↑d))⁻¹
rw [cast_mk_of_ne_zero, cast_mk_of_ne_zero, inv_div] <;> simp [n0, d0]
F : Type ?u.35260
ι : Type ?u.35263
α : Type u_1
β : Type ?u.35269
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑0 ≠ 0
d0 : ↑d ≠ 0
e : n = 0
⊢ False
F : Type ?u.35260
ι : Type ?u.35263
α : Type u_1
β : Type ?u.35269
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑d ≠ 0
e : n = 0
⊢ False
rw [e] at n0
no goals
F : Type ?u.35260
ι : Type ?u.35263
α : Type u_1
β : Type ?u.35269
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑0 ≠ 0
d0 : ↑d ≠ 0
e : n = 0
⊢ False
exact n0 Int.cast_zero
F : Type ?u.35260
ι : Type ?u.35263
α : Type u_1
β : Type ?u.35269
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑0 ≠ 0
x✝ : n ≠ 0
e : d = 0
⊢ False
F : Type ?u.35260
ι : Type ?u.35263
α : Type u_1
β : Type ?u.35269
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑d ≠ 0
x✝ : n ≠ 0
e : d = 0
⊢ False
rw [e] at d0
no goals
F : Type ?u.35260
ι : Type ?u.35263
α : Type u_1
β : Type ?u.35269
inst✝ : DivisionRing α
n : ℤ
d : ℕ
h : d ≠ 0
c : Nat.coprime (Int.natAbs n) d
n0 : ↑n ≠ 0
d0 : ↑0 ≠ 0
x✝ : n ≠ 0
e : d = 0
⊢ False
exact d0 Nat.cast_zero