awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p,
    ∀ (p : MvPolynomial (Fin n) R)
      (hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p) (h0 : p ≠ 0)
      (he : supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p = y),
      Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
        (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
t : Fin n →₀ ℕ :=
  (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin n → ℕ) → Fin n →₀ ℕ)
    (invAccumulate n n
      (⇑((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ) (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)) :
        (a : Fin n) → ℕ))
hd :
  Eq (α := Lex (Fin n →₀ ℕ))
    (supDegree (A := Fin n →₀ ℕ) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ))
      (esymmAlgHomMonomial (Fin n) t
        (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)))
    (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)
hne :
  p ≠
    esymmAlgHomMonomial (Fin n) t
      (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)
this :
  LT.lt (α := Lex (Fin n →₀ ℕ))
    (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ))
      (p -
        esymmAlgHomMonomial (Fin n) t
          (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)))
    (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)
right :
  p -
      esymmAlgHomMonomial (Fin n) t
        (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p) ≠
    0
⊢ Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
    (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
      Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
have right₁ : ∀
  (ih :
    Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
      (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
        Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x)
        (p -
          esymmAlgHomMonomial (Fin n) t
            (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p))
        sorry)),
  Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
    (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
      Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
Tactic: specialize ih _ this _ (Subalgebra.sub_mem _ hp <| isSymmetric_esymmAlgHomMonomial _ _) _ rfl
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p
h0 : p ≠ 0
t : Fin n →₀ ℕ :=
  (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin n → ℕ) → Fin n →₀ ℕ)
    (invAccumulate n n
      (⇑((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ) (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)) :
        (a : Fin n) → ℕ))
hd :
  Eq (α := Lex (Fin n →₀ ℕ))
    (supDegree (A := Fin n →₀ ℕ) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ))
      (esymmAlgHomMonomial (Fin n) t
        (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)))
    (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)
hne :
  p ≠
    esymmAlgHomMonomial (Fin n) t
      (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)
this :
  LT.lt (α := Lex (Fin n →₀ ℕ))
    (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ))
      (p -
        esymmAlgHomMonomial (Fin n) t
          (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)))
    (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)
ih :
  Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
    (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
      Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x)
      (p -
        esymmAlgHomMonomial (Fin n) t
          (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p))
      ⋯)
⊢ Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
    (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
      Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
have h : (↑(HAdd.hAdd (β := ↥(symmetricSubalgebra (Fin n) R))
        (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x)
          (p -
            esymmAlgHomMonomial (Fin n) t
              (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p))
          sorry)
        ((AlgHom.toRingHom (esymmAlgHom (Fin n) R n) : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin n) R))
            ((monomial t : (a : R) → MvPolynomial (Fin n) R)
              (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)) :
          ↥(symmetricSubalgebra (Fin n) R))) :
    MvPolynomial (Fin n) R) =
  p
Tactic: convert! ← Subalgebra.add_mem _ ih ⟨monomial t (p.leadingCoeff toLex), rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
inst : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p,
    ∀ (p : MvPolynomial (Fin n) R)
      (hp : Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) p) (h0 : p ≠ 0)
      (he : supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p = y),
      Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R)) (AlgHom.range (esymmAlgHom (Fin n) R n))
        (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial (Fin n) R)) (symmetricSubalgebra (Fin n) R) x) p hp)
t : Fin n →₀ ℕ :=
  (Equiv.symm Finsupp.equivFunOnFinite : (a : Fin n → ℕ) → Fin n →₀ ℕ)
    (invAccumulate n n
      (⇑((ofLex : (a : Lex (Fin n →₀ ℕ)) → Fin n →₀ ℕ) (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)) :
        (a : Fin n) → ℕ))
hd :
  Eq (α := Lex (Fin n →₀ ℕ))
    (supDegree (A := Fin n →₀ ℕ) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ))
      (esymmAlgHomMonomial (Fin n) t
        (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)))
    (supDegree (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)
hne :
  p ≠
    esymmAlgHomMonomial (Fin n) t
      (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)
⊢ leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p =
    leadingCoeff (A := Fin n →₀ ℕ) (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ))
      (esymmAlgHomMonomial (Fin n) t
          (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p) :
        MvPolynomial (Fin n) R)
have right : leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p =
  leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p
Tactic: rw [leadingCoeff_esymmAlgHomMonomial t le_rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
p : ↥(symmetricSubalgebra (Fin m) R)
⊢ ∃ (a : MvPolynomial (Fin n) R),
    (esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R)) a = p
have obtain : ∀ (q : MvPolynomial (Fin m) R),
  ∃ (a : MvPolynomial (Fin n) R),
    Eq (α := ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R)) a :
        ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) q :
        ↥(symmetricSubalgebra (Fin m) R))
Tactic: obtain ⟨q, rfl⟩ := (esymmAlgHom_fin_bijective R m).2 p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
r : R
⊢ Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R))
        ((C : (a : R) → MvPolynomial (Fin m) R) r) :
      ↥(symmetricSubalgebra (Fin m) R))
