awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
n : ℕ
npos : n ≠ 0
⊢ Eq (α := MvPolynomial σ R) (psumPart σ R (Nat.Partition.indiscrete n)) (psum σ R n)

Tactic:
simp [psumPart, npos]

Premises used: MvPolynomial.psumPart
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
n : ℕ
e : σ ≃ τ
simp_rw :
  Eq (α := MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R)
      (∑ i : σ, HPow.hPow (α := MvPolynomial σ R) (X i) n))
    (∑ i : τ, HPow.hPow (α := MvPolynomial τ R) (X i) n)
simp_rw₁ :
  Eq (α := MvPolynomial τ R)
    (∑ x : σ,
      (rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R)
        (HPow.hPow (α := MvPolynomial σ R) (X x) n))
    (∑ i : τ, HPow.hPow (α := MvPolynomial τ R) (X i) n)
simp_rw₂ :
  Eq (α := MvPolynomial τ R)
    (∑ x : σ,
      HPow.hPow (α := MvPolynomial τ R)
        ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X x) : MvPolynomial τ R) n)
    (∑ i : τ, HPow.hPow (α := MvPolynomial τ R) (X i) n)
simp_rw₃ :
  Eq (α := MvPolynomial τ R) (∑ x : σ, HPow.hPow (α := MvPolynomial τ R) (X ((e : (a : σ) → τ) x) : MvPolynomial τ R) n)
    (∑ i : τ, HPow.hPow (α := MvPolynomial τ R) (X i) n)
⊢ Eq (α := MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (psum σ R n) : MvPolynomial τ R)
    (psum τ R n : MvPolynomial τ R)

Tactic:
simp_rw [psum, map_sum, map_pow, rename_X, e.sum_comp (X · ^ n)]

Premises used: Equiv.sum_comp, MvPolynomial.X, map_pow, map_sum, HPow.hPow, MvPolynomial.psum, MvPolynomial.rename_X
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
n : ℕ
⊢ IsSymmetric (psum σ R n)

Tactic:
rename_psum _ _ n

Premises used: MvPolynomial.IsSymmetric, MvPolynomial.rename_psum
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
rw :
  Eq (α := MvPolynomial σ R)
    (Multiset.prod
        (Multiset.map X
          (↑(↑(Subtype.mk (p := fun (a : Sym σ 0) ↦ Nat.Partition.ofSym a = Nat.Partition.indiscrete 0) Sym.nil ⋯) :
                Sym σ 0) :
            Multiset σ)) :
      MvPolynomial σ R)
    (1 : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R) (msymm σ R (n := 0) (Nat.Partition.indiscrete 0)) 1

Tactic:
rw [msymm, Fintype.sum_subsingleton _ ⟨(Sym.nil : Sym σ 0), rfl⟩]

Premises used: MvPolynomial.msymm, Fintype.sum_subsingleton
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
⊢ Eq (α := MvPolynomial σ R)
    (Multiset.prod
        (Multiset.map X
          (↑(↑(Subtype.mk (p := fun (a : Sym σ 0) ↦ Nat.Partition.ofSym a = Nat.Partition.indiscrete 0) Sym.nil ⋯) :
                Sym σ 0) :
            Multiset σ)) :
      MvPolynomial σ R)
    (1 : MvPolynomial σ R)

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
⊢ Eq.{u_5 + 1} (α := (x : Sym σ 1) → Prop) (fun (x : Sym σ 1) ↦ Membership.mem (γ := Set (Sym σ 1)) Set.univ x)
    fun (x : Sym σ 1) ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1

Tactic:
have : (fun (x : Sym σ 1) ↦ x ∈ Set.univ) =
      (fun x ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1) := by
    simp_rw [Set.mem_univ, Nat.Partition.ofSym_one]
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
this :
  Eq.{u_5 + 1} (α := (x : Sym σ 1) → Prop) (fun (x : Sym σ 1) ↦ Membership.mem (γ := Set (Sym σ 1)) Set.univ x)
    fun (x : Sym σ 1) ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
