awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : σ →₀ ℕ
⊢ (↑(@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' := ⋯ }
      (attach (s.finsuppAntidiag p.2))
have insert : ∀ (a_1 b : σ →₀ ℕ),
  a_1 + b = d →
    ∀ (a_3 b_1 : σ →₀ ℕ),
      a_3 + b_1 = d →
        (a_1 = a_3 → ¬b = b_1) →
          ∀ (a_6 : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)),
            Membership.mem (γ := Finset (Finsupp.{u_4, u_1} ι (σ →₀ ℕ))) (s.finsuppAntidiag b) a_6 →
              ∀ (x : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)),
                Membership.mem (γ := Finset (Finsupp.{u_4, u_1} ι (σ →₀ ℕ))) (s.finsuppAntidiag b_1) x →
                  ¬x.update a a_3 = a_6.update a a_1
Tactic: simp only [Set.PairwiseDisjoint, Set.Pairwise, mem_coe, mem_antidiagonal, ne_eq,
        disjoint_left, mem_map, mem_attach, Function.Embedding.coeFn_mk, true_and, Subtype.exists,
        exists_prop, not_exists, not_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
        Prod.forall, Prod.mk.injEq]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
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 u' v' : σ →₀ ℕ
huv : u' + v' = u + v
h : u = u' → ¬v = v'
k l : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)
hkl : l.update a u' = k.update a u
⊢ False
have huv₁ : u' + v' = u' + v
Tactic: obtain rfl : u' = u := by
        simpa only [Finsupp.coe_update, Function.update_self] using DFunLike.congr_fun hkl a
Cleared hypotheses: u, huv, h, hkl
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
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 u' v' : σ →₀ ℕ
huv : u' + v' = u + v
h : u = u' → ¬v = v'
k l : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)
hkl : l.update a u' = k.update a u
huv₁ : u' + v' = u' + v
⊢ False
have h₁ : u' = u' → ¬v = v'
Tactic: obtain rfl : u' = u := by
        simpa only [Finsupp.coe_update, Function.update_self] using DFunLike.congr_fun hkl a
Cleared hypotheses: u, huv, h, hkl
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
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 u' v' : σ →₀ ℕ
huv : u' + v' = u + v
h : u = u' → ¬v = v'
k l : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)
hkl : l.update a u' = k.update a u
huv₁ : u' + v' = u' + v
h₁ : u' = u' → ¬v = v'
⊢ False
have hkl₁ : l.update a u' = k.update a u'
Tactic: obtain rfl : u' = u := by
        simpa only [Finsupp.coe_update, Function.update_self] using DFunLike.congr_fun hkl a
Cleared hypotheses: u, huv, h, hkl
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
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)
v u' v' : σ →₀ ℕ
k l : Finsupp.{u_4, u_1} ι (σ →₀ ℕ)
huv : u' + v' = u' + v
h : u' = u' → ¬v = v'
hkl : l.update a u' = k.update a u'
⊢ False
have huv₁ : v' = v
Tactic: simp only [add_right_inj] at huv
Cleared hypotheses: huv
-- 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 : σ →₀ ℕ
s : Finset ι
⊢ 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)
have empty : ∀ (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)
Tactic: induction s using Finset.induction_on generalizing d with
  | empty =>
    simp only [prod_empty, sum_const, nsmul_eq_mul, mul_one, coeff_one, finsuppAntidiag_empty]
    split_ifs
    · simp only [card_singleton, Nat.cast_one]
    · simp only [card_empty, Nat.cast_zero]
  | insert a s ha ih =>
    rw [finsuppAntidiag_insert ha, prod_insert ha, coeff_mul, sum_biUnion]
    · apply Finset.sum_congr rfl
      simp only [mem_antidiagonal, sum_map, Function.Embedding.coeFn_mk, coe_update, Prod.forall]
      rintro u v rfl
      rw [ih, Finset.mul_sum, ← Finset.sum_attach]
      apply Finset.sum_congr rfl
      simp only [mem_attach, Finset.prod_insert ha, Function.update_self, forall_true_left,
        Subtype.forall]
      rintro x -
      rw [Finset.prod_congr rfl]
      intro i hi
      rw [Function.update_of_ne]
      exact ne_of_mem_of_not_mem hi ha
    · simp only [Set.PairwiseDisjoint, Set.Pairwise, mem_coe, mem_antidiagonal, ne_eq,
        disjoint_left, mem_map, mem_attach, Function.Embedding.coeFn_mk, true_and, Subtype.exists,
        exists_prop, not_exists, not_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
        Prod.forall, Prod.mk.injEq]
      rintro u v rfl u' v' huv h k - l - hkl
      obtain rfl : u' = u := by
        simpa only [Finsupp.coe_update, Function.update_self] using DFunLike.congr_fun hkl a
      simp only [add_right_inj] at huv
      exact h rfl huv.symm
