awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) : ℕ)
inl :
  ∀
    (this :
      (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t ⟨(↑i : ℕ), ⋯⟩ =
        HAdd.hAdd (β := ℕ) (s (⟨(↑i : ℕ), ⋯⟩ : Fin n))
          ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t (⟨(↑i : ℕ) + 1, h⟩ : Fin m) : ℕ)),
    t i = s i
⊢ t i = s i
have inl₁ : ∀
  (this :
    HAdd.hAdd (β := ℕ) (t (⟨(↑i : ℕ), sorry⟩ : Fin n))
        ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t (⟨(↑i : ℕ) + 1, h⟩ : Fin m) : ℕ) =
      HAdd.hAdd (β := ℕ) (s (⟨(↑i : ℕ), sorry⟩ : Fin n))
        ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t ⟨(↑i : ℕ) + 1, h⟩ : ℕ)),
  t i = s i
Tactic: rwa [← he, accumulate_rec i.2 h t, add_right_cancel_iff] at this
Cleared hypotheses: this
-- 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) : ℕ)
inl :
  ∀
    (this :
      (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t ⟨(↑i : ℕ), ⋯⟩ =
        HAdd.hAdd (β := ℕ) (s (⟨(↑i : ℕ), ⋯⟩ : Fin n))
          ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t (⟨(↑i : ℕ) + 1, h⟩ : Fin m) : ℕ)),
    t i = s i
inl₁ :
  ∀
    (this :
      HAdd.hAdd (β := ℕ) (t (⟨(↑i : ℕ), ⋯⟩ : Fin n))
          ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t (⟨(↑i : ℕ) + 1, h⟩ : Fin m) : ℕ) =
        HAdd.hAdd (β := ℕ) (s (⟨(↑i : ℕ), ⋯⟩ : Fin n))
          ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t ⟨(↑i : ℕ) + 1, h⟩ : ℕ)),
    t i = s i
