awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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))
have rw : i + 1 = #(Iic (⟨i, him⟩ : Fin m))
Tactic: rw [(mem_powersetCard.1 ht).2, Fin.card_Iic]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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))
⊢ #t = #(Iic (⟨i, him⟩ : Fin m))
have rw₁ : i + 1 = (↑(⟨i, him⟩ : Fin m) : ℕ) + 1
Tactic: rw [(mem_powersetCard.1 ht).2, Fin.card_Iic]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (hypothesis)
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⟩
⊢ 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⟩)))
have ht' : #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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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))
⊢ 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⟩)))
have 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 →₀ ℕ))
Tactic: simp_rw [← single_eq_monomial, supDegree_single_ne_zero _ one_ne_zero,
    ← Finsupp.indicator_eq_sum_single]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (hypothesis)
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))
⊢ 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 →₀ ℕ))
have hne₁ : ∃ 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
Cleared hypotheses: hne, ht'
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (hypothesis)
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))
⊢ 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 →₀ ℕ))
have hne₁ : ∃ (x : Fin m), x ∈ Iic (⟨i, him⟩ : Fin m) \ t
Tactic: simp_rw [← mem_sdiff] at hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (hypothesis)
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
⊢ 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 →₀ ℕ))
have hkm : (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)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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 →₀ ℕ))
have 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 :
      ℕ)
Tactic: refine ⟨min' _ hne, fun k hk ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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 :
        ℕ)
⊢ 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 →₀ ℕ))
have 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))
Tactic: refine ⟨min' _ hne, fun k hk ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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)
⊢ 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 :
      ℕ)
have refine_2 : Eq (α := ℕ) (if hi : k ∈ t then 1 else 0) (if hi : k ∈ Iic (⟨i, him⟩ : Fin m) then 1 else 0)
Tactic: simp only [ofLex_toLex, Finsupp.indicator_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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
⊢ (@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))
have 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)
Tactic: simp only [ofLex_toLex, Finsupp.indicator_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (hypothesis)
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)
⊢ Eq (α := ℕ) (if hi : k ∈ t then 1 else 0) (if hi : k ∈ Iic (⟨i, him⟩ : Fin m) then 1 else 0)
have hki : k ∈ Iic (⟨i, him⟩ : Fin m)
Tactic: have hki := mem_Iic.2 (hk.le.trans <| mem_Iic.1 hkm.1)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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)
⊢ Eq (α := ℕ) (if hi : k ∈ t then 1 else 0) (if hi : k ∈ Iic (⟨i, him⟩ : Fin m) then 1 else 0)
have refine_2 : k ∈ t
Tactic: rw [dif_pos hki, dif_pos]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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)
⊢ k ∈ t
have refine_2 : ∀ (h : k ∉ t), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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 (α := ℕ) (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)
have refine_2 : LT.lt (α := ℕ) 0 1
Tactic: rw [dif_neg hkm.2, dif_pos hkm.1]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
i : Fin n
inst_1 : Nontrivial R
him : (↑i : ℕ) < m
⊢ 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) → ℕ))
have 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) → ℕ))
Tactic: rw [(supDegree_monic_esymm him).1, ofLex_toLex]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
i : Fin n
inst_1 : Nontrivial R
him : (↑i : ℕ) < m
⊢ 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) → ℕ))
have 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 : ℕ)
Tactic: ext j
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommSemiring R
i : Fin n
inst_1 : Nontrivial R
him : (↑i : ℕ) < m
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 : ℕ)
have 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 : ℕ)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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 : ℕ)
⊢ 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 : ℕ)
have 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 : ℕ)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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 : ℕ)
⊢ 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 : ℕ)
have 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 : ℕ)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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 : ℕ)
⊢ 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 : ℕ)
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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)
⊢ 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 : ℕ)
have h₄ : Eq (α := ℕ) (if j ≤ ⟨(↑i : ℕ), him⟩ then 1 else 0) (∑ x : Fin n with (↑j : ℕ) ≤ (↑x : ℕ), if i = x then 1 else 0)
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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
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)
⊢ 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 : ℕ)
have 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)
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]