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
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 : n ≤ (m : (a : σ) → ℕ) s
t : σ
⊢ Eq (α := ℕ) ((m - single s n + single s n : (a : σ) → ℕ) t : ℕ) ((m : (a : σ) → ℕ) t : ℕ)
have pos : ∀ (hst : s = t), Eq (α := ℕ) ((m - single s n + single s n : (a : σ) → ℕ) t : ℕ) ((m : (a : σ) → ℕ) t : ℕ)
Tactic: by_cases hst : s = t
-- 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 : n ≤ (m : (a : σ) → ℕ) s
t : σ
pos : ∀ (hst : s = t), Eq (α := ℕ) ((m - single s n + single s n : (a : σ) → ℕ) t : ℕ) ((m : (a : σ) → ℕ) t : ℕ)
⊢ Eq (α := ℕ) ((m - single s n + single s n : (a : σ) → ℕ) t : ℕ) ((m : (a : σ) → ℕ) t : ℕ)
have neg : ∀ (hst : ¬s = t), Eq (α := ℕ) ((m - single s n + single s n : (a : σ) → ℕ) t : ℕ) ((m : (a : σ) → ℕ) t : ℕ)
Tactic: by_cases hst : s = t
-- 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 : n ≤ (m : (a : σ) → ℕ) s
t : σ
hst : s = t
⊢ Eq (α := ℕ) ((m - single s n + single s n : (a : σ) → ℕ) t : ℕ) ((m : (a : σ) → ℕ) t : ℕ)
have pos : Eq (α := ℕ) ((m - single s n + single s n : (a : σ) → ℕ) s : ℕ) ((m : (a : σ) → ℕ) s : ℕ)
Tactic: subst t
Cleared hypotheses: t, hst
-- 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: classical
  constructor
  · rintro ⟨φ, rfl⟩ m h
    rw [coeff_mul, Finset.sum_eq_zero]
    rintro ⟨i, j⟩ hij
    rw [coeff_X_pow, if_neg, zero_mul]
    contrapose! h
    dsimp at h
    subst i
    rw [mem_antidiagonal] at hij
    rw [← hij, Finsupp.add_apply, Finsupp.single_eq_same]
    exact Nat.le_add_right n _
  · intro h
    refine ⟨fun m => coeff (m + single s n) φ, ?_⟩
    ext m
    by_cases H : m - single s n + single s n = m
    · rw [coeff_mul, Finset.sum_eq_single (single s n, m - single s n)]
      · rw [coeff_X_pow, if_pos rfl, one_mul]
        simpa using congr_arg (fun m : σ →₀ ℕ => coeff m φ) H.symm
      · rintro ⟨i, j⟩ hij hne
        rw [mem_antidiagonal] at hij
        rw [coeff_X_pow]
        split_ifs with hi
        · exfalso
          apply hne
          rw [← hij, ← hi, Prod.mk_inj]
          refine ⟨rfl, ?_⟩
          ext t
          simp only [add_tsub_cancel_left]
        · exact zero_mul _
      · intro hni
        exfalso
        apply hni
        rwa [mem_antidiagonal, add_comm]
    · rw [h, coeff_mul, Finset.sum_eq_zero]
      · rintro ⟨i, j⟩ hij
        rw [mem_antidiagonal] at hij
        rw [coeff_X_pow]
        split_ifs with hi
        · exfalso
          apply H
          rw [← hij, hi]
          ext
          rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm]
        · exact zero_mul _
      · contrapose! H
        ext t
        by_cases hst : s = t
        · subst t
          simpa using tsub_add_cancel_of_le H
        · simp [hst]
