awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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)
⊢ Eq (α := MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (psum σ R n) : MvPolynomial τ R)
    (psum τ R n : MvPolynomial τ R)
have 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)
Tactic: simp_rw [psum, map_sum, map_pow, rename_X, e.sum_comp (X · ^ n)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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)
⊢ Eq (α := MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (psum σ R n) : MvPolynomial τ R)
    (psum τ R n : MvPolynomial τ R)
have 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)
Tactic: simp_rw [psum, map_sum, map_pow, rename_X, e.sum_comp (X · ^ n)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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)
⊢ Eq (α := MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (psum σ R n) : MvPolynomial τ R)
    (psum τ R n : MvPolynomial τ R)
have 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)
Tactic: simp_rw [psum, map_sum, map_pow, rename_X, e.sum_comp (X · ^ n)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
⊢ Eq (α := MvPolynomial σ R) (msymm σ R (n := 0) (Nat.Partition.indiscrete 0)) 1
have 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 sorry) :
              Sym σ 0) :
          Multiset σ)) :
    MvPolynomial σ R)
  (1 : MvPolynomial σ R)
Tactic: rw [msymm, Fintype.sum_subsingleton _ ⟨(Sym.nil : Sym σ 0), rfl⟩]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (hypothesis)
Goal:
σ : Type u_5
R : Type u_6
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : DecidableEq σ
⊢ Eq (α := MvPolynomial σ R) (msymm σ R (n := 1) (Nat.Partition.indiscrete 1)) (∑ i : σ, X i)
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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
⊢ Eq (α := MvPolynomial σ R) (msymm σ R (n := 1) (Nat.Partition.indiscrete 1)) (∑ i : σ, X i)
have symm : Eq (α := MvPolynomial σ R) (∑ i : σ, X i) (msymm σ R (n := 1) (Nat.Partition.indiscrete 1))
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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
⊢ Eq (α := MvPolynomial σ R) (∑ i : σ, X i) (msymm σ R (n := 1) (Nat.Partition.indiscrete 1))
have 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))
Tactic: rw [Fintype.sum_equiv (Equiv.trans Sym.oneEquiv (Equiv.Set.univ (Sym σ 1)).symm)
    _ (fun s ↦ (s.1.1.map X).prod)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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))
⊢ Eq (α := MvPolynomial σ R) (∑ i : σ, X i) (msymm σ R (n := 1) (Nat.Partition.indiscrete 1))
have 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 σ)))
Tactic: rw [Fintype.sum_equiv (Equiv.trans Sym.oneEquiv (Equiv.Set.univ (Sym σ 1)).symm)
    _ (fun s ↦ (s.1.1.map X).prod)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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
⊢ 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))
have 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 σ)))
Tactic: apply Fintype.sum_equiv (Equiv.subtypeEquivProp this)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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) (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 σ)))
have 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 σ)))
Tactic: rw [← Multiset.prod_singleton (X x), ← Multiset.map_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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 : σ ≃ τ
⊢ Eq (α := MvPolynomial τ R)
    ((rename (⇑e : (a : σ) → τ) : (a : MvPolynomial σ R) → MvPolynomial τ R) (msymm σ R μ) : MvPolynomial τ R)
    (msymm τ R μ : MvPolynomial τ R)
have 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 μ)
Tactic: rw [msymm, map_sum]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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 : σ ≃ τ
⊢ 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 μ)
have 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)
Tactic: apply Fintype.sum_equiv (Nat.Partition.ofSymShapeEquiv μ e)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.Defs (goal)
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)
    ((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)
have 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))
                          sorry,
                      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))
                          sorry,
                      left_inv := sorry, right_inv := sorry } :
                    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: rw [← Multiset.prod_hom, Multiset.map_map, Nat.Partition.ofSymShapeEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ (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) : ℕ)