Cleared hypotheses: d, s
-- 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 : σ →₀ ℕ
s : Finset ι
empty :
  ∀ (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)
⊢ 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)
have insert : ∀ (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)
Tactic: induction s using Finset.induction_on generalizing d with
  | empty =>
    simp only [prod_empty, sum_const, nsmul_eq_mul, mul_one, coeff_one, finsuppAntidiag_empty]
    split_ifs
    · simp only [card_singleton, Nat.cast_one]
    · simp only [card_empty, Nat.cast_zero]
  | insert a s ha ih =>
    rw [finsuppAntidiag_insert ha, prod_insert ha, coeff_mul, sum_biUnion]
    · apply Finset.sum_congr rfl
      simp only [mem_antidiagonal, sum_map, Function.Embedding.coeFn_mk, coe_update, Prod.forall]
      rintro u v rfl
      rw [ih, Finset.mul_sum, ← Finset.sum_attach]
      apply Finset.sum_congr rfl
      simp only [mem_attach, Finset.prod_insert ha, Function.update_self, forall_true_left,
        Subtype.forall]
      rintro x -
      rw [Finset.prod_congr rfl]
      intro i hi
      rw [Function.update_of_ne]
      exact ne_of_mem_of_not_mem hi ha
    · simp only [Set.PairwiseDisjoint, Set.Pairwise, mem_coe, mem_antidiagonal, ne_eq,
        disjoint_left, mem_map, mem_attach, Function.Embedding.coeFn_mk, true_and, Subtype.exists,
        exists_prop, not_exists, not_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
        Prod.forall, Prod.mk.injEq]
      rintro u v rfl u' v' huv h k - l - hkl
      obtain rfl : u' = u := by
        simpa only [Finsupp.coe_update, Function.update_self] using DFunLike.congr_fun hkl a
      simp only [add_right_inj] at huv
      exact h rfl huv.symm
Cleared hypotheses: d, s
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
f : ι → σ →₀ ℕ
g : ι → R
s : Finset ι
⊢ Eq (α := MvPowerSeries σ R) (∏ i ∈ s, (monomial (f i) : (a : R) → MvPowerSeries σ R) (g i))
    ((monomial (∑ i ∈ s, f i) : (a : R) → MvPowerSeries σ R) (∏ i ∈ s, g i))
have empty : Eq (α := MvPowerSeries σ R) (∏ i ∈ ∅, (monomial (f i) : (a : R) → MvPowerSeries σ R) (g i))
  ((monomial (∑ i ∈ ∅, f i) : (a : R) → MvPowerSeries σ R) (∏ i ∈ ∅, g i))
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha h => simp [h, monomial_mul_monomial]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_4
f : ι → σ →₀ ℕ
g : ι → R
s : Finset ι
empty :
  Eq (α := MvPowerSeries σ R) (∏ i ∈ ∅, (monomial (f i) : (a : R) → MvPowerSeries σ R) (g i))
    ((monomial (∑ i ∈ ∅, f i) : (a : R) → MvPowerSeries σ R) (∏ i ∈ ∅, g i))
⊢ Eq (α := MvPowerSeries σ R) (∏ i ∈ s, (monomial (f i) : (a : R) → MvPowerSeries σ R) (g i))
    ((monomial (∑ i ∈ s, f i) : (a : R) → MvPowerSeries σ R) (∏ i ∈ s, g i))