symm : Eq (α := MvPolynomial σ R) (∑ i : σ, X i) (msymm σ R (n := 1) (Nat.Partition.indiscrete 1))
⊢ Eq (α := MvPolynomial σ R) (msymm σ R (n := 1) (Nat.Partition.indiscrete 1)) (∑ i : σ, X i)

Tactic:
symm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
this :
  Eq.{u_5 + 1} (α := (x : Sym σ 1) → Prop) (fun (x : Sym σ 1) ↦ Membership.mem (γ := Set (Sym σ 1)) Set.univ x)
    fun (x : Sym σ 1) ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
rw :
  Eq (α := MvPolynomial σ R)
    (∑ x : (↑Set.univ : Type u_5), Multiset.prod (Multiset.map X (↑(↑x : Sym σ 1) : Multiset σ)))
    (msymm σ R (n := 1) (Nat.Partition.indiscrete 1))
rw₁ :
  ∀ (x : σ),
    Eq (α := MvPolynomial σ R) (X x)
      (Multiset.prod
        (Multiset.map X
          (↑(↑((Equiv.trans Sym.oneEquiv (Equiv.symm (Equiv.Set.univ (Sym σ 1))) : (a : σ) → (↑Set.univ : Type u_5))
                    x) :
                Sym σ 1) :
            Multiset σ)))
⊢ Eq (α := MvPolynomial σ R) (∑ i : σ, X i) (msymm σ R (n := 1) (Nat.Partition.indiscrete 1))

Tactic:
rw [Fintype.sum_equiv (Equiv.trans Sym.oneEquiv (Equiv.Set.univ (Sym σ 1)).symm)
    _ (fun s ↦ (s.1.1.map X).prod)]

Premises used: Multiset.map, Equiv.trans, Multiset.prod, MvPolynomial.X, Sym.oneEquiv, Sym, Equiv.symm, OfNat.ofNat, Fintype.sum_equiv, Subtype.val, Equiv.Set.univ
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
this :
  Eq.{u_5 + 1} (α := (x : Sym σ 1) → Prop) (fun (x : Sym σ 1) ↦ Membership.mem (γ := Set (Sym σ 1)) Set.univ x)
    fun (x : Sym σ 1) ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
