case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(Int.negOfNat (Nat.succ n)) * ⅟↑d)⁻¹ (Int.negOfNat d) (Nat.succ n)
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsRat a (Int.negOfNat (Nat.succ n)) d → IsRat a⁻¹ (Int.negOfNat d) (Nat.succ n)
rintro ⟨_, rfl⟩
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(-Int.ofNat (Nat.succ n)) * ⅟↑d)⁻¹ (-Int.ofNat d) (Nat.succ n)
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(Int.negOfNat (Nat.succ n)) * ⅟↑d)⁻¹ (Int.negOfNat d) (Nat.succ n)
simp only [Int.negOfNat_eq]
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑(Nat.succ n)
⊢ IsRat (↑(-Int.ofNat (Nat.succ n)) * ⅟↑d)⁻¹ (-Int.ofNat d) (Nat.succ n)
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
⊢ IsRat (↑(-Int.ofNat (Nat.succ n)) * ⅟↑d)⁻¹ (-Int.ofNat d) (Nat.succ n)
have := invertibleOfNonzero (α := α) (Nat.cast_ne_zero.2 (Nat.succ_ne_zero n))
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n✝ d : ℕ
inv✝ : Invertible ↑d
n : ℕ
this : Invertible ↑n
⊢ IsRat (↑(-Int.ofNat n) * ⅟↑d)⁻¹ (-Int.ofNat d) n
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑(Nat.succ n)
⊢ IsRat (↑(-Int.ofNat (Nat.succ n)) * ⅟↑d)⁻¹ (-Int.ofNat d) (Nat.succ n)
generalize Nat.succ n = n at *
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n✝ d : ℕ
inv✝ : Invertible ↑d
n : ℕ
this : Invertible ↑n
⊢ (↑(-Int.ofNat n) * ⅟↑d)⁻¹ = ↑(-Int.ofNat d) * ⅟↑n
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n✝ d : ℕ
inv✝ : Invertible ↑d
n : ℕ
this : Invertible ↑n
⊢ IsRat (↑(-Int.ofNat n) * ⅟↑d)⁻¹ (-Int.ofNat d) n
use this
no goals
case mk
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n✝ d : ℕ
inv✝ : Invertible ↑d
n : ℕ
this : Invertible ↑n
⊢ (↑(-Int.ofNat n) * ⅟↑d)⁻¹ = ↑(-Int.ofNat d) * ⅟↑n
simp only [Int.ofNat_eq_coe, Int.cast_neg,
Int.cast_ofNat, invOf_eq_inv, inv_neg,  neg_mul, mul_inv_rev, inv_inv]