awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
refine_3 :
  ∀
    (this :
      Eq (α := Lex (Fin m →₀ ℕ))
          (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1))
          (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            ((monomial (∑ j ∈ Iic (⟨i, him⟩ : Fin m), fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1)) ∧
        Eq.{u_3 + 1} (α := R)
          (leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (∑ j ∈ powersetCard (i + 1) univ, (monomial (∑ j ∈ j, fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1))
          (leadingCoeff (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            ((monomial (∑ j ∈ Iic (⟨i, him⟩ : Fin m), fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1))),
    Eq (α := Lex (Fin m →₀ ℕ))
        (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R (i + 1)) :
          Lex (Fin m →₀ ℕ))
        ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1) :
          Lex (Fin m →₀ ℕ)) ∧
      Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
        (esymm (Fin m) R (i + 1))
refine_1 : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) (Iic (⟨i, him⟩ : Fin m))
refine_2 :
  ∀ (j : Finset (Fin m)),
    Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) j →
      j ≠ Iic ⟨i, him⟩ →
        LT.lt (α := Lex (Fin m →₀ ℕ))
          (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            ((fun (s : Finset (Fin m)) ↦
                ((monomial (∑ j ∈ s, fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1 : MvPolynomial (Fin m) R))
              j))
          (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            ((fun (s : Finset (Fin m)) ↦
                ((monomial (∑ j ∈ s, fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1 : MvPolynomial (Fin m) R))
              (Iic ⟨i, him⟩)))
⊢ Eq (α := Lex (Fin m →₀ ℕ))
      (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R (i + 1)) :
        Lex (Fin m →₀ ℕ))
      ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
          (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1) :
        Lex (Fin m →₀ ℕ)) ∧
    Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      (esymm (Fin m) R (i + 1))

Tactic:
have := supDegree_leadingCoeff_sum_eq (D := toLex) (s := univ.powersetCard (i + 1))
    (i := Iic (⟨i, him⟩ : Fin m)) ?_ (f := fun s ↦ monomial (∑ j ∈ s, fun₀ | j => 1) (1 : R)) ?_
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
⊢ Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) (Iic (⟨i, him⟩ : Fin m))

Tactic:
mem_powersetCard.2 ⟨subset_univ _, Fin.card_Iic _⟩

Premises used: Iff.mpr, Finset.mem_powersetCard, Fin.card_Iic, And.intro, Finset.subset_univ
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
⊢ Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) (Iic (⟨i, him⟩ : Fin m))

Tactic:
exact mem_powersetCard.2 ⟨subset_univ _, Fin.card_Iic _⟩

Premises used: Iff.mpr, Finset.mem_powersetCard, Fin.card_Iic, And.intro, Finset.subset_univ
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
hne : t ≠ Iic ⟨i, him⟩
rw : i + 1 = #(Iic (⟨i, him⟩ : Fin m))
rw₁ rw₂ : i + 1 = (↑(⟨i, him⟩ : Fin m) : ℕ) + 1
⊢ #t = #(Iic (⟨i, him⟩ : Fin m))

Tactic:
rw [(mem_powersetCard.1 ht).2, Fin.card_Iic]

Premises used: Finset.mem_powersetCard, And.right, Fin.card_Iic, Iff.mp
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
hne : t ≠ Iic ⟨i, him⟩
⊢ #t = #(Iic (⟨i, him⟩ : Fin m))

Tactic:
have ht' : #t = #(Iic (⟨i, him⟩ : Fin m)) := by
    rw [(mem_powersetCard.1 ht).2, Fin.card_Iic]
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
hne : t ≠ Iic ⟨i, him⟩
ht' : #t = #(Iic (⟨i, him⟩ : Fin m))
refine_2 :
  LT.lt (α := Lex (Fin m →₀ ℕ))
    ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (Finsupp.indicator t fun (x : Fin m) (x_1 : x ∈ t) ↦ 1) :
      Lex (Fin m →₀ ℕ))
    ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
        (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1) :
      Lex (Fin m →₀ ℕ))