h :
  ∀ (x : { x : Sym σ 1 // Membership.mem (γ := Set (Sym σ 1)) Set.univ x }),
    Eq (α := MvPolynomial σ R) (Multiset.prod (Multiset.map X (↑(↑x : Sym σ 1) : Multiset σ)))
      (Multiset.prod
        (Multiset.map X
          (↑(↑((Equiv.subtypeEquivProp (p := fun (x : Sym σ 1) ↦ Membership.mem (γ := Set (Sym σ 1)) Set.univ x) (q :=
                        fun (x : Sym σ 1) ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1) this :
                      (a : { x : Sym σ 1 // x ∈ Set.univ }) →
                        { x : Sym σ 1 // Nat.Partition.ofSym x = Nat.Partition.indiscrete 1 })
                    x) :
                Sym σ 1) :
            Multiset σ)))
⊢ Eq (α := MvPolynomial σ R)
    (∑ x : (↑Set.univ : Type u_5), Multiset.prod (Multiset.map X (↑(↑x : Sym σ 1) : Multiset σ)))
    (msymm σ R (n := 1) (Nat.Partition.indiscrete 1))

Tactic:
apply Fintype.sum_equiv (Equiv.subtypeEquivProp this)

Premises used: Equiv.subtypeEquivProp, Fintype.sum_equiv
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
this :
  Eq.{u_5 + 1} (α := (x : Sym σ 1) → Prop) (fun (x : Sym σ 1) ↦ Membership.mem (γ := Set (Sym σ 1)) Set.univ x)
    fun (x : Sym σ 1) ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
x : { x : Sym σ 1 // Membership.mem (γ := Set (Sym σ 1)) Set.univ x }
⊢ Eq (α := MvPolynomial σ R) (Multiset.prod (Multiset.map X (↑(↑x : Sym σ 1) : Multiset σ)))
    (Multiset.prod
      (Multiset.map X
        (↑(↑((Equiv.subtypeEquivProp (p := fun (x : Sym σ 1) ↦ Membership.mem (γ := Set (Sym σ 1)) Set.univ x) (q :=
                      fun (x : Sym σ 1) ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1) this :
                    (a : { x : Sym σ 1 // x ∈ Set.univ }) →
                      { x : Sym σ 1 // Nat.Partition.ofSym x = Nat.Partition.indiscrete 1 })
                  x) :
              Sym σ 1) :
          Multiset σ)))

Tactic:
congr
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
this :
  Eq.{u_5 + 1} (α := (x : Sym σ 1) → Prop) (fun (x : Sym σ 1) ↦ Membership.mem (γ := Set (Sym σ 1)) Set.univ x)
    fun (x : Sym σ 1) ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
x : σ
rw :
  Eq (α := MvPolynomial σ R) (Multiset.prod (Multiset.map X {x}))
    (Multiset.prod
      (Multiset.map X
        (↑(↑((Equiv.trans Sym.oneEquiv (Equiv.symm (Equiv.Set.univ (Sym σ 1))) : (a : σ) → (↑Set.univ : Type u_5)) x) :
              Sym σ 1) :
          Multiset σ)))
⊢ Eq (α := MvPolynomial σ R) (X x)
    (Multiset.prod
      (Multiset.map X
        (↑(↑((Equiv.trans Sym.oneEquiv (Equiv.symm (Equiv.Set.univ (Sym σ 1))) : (a : σ) → (↑Set.univ : Type u_5)) x) :
              Sym σ 1) :
          Multiset σ)))

Tactic:
rw [← Multiset.prod_singleton (X x), ← Multiset.map_singleton]

Premises used: Multiset.map_singleton, MvPolynomial.X, Multiset.prod_singleton
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
this :
  Eq.{u_5 + 1} (α := (x : Sym σ 1) → Prop) (fun (x : Sym σ 1) ↦ Membership.mem (γ := Set (Sym σ 1)) Set.univ x)
    fun (x : Sym σ 1) ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
x : σ
⊢ Eq (α := MvPolynomial σ R) (Multiset.prod (Multiset.map X {x}))
    (Multiset.prod
      (Multiset.map X
        (↑(↑((Equiv.trans Sym.oneEquiv (Equiv.symm (Equiv.Set.univ (Sym σ 1))) : (a : σ) → (↑Set.univ : Type u_5)) x) :
              Sym σ 1) :
          Multiset σ)))

Tactic:
congr
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
inst_3 : DecidableEq σ
inst_4 : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
rw :
  Eq (α := MvPolynomial τ R)
    (∑ x : { a : Sym σ n // Nat.Partition.ofSym a = μ },
      (rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R)
        (Multiset.prod (Multiset.map X (↑(↑x : Sym σ n) : Multiset σ))))
    (msymm τ R μ)
⊢ Eq (α := MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (msymm σ R μ) : MvPolynomial τ R)
    (msymm τ R μ : MvPolynomial τ R)

Tactic:
rw [msymm, map_sum]

Premises used: map_sum, MvPolynomial.msymm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
inst_3 : DecidableEq σ
inst_4 : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
h :
  ∀ (x : { x : Sym σ n // Nat.Partition.ofSym x = μ }),
    Eq (α := MvPolynomial τ R)
      ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R)
          (Multiset.prod (Multiset.map X (↑(↑x : Sym σ n) : Multiset σ))) :
        MvPolynomial τ R)
      (Multiset.prod
          (Multiset.map X
            (↑(↑(((μ.ofSymShapeEquiv e :
                          Equiv.{u_5 + 1, u_2 + 1} { x : Sym σ n // Nat.Partition.ofSym x = μ }
                            { x : Sym τ n // Nat.Partition.ofSym x = μ }) :
                        (a : { x : Sym σ n // Nat.Partition.ofSym x = μ }) →
                          { x : Sym τ n // Nat.Partition.ofSym x = μ })
                      x) :
                  Sym τ n) :
              Multiset τ)) :
        MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    (∑ x : { a : Sym σ n // Nat.Partition.ofSym a = μ },
      (rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R)
        (Multiset.prod (Multiset.map X (↑(↑x : Sym σ n) : Multiset σ))))
    (msymm τ R μ)

Tactic:
apply Fintype.sum_equiv (Nat.Partition.ofSymShapeEquiv μ e)

Premises used: Nat.Partition.ofSymShapeEquiv, Fintype.sum_equiv
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
inst_3 : DecidableEq σ
inst_4 : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
x : { x : Sym σ n // Nat.Partition.ofSym x = μ }
h :
  Eq (α := MvPolynomial τ R)
    (Multiset.prod
      (Multiset.map
        (Function.comp (β := MvPolynomial σ R)
          (⇑(rename (⇑e : (a : σ) → τ)) : (a : MvPolynomial σ R) → MvPolynomial τ R) X)
        (↑(↑x : Sym σ n) : Multiset σ)))
    (Multiset.prod
      (Multiset.map X
        (↑(↑((({
                        toFun := fun (x : { x : Sym σ n // Nat.Partition.ofSym x = μ }) ↦
                          Subtype.mk (p := fun (x : Sym τ n) ↦ Nat.Partition.ofSym x = μ)
                            (((Sym.equivCongr e : Equiv.{u_5 + 1, u_2 + 1} (Sym σ n) (Sym τ n)) :
                                (a : Sym σ n) → Sym τ n)
                              (↑x : Sym σ n))
                            ⋯,
                        invFun := fun (x : { x : Sym τ n // Nat.Partition.ofSym x = μ }) ↦
                          Subtype.mk (p := fun (x : Sym σ n) ↦ Nat.Partition.ofSym x = μ)
                            (((Sym.equivCongr e.symm : Equiv.{u_2 + 1, u_5 + 1} (Sym τ n) (Sym σ n)) :
                                (a : Sym τ n) → Sym σ n)
                              (↑x : Sym τ n))
                            ⋯,
                        left_inv := ⋯, right_inv := ⋯ } :
                      Equiv.{u_5 + 1, u_2 + 1} { x : Sym σ n // Nat.Partition.ofSym x = μ }
                        { x : Sym τ n // Nat.Partition.ofSym x = μ }) :
                    (a : { x : Sym σ n // Nat.Partition.ofSym x = μ }) → { x : Sym τ n // Nat.Partition.ofSym x = μ })
                  x) :
              Sym τ n) :
          Multiset τ)))
⊢ Eq (α := MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R)
        (Multiset.prod (Multiset.map X (↑(↑x : Sym σ n) : Multiset σ))) :
      MvPolynomial τ R)
    (Multiset.prod
        (Multiset.map X
          (↑(↑(((μ.ofSymShapeEquiv e :
                        Equiv.{u_5 + 1, u_2 + 1} { x : Sym σ n // Nat.Partition.ofSym x = μ }
                          { x : Sym τ n // Nat.Partition.ofSym x = μ }) :
                      (a : { x : Sym σ n // Nat.Partition.ofSym x = μ }) → { x : Sym τ n // Nat.Partition.ofSym x = μ })
                    x) :
                Sym τ n) :
            Multiset τ)) :
      MvPolynomial τ R)

Tactic:
rw [← Multiset.prod_hom, Multiset.map_map, Nat.Partition.ofSymShapeEquiv]

Premises used: Nat.Partition.ofSymShapeEquiv, Multiset.prod_hom, Multiset.map_map
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
τ : Type u_2
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
inst_3 : DecidableEq σ
inst_4 : DecidableEq τ
n : ℕ
μ : n.Partition
e : σ ≃ τ
x : { x : Sym σ n // Nat.Partition.ofSym x = μ }
⊢ Eq (α := MvPolynomial τ R)
    (Multiset.prod
      (Multiset.map
        (Function.comp (β := MvPolynomial σ R)
          (⇑(rename (⇑e : (a : σ) → τ)) : (a : MvPolynomial σ R) → MvPolynomial τ R) X)
        (↑(↑x : Sym σ n) : Multiset σ)))
    (Multiset.prod
      (Multiset.map X
        (↑(↑((({
                        toFun := fun (x : { x : Sym σ n // Nat.Partition.ofSym x = μ }) ↦
                          Subtype.mk (p := fun (x : Sym τ n) ↦ Nat.Partition.ofSym x = μ)
                            (((Sym.equivCongr e : Equiv.{u_5 + 1, u_2 + 1} (Sym σ n) (Sym τ n)) :
                                (a : Sym σ n) → Sym τ n)
                              (↑x : Sym σ n))
                            ⋯,
                        invFun := fun (x : { x : Sym τ n // Nat.Partition.ofSym x = μ }) ↦
                          Subtype.mk (p := fun (x : Sym σ n) ↦ Nat.Partition.ofSym x = μ)
                            (((Sym.equivCongr e.symm : Equiv.{u_2 + 1, u_5 + 1} (Sym τ n) (Sym σ n)) :
                                (a : Sym τ n) → Sym σ n)
                              (↑x : Sym τ n))
                            ⋯,
                        left_inv := ⋯, right_inv := ⋯ } :
                      Equiv.{u_5 + 1, u_2 + 1} { x : Sym σ n // Nat.Partition.ofSym x = μ }
                        { x : Sym τ n // Nat.Partition.ofSym x = μ }) :
                    (a : { x : Sym σ n // Nat.Partition.ofSym x = μ }) → { x : Sym τ n // Nat.Partition.ofSym x = μ })
                  x) :
              Sym τ n) :
          Multiset τ)))

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
n : ℕ
μ : n.Partition
⊢ IsSymmetric (msymm σ R μ)

Tactic:
rename_msymm _ _ μ

Premises used: MvPolynomial.IsSymmetric, MvPolynomial.rename_msymm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
simp_rw : ∑ x : Fin n with i ≤ (↑x : ℕ), t x = t (⟨i, hin⟩ : Fin n) + ∑ x : Fin n with i + 1 ≤ (↑x : ℕ), t x
⊢ (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t ⟨i, ⋯⟩ =
    HAdd.hAdd (β := ℕ) (t (⟨i, hin⟩ : Fin n))
      ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t (⟨i + 1, him⟩ : Fin m) : ℕ)

Tactic:
simp_rw [accumulate_apply]

Premises used: Fin.accumulate_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ ∑ x : Fin n with i ≤ (↑x : ℕ), t x =
    t (⟨i, hin⟩ : Fin n) + ∑ x ∈ Finset.erase {x : Fin n | i ≤ (↑x : ℕ)} (⟨i, hin⟩ : Fin n), t x

Tactic:
(add_sum_erase _ _ _).symm

Premises used: Finset.add_sum_erase, Eq.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
h : {x : Fin n | i + 1 ≤ (↑x : ℕ)} = Finset.erase {x : Fin n | i ≤ (↑x : ℕ)} (⟨i, hin⟩ : Fin n)
convert_3 : DecidableEq (Fin n)
convert_7 : Membership.mem (γ := Finset (Fin n)) {x : Fin n | i ≤ (↑x : ℕ)} (⟨i, hin⟩ : Fin n)
⊢ ∑ x : Fin n with i ≤ (↑x : ℕ), t x = t (⟨i, hin⟩ : Fin n) + ∑ x : Fin n with i + 1 ≤ (↑x : ℕ), t x

Tactic:
convert! (add_sum_erase _ _ _).symm

Premises used: Finset.add_sum_erase, Eq.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
h :
  ∀ (a : Fin n),
    Membership.mem (γ := Finset (Fin n)) {x : Fin n | i + 1 ≤ (↑x : ℕ)} a ↔
      a ∈ Finset.erase {x : Fin n | i ≤ (↑x : ℕ)} (⟨i, hin⟩ : Fin n)
⊢ {x : Fin n | i + 1 ≤ (↑x : ℕ)} = Finset.erase {x : Fin n | i ≤ (↑x : ℕ)} (⟨i, hin⟩ : Fin n)

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
a : Fin n
h :
  Membership.mem (γ := Finset (Fin n)) {x : Fin n | i + 1 ≤ (↑x : ℕ)} a ↔
    a ≠ ⟨i, hin⟩ ∧ Membership.mem (γ := Finset (Fin n)) {x : Fin n | i ≤ (↑x : ℕ)} a
⊢ Membership.mem (γ := Finset (Fin n)) {x : Fin n | i + 1 ≤ (↑x : ℕ)} a ↔
    a ∈ Finset.erase {x : Fin n | i ≤ (↑x : ℕ)} (⟨i, hin⟩ : Fin n)

Tactic:
rw [mem_erase]

Premises used: Finset.mem_erase
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
a : Fin n
h : i ≤ (↑a : ℕ) ∧ i ≠ (↑a : ℕ) ↔ a ≠ ⟨i, hin⟩ ∧ i ≤ (↑a : ℕ)
⊢ Membership.mem (γ := Finset (Fin n)) {x : Fin n | i + 1 ≤ (↑x : ℕ)} a ↔
    a ≠ ⟨i, hin⟩ ∧ Membership.mem (γ := Finset (Fin n)) {x : Fin n | i ≤ (↑x : ℕ)} a

Tactic:
simp_rw [mem_filter_univ, i.succ_le_iff, lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne, Finset.mem_filter_univ, Nat.succ_le_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
a : Fin n
h : i ≠ (↑a : ℕ) ∧ i ≤ (↑a : ℕ) ↔ a ≠ ⟨i, hin⟩ ∧ i ≤ (↑a : ℕ)
h₁ : (↑a : ℕ) ≠ i ∧ i ≤ (↑a : ℕ) ↔ a ≠ ⟨i, hin⟩ ∧ i ≤ (↑a : ℕ)
h₂ h₃ : (↑a : ℕ) ≠ i ∧ i ≤ (↑a : ℕ) ↔ (↑a : ℕ) ≠ (↑(⟨i, hin⟩ : Fin n) : ℕ) ∧ i ≤ (↑a : ℕ)
⊢ i ≤ (↑a : ℕ) ∧ i ≠ (↑a : ℕ) ↔ a ≠ ⟨i, hin⟩ ∧ i ≤ (↑a : ℕ)

Tactic:
rw [and_comm, ne_comm, ← Fin.val_ne_iff]

Premises used: Fin.val_ne_iff, and_comm, ne_comm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ Membership.mem (γ := Finset (Fin n)) {x : Fin n | i ≤ (↑x : ℕ)} (⟨i, hin⟩ : Fin n)

Tactic:
mem_filter.2 ⟨mem_univ _, le_rfl⟩

Premises used: Iff.mpr, Finset.mem_univ, le_rfl, And.intro, Finset.mem_filter
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ Membership.mem (γ := Finset (Fin n)) {x : Fin n | i ≤ (↑x : ℕ)} (⟨i, hin⟩ : Fin n)

Tactic:
exact mem_filter.2 ⟨mem_univ _, le_rfl⟩

Premises used: Iff.mpr, Finset.mem_univ, le_rfl, And.intro, Finset.mem_filter
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ (↑j : ℕ) → t j = 0
rw : ∑ i : Fin n with (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑i : ℕ), t i = t (⟨i, hin⟩ : Fin n)
⊢ (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t ⟨i, ⋯⟩ = t (⟨i, hin⟩ : Fin n)

Tactic:
rw [accumulate_apply]

Premises used: Fin.accumulate_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ (↑j : ℕ) → t j = 0
h : Membership.mem (γ := Finset (Fin n)) {i_1 : Fin n | (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑i_1 : ℕ)} (⟨i, hin⟩ : Fin n)
h₀ :
  ∀ (b : Fin n),
    Membership.mem (γ := Finset (Fin n)) {i_1 : Fin n | (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑i_1 : ℕ)} b → b ≠ ⟨i, hin⟩ → t b = 0
⊢ ∑ i : Fin n with (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑i : ℕ), t i = t (⟨i, hin⟩ : Fin n)

Tactic:
apply sum_eq_single_of_mem

Premises used: Finset.sum_eq_single_of_mem
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ (↑j : ℕ) → t j = 0
h : Membership.mem (γ := Finset (Fin n)) univ (⟨i, hin⟩ : Fin n) ∧ (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑(⟨i, hin⟩ : Fin n) : ℕ)
⊢ Membership.mem (γ := Finset (Fin n)) {i_1 : Fin n | (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑i_1 : ℕ)} (⟨i, hin⟩ : Fin n)

Tactic:
rw [mem_filter]

Premises used: Finset.mem_filter
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ (↑j : ℕ) → t j = 0
⊢ Membership.mem (γ := Finset (Fin n)) univ (⟨i, hin⟩ : Fin n) ∧ (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑(⟨i, hin⟩ : Fin n) : ℕ)

Tactic:
⟨mem_univ _, le_rfl⟩

Premises used: Finset.mem_univ, le_rfl, And.intro
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ (↑j : ℕ) → t j = 0
⊢ Membership.mem (γ := Finset (Fin n)) univ (⟨i, hin⟩ : Fin n) ∧ (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑(⟨i, hin⟩ : Fin n) : ℕ)

Tactic:
exact ⟨mem_univ _, le_rfl⟩
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ (↑j : ℕ) → t j = 0
⊢ ∀ (b : Fin n),
    Membership.mem (γ := Finset (Fin n)) {i_1 : Fin n | (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑i_1 : ℕ)} b → b ≠ ⟨i, hin⟩ → t b = 0

Tactic:
fun j hij hji ↦ ht j ?_
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ (↑j : ℕ) → t j = 0
h₀ :
  ∀ (j : Fin n) (hij : Membership.mem (γ := Finset (Fin n)) {i_1 : Fin n | (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑i_1 : ℕ)} j)
    (hji : j ≠ ⟨i, hin⟩), m ≤ (↑j : ℕ)
⊢ ∀ (b : Fin n),
    Membership.mem (γ := Finset (Fin n)) {i_1 : Fin n | (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑i_1 : ℕ)} b → b ≠ ⟨i, hin⟩ → t b = 0

Tactic:
refine fun j hij hji ↦ ht j ?_
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ (↑j : ℕ) → t j = 0
j : Fin n
hij : Membership.mem (γ := Finset (Fin n)) {i_1 : Fin n | (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑i_1 : ℕ)} j
hji : j ≠ ⟨i, hin⟩
⊢ (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑j : ℕ)

Tactic:
rw [mem_filter_univ] at hij

Premises used: Finset.mem_filter_univ
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ (↑j : ℕ) → t j = 0
j : Fin n
hij : Membership.mem (γ := Finset (Fin n)) {i_1 : Fin n | (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑i_1 : ℕ)} j
hji : j ≠ ⟨i, hin⟩
hij₁ : (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑j : ℕ)
⊢ j ≠ ⟨i, hin⟩

Tactic:
rw [mem_filter_univ] at hij

Premises used: Finset.mem_filter_univ