σ : Type u_1
R : Type ?u.1782406
k : Type u_2
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : ↑(constantCoeff σ k) φ = ↑u
⊢ invOfUnit φ u = invOfUnit φ (Units.mk0 (↑(constantCoeff σ k) φ) (_ : ↑(constantCoeff σ k) φ ≠ 0))
σ : Type u_1
R : Type ?u.1782406
k : Type u_2
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : ↑(constantCoeff σ k) φ = ↑u
⊢ invOfUnit φ u = φ⁻¹
rw [← invOfUnit_eq φ (h.symm ▸ u.ne_zero)]
σ : Type u_1
R : Type ?u.1782406
k : Type u_2
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : ↑(constantCoeff σ k) φ = ↑u
⊢ u = Units.mk0 (↑(constantCoeff σ k) φ) (_ : ↑(constantCoeff σ k) φ ≠ 0)
σ : Type u_1
R : Type ?u.1782406
k : Type u_2
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : ↑(constantCoeff σ k) φ = ↑u
⊢ invOfUnit φ u = invOfUnit φ (Units.mk0 (↑(constantCoeff σ k) φ) (_ : ↑(constantCoeff σ k) φ ≠ 0))
apply congrArg (invOfUnit φ)
σ : Type u_1
R : Type ?u.1782406
k : Type u_2
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : ↑(constantCoeff σ k) φ = ↑u
⊢ ↑u = ↑(Units.mk0 (↑(constantCoeff σ k) φ) (_ : ↑(constantCoeff σ k) φ ≠ 0))
σ : Type u_1
R : Type ?u.1782406
k : Type u_2
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : ↑(constantCoeff σ k) φ = ↑u
⊢ u = Units.mk0 (↑(constantCoeff σ k) φ) (_ : ↑(constantCoeff σ k) φ ≠ 0)
rw [Units.ext_iff]
no goals
σ : Type u_1
R : Type ?u.1782406
k : Type u_2
inst✝ : Field k
φ : MvPowerSeries σ k
u : kˣ
h : ↑(constantCoeff σ k) φ = ↑u
⊢ ↑u = ↑(Units.mk0 (↑(constantCoeff σ k) φ) (_ : ↑(constantCoeff σ k) φ ≠ 0))
exact h.symm