have cons : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (h :
    Eq (α := MvPowerSeries σ R) (∏ i ∈ s, (monomial (f i) : (a : R) → MvPowerSeries σ R) (g i))
      ((monomial (∑ i ∈ s, f i) : (a : R) → MvPowerSeries σ R) (∏ i ∈ s, g i))),
  Eq (α := MvPowerSeries σ R) (∏ i ∈ cons a s ha, (monomial (f i) : (a : R) → MvPowerSeries σ R) (g i))
    ((monomial (∑ i ∈ cons a s ha, f i) : (a : R) → MvPowerSeries σ R) (∏ i ∈ cons a s ha, g i))
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons a s ha h => simp [h, monomial_mul_monomial]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
this : f ^ n = ∏ x ∈ range n, f
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f ^ n) : R)
    (∑ l ∈ (range n).finsuppAntidiag d,
        ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f :
      R)
have rw : Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ x ∈ range n, f) : R)
  (∑ l ∈ (range n).finsuppAntidiag d,
      ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f :
    R)
Tactic: rw [this, coeff_prod]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
this : f ^ n = ∏ x ∈ range n, f
rw :
  Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (∏ x ∈ range n, f) : R)
    (∑ l ∈ (range n).finsuppAntidiag d,
        ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f :
      R)
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f ^ n) : R)
    (∑ l ∈ (range n).finsuppAntidiag d,
        ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f :
      R)
have rw₁ : Eq.{u_3 + 1} (α := R)
  (∑ l ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f)
  (∑ l ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f)
Tactic: rw [this, coeff_prod]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f ^ n) : R)
    (∑ l ∈ (range n).finsuppAntidiag d,
        ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f :
      R)
have suffices : f ^ n = ∏ x ∈ range n, f
Tactic: suffices f ^ n = (Finset.range n).prod fun _ ↦ f by
    rw [this, coeff_prod]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
⊢ f ^ n = ∏ x ∈ range n, f
have rw : f ^ n = f ^ #(range n)
Tactic: rw [Finset.prod_const, card_range]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
inst_1 : DecidableEq σ
f : MvPowerSeries σ R
n : ℕ
d : σ →₀ ℕ
rw : f ^ n = f ^ #(range n)
⊢ f ^ n = ∏ x ∈ range n, f
have rw₁ : f ^ n = f ^ n
Tactic: rw [Finset.prod_const, card_range]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
m : σ →₀ ℕ
a : R
n : ℕ
⊢ HPow.hPow (α := MvPowerSeries σ R) ((monomial m : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) n =
    (monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n)
have rw : Eq (α := MvPowerSeries σ R) (∏ _k ∈ range n, (monomial m : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)
  ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n) : MvPowerSeries σ R)
Tactic: rw [Finset.pow_eq_prod_const, prod_monomial, ← Finset.nsmul_eq_sum_const,
    ← Finset.pow_eq_prod_const]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
m : σ →₀ ℕ
a : R
n : ℕ
rw :
  Eq (α := MvPowerSeries σ R) (∏ _k ∈ range n, (monomial m : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)
    ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n) : MvPowerSeries σ R)
⊢ HPow.hPow (α := MvPowerSeries σ R) ((monomial m : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) n =
    (monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n)
have rw₁ : Eq (α := MvPowerSeries σ R)
  ((monomial (∑ i ∈ range n, m) : (a : R) → MvPowerSeries σ R) (∏ i ∈ range n, a) : MvPowerSeries σ R)
  ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n) : MvPowerSeries σ R)
Tactic: rw [Finset.pow_eq_prod_const, prod_monomial, ← Finset.nsmul_eq_sum_const,
    ← Finset.pow_eq_prod_const]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
m : σ →₀ ℕ
a : R
n : ℕ
rw :
  Eq (α := MvPowerSeries σ R) (∏ _k ∈ range n, (monomial m : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)
    ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n) : MvPowerSeries σ R)
rw₁ :
  Eq (α := MvPowerSeries σ R)
    ((monomial (∑ i ∈ range n, m) : (a : R) → MvPowerSeries σ R) (∏ i ∈ range n, a) : MvPowerSeries σ R)
    ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n) : MvPowerSeries σ R)
⊢ HPow.hPow (α := MvPowerSeries σ R) ((monomial m : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) n =
    (monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n)
have rw₂ : Eq (α := MvPowerSeries σ R) ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (∏ i ∈ range n, a) : MvPowerSeries σ R)
  ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n) : MvPowerSeries σ R)