⊢ t i = s i
have inl₂ : ∀ (this : t (⟨(↑i : ℕ), sorry⟩ : Fin n) = s ⟨(↑i : ℕ), sorry⟩), t i = s i
Tactic: rwa [← he, accumulate_rec i.2 h t, add_right_cancel_iff] at this
Cleared hypotheses: this
-- 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 : m ≤ (↑i : ℕ) + 1
⊢ t i = s i
have this : m = (↑i : ℕ) + 1
Tactic: have := h.antisymm (i.2.nat_succ_le.trans hnm)
-- 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 : m ≤ (↑i : ℕ) + 1
this : m = (↑i : ℕ) + 1
⊢ t i = s i
have inr : ∀ (j : Fin n), m ≤ (↑j : ℕ) → s j = 0
Tactic: rw [← accumulate_last i.2 this t, ← accumulate_last i.2 this s, he]
-- 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 : m ≤ (↑i : ℕ) + 1
this : m = (↑i : ℕ) + 1
inr : ∀ (j : Fin n), m ≤ (↑j : ℕ) → s j = 0
⊢ t i = s i
have inr₁ : ∀ (j : Fin n), m ≤ (↑j : ℕ) → t j = 0
Tactic: rw [← accumulate_last i.2 this t, ← accumulate_last i.2 this s, he]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (hypothesis)
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i : ℕ
hi : i < m
⊢ (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i, hi⟩ = s (⟨i, hi⟩ : Fin m)
have this : i ≤ m - 1
Tactic: have := Nat.le_sub_one_of_lt hi
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i : ℕ
hi : i < m
this : i ≤ m - 1
⊢ (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i, hi⟩ = s (⟨i, hi⟩ : Fin m)
have revert : ∀ (hi : i < m), (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i, hi⟩ = s (⟨i, hi⟩ : Fin m)
Tactic: revert hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i : ℕ
this : i ≤ m - 1
⊢ ∀ (hi : i < m), (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i, hi⟩ = s (⟨i, hi⟩ : Fin m)
have refine_1 : ∀ (i_1 : ℕ) (hi : i_1 < m - 1),
  i ≤ i_1 →
    ∀
      (ih :
        ∀ (hi : i_1 + 1 < m),
          (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i_1 + 1, hi⟩ =
            s (⟨i_1 + 1, hi⟩ : Fin m))
      (him : i_1 < m),
      (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i_1, him⟩ = s (⟨i_1, him⟩ : Fin m)
Tactic: refine Nat.decreasingInduction' (fun i hi _ ih him ↦ ?_) this fun hm ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i : ℕ
this : i ≤ m - 1
refine_1 :
  ∀ (i_1 : ℕ) (hi : i_1 < m - 1),
    i ≤ i_1 →
      ∀
        (ih :
          ∀ (hi : i_1 + 1 < m),
            (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i_1 + 1, hi⟩ =
              s (⟨i_1 + 1, hi⟩ : Fin m))
        (him : i_1 < m),
        (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i_1, him⟩ = s (⟨i_1, him⟩ : Fin m)
⊢ ∀ (hi : i < m), (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i, hi⟩ = s (⟨i, hi⟩ : Fin m)
have refine_2 : ∀ (hm : m - 1 < m),
  (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨m - 1, hm⟩ = s (⟨m - 1, hm⟩ : Fin m)
Tactic: refine Nat.decreasingInduction' (fun i hi _ ih him ↦ ?_) this fun hm ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i_1 : ℕ
this : i_1 ≤ m - 1
i : ℕ
hi : i < m - 1
h : i_1 ≤ i
ih :
  ∀ (hi : i + 1 < m),
    (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i + 1, hi⟩ = s (⟨i + 1, hi⟩ : Fin m)
him : i < m
⊢ (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i, him⟩ = s (⟨i, him⟩ : Fin m)
have refine_1 : ∀ (hi : i + 1 < m),
  i_1 ≤ i →
    ∀
      (ih :
        ∀ (hi : i + 1 < m),
          (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i + 1, hi⟩ = s (⟨i + 1, hi⟩ : Fin m))
      (him : i < m),
      (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i, him⟩ = s (⟨i, him⟩ : Fin m)
Tactic: rw [← Nat.pred_eq_sub_one, Nat.lt_pred_iff, Nat.succ_eq_add_one] at hi
Cleared hypotheses: hi, h, ih, him
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i_1 : ℕ
this : i_1 ≤ m - 1
i : ℕ
hi : i + 1 < m
h : i_1 ≤ i
ih :
  ∀ (hi : i + 1 < m),
    (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i + 1, hi⟩ = s (⟨i + 1, hi⟩ : Fin m)
him : i < m
⊢ (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i, him⟩ = s (⟨i, him⟩ : Fin m)
have refine_1 : s (⟨(↑(⟨i, sorry⟩ : Fin n) : ℕ), him⟩ : Fin m) - s (⟨(↑(⟨i, sorry⟩ : Fin n) : ℕ) + 1, hi⟩ : Fin m) + s (⟨i + 1, hi⟩ : Fin m) =
  s ⟨i, him⟩
Tactic: rw [accumulate_rec (him.trans_le hmn) hi, ih hi, invAccumulate, dif_pos him, dif_pos hi]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i_1 : ℕ
this : i_1 ≤ m - 1
i : ℕ
hi : i + 1 < m
h : i_1 ≤ i
ih :
  ∀ (hi : i + 1 < m),
    (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i + 1, hi⟩ = s (⟨i + 1, hi⟩ : Fin m)
him : i < m
⊢ s (⟨(↑(⟨i, ⋯⟩ : Fin n) : ℕ), him⟩ : Fin m) - s (⟨(↑(⟨i, ⋯⟩ : Fin n) : ℕ) + 1, hi⟩ : Fin m) + s (⟨i + 1, hi⟩ : Fin m) =
    s ⟨i, him⟩
have refine_1 : s (⟨i, him⟩ : Fin m) - s (⟨i + 1, hi⟩ : Fin m) + s (⟨i + 1, hi⟩ : Fin m) = s ⟨i, him⟩
Tactic: simp only
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (hypothesis)
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i : ℕ
this : i ≤ m - 1
hm : m - 1 < m
⊢ (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨m - 1, hm⟩ = s (⟨m - 1, hm⟩ : Fin m)
have this₁ : m = m - 1 + 1
Tactic: have := (Nat.sub_one_add_one <| Nat.ne_zero_of_lt hm).symm
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i : ℕ
this_1 : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
⊢ (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨m - 1, hm⟩ = s (⟨m - 1, hm⟩ : Fin m)
have refine_2 : ∀ (j : Fin n), m ≤ (↑j : ℕ) → invAccumulate n m s j = 0
Tactic: rw [accumulate_last (hm.trans_le hmn) this, invAccumulate, dif_pos hm, dif_neg this.not_gt,
      Nat.sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i : ℕ
this_1 : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
j : Fin n
hj : m ≤ (↑j : ℕ)
⊢ invAccumulate n m s j = 0
have refine_2 : HSub.hSub (α := ℕ) (if hi : (↑j : ℕ) < m then s (⟨(↑j : ℕ), hi⟩ : Fin m) else 0)
    (if hi : (↑j : ℕ) + 1 < m then s (⟨(↑j : ℕ) + 1, hi⟩ : Fin m) else 0) =
  0
Tactic: rw [invAccumulate, dif_neg hj.not_gt, Nat.zero_sub]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i : ℕ
this_1 : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
j : Fin n
hj : m ≤ (↑j : ℕ)
refine_2 :
  HSub.hSub (α := ℕ) (if hi : (↑j : ℕ) < m then s (⟨(↑j : ℕ), hi⟩ : Fin m) else 0)
      (if hi : (↑j : ℕ) + 1 < m then s (⟨(↑j : ℕ) + 1, hi⟩ : Fin m) else 0) =
    0
⊢ invAccumulate n m s j = 0
have refine_2₁ : HSub.hSub (α := ℕ) 0 (if hi : (↑j : ℕ) + 1 < m then s (⟨(↑j : ℕ) + 1, hi⟩ : Fin m) else 0) = 0
Tactic: rw [invAccumulate, dif_neg hj.not_gt, Nat.zero_sub]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i : ℕ
this_1 : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
j : Fin n
hj : m ≤ (↑j : ℕ)
refine_2 :
  HSub.hSub (α := ℕ) (if hi : (↑j : ℕ) < m then s (⟨(↑j : ℕ), hi⟩ : Fin m) else 0)
      (if hi : (↑j : ℕ) + 1 < m then s (⟨(↑j : ℕ) + 1, hi⟩ : Fin m) else 0) =
    0
refine_2₁ : HSub.hSub (α := ℕ) 0 (if hi : (↑j : ℕ) + 1 < m then s (⟨(↑j : ℕ) + 1, hi⟩ : Fin m) else 0) = 0
⊢ invAccumulate n m s j = 0
have refine_2₂ : Eq (α := ℕ) 0 0
Tactic: rw [invAccumulate, dif_neg hj.not_gt, Nat.zero_sub]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
e : σ ≃ τ
⊢ Eq (α := MvPolynomial (Fin n) R →ₐ[R] ↥(symmetricSubalgebra τ R))
    (AlgHom.comp (↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R))
      (esymmAlgHom σ R n))
    (esymmAlgHom τ R n)
have hf : ∀ (i : Fin n),
  Eq (α := MvPolynomial τ R)
    (↑((AlgHom.comp (↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R))
              (esymmAlgHom σ R n) :
            (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R))
          (X i)) :
      MvPolynomial τ R)
    (↑((esymmAlgHom τ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R)) (X i)) : MvPolynomial τ R)
Tactic: ext i : 2
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
e : σ ≃ τ
i : Fin n
⊢ Eq (α := MvPolynomial τ R)
    (↑((AlgHom.comp (↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R))
              (esymmAlgHom σ R n) :
            (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R))
          (X i)) :
      MvPolynomial τ R)
    (↑((esymmAlgHom τ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R)) (X i)) : MvPolynomial τ R)
have hf : Eq (α := MvPolynomial τ R)
  (↑(((↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R)) :
          (a : ↥(symmetricSubalgebra σ R)) → ↥(symmetricSubalgebra τ R))
        ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R)) (X i))) :
    MvPolynomial τ R)
  (↑((esymmAlgHom τ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R)) (X i)) : MvPolynomial τ R)
Tactic: simp_rw [AlgHom.comp_apply, esymmAlgHom, aeval_X, AlgEquiv.coe_algHom,
    renameSymmetricSubalgebra_apply_coe, rename_esymm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
e : σ ≃ τ
i : Fin n
hf :
  Eq (α := MvPolynomial τ R)
    (↑(((↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R)) :
            (a : ↥(symmetricSubalgebra σ R)) → ↥(symmetricSubalgebra τ R))
          ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R)) (X i))) :
      MvPolynomial τ R)
    (↑((esymmAlgHom τ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R)) (X i)) : MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    (↑((AlgHom.comp (↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R))
              (esymmAlgHom σ R n) :
            (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R))
          (X i)) :
      MvPolynomial τ R)
    (↑((esymmAlgHom τ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R)) (X i)) : MvPolynomial τ R)
have hf₁ : Eq (α := MvPolynomial τ R)
  (↑(((↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R)) :
          (a : ↥(symmetricSubalgebra σ R)) → ↥(symmetricSubalgebra τ R))
        ((aeval fun (i : Fin n) ↦
              Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
                Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x)
                (esymm σ R ((↑i : ℕ) + 1)) sorry :
            (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
          (X i))) :
    MvPolynomial τ R)
  (↑((aeval fun (i : Fin n) ↦
            Subtype.mk (p := fun (x : MvPolynomial τ R) ↦
              Membership.mem (γ := Subalgebra R (MvPolynomial τ R)) (symmetricSubalgebra τ R) x)
              (esymm τ R ((↑i : ℕ) + 1)) sorry :
          (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R))
        (X i)) :
    MvPolynomial τ R)
Tactic: simp_rw [AlgHom.comp_apply, esymmAlgHom, aeval_X, AlgEquiv.coe_algHom,
    renameSymmetricSubalgebra_apply_coe, rename_esymm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
e : σ ≃ τ
i : Fin n
hf :
  Eq (α := MvPolynomial τ R)
    (↑(((↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R)) :
            (a : ↥(symmetricSubalgebra σ R)) → ↥(symmetricSubalgebra τ R))
          ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R)) (X i))) :
      MvPolynomial τ R)
    (↑((esymmAlgHom τ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R)) (X i)) : MvPolynomial τ R)
hf₁ :
  Eq (α := MvPolynomial τ R)
    (↑(((↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R)) :
            (a : ↥(symmetricSubalgebra σ R)) → ↥(symmetricSubalgebra τ R))
          ((aeval fun (i : Fin n) ↦
                Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
                  Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x)
                  (esymm σ R ((↑i : ℕ) + 1)) ⋯ :
              (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            (X i))) :
      MvPolynomial τ R)
    (↑((aeval fun (i : Fin n) ↦
              Subtype.mk (p := fun (x : MvPolynomial τ R) ↦
                Membership.mem (γ := Subalgebra R (MvPolynomial τ R)) (symmetricSubalgebra τ R) x)
                (esymm τ R ((↑i : ℕ) + 1)) ⋯ :
            (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R))
          (X i)) :
      MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    (↑((AlgHom.comp (↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R))
              (esymmAlgHom σ R n) :
            (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R))
          (X i)) :
      MvPolynomial τ R)
    (↑((esymmAlgHom τ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R)) (X i)) : MvPolynomial τ R)
