awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : ∀ (x y : R), v (x + y) ≤ max (v x) (v y)
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
      max
        (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
        (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
h :
  max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) f) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)
inl :
  max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)) ≤
    gaussNorm v c f
⊢ max
        (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
        (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)) ≤
      gaussNorm v c f ∨
    max
        (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
        (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)) ≤
      gaussNorm v c g

Tactic:
left
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : ∀ (x y : R), v (x + y) ≤ max (v x) (v y)
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
      max
        (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
        (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
h :
  max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) f) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)
⊢ max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)) ≤
    gaussNorm v c f

Tactic:
simpa [h] using le_gaussNorm v c f hbfd t

Premises used: MvPowerSeries.le_gaussNorm
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : ∀ (x y : R), v (x + y) ≤ max (v x) (v y)
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
      max
        (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
        (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
h :
  max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) g) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)
inr :
  max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)) ≤
    gaussNorm v c g
⊢ max
        (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
        (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)) ≤
      gaussNorm v c f ∨
    max
        (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
        (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)) ≤
      gaussNorm v c g

Tactic:
right
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : ∀ (x y : R), v (x + y) ≤ max (v x) (v y)
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
      max
        (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
        (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
t : σ →₀ ℕ
h :
  max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)) =
    v ((coeff t : (a : MvPowerSeries σ R) → R) g) * ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)
⊢ max
      (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
      (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ)) ≤
    gaussNorm v c g

Tactic:
simpa [h] using le_gaussNorm v c g hbgd t