Tactic: rw [Finset.pow_eq_prod_const, prod_monomial, ← Finset.nsmul_eq_sum_const,
    ← Finset.pow_eq_prod_const]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
m : σ →₀ ℕ
a : R
n : ℕ
rw :
  Eq (α := MvPowerSeries σ R) (∏ _k ∈ range n, (monomial m : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R)
    ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n) : MvPowerSeries σ R)
rw₁ :
  Eq (α := MvPowerSeries σ R)
    ((monomial (∑ i ∈ range n, m) : (a : R) → MvPowerSeries σ R) (∏ i ∈ range n, a) : MvPowerSeries σ R)
    ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n) : MvPowerSeries σ R)
rw₂ :
  Eq (α := MvPowerSeries σ R) ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (∏ i ∈ range n, a) : MvPowerSeries σ R)
    ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n) : MvPowerSeries σ R)
⊢ HPow.hPow (α := MvPowerSeries σ R) ((monomial m : (a : R) → MvPowerSeries σ R) a : MvPowerSeries σ R) n =
    (monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n)
have rw₃ : Eq (α := MvPowerSeries σ R) ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n) : MvPowerSeries σ R)
  ((monomial (n • m) : (a : R) → MvPowerSeries σ R) (a ^ n) : MvPowerSeries σ R)
Tactic: rw [Finset.pow_eq_prod_const, prod_monomial, ← Finset.nsmul_eq_sum_const,
    ← Finset.pow_eq_prod_const]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
⊢ Eq.{u_3 + 1} (α := R) ((coeff d : (a : MvPowerSeries σ R) → R) (f ^ n) : R) (0 : R)
have rw : Eq.{u_3 + 1} (α := R)
  (∑ l ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f)
  0
Tactic: rw [coeff_pow]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
⊢ Eq.{u_3 + 1} (α := R)
    (∑ l ∈ (range n).finsuppAntidiag d,
      ∏ i ∈ range n, (coeff ((l : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f)
    0
have h : ∀ (x : ℕ →₀ σ →₀ ℕ),
  Membership.mem (γ := Finset (ℕ →₀ σ →₀ ℕ)) ((range n).finsuppAntidiag d) x →
    Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((x : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
Tactic: apply sum_eq_zero
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : Membership.mem (γ := Finset (ℕ →₀ σ →₀ ℕ)) ((range n).finsuppAntidiag d) k
⊢ Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
have hk₁ : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n
Tactic: rw [mem_finsuppAntidiag] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n
⊢ Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
have hs_def : let s := {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)};
s = {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
Tactic: set s := {i ∈ range n | k i = 0} with hs_def
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs_def : s = {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
⊢ Eq.{u_3 + 1} (α := R) (∏ i ∈ range n, (coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f) 0
have hs : s ⊆ range n
Tactic: have hs : s ⊆ range n := filter_subset _ _
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs_def : s = {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs : s ⊆ range n
i : ℕ
hi : i ∈ s
⊢ Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
have hi₁ : i ∈ range n ∧ Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
Tactic: simp only [hs_def, mem_filter] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : HPow.hPow (α := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R) m = 0
d : σ →₀ ℕ
n : ℕ
hn : HAdd.hAdd (β := ℕ) m ((degree : (a : σ →₀ ℕ) → ℕ) d : ℕ) ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum (⇑k : (a : ℕ) → σ →₀ ℕ) = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs_def : s = {i ∈ range n | Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)}
hs : s ⊆ range n
i : ℕ
hi : i ∈ range n ∧ Eq (α := σ →₀ ℕ) ((k : (a : ℕ) → σ →₀ ℕ) i : σ →₀ ℕ) (0 : σ →₀ ℕ)
⊢ Eq.{u_3 + 1} (α := R) ((coeff ((k : (a : ℕ) → σ →₀ ℕ) i) : (a : MvPowerSeries σ R) → R) f : R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
have rw : Eq.{u_3 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) f : R)
  ((constantCoeff : (a : MvPowerSeries σ R) → R) f : R)
Tactic: rw [hi.2, coeff_zero_eq_constantCoeff]