have C : Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
  (AlgHom.range (esymmAlgHom (Fin m) R n))
  ((algebraMap R ↥(symmetricSubalgebra (Fin m) R) : (a : R) → ↥(symmetricSubalgebra (Fin m) R)) r :
    ↥(symmetricSubalgebra (Fin m) R))
Tactic: rw [← algebraMap_eq, AlgHom.commutes]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
p q : MvPolynomial (Fin m) R
hp :
  Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
      ↥(symmetricSubalgebra (Fin m) R))
hq :
  Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) q :
      ↥(symmetricSubalgebra (Fin m) R))
⊢ Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (p + q) :
      ↥(symmetricSubalgebra (Fin m) R))
have add : Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R)) (AlgHom.range (esymmAlgHom (Fin m) R n))
  (HAdd.hAdd (α := ↥(symmetricSubalgebra (Fin m) R)) (β := ↥(symmetricSubalgebra (Fin m) R))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
      ↥(symmetricSubalgebra (Fin m) R))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) q :
      ↥(symmetricSubalgebra (Fin m) R)))
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp :
  Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
      ↥(symmetricSubalgebra (Fin m) R))
⊢ Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (p * X i) :
      ↥(symmetricSubalgebra (Fin m) R))
have mul_X : Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R)) (AlgHom.range (esymmAlgHom (Fin m) R n))
  (HMul.hMul (α := ↥(symmetricSubalgebra (Fin m) R)) (β := ↥(symmetricSubalgebra (Fin m) R))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
      ↥(symmetricSubalgebra (Fin m) R))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (X i) :
      ↥(symmetricSubalgebra (Fin m) R)))
Tactic: rw [map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp :
  Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
      ↥(symmetricSubalgebra (Fin m) R))
⊢ Membership.mem (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R)) (AlgHom.range (esymmAlgHom (Fin m) R n))
    (HMul.hMul (α := ↥(symmetricSubalgebra (Fin m) R)) (β := ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
        ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (X i) :
        ↥(symmetricSubalgebra (Fin m) R)))
have mul_X : Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
  (AlgHom.range (esymmAlgHom (Fin m) R n))
  ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (X i) :
    ↥(symmetricSubalgebra (Fin m) R))
Tactic: apply Subalgebra.mul_mem _ hp
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp :
  Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
      ↥(symmetricSubalgebra (Fin m) R))
⊢ ∃ (x : MvPolynomial (Fin n) R),
    Eq (α := ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R)) x :
        ↥(symmetricSubalgebra (Fin m) R))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (X i) :
        ↥(symmetricSubalgebra (Fin m) R))
have mul_X : Eq (α := ↥(symmetricSubalgebra (Fin m) R))
  ((esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R)) (X ⟨(↑i : ℕ), sorry⟩) :
    ↥(symmetricSubalgebra (Fin m) R))
  ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (X i) :
    ↥(symmetricSubalgebra (Fin m) R))
Tactic: refine ⟨X ⟨i, i.2.trans_le h⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
q : MvPolynomial (Fin m) R
⊢ Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) q :
      ↥(symmetricSubalgebra (Fin m) R))
have C : ∀ (r : R),
  Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R))
        ((C : (a : R) → MvPolynomial (Fin m) R) r) :
      ↥(symmetricSubalgebra (Fin m) R))
Tactic: induction q using MvPolynomial.induction_on with
  | C r => rw [← algebraMap_eq, AlgHom.commutes]; apply Subalgebra.algebraMap_mem
  | add p q hp hq => rw [map_add]; exact Subalgebra.add_mem _ hp hq
  | mul_X p i hp =>
    rw [map_mul]
    apply Subalgebra.mul_mem _ hp
    rw [AlgHom.mem_range]
    refine ⟨X ⟨i, i.2.trans_le h⟩, ?_⟩
    simp_rw [esymmAlgHom, aeval_X]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
q : MvPolynomial (Fin m) R
C :
  ∀ (r : R),
    Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
      (AlgHom.range (esymmAlgHom (Fin m) R n))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R))
          ((MvPolynomial.C : (a : R) → MvPolynomial (Fin m) R) r) :
        ↥(symmetricSubalgebra (Fin m) R))
⊢ Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) q :
      ↥(symmetricSubalgebra (Fin m) R))
have add : ∀ (p q : MvPolynomial (Fin m) R)
  (hp :
    Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
      (AlgHom.range (esymmAlgHom (Fin m) R n))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
        ↥(symmetricSubalgebra (Fin m) R)))
  (hq :
    Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
      (AlgHom.range (esymmAlgHom (Fin m) R n))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) q :
        ↥(symmetricSubalgebra (Fin m) R))),
  Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (p + q) :
      ↥(symmetricSubalgebra (Fin m) R))