Premises used: MvPowerSeries.le_gaussNorm
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : ∀ (x y : R), v (x + y) ≤ max (v x) (v y)
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
      max
        (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
        (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
⊢ ∀ (i : σ →₀ ℕ),
    (v ((coeff i : (a : MvPowerSeries σ R) → R) (f + g)) * i.prod fun (x1 : σ) (x2 : ℕ) ↦ c x1 ^ x2) ≤
      max (gaussNorm v c f) (gaussNorm v c g)

Tactic:
refine fun t ↦ calc
    _ ≤ _ := Final t
    _ ≤ max (gaussNorm v c f) (gaussNorm v c g) := by
      simp only [le_sup_iff]
      rcases max_choice (v ((coeff t) f) * ∏ i ∈ t.support, c i ^ t i)
        (v ((coeff t) g) * ∏ i ∈ t.support, c i ^ t i) with h | h
      · left
        simpa [h] using le_gaussNorm v c f hbfd t
      · right
        simpa [h] using le_gaussNorm v c g hbgd t

Premises used: Trans.trans
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : ∀ (x y : R), v (x + y) ≤ max (v x) (v y)
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
      max
        (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
        (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
refine_2 : 0 ≤ gaussNorm v c f ∨ 0 ≤ gaussNorm v c g
⊢ 0 ≤ max (gaussNorm v c f) (gaussNorm v c g)

Tactic:
simp only [le_sup_iff]

Premises used: le_sup_iff
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : ∀ (x y : R), v (x + y) ≤ max (v x) (v y)
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
      max
        (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
        (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
refine_2 : 0 ≤ gaussNorm v c f
⊢ 0 ≤ gaussNorm v c f ∨ 0 ≤ gaussNorm v c g

Tactic:
left
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : ∀ (x y : R), v (x + y) ≤ max (v x) (v y)
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
      max
        (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
        (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
⊢ 0 ≤ gaussNorm v c f

Tactic:
gaussNorm_nonneg v c f vNonneg

Premises used: MvPowerSeries.gaussNorm_nonneg
-- Module: Mathlib.RingTheory.MvPowerSeries.GaussNorm
Goal:
R : Type u_1
σ : Type u_2
inst : Semiring R
v : R → ℝ
c : σ → ℝ
f g : MvPowerSeries σ R
hc : 0 ≤ c
vNonneg : ∀ (a : R), v a ≥ 0
hv : ∀ (x y : R), v (x + y) ≤ max (v x) (v y)
hbfd : HasGaussNorm v c f
hbgd : HasGaussNorm v c g
H : ∀ (t : σ →₀ ℕ), LE.le (α := ℝ) 0 (∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
Final :
  ∀ (t : σ →₀ ℕ),
    v ((coeff t : (a : MvPowerSeries σ R) → R) (f + g)) *
        ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ) ≤
      max
        (v ((coeff t : (a : MvPowerSeries σ R) → R) f) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
        (v ((coeff t : (a : MvPowerSeries σ R) → R) g) *
          ∏ i ∈ t.support, HPow.hPow (β := ℕ) (c i) ((t : (a : σ) → ℕ) i : ℕ))
⊢ 0 ≤ gaussNorm v c f

Tactic:
exact gaussNorm_nonneg v c f vNonneg

Premises used: MvPowerSeries.gaussNorm_nonneg
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : DecidableEq σ
n : σ →₀ ℕ
a : R
φ : MvPowerSeries σ R
refl :
  inv.aux a φ n =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
              ((coeff x.2 : (a : MvPowerSeries σ R) → R) (inv.aux a φ) : R)
          else 0
⊢ inv.aux a φ n =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
              ((coeff x.2 : (a : MvPowerSeries σ R) → R) (inv.aux a φ) : R)
          else 0

Tactic:
cases Subsingleton.elim ‹DecidableEq σ› (Classical.decEq σ)

Premises used: Subsingleton.elim, Classical.decEq
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
n : σ →₀ ℕ
a : R
φ : MvPowerSeries σ R
refl :
  (if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
          if x_1 : x.2 < n then HMul.hMul (α := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R) (inv.aux a φ x.2)
          else 0) =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
              ((coeff x.2 : (a : MvPowerSeries σ R) → R) (inv.aux a φ) : R)
          else 0
⊢ inv.aux a φ n =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
              ((coeff x.2 : (a : MvPowerSeries σ R) → R) (inv.aux a φ) : R)
          else 0

Tactic:
rw [inv.aux]

Premises used: MvPowerSeries.inv.aux
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
n : σ →₀ ℕ
a : R
φ : MvPowerSeries σ R
⊢ (if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
          if x_1 : x.2 < n then HMul.hMul (α := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R) (inv.aux a φ x.2)
          else 0) =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
              ((coeff x.2 : (a : MvPowerSeries σ R) → R) (inv.aux a φ) : R)
          else 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
u : Rˣ
⊢ (coeff n : (a : MvPowerSeries σ R) → R) (inv.aux (↑u⁻¹ : R) φ) =
    if n = 0 then (↑u⁻¹ : R)
    else
      -(↑u⁻¹ : R) *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
              ((coeff x.2 : (a : MvPowerSeries σ R) → R) (inv.aux (↑u⁻¹ : R) φ) : R)
          else 0

Tactic:
coeff_inv_aux n (↑u⁻¹) φ

Premises used: MvPowerSeries.coeff_inv_aux
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ R
u : Rˣ
⊢ (coeff n : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) =
    if n = 0 then (↑u⁻¹ : R)
    else
      -(↑u⁻¹ : R) *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
              ((coeff x.2 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R)
          else 0

Tactic:
convert! coeff_inv_aux n (↑u⁻¹) φ

Premises used: MvPowerSeries.coeff_inv_aux
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
rw : (coeff 0 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
rw₁ :
  (if Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0 then (↑u⁻¹ : R)
    else
      -(↑u⁻¹ : R) *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ 0,
          if x.2 < 0 then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
              ((coeff x.2 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R)
          else 0) =
    (↑u⁻¹ : R)
rw₂ rw₃ : (↑u⁻¹ : R) = (↑u⁻¹ : R)
⊢ (constantCoeff : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)

Tactic:
rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff_apply, if_pos, MvPowerSeries.coeff_invOfUnit, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
rw : (coeff 0 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
rw₁ :
  (if Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0 then (↑u⁻¹ : R)
    else
      -(↑u⁻¹ : R) *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ 0,
          if x.2 < 0 then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
              ((coeff x.2 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R)
          else 0) =
    (↑u⁻¹ : R)
rw₂ rw₃ : (↑u⁻¹ : R) = (↑u⁻¹ : R)
⊢ (constantCoeff : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)

Tactic:
classical
  rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff_apply, if_pos, MvPowerSeries.coeff_invOfUnit, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff : (a : MvPowerSeries σ R) → R) φ = (↑u : R)
n : σ →₀ ℕ
this : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : n = 0
rw :
  Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) (φ * φ.invOfUnit u) : R)
    ((coeff 0 : (a : MvPowerSeries σ R) → R) 1 : R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * φ.invOfUnit u) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R)

Tactic:
rw [H]
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff : (a : MvPowerSeries σ R) → R) φ = (↑u : R)
n : σ →₀ ℕ
this : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : n = 0
⊢ Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) (φ * φ.invOfUnit u) : R)
    ((coeff 0 : (a : MvPowerSeries σ R) → R) 1 : R)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff : (a : MvPowerSeries σ R) → R) φ = (↑u : R)
n : σ →₀ ℕ
this : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
rw : (0, n).1 + (0, n).2 = n
rw₁ rw₂ : (0, n).2 = n
⊢ (0, n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n

Tactic:
rw [mem_antidiagonal, zero_add]

Premises used: zero_add, Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff : (a : MvPowerSeries σ R) → R) φ = (↑u : R)
n : σ →₀ ℕ
this : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
⊢ (0, n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n

Tactic:
have : ((0 : σ →₀ ℕ), n) ∈ antidiagonal n := by rw [mem_antidiagonal, zero_add]
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff : (a : MvPowerSeries σ R) → R) φ = (↑u : R)
n : σ →₀ ℕ
this_1 : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n
rw :
  ∀ x ∈ (@antidiagonal _ Finsupp.instAddMonoid _ n).erase (0, n),
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R) =
      if x.2 < (0, n).2 then
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R)
      else 0
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * φ.invOfUnit u) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R)

Tactic:
rw [coeff_one, if_neg H, coeff_mul, ← Finset.insert_erase this,
        Finset.sum_insert (Finset.notMem_erase _ _), coeff_zero_eq_constantCoeff_apply, h,
        coeff_invOfUnit, if_neg H, neg_mul, mul_neg, Units.mul_inv_cancel_left, ←
        Finset.insert_erase this, Finset.sum_insert (Finset.notMem_erase _ _),
        Finset.insert_erase this, if_neg (not_lt_of_ge <| le_rfl), zero_add, add_comm, ←
        sub_eq_add_neg, sub_eq_zero, Finset.sum_congr rfl]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff_apply, le_rfl, sub_eq_zero, sub_eq_add_neg, MvPowerSeries.coeff_one, zero_add, add_comm, Units.mul_inv_cancel_left, MvPowerSeries.coeff_invOfUnit, neg_mul, Finset.notMem_erase, Finset.sum_insert, Finset.insert_erase, if_neg, Finset.sum_congr, rfl, mul_neg, MvPowerSeries.coeff_mul, not_lt_of_ge
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff : (a : MvPowerSeries σ R) → R) φ = (↑u : R)
n : σ →₀ ℕ
this_1 : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n
i j : σ →₀ ℕ
hij : (i, j) ∈ (@antidiagonal _ Finsupp.instAddMonoid _ n).erase (0, n)
⊢ (i, j) ≠ (0, n) ∧ (i, j).1 + (i, j).2 = n

Tactic:
rw [Finset.mem_erase, mem_antidiagonal] at hij

Premises used: Finset.mem_erase, Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff : (a : MvPowerSeries σ R) → R) φ = (↑u : R)
n : σ →₀ ℕ
this_1 : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n
i j : σ →₀ ℕ
hij : (i, j) ≠ (0, n) ∧ (i, j).1 + (i, j).2 = n
obtain :
  ∀ (H : ¬(i, j).1 + (i, j).2 = 0)
    (this : (0, (i, j).1 + (i, j).2) ∈ @antidiagonal _ Finsupp.instAddMonoid _ ((i, j).1 + (i, j).2))
    (h₁ : (i, j) ≠ (0, (i, j).1 + (i, j).2)),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R) =
      if (i, j).2 < (0, (i, j).1 + (i, j).2).2 then
        HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R)
      else 0
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R) =
    if (i, j).2 < (0, n).2 then
      HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R)
    else 0

Tactic:
obtain ⟨h₁, rfl⟩ := hij

Premises used: rfl