-- 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: classical
  constructor
  · rintro ⟨φ, rfl⟩ m h
    rw [coeff_mul, Finset.sum_eq_zero]
    rintro ⟨i, j⟩ hij
    rw [coeff_X_pow, if_neg, zero_mul]
    contrapose! h
    dsimp at h
    subst i
    rw [mem_antidiagonal] at hij
    rw [← hij, Finsupp.add_apply, Finsupp.single_eq_same]
    exact Nat.le_add_right n _
  · intro h
    refine ⟨fun m => coeff (m + single s n) φ, ?_⟩
    ext m
    by_cases H : m - single s n + single s n = m
    · rw [coeff_mul, Finset.sum_eq_single (single s n, m - single s n)]
      · rw [coeff_X_pow, if_pos rfl, one_mul]
        simpa using congr_arg (fun m : σ →₀ ℕ => coeff m φ) H.symm
      · rintro ⟨i, j⟩ hij hne
        rw [mem_antidiagonal] at hij
        rw [coeff_X_pow]
        split_ifs with hi
        · exfalso
          apply hne
          rw [← hij, ← hi, Prod.mk_inj]
          refine ⟨rfl, ?_⟩
          ext t
          simp only [add_tsub_cancel_left]
        · exact zero_mul _
      · intro hni
        exfalso
        apply hni
        rwa [mem_antidiagonal, add_comm]
    · rw [h, coeff_mul, Finset.sum_eq_zero]
      · rintro ⟨i, j⟩ hij
        rw [mem_antidiagonal] at hij
        rw [coeff_X_pow]
        split_ifs with hi
        · exfalso
          apply H
          rw [← hij, hi]
          ext
          rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm]
        · exact zero_mul _
      · contrapose! H
        ext t
        by_cases hst : s = t
        · subst t
          simpa using tsub_add_cancel_of_le H
        · simp [hst]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ X s ∣ φ ↔
    ∀ (m : σ →₀ ℕ),
      Eq (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) →
        Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have rw : (∀ (m : σ →₀ ℕ),
    LT.lt (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (1 : ℕ) →
      Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)) ↔
  ∀ (m : σ →₀ ℕ),
    Eq (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) →
      Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
Tactic: rw [← pow_one (X s : MvPowerSeries σ R), X_pow_dvd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ (∀ (m : σ →₀ ℕ),
      LT.lt (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (1 : ℕ) →
        Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)) ↔
    ∀ (m : σ →₀ ℕ),
      Eq (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) →
        Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have mp : (∀ (m : σ →₀ ℕ),
    LT.lt (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (1 : ℕ) →
      Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)) →
  ∀ (m : σ →₀ ℕ),
    Eq (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) →
      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 : σ
φ : MvPowerSeries σ R
mp :
  (∀ (m : σ →₀ ℕ),
      LT.lt (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (1 : ℕ) →
        Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)) →
    ∀ (m : σ →₀ ℕ),
      Eq (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) →
        Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
⊢ (∀ (m : σ →₀ ℕ),
      LT.lt (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (1 : ℕ) →
        Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)) ↔
    ∀ (m : σ →₀ ℕ),
      Eq (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) →
        Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)
have mpr : (∀ (m : σ →₀ ℕ),
    Eq (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (0 : ℕ) →
      Eq.{u_2 + 1} (α := R) ((coeff m : (a : MvPowerSeries σ R) → R) φ : R) (0 : R)) →
  ∀ (m : σ →₀ ℕ),
    LT.lt (α := ℕ) ((m : (a : σ) → ℕ) s : ℕ) (1 : ℕ) →
      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_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ ∅, f j) : R)
    (∑ l ∈ finsuppAntidiag ∅ d, ∏ i ∈ ∅, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)
have empty : Eq.{u_3 + 1} (α := R) (if d = 0 then 1 else 0)
  (↑(card (α := Finsupp.{u_4, u_1} ι (σ →₀ ℕ)) (if d = 0 then {0} else ∅)) : R)
Tactic: simp only [prod_empty, sum_const, nsmul_eq_mul, mul_one, coeff_one, finsuppAntidiag_empty]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := R) (if d = 0 then 1 else 0)
    (↑(card (α := Finsupp.{u_4, u_1} ι (σ →₀ ℕ)) (if d = 0 then {0} else ∅)) : R)
