awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
rw :
  Eq.{u_3 + 1} (α := S)
    ((f : (a : R) → S)
        (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
          HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff p.2 : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
    ((coeff n : (a : MvPowerSeries σ S) → S)
        (HMul.hMul (α := MvPowerSeries σ S)
          (fun (n : σ →₀ ℕ) ↦ (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
rw₁ :
  Eq.{u_3 + 1} (α := S)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
        (f : (a : R) → S)
          (HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff x.2 : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
    ((coeff n : (a : MvPowerSeries σ S) → S)
        (HMul.hMul (α := MvPowerSeries σ S)
          (fun (n : σ →₀ ℕ) ↦ (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
rw₂ rw₃ rw₄ :
  Eq.{u_3 + 1} (α := S)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
      (f : (a : R) → S)
        (HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) ψ : R)))
    (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
      HMul.hMul (α := S) (β := S)
        ((coeff p.1 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
            (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) :
          S)
        ((coeff p.2 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
            (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) :
          S))
⊢ Eq.{u_3 + 1} (α := S) ((f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * ψ) : R) : S)
    ((coeff n : (a : MvPowerSeries σ S) → S)
        (HMul.hMul (α := MvPowerSeries σ S)
          (fun (n : σ →₀ ℕ) ↦ (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R)) :
      S)
have rw₅ : ∀ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
  (f : (a : R) → S)
      (HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) ψ : R)) =
    HMul.hMul (α := S) (β := S)
      ((coeff x.1 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R) :
        S)
      ((coeff x.2 : (a : MvPowerSeries σ S) → S) fun (n : σ →₀ ℕ) ↦
          (f : (a : R) → S) ((coeff n : (a : MvPowerSeries σ R) → R) ψ : R) :
        S)
Tactic: classical
        rw [coeff_mul, map_sum, coeff_mul]
        apply Finset.sum_congr rfl
        rintro ⟨i, j⟩ _; rw [f.map_mul]; rfl
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
n : σ →₀ ℕ
a : R
⊢ Eq (α := MvPowerSeries σ S)
    ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) ((monomial n : (a : R) → MvPowerSeries σ R) a) :
      MvPowerSeries σ S)
    ((monomial n : (a : S) → MvPowerSeries σ S) ((f : (a : R) → S) a) : MvPowerSeries σ S)
have h : ∀ (m : σ →₀ ℕ),
  Eq.{u_3 + 1} (α := S)
    ((coeff m : (a : MvPowerSeries σ S) → S)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) ((monomial n : (a : R) → MvPowerSeries σ R) a) :
          MvPowerSeries σ S) :
      S)
    ((coeff m : (a : MvPowerSeries σ S) → S)
        ((monomial n : (a : S) → MvPowerSeries σ S) ((f : (a : R) → S) a) : MvPowerSeries σ S) :
      S)
Tactic: ext m
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
n : σ →₀ ℕ
a : R
⊢ Eq (α := MvPowerSeries σ S)
    ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) ((monomial n : (a : R) → MvPowerSeries σ R) a) :
      MvPowerSeries σ S)
    ((monomial n : (a : S) → MvPowerSeries σ S) ((f : (a : R) → S) a) : MvPowerSeries σ S)
have h : ∀ (m : σ →₀ ℕ),
  Eq.{u_3 + 1} (α := S)
    ((coeff m : (a : MvPowerSeries σ S) → S)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) ((monomial n : (a : R) → MvPowerSeries σ R) a) :
          MvPowerSeries σ S) :
      S)
    ((coeff m : (a : MvPowerSeries σ S) → S)
        ((monomial n : (a : S) → MvPowerSeries σ S) ((f : (a : R) → S) a) : MvPowerSeries σ S) :
      S)
Tactic: classical
  ext m
  simp [coeff_monomial, apply_ite f]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
S₁ : Type u_5
S₂ : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
f : R →+* S₁
g : S₁ →+* S₂
p : MvPowerSeries σ R
⊢ Eq (α := MvPowerSeries σ S₂)
    ((map g : (a : MvPowerSeries σ S₁) → MvPowerSeries σ S₂)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S₁) p) :
      MvPowerSeries σ S₂)
    ((map (g.comp f) : (a : MvPowerSeries σ R) → MvPowerSeries σ S₂) p : MvPowerSeries σ S₂)
have h : ∀ (n : σ →₀ ℕ),
  Eq.{u_6 + 1} (α := S₂)
    ((coeff n : (a : MvPowerSeries σ S₂) → S₂)
        ((map g : (a : MvPowerSeries σ S₁) → MvPowerSeries σ S₂)
            ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S₁) p) :
          MvPowerSeries σ S₂) :
      S₂)
    ((coeff n : (a : MvPowerSeries σ S₂) → S₂)
        ((map (g.comp f) : (a : MvPowerSeries σ R) → MvPowerSeries σ S₂) p : MvPowerSeries σ S₂) :
      S₂)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : DivisionSemiring R