have simp_rw : ∑ x : Fin n with i ≤ (↑x : ℕ), t x = t (⟨i, hin⟩ : Fin n) + ∑ x : Fin n with i + 1 ≤ (↑x : ℕ), t x
Tactic: simp_rw [accumulate_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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 : Fin n with i + 1 ≤ (↑x : ℕ), t x
have h : {x : Fin n | i + 1 ≤ (↑x : ℕ)} = Finset.erase {x : Fin n | i ≤ (↑x : ℕ)} (⟨i, hin⟩ : Fin n)
Tactic: convert! (add_sum_erase _ _ _).symm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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)
⊢ ∑ x : Fin n with i ≤ (↑x : ℕ), t x = t (⟨i, hin⟩ : Fin n) + ∑ x : Fin n with i + 1 ≤ (↑x : ℕ), t x
have convert_3 : DecidableEq (Fin n)
Tactic: convert! (add_sum_erase _ _ _).symm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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)
⊢ ∑ x : Fin n with i ≤ (↑x : ℕ), t x = t (⟨i, hin⟩ : Fin n) + ∑ x : Fin n with i + 1 ≤ (↑x : ℕ), t x
have convert_7 : Membership.mem (γ := Finset (Fin n)) {x : Fin n | i ≤ (↑x : ℕ)} (⟨i, hin⟩ : Fin n)
Tactic: convert! (add_sum_erase _ _ _).symm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
⊢ {x : Fin n | i + 1 ≤ (↑x : ℕ)} = Finset.erase {x : Fin n | i ≤ (↑x : ℕ)} (⟨i, hin⟩ : Fin n)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
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)
have 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
Tactic: rw [mem_erase]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
a : Fin n
⊢ 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
have h : i ≤ (↑a : ℕ) ∧ i ≠ (↑a : ℕ) ↔ a ≠ ⟨i, hin⟩ ∧ i ≤ (↑a : ℕ)
Tactic: simp_rw [mem_filter_univ, i.succ_le_iff, lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
i n m : ℕ
hin : i < n
him : i + 1 < m
t : Fin n → ℕ
a : Fin n
⊢ i ≤ (↑a : ℕ) ∧ i ≠ (↑a : ℕ) ↔ a ≠ ⟨i, hin⟩ ∧ i ≤ (↑a : ℕ)
have h : i ≠ (↑a : ℕ) ∧ i ≤ (↑a : ℕ) ↔ a ≠ ⟨i, hin⟩ ∧ i ≤ (↑a : ℕ)
Tactic: rw [and_comm, ne_comm, ← Fin.val_ne_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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 : ℕ)
⊢ i ≤ (↑a : ℕ) ∧ i ≠ (↑a : ℕ) ↔ a ≠ ⟨i, hin⟩ ∧ i ≤ (↑a : ℕ)
have h₁ : (↑a : ℕ) ≠ i ∧ i ≤ (↑a : ℕ) ↔ a ≠ ⟨i, hin⟩ ∧ i ≤ (↑a : ℕ)
Tactic: rw [and_comm, ne_comm, ← Fin.val_ne_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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 : ℕ)
⊢ i ≤ (↑a : ℕ) ∧ i ≠ (↑a : ℕ) ↔ a ≠ ⟨i, hin⟩ ∧ i ≤ (↑a : ℕ)
have h₂ : (↑a : ℕ) ≠ i ∧ i ≤ (↑a : ℕ) ↔ (↑a : ℕ) ≠ (↑(⟨i, hin⟩ : Fin n) : ℕ) ∧ i ≤ (↑a : ℕ)
Tactic: rw [and_comm, ne_comm, ← Fin.val_ne_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ (↑j : ℕ) → t j = 0
⊢ (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t ⟨i, ⋯⟩ = t (⟨i, hin⟩ : Fin n)
have rw : ∑ i : Fin n with (↑(⟨i, sorry⟩ : Fin m) : ℕ) ≤ (↑i : ℕ), t i = t (⟨i, hin⟩ : Fin n)
Tactic: rw [accumulate_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ (↑j : ℕ) → t j = 0
⊢ ∑ i : Fin n with (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑i : ℕ), t i = t (⟨i, hin⟩ : Fin n)
have h : Membership.mem (γ := Finset (Fin n)) {i_1 : Fin n | (↑(⟨i, sorry⟩ : Fin m) : ℕ) ≤ (↑i_1 : ℕ)} (⟨i, hin⟩ : Fin n)
Tactic: apply sum_eq_single_of_mem
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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)
⊢ ∑ i : Fin n with (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑i : ℕ), t i = t (⟨i, hin⟩ : Fin n)
have h₀ : ∀ (b : Fin n),
  Membership.mem (γ := Finset (Fin n)) {i_1 : Fin n | (↑(⟨i, sorry⟩ : Fin m) : ℕ) ≤ (↑i_1 : ℕ)} b → b ≠ ⟨i, hin⟩ → t b = 0
Tactic: apply sum_eq_single_of_mem
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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)) {i_1 : Fin n | (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑i_1 : ℕ)} (⟨i, hin⟩ : Fin n)
have h : Membership.mem (γ := Finset (Fin n)) univ (⟨i, hin⟩ : Fin n) ∧ (↑(⟨i, sorry⟩ : Fin m) : ℕ) ≤ (↑(⟨i, hin⟩ : Fin n) : ℕ)
Tactic: rw [mem_filter]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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
have h₀ : ∀ (j : Fin n) (hij : Membership.mem (γ := Finset (Fin n)) {i_1 : Fin n | (↑(⟨i, sorry⟩ : Fin m) : ℕ) ≤ (↑i_1 : ℕ)} j)
  (hji : j ≠ ⟨i, hin⟩), m ≤ (↑j : ℕ)
Tactic: refine fun j hij hji ↦ ht j ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (hypothesis)
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⟩
⊢ m ≤ (↑j : ℕ)
have hij₁ : (↑(⟨i, sorry⟩ : Fin m) : ℕ) ≤ (↑j : ℕ)
Tactic: rw [mem_filter_univ] at hij
Cleared hypotheses: hij, hji
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
n m : ℕ
hnm : n ≤ m
⊢ Function.Injective (α := Fin n → ℕ) (β := Fin m → ℕ) (⇑(accumulate n m) : (a : Fin n → ℕ) → Fin m → ℕ)
have refine : ∀ (t s : Fin n → ℕ)
  (he :
    Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t : Fin m → ℕ)
      ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s : Fin m → ℕ))
  (i : Fin n), t i = s i