have pos : d = 0 → Eq.{u_3 + 1} (α := R) 1 (↑(card (α := Finsupp.{u_4, u_1} ι (σ →₀ ℕ)) {0}) : R)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
d : σ →₀ ℕ
pos : d = 0 → Eq.{u_3 + 1} (α := R) 1 (↑(card (α := Finsupp.{u_4, u_1} ι (σ →₀ ℕ)) {0}) : R)
⊢ Eq.{u_3 + 1} (α := R) (if d = 0 then 1 else 0)
    (↑(card (α := Finsupp.{u_4, u_1} ι (σ →₀ ℕ)) (if d = 0 then {0} else ∅)) : R)
have neg : ¬d = 0 → Eq.{u_3 + 1} (α := R) 0 (↑(card (α := Finsupp.{u_4, u_1} ι (σ →₀ ℕ)) ∅) : R)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ s, f j) : R)
      (∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)
d : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ insert a s, f j) : R)
    (∑ l ∈ (insert a s).finsuppAntidiag d,
        ∏ i ∈ insert a s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) :
      R)
have insert : Eq.{u_3 + 1} (α := R)
  (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ d,
    HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) (f a) : R)
      ((coeff p.2 : (a : MvPowerSeries σ R) → R) (∏ x ∈ s, f x) : R))
  (∑ x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ d,
    ∑
      i ∈
        Finset.map (α := ↥(s.finsuppAntidiag x.2))
          { toFun := fun (f : ↥(s.finsuppAntidiag x.2)) ↦ (↑f : ι →₀ σ →₀ ℕ).update a x.1, inj' := sorry }
          (attach (s.finsuppAntidiag x.2)),
      ∏ i_1 ∈ insert a s, (coeff ((i : (a : ι) → σ →₀ ℕ) i_1) : (a : MvPowerSeries σ R) → R) (f i_1))
Tactic: rw [finsuppAntidiag_insert ha, prod_insert ha, coeff_mul, sum_biUnion]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ s, f j) : R)
      (∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)
d : σ →₀ ℕ
insert :
  Eq.{u_3 + 1} (α := R)
    (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ d,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) (f a) : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) (∏ x ∈ s, f x) : R))
    (∑ x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ d,
      ∑
        i ∈
          Finset.map (α := ↥(s.finsuppAntidiag x.2))
            { toFun := fun (f : ↥(s.finsuppAntidiag x.2)) ↦ (↑f : ι →₀ σ →₀ ℕ).update a x.1, inj' := ⋯ }
            (attach (s.finsuppAntidiag x.2)),
        ∏ i_1 ∈ Insert.insert a s, (coeff ((i : (a : ι) → σ →₀ ℕ) i_1) : (a : MvPowerSeries σ R) → R) (f i_1))
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ Insert.insert a s, f j) : R)
    (∑ l ∈ (Insert.insert a s).finsuppAntidiag d,
        ∏ i ∈ Insert.insert a s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) :
      R)
have insert₁ : (↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ d) : Set ((σ →₀ ℕ) × (σ →₀ ℕ))).PairwiseDisjoint (α :=
  Finset (Finsupp.{u_4, u_1} ι (σ →₀ ℕ))) fun (p : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦
  Finset.map (α := ↥(s.finsuppAntidiag p.2))
    { toFun := fun (f : ↥(s.finsuppAntidiag p.2)) ↦ (↑f : ι →₀ σ →₀ ℕ).update a p.1, inj' := sorry }
    (attach (s.finsuppAntidiag p.2))
Tactic: rw [finsuppAntidiag_insert ha, prod_insert ha, coeff_mul, sum_biUnion]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ s, f j) : R)
      (∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)
d : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := R)
    (∑ p ∈ @antidiagonal _ Finsupp.instAddMonoid _ d,
      HMul.hMul (α := R) (β := R) ((coeff p.1 : (a : MvPowerSeries σ R) → R) (f a) : R)
        ((coeff p.2 : (a : MvPowerSeries σ R) → R) (∏ x ∈ s, f x) : R))
    (∑ x ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ d,
      ∑
        i ∈
          Finset.map (α := ↥(s.finsuppAntidiag x.2))
            { toFun := fun (f : ↥(s.finsuppAntidiag x.2)) ↦ (↑f : ι →₀ σ →₀ ℕ).update a x.1, inj' := ⋯ }
            (attach (s.finsuppAntidiag x.2)),
        ∏ i_1 ∈ insert a s, (coeff ((i : (a : ι) → σ →₀ ℕ) i_1) : (a : MvPowerSeries σ R) → R) (f i_1))
have insert : ∀ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ d,
  HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) (f a) : R)
      ((coeff x.2 : (a : MvPowerSeries σ R) → R) (∏ x ∈ s, f x) : R) =
    ∑
      i ∈
        Finset.map (α := ↥(s.finsuppAntidiag x.2))
          { toFun := fun (f : ↥(s.finsuppAntidiag x.2)) ↦ (↑f : ι →₀ σ →₀ ℕ).update a x.1, inj' := sorry }
          (attach (s.finsuppAntidiag x.2)),
      ∏ i_1 ∈ insert a s, (coeff ((i : (a : ι) → σ →₀ ℕ) i_1) : (a : MvPowerSeries σ R) → R) (f i_1)
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ s, f j) : R)
      (∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)
d : σ →₀ ℕ
⊢ ∀ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ d,
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) (f a) : R)
        ((coeff x.2 : (a : MvPowerSeries σ R) → R) (∏ x ∈ s, f x) : R) =
      ∑
        i ∈
          Finset.map (α := ↥(s.finsuppAntidiag x.2))
            { toFun := fun (f : ↥(s.finsuppAntidiag x.2)) ↦ (↑f : ι →₀ σ →₀ ℕ).update a x.1, inj' := ⋯ }
            (attach (s.finsuppAntidiag x.2)),
        ∏ i_1 ∈ insert a s, (coeff ((i : (a : ι) → σ →₀ ℕ) i_1) : (a : MvPowerSeries σ R) → R) (f i_1)
have insert : ∀ (a_1 b : σ →₀ ℕ),
  a_1 + b = d →
    HMul.hMul (α := R) (β := R) ((coeff a_1 : (a : MvPowerSeries σ R) → R) (f a) : R)
        ((coeff b : (a : MvPowerSeries σ R) → R) (∏ x ∈ s, f x) : R) =
      ∑ x ∈ attach (s.finsuppAntidiag b),
        ∏ x_1 ∈ insert a s,
          (coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑(↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) a a_1 x_1) :
              (a : MvPowerSeries σ R) → R)
            (f x_1)
Tactic: simp only [mem_antidiagonal, sum_map, Function.Embedding.coeFn_mk, coe_update, Prod.forall]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ s, f j) : R)
      (∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)
u v : σ →₀ ℕ
⊢ HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
      ((coeff v : (a : MvPowerSeries σ R) → R) (∏ x ∈ s, f x) : R) =
    ∑ x ∈ attach (s.finsuppAntidiag v),
      ∏ x_1 ∈ insert a s,
        (coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑(↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) a u x_1) :
            (a : MvPowerSeries σ R) → R)
          (f x_1)