inst_1 : Semiring S
inst_2 : Nontrivial S
φ : MvPowerSeries σ R
f : R →+* S
⊢ Eq (α := MvPowerSeries σ S) ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ : MvPowerSeries σ S)
      (0 : MvPowerSeries σ S) ↔
    φ = 0
have simp : (∀ (n : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := S)
      ((coeff n : (a : MvPowerSeries σ S) → S)
          ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ : MvPowerSeries σ S) :
        S)
      ((coeff n : (a : MvPowerSeries σ S) → S) 0 : S)) ↔
  ∀ (n : σ →₀ ℕ),
    Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)
Tactic: simp only [MvPowerSeries.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : DivisionSemiring R
inst_1 : Semiring S
inst_2 : Nontrivial S
φ : MvPowerSeries σ R
f : R →+* S
⊢ (∀ (n : σ →₀ ℕ),
      Eq.{u_3 + 1} (α := S)
        ((coeff n : (a : MvPowerSeries σ S) → S)
            ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ : MvPowerSeries σ S) :
          S)
        ((coeff n : (a : MvPowerSeries σ S) → S) 0 : S)) ↔
    ∀ (n : σ →₀ ℕ),
      Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)
have a : ∀ (n : σ →₀ ℕ),
  Eq.{u_3 + 1} (α := S)
      ((coeff n : (a : MvPowerSeries σ S) → S)
          ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ : MvPowerSeries σ S) :
        S)
      ((coeff n : (a : MvPowerSeries σ S) → S) 0 : S) ↔
    Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) 0 : R)
Tactic: congr! with n
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
⊢ HPow.hPow (α := MvPowerSeries σ R) (X s) n ∣ φ ↔
    ∀ (m : σ →₀ ℕ),
      (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have mp : HPow.hPow (α := MvPowerSeries σ R) (X s) n ∣ φ →
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
mp :
  HPow.hPow (α := MvPowerSeries σ R) (X s) n ∣ φ →
    ∀ (m : σ →₀ ℕ),
      (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
⊢ HPow.hPow (α := MvPowerSeries σ R) (X s) n ∣ φ ↔
    ∀ (m : σ →₀ ℕ),
      (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have mpr : (∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)) →
  HPow.hPow (α := MvPowerSeries σ R) (X s) n ∣ φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : (m : (a : σ) → ℕ) s < n
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n * φ) : R)
    (0 : R)
have mp : ∀ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
  HMul.hMul (α := R) (β := R)
      ((coeff x.1 : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) φ : R) =
    0
Tactic: rw [coeff_mul, Finset.sum_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : (m : (a : σ) → ℕ) s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
⊢ HMul.hMul (α := R) (β := R)
      ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) φ : R) =
    0
have mp : ¬(i, j).1 = single s n
Tactic: rw [coeff_X_pow, if_neg, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m : σ →₀ ℕ
h : (m : (a : σ) → ℕ) s < n
i j : σ →₀ ℕ
hij : (i, j) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
⊢ ¬(i, j).1 = single s n
have mp : ∀ (h : (i, j).1 = single s n), n ≤ (m : (a : σ) → ℕ) s
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m i j : σ →₀ ℕ
hij : (i, j) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
h : i = single s n
⊢ n ≤ (m : (a : σ) → ℕ) s
have hij₁ : (single s n, j) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
Tactic: subst i
Cleared hypotheses: i, hij, h
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
⊢ n ≤ (m : (a : σ) → ℕ) s
have hij₁ : (single s n, j).1 + (single s n, j).2 = m
Tactic: rw [mem_antidiagonal] at hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
m j : σ →₀ ℕ
hij : (single s n, j).1 + (single s n, j).2 = m
⊢ n ≤ (m : (a : σ) → ℕ) s
have mp : n ≤ HAdd.hAdd (β := ℕ) n (((single s n, j).2 : (a : σ) → ℕ) s : ℕ)
Tactic: rw [← hij, Finsupp.add_apply, Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
⊢ HPow.hPow (α := MvPowerSeries σ R) (X s) n ∣ φ
have mpr : φ =
  HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
    (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ
Tactic: refine ⟨fun m => coeff (m + single s n) φ, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
⊢ φ =
    HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
      (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ
have mpr : ∀ (m : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ) :
      R)
Tactic: ext m
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ) :
      R)
have pos : ∀ (H : m - single s n + single s n = m),
  Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ) :
      R)