have hf₂ : Eq (α := MvPolynomial τ R)
  (↑(((↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R)) :
          (a : ↥(symmetricSubalgebra σ R)) → ↥(symmetricSubalgebra τ R))
        (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x) (esymm σ R ((↑i : ℕ) + 1))
          sorry)) :
    MvPolynomial τ R)
  (esymm τ R ((↑i : ℕ) + 1))
Tactic: simp_rw [AlgHom.comp_apply, esymmAlgHom, aeval_X, AlgEquiv.coe_algHom,
    renameSymmetricSubalgebra_apply_coe, rename_esymm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
e : σ ≃ τ
i : Fin n
hf :
  Eq (α := MvPolynomial τ R)
    (↑(((↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R)) :
            (a : ↥(symmetricSubalgebra σ R)) → ↥(symmetricSubalgebra τ R))
          ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R)) (X i))) :
      MvPolynomial τ R)
    (↑((esymmAlgHom τ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R)) (X i)) : MvPolynomial τ R)
hf₁ :
  Eq (α := MvPolynomial τ R)
    (↑(((↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R)) :
            (a : ↥(symmetricSubalgebra σ R)) → ↥(symmetricSubalgebra τ R))
          ((aeval fun (i : Fin n) ↦
                Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
                  Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x)
                  (esymm σ R ((↑i : ℕ) + 1)) ⋯ :
              (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            (X i))) :
      MvPolynomial τ R)
    (↑((aeval fun (i : Fin n) ↦
              Subtype.mk (p := fun (x : MvPolynomial τ R) ↦
                Membership.mem (γ := Subalgebra R (MvPolynomial τ R)) (symmetricSubalgebra τ R) x)
                (esymm τ R ((↑i : ℕ) + 1)) ⋯ :
            (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R))
          (X i)) :
      MvPolynomial τ R)