Tactic: induction q using MvPolynomial.induction_on with
  | C r => rw [← algebraMap_eq, AlgHom.commutes]; apply Subalgebra.algebraMap_mem
  | add p q hp hq => rw [map_add]; exact Subalgebra.add_mem _ hp hq
  | mul_X p i hp =>
    rw [map_mul]
    apply Subalgebra.mul_mem _ hp
    rw [AlgHom.mem_range]
    refine ⟨X ⟨i, i.2.trans_le h⟩, ?_⟩
    simp_rw [esymmAlgHom, aeval_X]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
q : MvPolynomial (Fin m) R
C :
  ∀ (r : R),
    Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
      (AlgHom.range (esymmAlgHom (Fin m) R n))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R))
          ((MvPolynomial.C : (a : R) → MvPolynomial (Fin m) R) r) :
        ↥(symmetricSubalgebra (Fin m) R))
add :
  ∀ (p q : MvPolynomial (Fin m) R)
    (hp :
      Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
        (AlgHom.range (esymmAlgHom (Fin m) R n))
        ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
          ↥(symmetricSubalgebra (Fin m) R)))
    (hq :
      Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
        (AlgHom.range (esymmAlgHom (Fin m) R n))
        ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) q :
          ↥(symmetricSubalgebra (Fin m) R))),
    Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
      (AlgHom.range (esymmAlgHom (Fin m) R n))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (p + q) :
        ↥(symmetricSubalgebra (Fin m) R))
⊢ Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) q :
      ↥(symmetricSubalgebra (Fin m) R))
have mul_X : ∀ (p : MvPolynomial (Fin m) R) (i : Fin m)
  (hp :
    Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
      (AlgHom.range (esymmAlgHom (Fin m) R n))
      ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) p :
        ↥(symmetricSubalgebra (Fin m) R))),
  Membership.mem (α := ↥(symmetricSubalgebra (Fin m) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin m) R))
    (AlgHom.range (esymmAlgHom (Fin m) R n))
    ((esymmAlgHom (Fin m) R m : (a : MvPolynomial (Fin m) R) → ↥(symmetricSubalgebra (Fin m) R)) (p * X i) :
      ↥(symmetricSubalgebra (Fin m) R))
Tactic: induction q using MvPolynomial.induction_on with
  | C r => rw [← algebraMap_eq, AlgHom.commutes]; apply Subalgebra.algebraMap_mem
  | add p q hp hq => rw [map_add]; exact Subalgebra.add_mem _ hp hq
  | mul_X p i hp =>
    rw [map_mul]
    apply Subalgebra.mul_mem _ hp
    rw [AlgHom.mem_range]
    refine ⟨X ⟨i, i.2.trans_le h⟩, ?_⟩
    simp_rw [esymmAlgHom, aeval_X]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : Fintype σ
inst_1 : CommRing R
hn : Fintype.card σ ≤ n
⊢ Function.Surjective (α := MvPolynomial (Fin n) R) (β := ↥(symmetricSubalgebra σ R))
    (⇑(esymmAlgHom σ R n) : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
have rw : Function.Surjective (α := MvPolynomial (Fin n) R) (β := ↥(symmetricSubalgebra σ R))
  (Function.comp (β := ↥(symmetricSubalgebra (Fin (Fintype.card σ)) R))
    (⇑(↑(renameSymmetricSubalgebra (Equiv.symm (Fintype.equivFin σ))) :
          ↥(symmetricSubalgebra (Fin (Fintype.card σ)) R) →ₐ[R] ↥(symmetricSubalgebra σ R)) :
      (a : ↥(symmetricSubalgebra (Fin (Fintype.card σ)) R)) → ↥(symmetricSubalgebra σ R))
    (⇑(esymmAlgHom (Fin (Fintype.card σ)) R n) :
      (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin (Fintype.card σ)) R)))
Tactic: rw [← rename_esymmAlgHom (Fintype.equivFin σ).symm, AlgHom.coe_comp]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem (goal)
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : Fintype σ
inst_1 : CommRing R
hn : Fintype.card σ = n
i : Fin n
⊢ Eq.{u_3 + 1} (α := MvPolynomial (Fin n) R)
    ((AlgEquiv.symm (esymmAlgEquiv σ R hn) : (a : ↥(symmetricSubalgebra σ R)) → MvPolynomial (Fin n) R)
        (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x) (esymm σ R ((↑i : ℕ) + 1))
          ⋯) :
      MvPolynomial (Fin n) R)
    (X i : MvPolynomial (Fin n) R)
have apply_fun : Eq (α := ↥(symmetricSubalgebra σ R))
  ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
      ((AlgEquiv.symm (esymmAlgEquiv σ R hn) : (a : ↥(symmetricSubalgebra σ R)) → MvPolynomial (Fin n) R)
        (Subtype.mk (p := fun (x : MvPolynomial σ R) ↦
          Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (symmetricSubalgebra σ R) x) (esymm σ R ((↑i : ℕ) + 1))
          sorry)) :
    ↥(symmetricSubalgebra σ R))
  ((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R)) (X i) : ↥(symmetricSubalgebra σ R))
Tactic: apply_fun esymmAlgHom σ R n using esymmAlgHom_injective R hn.ge