Tactic: by_cases H : m - single s n + single s n = m
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
pos :
  ∀ (H : m - single s n + single s n = m),
    Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
      ((coeff m : (a : MvPowerSeries σ R) → R)
          (HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
            (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ) :
        R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ) :
      R)
have neg : ∀ (H : ¬m - single s n + single s n = m),
  Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ) :
      R)
Tactic: by_cases H : m - single s n + single s n = m
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : m - single s n + single s n = m
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ) :
      R)
have pos : (coeff m : (a : MvPowerSeries σ R) → R) φ =
  HMul.hMul (α := R) (β := R)
    ((coeff (single s n, m - single s n).1 : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) :
      R)
    ((coeff (single s n, m - single s n).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
        (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
      R)
Tactic: rw [coeff_mul, Finset.sum_eq_single (single s n, m - single s n)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : m - single s n + single s n = m
pos :
  (coeff m : (a : MvPowerSeries σ R) → R) φ =
    HMul.hMul (α := R) (β := R)
      ((coeff (single s n, m - single s n).1 : (a : MvPowerSeries σ R) → R)
          (HPow.hPow (α := MvPowerSeries σ R) (X s) n) :
        R)
      ((coeff (single s n, m - single s n).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R)
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ) :
      R)
have pos₁ : ∀ b ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
  b ≠ (single s n, m - single s n) →
    HMul.hMul (α := R) (β := R)
        ((coeff b.1 : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) : R)
        ((coeff b.2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
            (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
          R) =
      0
Tactic: rw [coeff_mul, Finset.sum_eq_single (single s n, m - single s n)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : m - single s n + single s n = m
pos :
  (coeff m : (a : MvPowerSeries σ R) → R) φ =
    HMul.hMul (α := R) (β := R)
      ((coeff (single s n, m - single s n).1 : (a : MvPowerSeries σ R) → R)
          (HPow.hPow (α := MvPowerSeries σ R) (X s) n) :
        R)
      ((coeff (single s n, m - single s n).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R)
pos₁ :
  ∀ b ∈ @antidiagonal _ Finsupp.instAddMonoid _ m,
    b ≠ (single s n, m - single s n) →
      HMul.hMul (α := R) (β := R)
          ((coeff b.1 : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) : R)
          ((coeff b.2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
              (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
            R) =
        0
⊢ Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
    ((coeff m : (a : MvPowerSeries σ R) → R)
        (HPow.hPow (α := MvPowerSeries σ R) (X s) n * fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ) :
      R)
have pos₂ : (single s n, m - single s n) ∉ @antidiagonal _ Finsupp.instAddMonoid _ m →
  HMul.hMul (α := R) (β := R)
      ((coeff (single s n, m - single s n).1 : (a : MvPowerSeries σ R) → R)
          (HPow.hPow (α := MvPowerSeries σ R) (X s) n) :
        R)
      ((coeff (single s n, m - single s n).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0
Tactic: rw [coeff_mul, Finset.sum_eq_single (single s n, m - single s n)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : m - single s n + single s n = m
⊢ (coeff m : (a : MvPowerSeries σ R) → R) φ =
    HMul.hMul (α := R) (β := R)
      ((coeff (single s n, m - single s n).1 : (a : MvPowerSeries σ R) → R)
          (HPow.hPow (α := MvPowerSeries σ R) (X s) n) :
        R)
      ((coeff (single s n, m - single s n).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R)
have pos : Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R)
  ((coeff (single s n, m - single s n).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
      (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
    R)
Tactic: rw [coeff_X_pow, if_pos rfl, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j) ∈ @antidiagonal _ Finsupp.instAddMonoid _ m
hne : (i, j) ≠ (single s n, m - single s n)
⊢ HMul.hMul (α := R) (β := R)
      ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0
have hij₁ : (i, j).1 + (i, j).2 = m
Tactic: rw [mem_antidiagonal] at hij
Cleared hypotheses: hij, hne
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
⊢ HMul.hMul (α := R) (β := R)
      ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) (HPow.hPow (α := MvPowerSeries σ R) (X s) n) : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0
have pos : HMul.hMul (α := R) (β := R) (if (i, j).1 = single s n then 1 else 0 : R)
    ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
        (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
      R) =
  0
Tactic: rw [coeff_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h :
  ∀ (m : σ →₀ ℕ),
    (m : (a : σ) → ℕ) s < n → Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
⊢ HMul.hMul (α := R) (β := R) (if (i, j).1 = single s n then 1 else 0 : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0
have pos : ∀ (hi : (i, j).1 = single s n),
  HMul.hMul (α := R) (β := R) (1 : R)
      ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) fun (m : σ →₀ ℕ) ↦
          (coeff (m + single s n) : (a : MvPowerSeries σ R) → R) φ :
        R) =
    0
Tactic: split_ifs with hi