awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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)
he :
  p =
    esymmAlgHomMonomial (Fin n) t
      (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)
⊢ Membership.mem (α := ↥(symmetricSubalgebra (Fin n) R)) (γ := Subalgebra R ↥(symmetricSubalgebra (Fin n) R))
    (AlgHom.range (esymmAlgHom (Fin n) R n))
    ((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))

Tactic:
AlgHom.mem_range_self _ (monomial t <| p.leadingCoeff toLex)

Premises used: AlgHom.mem_range_self, MvPolynomial.monomial, AddMonoidAlgebra.leadingCoeff, DFunLike.coe, toLex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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)
he :
  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)

Tactic:
convert! AlgHom.mem_range_self _ (monomial t <| p.leadingCoeff toLex)

Premises used: AlgHom.mem_range_self, MvPolynomial.monomial, AddMonoidAlgebra.leadingCoeff, DFunLike.coe, toLex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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)
right :
  ∀
    (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)),
    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)
right₁ :
  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)
⊢ 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:
have := (supDegree_sub_lt_of_leadingCoeff_eq toLex.injective hd.symm ?_).resolve_right hne
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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 right₁ right₂ right₃ :
  p ≠
    esymmAlgHomMonomial (Fin n) t
      (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p)
⊢ p -
      esymmAlgHomMonomial (Fin n) t
        (leadingCoeff (B := Lex (Fin n →₀ ℕ)) (⇑toLex : (a : Fin n →₀ ℕ) → Lex (Fin n →₀ ℕ)) p) ≠
    0

Tactic:
rwa [sub_ne_zero]

Premises used: sub_ne_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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))
    (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))
        ⋯)
      ((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)))

Tactic:
Subalgebra.add_mem _ ih ⟨monomial t (p.leadingCoeff toLex), rfl⟩

Premises used: Subalgebra.add_mem, MvPolynomial.monomial, Exists.intro, AddMonoidAlgebra.leadingCoeff, DFunLike.coe, rfl, toLex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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))
      ⋯)
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))
            ⋯)
          ((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
⊢ 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:
convert! ← Subalgebra.add_mem _ ih ⟨monomial t (p.leadingCoeff toLex), rfl⟩

Premises used: Subalgebra.add_mem, MvPolynomial.monomial, Exists.intro, AddMonoidAlgebra.leadingCoeff, DFunLike.coe, rfl, toLex
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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))
      ⋯)
⊢ (↑(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))
            ⋯)
          ((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:
apply sub_add_cancel p

Premises used: sub_add_cancel
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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)
right 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
⊢ 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)

Tactic:
rw [leadingCoeff_esymmAlgHomMonomial t le_rfl]

Premises used: le_rfl, MvPolynomial.leadingCoeff_esymmAlgHomMonomial
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
p : ↥(symmetricSubalgebra (Fin m) R)
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))
⊢ ∃ (a : MvPolynomial (Fin n) R),
    (esymmAlgHom (Fin m) R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra (Fin m) R)) a = p

Tactic:
obtain ⟨q, rfl⟩ := (esymmAlgHom_fin_bijective R m).2 p

Premises used: And.right, MvPolynomial.esymmAlgHom_fin_bijective, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
R : Type u_3
n m : ℕ
inst : CommRing R
h : m ≤ n
r : R
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))
⊢ 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))

Tactic:
rw [← algebraMap_eq, AlgHom.commutes]

Premises used: MvPolynomial.algebraMap_eq, AlgHom.commutes
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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))
    ((algebraMap R ↥(symmetricSubalgebra (Fin m) R) : (a : R) → ↥(symmetricSubalgebra (Fin m) R)) r :
      ↥(symmetricSubalgebra (Fin m) R))

Tactic:
apply Subalgebra.algebraMap_mem

Premises used: Subalgebra.algebraMap_mem
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
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))
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)))
⊢ 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:
rw [map_add]

Premises used: map_add