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)
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
a : α
n d : ℕ
⊢ IsRat a (Int.ofNat (Nat.succ n)) d → IsRat a⁻¹ (Int.ofNat d) (Nat.succ n)
rintro ⟨_, rfl⟩
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))
no goals
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)
refine ⟨this, by simp⟩
no goals
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
n d : ℕ
inv✝ : Invertible ↑d
this : Invertible ↑(Nat.succ n)
⊢ (↑(Int.ofNat (Nat.succ n)) * ⅟↑d)⁻¹ = ↑(Int.ofNat d) * ⅟↑(Nat.succ n)
simp