hf₂ :
  Eq (α := MvPolynomial τ R)
    (↑(((↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R)) :
            (a : ↥(symmetricSubalgebra σ R)) → ↥(symmetricSubalgebra τ R))
          (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
            Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x)
            (esymm σ R ((↑i : ℕ) + 1)) ⋯)) :
      MvPolynomial τ R)
    (esymm τ R ((↑i : ℕ) + 1))
⊢ Eq (α := MvPolynomial τ R)
    (↑((AlgHom.comp (↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R))
              (esymmAlgHom σ R n) :
            (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R))
          (X i)) :
      MvPolynomial τ R)
    (↑((esymmAlgHom τ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R)) (X i)) : MvPolynomial τ R)
have hf₃ : Eq (α := MvPolynomial τ R)
  (↑((renameSymmetricSubalgebra e : (a : ↥(symmetricSubalgebra σ R)) → ↥(symmetricSubalgebra τ R))
        (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x) (esymm σ R ((↑i : ℕ) + 1))
          sorry)) :
    MvPolynomial τ R)
  (esymm τ R ((↑i : ℕ) + 1))
Tactic: simp_rw [AlgHom.comp_apply, esymmAlgHom, aeval_X, AlgEquiv.coe_algHom,
    renameSymmetricSubalgebra_apply_coe, rename_esymm]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n k : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
