case pos
σ : Type u_1
R : Type ?u.1945318
k : Type u_2
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ↑(constantCoeff σ k) (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

case neg
σ : Type u_1
R : Type ?u.1945318
k : Type u_2
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬↑(constantCoeff σ k) (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
σ : Type u_1
R : Type ?u.1945318
k : Type u_2
inst✝ : Field k
φ ψ : MvPowerSeries σ k
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
by_cases h : constantCoeff σ k (φ * ψ) = 0
case pos
σ : Type u_1
R : Type ?u.1945318
k : Type u_2
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ↑(constantCoeff σ k) (φ * ψ) = 0
⊢ 0 = ψ⁻¹ * φ⁻¹
case pos
σ : Type u_1
R : Type ?u.1945318
k : Type u_2
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ↑(constantCoeff σ k) (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
rw [inv_eq_zero.mpr h]
case pos
σ : Type u_1
R : Type ?u.1945318
k : Type u_2
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ↑(constantCoeff σ k) φ = 0 ∨ ↑(constantCoeff σ k) ψ = 0
⊢ 0 = ψ⁻¹ * φ⁻¹
case pos
σ : Type u_1
R : Type ?u.1945318
k : Type u_2
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ↑(constantCoeff σ k) (φ * ψ) = 0
⊢ 0 = ψ⁻¹ * φ⁻¹
simp only [map_mul, mul_eq_zero] at h
no goals
case pos
σ : Type u_1
R : Type ?u.1945318
k : Type u_2
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ↑(constantCoeff σ k) φ = 0 ∨ ↑(constantCoeff σ k) ψ = 0
⊢ 0 = ψ⁻¹ * φ⁻¹
cases' h with h h <;> simp [inv_eq_zero.mpr h]
case neg
σ : Type u_1
R : Type ?u.1945318
k : Type u_2
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬↑(constantCoeff σ k) (φ * ψ) = 0
⊢ ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1
case neg
σ : Type u_1
R : Type ?u.1945318
k : Type u_2
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬↑(constantCoeff σ k) (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
rw [MvPowerSeries.inv_eq_iff_mul_eq_one h]
case neg
σ : Type u_1
R : Type ?u.1945318
k : Type u_2
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬↑(constantCoeff σ k) φ = 0 ∧ ¬↑(constantCoeff σ k) ψ = 0
⊢ ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1
case neg
σ : Type u_1
R : Type ?u.1945318
k : Type u_2
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬↑(constantCoeff σ k) (φ * ψ) = 0
⊢ ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1
simp only [not_or, map_mul, mul_eq_zero] at h
no goals
case neg
σ : Type u_1
R : Type ?u.1945318
k : Type u_2
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬↑(constantCoeff σ k) φ = 0 ∧ ¬↑(constantCoeff σ k) ψ = 0
⊢ ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1
rw [← mul_assoc, mul_assoc _⁻¹, MvPowerSeries.inv_mul_cancel _ h.left, mul_one,
  MvPowerSeries.inv_mul_cancel _ h.right]