case inl
σ : Type u_1
R : Type ?u.1971115
k : Type u_2
inst✝ : Field k
⊢ (↑(C σ k) 0)⁻¹ = ↑(C σ k) 0⁻¹

case inr
σ : Type u_1
R : Type ?u.1971115
k : Type u_2
inst✝ : Field k
r : k
hr : r ≠ 0
⊢ (↑(C σ k) r)⁻¹ = ↑(C σ k) r⁻¹
σ : Type u_1
R : Type ?u.1971115
k : Type u_2
inst✝ : Field k
r : k
⊢ (↑(C σ k) r)⁻¹ = ↑(C σ k) r⁻¹
rcases eq_or_ne r 0 with (rfl | hr)
case inr
σ : Type u_1
R : Type ?u.1971115
k : Type u_2
inst✝ : Field k
r : k
hr : r ≠ 0
⊢ ↑(constantCoeff σ k) (↑(C σ k) r) ≠ 0
case inr
σ : Type u_1
R : Type ?u.1971115
k : Type u_2
inst✝ : Field k
r : k
hr : r ≠ 0
⊢ (↑(C σ k) r)⁻¹ = ↑(C σ k) r⁻¹
rw [MvPowerSeries.inv_eq_iff_mul_eq_one, ← map_mul, inv_mul_cancel hr, map_one]
no goals
case inr
σ : Type u_1
R : Type ?u.1971115
k : Type u_2
inst✝ : Field k
r : k
hr : r ≠ 0
⊢ ↑(constantCoeff σ k) (↑(C σ k) r) ≠ 0
simpa using hr
no goals
case inl
σ : Type u_1
R : Type ?u.1971115
k : Type u_2
inst✝ : Field k
⊢ (↑(C σ k) 0)⁻¹ = ↑(C σ k) 0⁻¹
simp