Tactic: refine fun t s he ↦ funext fun i ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he :
  Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t : Fin m → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s : Fin m → ℕ)
i : Fin n
⊢ t i = s i
have inl : ∀ (h : (↑i : ℕ) + 1 < m), t i = s i
Tactic: obtain h | h := lt_or_ge (i.1 + 1) m
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he :
  Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t : Fin m → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s : Fin m → ℕ)
i : Fin n
inl : ∀ (h : (↑i : ℕ) + 1 < m), t i = s i
⊢ t i = s i
have inr : ∀ (h : m ≤ (↑i : ℕ) + 1), t i = s i
Tactic: obtain h | h := lt_or_ge (i.1 + 1) m
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (hypothesis)
Goal:
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he :
  Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t : Fin m → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s : Fin m → ℕ)
i : Fin n
h : (↑i : ℕ) + 1 < m
⊢ t i = s i
have this : (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s ⟨(↑i : ℕ), sorry⟩ =
  HAdd.hAdd (β := ℕ) (s (⟨(↑i : ℕ), sorry⟩ : Fin n))
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s (⟨(↑i : ℕ) + 1, h⟩ : Fin m) : ℕ)
Tactic: have := accumulate_rec i.2 h s
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he :
  Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t : Fin m → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s : Fin m → ℕ)
i : Fin n
h : (↑i : ℕ) + 1 < m
this :
  (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s ⟨(↑i : ℕ), ⋯⟩ =
    HAdd.hAdd (β := ℕ) (s (⟨(↑i : ℕ), ⋯⟩ : Fin n))
      ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s (⟨(↑i : ℕ) + 1, h⟩ : Fin m) : ℕ)
⊢ t i = s i
have inl : ∀
  (this :
    (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t ⟨(↑i : ℕ), sorry⟩ =
      HAdd.hAdd (β := ℕ) (s (⟨(↑i : ℕ), sorry⟩ : Fin n))
        ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t (⟨(↑i : ℕ) + 1, h⟩ : Fin m) : ℕ)),
  t i = s i
Tactic: rwa [← he, accumulate_rec i.2 h t, add_right_cancel_iff] at this
Cleared hypotheses: this