i : Fin n
r : R
⊢ esymmAlgHomMonomial σ (fun₀ | i => k) r =
    HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k)
have rw : HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (esymm σ R ((↑i : ℕ) + 1)) 0 = 1
Tactic: rw [esymmAlgHomMonomial, esymmAlgHom_apply, aeval_monomial, algebraMap_eq,
    Finsupp.prod_single_index]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n k : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
i : Fin n
⊢ esymmAlgHomMonomial σ (fun₀ | i => k) 1 = HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k
have rw : (C : (a : R) → MvPolynomial σ R) 1 * HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k =
  HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k
Tactic: rw [esymmAlgHomMonomial_single, map_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n k : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
i : Fin n
rw :
  (C : (a : R) → MvPolynomial σ R) 1 * HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k =
    HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k
⊢ esymmAlgHomMonomial σ (fun₀ | i => k) 1 = HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k
have rw₁ : 1 * HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k =
  HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k
Tactic: rw [esymmAlgHomMonomial_single, map_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n k : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
i : Fin n
rw :
  (C : (a : R) → MvPolynomial σ R) 1 * HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k =
    HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k
rw₁ :
  1 * HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k =
    HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k
⊢ esymmAlgHomMonomial σ (fun₀ | i => k) 1 = HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k
have rw₂ : HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k =
  HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k
Tactic: rw [esymmAlgHomMonomial_single, map_one, one_mul]