have insert : Eq.{u_3 + 1} (α := R)
  (∑ x ∈ attach (s.finsuppAntidiag v),
    HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
      (∏ i ∈ s, (coeff (((↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R))
  (∑ x ∈ attach (s.finsuppAntidiag v),
    ∏ x_1 ∈ insert a s,
      (coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑(↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) a u x_1) :
          (a : MvPowerSeries σ R) → R)
        (f x_1))
Tactic: rw [ih, Finset.mul_sum, ← Finset.sum_attach]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ s, f j) : R)
      (∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)
u v : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := R)
    (∑ x ∈ attach (s.finsuppAntidiag v),
      HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
        (∏ i ∈ s, (coeff (((↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R))
    (∑ x ∈ attach (s.finsuppAntidiag v),
      ∏ x_1 ∈ insert a s,
        (coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑(↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) a u x_1) :
            (a : MvPowerSeries σ R) → R)
          (f x_1))
have insert : ∀ (x : ↥(s.finsuppAntidiag v)),
  Membership.mem (γ := Finset ↥(s.finsuppAntidiag v)) (attach (s.finsuppAntidiag v)) x →
    HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
        (∏ i ∈ s, (coeff (((↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R) =
      ∏ x_1 ∈ insert a s,
        (coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑(↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) a u x_1) :
            (a : MvPowerSeries σ R) → R)
          (f x_1)
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ s, f j) : R)
      (∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)
u v : σ →₀ ℕ
⊢ ∀ (x : ↥(s.finsuppAntidiag v)),
    Membership.mem (γ := Finset ↥(s.finsuppAntidiag v)) (attach (s.finsuppAntidiag v)) x →
      HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
          (∏ i ∈ s, (coeff (((↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R) =
        ∏ x_1 ∈ insert a s,
          (coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑(↑x : ι →₀ σ →₀ ℕ) : (a : ι) → σ →₀ ℕ) a u x_1) :
              (a : MvPowerSeries σ R) → R)
            (f x_1)
have insert : ∀ (a_1 : Finsupp.{u_4, u_1} ι (σ →₀ ℕ))
  (b : Membership.mem (γ := Finset (Finsupp.{u_4, u_1} ι (σ →₀ ℕ))) (s.finsuppAntidiag v) a_1),
  HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
      (∏ x ∈ s, (coeff ((a_1 : (a : ι) → σ →₀ ℕ) x) : (a : MvPowerSeries σ R) → R) (f x) : R) =
    HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
      (∏ x ∈ s,
          (coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑a_1 : (a : ι) → σ →₀ ℕ) a u x) :
              (a : MvPowerSeries σ R) → R)
            (f x) :
        R)
Tactic: simp only [mem_attach, Finset.prod_insert ha, Function.update_self, forall_true_left,
        Subtype.forall]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ s, f j) : R)
      (∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)
u v : σ →₀ ℕ
x : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)
⊢ HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
      (∏ x_1 ∈ s, (coeff ((x : (a : ι) → σ →₀ ℕ) x_1) : (a : MvPowerSeries σ R) → R) (f x_1) : R) =
    HMul.hMul (α := R) (β := R) ((coeff u : (a : MvPowerSeries σ R) → R) (f a) : R)
      (∏ x_1 ∈ s,
          (coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑x : (a : ι) → σ →₀ ℕ) a u x_1) :
              (a : MvPowerSeries σ R) → R)
            (f x_1) :
        R)
have insert : ∀ x_1 ∈ s,
  Eq.{u_3 + 1} (α := R) ((coeff ((x : (a : ι) → σ →₀ ℕ) x_1) : (a : MvPowerSeries σ R) → R) (f x_1) : R)
    ((coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑x : (a : ι) → σ →₀ ℕ) a u x_1) : (a : MvPowerSeries σ R) → R)
        (f x_1) :
      R)
Tactic: rw [Finset.prod_congr rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
inst_1 : DecidableEq ι
inst_2 : DecidableEq σ
f : ι → MvPowerSeries σ R
a : ι
s : Finset ι
ha : a ∉ s
ih :
  ∀ (d : σ →₀ ℕ),
    Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ j ∈ s, f j) : R)
      (∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (coeff ((l : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)
u v : σ →₀ ℕ
x : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)
i : ι
hi : i ∈ s
⊢ Eq.{u_3 + 1} (α := R) ((coeff ((x : (a : ι) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) (f i) : R)
    ((coeff (Function.update (β := fun (a : ι) ↦ σ →₀ ℕ) (⇑x : (a : ι) → σ →₀ ℕ) a u i) : (a : MvPowerSeries σ R) → R)
        (f i) :
      R)
have insert : i ≠ a
Tactic: rw [Function.update_of_ne]