⊢ LT.lt (α := Lex (Fin m →₀ ℕ))
    (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      ((fun (s : Finset (Fin m)) ↦
          ((monomial (∑ j ∈ s, fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1 : MvPolynomial (Fin m) R))
        t))
    (supDegree.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
      ((fun (s : Finset (Fin m)) ↦
          ((monomial (∑ j ∈ s, fun₀ | j => 1) : (a : R) → MvPolynomial (Fin m) R) 1 : MvPolynomial (Fin m) R))
        (Iic ⟨i, him⟩)))

Tactic:
simp_rw [← single_eq_monomial, supDegree_single_ne_zero _ one_ne_zero,
    ← Finsupp.indicator_eq_sum_single]

Premises used: MvPolynomial.single_eq_monomial, AddMonoidAlgebra.supDegree_single_ne_zero, Finsupp.indicator_eq_sum_single, one_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
hne : t ≠ Iic ⟨i, him⟩
ht' : #t = #(Iic (⟨i, him⟩ : Fin m))
⊢ ∃ x ∈ Iic (⟨i, him⟩ : Fin m), x ∉ t

Tactic:
rw [ne_comm, Ne, ← subset_iff_eq_of_card_le ht'.le, not_subset] at hne

Premises used: Eq.le, Ne, Finset.subset_iff_eq_of_card_le, ne_comm, Finset.not_subset
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
hne : t ≠ Iic ⟨i, him⟩
ht' : #t = #(Iic (⟨i, him⟩ : Fin m))
hne₁ : ∃ x ∈ Iic (⟨i, him⟩ : Fin m), x ∉ t
⊢ #t = #(Iic (⟨i, him⟩ : Fin m))

Tactic:
rw [ne_comm, Ne, ← subset_iff_eq_of_card_le ht'.le, not_subset] at hne

Premises used: Eq.le, Ne, Finset.subset_iff_eq_of_card_le, ne_comm, Finset.not_subset
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
hne : ∃ x ∈ Iic (⟨i, him⟩ : Fin m), x ∉ t
ht' : #t = #(Iic (⟨i, him⟩ : Fin m))
⊢ ∃ (x : Fin m), x ∈ Iic (⟨i, him⟩ : Fin m) \ t

Tactic:
simp_rw [← mem_sdiff] at hne

Premises used: Finset.mem_sdiff
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
ht' : #t = #(Iic (⟨i, him⟩ : Fin m))
hne : ∃ (x : Fin m), x ∈ Iic (⟨i, him⟩ : Fin m) \ t
⊢ (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∈ Iic (⟨i, him⟩ : Fin m) ∧ (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∉ t

Tactic:
have hkm := mem_sdiff.1 (min'_mem _ hne)
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
ht' : #t = #(Iic (⟨i, him⟩ : Fin m))
hne : ∃ (x : Fin m), x ∈ Iic (⟨i, him⟩ : Fin m) \ t
hkm : (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∈ Iic (⟨i, him⟩ : Fin m) ∧ (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∉ t
⊢ LT.lt (α := Lex (Fin m →₀ ℕ))
    ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (Finsupp.indicator t fun (x : Fin m) (x_1 : x ∈ t) ↦ 1) :
      Lex (Fin m →₀ ℕ))
    ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
        (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1) :
      Lex (Fin m →₀ ℕ))

Tactic:
⟨min' _ hne, fun k hk ↦ ?_, ?_⟩

Premises used: Finset.min', Pi.Lex, And.intro, Exists.intro, Finsupp.Lex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
ht' : #t = #(Iic (⟨i, him⟩ : Fin m))
hne : ∃ (x : Fin m), x ∈ Iic (⟨i, him⟩ : Fin m) \ t
hkm : (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∈ Iic (⟨i, him⟩ : Fin m) ∧ (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∉ t
refine_2 :
  ∀ (k : Fin m) (hk : (fun (x1 x2 : Fin m) ↦ x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)),
    Eq (α := (@fun {i : Fin m} ↦ ℕ) k)
      ((((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
                ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
                  (Finsupp.indicator t fun (x : Fin m) (x_1 : x ∈ t) ↦ 1)) :
              Fin m →₀ ℕ) :
            (a : Fin m) → ℕ)
          k :
        ℕ)
      ((((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
                ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
                  (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1)) :
              Fin m →₀ ℕ) :
            (a : Fin m) → ℕ)
          k :
        ℕ)
refine_2₁ :
  (@fun {i : Fin m} (x1 x2 : ℕ) ↦ x1 < x2) ((Iic ⟨i, him⟩ \ t).min' hne)
    ((((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
            ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (Finsupp.indicator t fun (x : Fin m) (x_1 : x ∈ t) ↦ 1)) :
          Fin m →₀ ℕ) :
        (a : Fin m) → ℕ)
      ((Iic (⟨i, him⟩ : Fin m) \ t).min' hne))
    ((((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
            ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
              (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1)) :
          Fin m →₀ ℕ) :
        (a : Fin m) → ℕ)
      ((Iic (⟨i, him⟩ : Fin m) \ t).min' hne))
⊢ LT.lt (α := Lex (Fin m →₀ ℕ))
    ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (Finsupp.indicator t fun (x : Fin m) (x_1 : x ∈ t) ↦ 1) :
      Lex (Fin m →₀ ℕ))
    ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
        (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1) :
      Lex (Fin m →₀ ℕ))

Tactic:
refine ⟨min' _ hne, fun k hk ↦ ?_, ?_⟩
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
ht' : #t = #(Iic (⟨i, him⟩ : Fin m))
hne : ∃ (x : Fin m), x ∈ Iic (⟨i, him⟩ : Fin m) \ t
hkm : (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∈ Iic (⟨i, him⟩ : Fin m) ∧ (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∉ t
k : Fin m
hk : (fun (x1 x2 : Fin m) ↦ x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
refine_2 : Eq (α := ℕ) (if hi : k ∈ t then 1 else 0) (if hi : k ∈ Iic (⟨i, him⟩ : Fin m) then 1 else 0)
⊢ Eq (α := (@fun {i : Fin m} ↦ ℕ) k)
    ((((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
              ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (Finsupp.indicator t fun (x : Fin m) (x_1 : x ∈ t) ↦ 1)) :
            Fin m →₀ ℕ) :
          (a : Fin m) → ℕ)
        k :
      ℕ)
    ((((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
              ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
                (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1)) :
            Fin m →₀ ℕ) :
          (a : Fin m) → ℕ)
        k :
      ℕ)

Tactic:
simp only [ofLex_toLex, Finsupp.indicator_apply]

Premises used: Finsupp.indicator_apply, ofLex_toLex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
ht' : #t = #(Iic (⟨i, him⟩ : Fin m))
hne : ∃ (x : Fin m), x ∈ Iic (⟨i, him⟩ : Fin m) \ t
hkm : (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∈ Iic (⟨i, him⟩ : Fin m) ∧ (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∉ t
refine_2 :
  LT.lt (α := ℕ) (if hi : (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∈ t then 1 else 0)
    (if hi : (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∈ Iic (⟨i, him⟩ : Fin m) then 1 else 0)
⊢ (@fun {i : Fin m} (x1 x2 : ℕ) ↦ x1 < x2) ((Iic ⟨i, him⟩ \ t).min' hne)
    ((((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
            ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (Finsupp.indicator t fun (x : Fin m) (x_1 : x ∈ t) ↦ 1)) :
          Fin m →₀ ℕ) :
        (a : Fin m) → ℕ)
      ((Iic (⟨i, him⟩ : Fin m) \ t).min' hne))
    ((((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
            ((toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
              (Finsupp.indicator (Iic ⟨i, him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨i, him⟩ : Fin m)) ↦ 1)) :
          Fin m →₀ ℕ) :
        (a : Fin m) → ℕ)
      ((Iic (⟨i, him⟩ : Fin m) \ t).min' hne))

Tactic:
simp only [ofLex_toLex, Finsupp.indicator_apply]

Premises used: Finsupp.indicator_apply, ofLex_toLex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
ht' : #t = #(Iic (⟨i, him⟩ : Fin m))
hne : ∃ (x : Fin m), x ∈ Iic (⟨i, him⟩ : Fin m) \ t
hkm : (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∈ Iic (⟨i, him⟩ : Fin m) ∧ (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∉ t
k : Fin m
hk : (fun (x1 x2 : Fin m) ↦ x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
⊢ k ∈ Iic (⟨i, him⟩ : Fin m)

Tactic:
have hki := mem_Iic.2 (hk.le.trans <| mem_Iic.1 hkm.1)
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
ht' : #t = #(Iic (⟨i, him⟩ : Fin m))
hne : ∃ (x : Fin m), x ∈ Iic (⟨i, him⟩ : Fin m) \ t
hkm : (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∈ Iic (⟨i, him⟩ : Fin m) ∧ (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∉ t
k : Fin m
hk : (fun (x1 x2 : Fin m) ↦ x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
hki : k ∈ Iic (⟨i, him⟩ : Fin m)
refine_2 : k ∈ t
⊢ Eq (α := ℕ) (if hi : k ∈ t then 1 else 0) (if hi : k ∈ Iic (⟨i, him⟩ : Fin m) then 1 else 0)

Tactic:
rw [dif_pos hki, dif_pos]

Premises used: dif_pos
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
ht' : #t = #(Iic (⟨i, him⟩ : Fin m))
hne : ∃ (x : Fin m), x ∈ Iic (⟨i, him⟩ : Fin m) \ t
hkm : (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∈ Iic (⟨i, him⟩ : Fin m) ∧ (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∉ t
k : Fin m
hk : (fun (x1 x2 : Fin m) ↦ x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
hki : k ∈ Iic (⟨i, him⟩ : Fin m)
refine_2 : ∀ (h : k ∉ t), False
⊢ k ∈ t

Tactic:
by_contra h
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
ht' : #t = #(Iic (⟨i, him⟩ : Fin m))
hne : ∃ (x : Fin m), x ∈ Iic (⟨i, him⟩ : Fin m) \ t
hkm : (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∈ Iic (⟨i, him⟩ : Fin m) ∧ (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∉ t
k : Fin m
hk : (fun (x1 x2 : Fin m) ↦ x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
hki : k ∈ Iic (⟨i, him⟩ : Fin m)
h : k ∉ t
⊢ False

Tactic:
lt_irrefl k <| ((lt_min'_iff _ _).1 hk) _ <| mem_sdiff.2 ⟨hki, h⟩

Premises used: Iff.mpr, lt_irrefl, Finset.mem_sdiff, And.intro, Iff.mp, Finset.lt_min'_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
ht' : #t = #(Iic (⟨i, him⟩ : Fin m))
hne : ∃ (x : Fin m), x ∈ Iic (⟨i, him⟩ : Fin m) \ t
hkm : (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∈ Iic (⟨i, him⟩ : Fin m) ∧ (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∉ t
k : Fin m
hk : (fun (x1 x2 : Fin m) ↦ x1 < x2) k ((Iic ⟨i, him⟩ \ t).min' hne)
hki : k ∈ Iic (⟨i, him⟩ : Fin m)
h : k ∉ t
⊢ False

Tactic:
exact lt_irrefl k <| ((lt_min'_iff _ _).1 hk) _ <| mem_sdiff.2 ⟨hki, h⟩

Premises used: Iff.mpr, lt_irrefl, Finset.mem_sdiff, And.intro, Iff.mp, Finset.lt_min'_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
ht' : #t = #(Iic (⟨i, him⟩ : Fin m))
hne : ∃ (x : Fin m), x ∈ Iic (⟨i, him⟩ : Fin m) \ t
hkm : (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∈ Iic (⟨i, him⟩ : Fin m) ∧ (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∉ t
refine_2 : LT.lt (α := ℕ) 0 1
⊢ LT.lt (α := ℕ) (if hi : (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∈ t then 1 else 0)
    (if hi : (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∈ Iic (⟨i, him⟩ : Fin m) then 1 else 0)

Tactic:
rw [dif_neg hkm.2, dif_pos hkm.1]

Premises used: dif_pos, dif_neg, And.right, And.left
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
ht' : #t = #(Iic (⟨i, him⟩ : Fin m))
hne : ∃ (x : Fin m), x ∈ Iic (⟨i, him⟩ : Fin m) \ t
hkm : (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∈ Iic (⟨i, him⟩ : Fin m) ∧ (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∉ t
⊢ LT.lt (α := ℕ) 0 1

Tactic:
Nat.zero_lt_one

Premises used: Nat.zero_lt_one
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
inst_1 : Nontrivial R
i : ℕ
him : i < m
t : Finset (Fin m)
ht : Membership.mem (γ := Finset (Finset (Fin m))) (powersetCard (i + 1) univ) t
ht' : #t = #(Iic (⟨i, him⟩ : Fin m))
hne : ∃ (x : Fin m), x ∈ Iic (⟨i, him⟩ : Fin m) \ t
hkm : (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∈ Iic (⟨i, him⟩ : Fin m) ∧ (Iic (⟨i, him⟩ : Fin m) \ t).min' hne ∉ t
⊢ LT.lt (α := ℕ) 0 1

Tactic:
exact Nat.zero_lt_one

Premises used: Nat.zero_lt_one
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
i : Fin n
inst_1 : Nontrivial R
him : (↑i : ℕ) < m
rw :
  Eq (α := (a : Fin m) → ℕ)
    (⇑(Finsupp.indicator (Iic ⟨(↑i : ℕ), him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨(↑i : ℕ), him⟩ : Fin m)) ↦ 1) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑fun₀ | i => 1 : (a : Fin n) → ℕ))
⊢ Eq (α := (a : Fin m) → ℕ)
    (⇑((ofLex : (a : Lex (Fin m →₀ ℕ)) → Fin m →₀ ℕ)
          (supDegree (A := Fin m →₀ ℕ) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ))
            (esymm (Fin m) R ((↑i : ℕ) + 1)))) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑fun₀ | i => 1 : (a : Fin n) → ℕ))

Tactic:
rw [(supDegree_monic_esymm him).1, ofLex_toLex]

Premises used: ofLex_toLex, And.left, _private.0.MvPolynomial.supDegree_monic_esymm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
i : Fin n
inst_1 : Nontrivial R
him : (↑i : ℕ) < m
h :
  ∀ (j : Fin m),
    Eq (α := ℕ)
      ((Finsupp.indicator (Iic ⟨(↑i : ℕ), him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨(↑i : ℕ), him⟩ : Fin m)) ↦ 1 :
            (a : Fin m) → ℕ)
          j :
        ℕ)
      ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑fun₀ | i => 1 : (a : Fin n) → ℕ) j : ℕ)
⊢ Eq (α := (a : Fin m) → ℕ)
    (⇑(Finsupp.indicator (Iic ⟨(↑i : ℕ), him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨(↑i : ℕ), him⟩ : Fin m)) ↦ 1) :
      (a : Fin m) → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑fun₀ | i => 1 : (a : Fin n) → ℕ))

Tactic:
ext j
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
i : Fin n
inst_1 : Nontrivial R
him : (↑i : ℕ) < m
j : Fin m
h :
  Eq (α := ℕ) (if hi : j ∈ Iic (⟨(↑i : ℕ), him⟩ : Fin m) then 1 else 0 : ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑fun₀ | i => 1 : (a : Fin n) → ℕ) j : ℕ)
h₁ :
  Eq (α := ℕ) (if j ∈ Iic (⟨(↑i : ℕ), him⟩ : Fin m) then 1 else 0 : ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑fun₀ | i => 1 : (a : Fin n) → ℕ) j : ℕ)
h₂ :
  Eq (α := ℕ) (if j ≤ ⟨(↑i : ℕ), him⟩ then 1 else 0 : ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑fun₀ | i => 1 : (a : Fin n) → ℕ) j : ℕ)
h₃ :
  Eq (α := ℕ) (if j ≤ ⟨(↑i : ℕ), him⟩ then 1 else 0)
    (∑ i_1 : Fin n with (↑j : ℕ) ≤ (↑i_1 : ℕ), (fun₀ | i => 1 : (a : Fin n) → ℕ) i_1)
h₄ : Eq (α := ℕ) (if j ≤ ⟨(↑i : ℕ), him⟩ then 1 else 0) (∑ x : Fin n with (↑j : ℕ) ≤ (↑x : ℕ), if i = x then 1 else 0)
h₅ :
  Eq (α := ℕ) (if j ≤ ⟨(↑i : ℕ), him⟩ then 1 else 0)
    (if Membership.mem (γ := Finset (Fin n)) {i : Fin n | (↑j : ℕ) ≤ (↑i : ℕ)} i then 1 else 0)
h₆ : Eq (α := ℕ) (if j ≤ ⟨(↑i : ℕ), him⟩ then 1 else 0) (if (↑j : ℕ) ≤ (↑i : ℕ) then 1 else 0)
⊢ Eq (α := ℕ)
    ((Finsupp.indicator (Iic ⟨(↑i : ℕ), him⟩) fun (x : Fin m) (x_1 : x ∈ Iic (⟨(↑i : ℕ), him⟩ : Fin m)) ↦ 1 :
          (a : Fin m) → ℕ)
        j :
      ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (⇑fun₀ | i => 1 : (a : Fin n) → ℕ) j : ℕ)

Tactic:
simp_rw [Finsupp.indicator_apply, dite_eq_ite, mem_Iic, accumulate_apply, Finsupp.single_apply,
    sum_ite_eq, mem_filter_univ, Fin.le_def]

Premises used: Finset.mem_filter_univ, Finset.mem_Iic, Finsupp.indicator_apply, Fin.accumulate_apply, Fin.le_def, Finsupp.single_apply, dite_eq_ite, Finset.sum_ite_eq
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
him : 0 ≤ m
zero :
  Monic.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) 1
⊢ Monic (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) (esymm (Fin m) R 0)

Tactic:
rw [esymm_zero]

Premises used: MvPolynomial.esymm_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
him : 0 ≤ m
⊢ Monic.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) 1

Tactic:
monic_one toLex.injective

Premises used: AddMonoidAlgebra.monic_one, Equiv.injective, toLex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
m : ℕ
inst : CommSemiring R
him : 0 ≤ m
⊢ Monic.{u_3, 0, 0} (R := R) (A := Fin m →₀ ℕ) (B := Lex (Fin m →₀ ℕ)) (⇑toLex : (a : Fin m →₀ ℕ) → Lex (Fin m →₀ ℕ)) 1

Tactic:
exact monic_one toLex.injective

Premises used: AddMonoidAlgebra.monic_one, Equiv.injective, toLex