-- Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
lemma esymmAlgHom_fin_bijective (n : ℕ) :
    Function.Bijective (esymmAlgHom (Fin n) R n)

Proof state:
case right.mk.inr.ind.inr.refine_2
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
t : Fin n →₀ ℕ := Finsupp.equivFunOnFinite.symm (invAccumulate n n ⇑(ofLex (supDegree (⇑toLex) p)))
hd : supDegree (⇑toLex) (esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) = supDegree (⇑toLex) p
hne : p ≠ esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)
this : supDegree (⇑toLex) (p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) < supDegree (⇑toLex) p
ih : ⟨p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p), ⋯⟩ ∈ (esymmAlgHom (Fin n) R n).range
⊢ ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range

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

Result:
case h.e'_5.h.e'_3
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
t : Fin n →₀ ℕ := Finsupp.equivFunOnFinite.symm (invAccumulate n n ⇑(ofLex (supDegree (⇑toLex) p)))
hd : supDegree (⇑toLex) (esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) = supDegree (⇑toLex) p
hne : p ≠ esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)
this : supDegree (⇑toLex) (p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) < supDegree (⇑toLex) p
ih : ⟨p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p), ⋯⟩ ∈ (esymmAlgHom (Fin n) R n).range
⊢ ↑(⟨p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p), ⋯⟩ +
        (esymmAlgHom (Fin n) R n).toRingHom ((monomial t) (leadingCoeff (⇑toLex) p))) =
    p

Proof state:
case right.mk.inr.ind.inl
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex) p,
    ∀ (p : MvPolynomial (Fin n) R) (hp : p ∈ symmetricSubalgebra (Fin n) R),
      p ≠ 0 → supDegree (⇑toLex) p = y → ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
t : Fin n →₀ ℕ := Finsupp.equivFunOnFinite.symm (invAccumulate n n ⇑(ofLex (supDegree (⇑toLex) p)))
hd : supDegree (⇑toLex) (esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) = supDegree (⇑toLex) p
he : p = esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)
⊢ ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range

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

Result:
no goals

Proof state:
case right
R : Type u_3
inst✝ : CommRing R
n : ℕ
⊢ Function.Surjective ⇑(esymmAlgHom (Fin n) R n)

Tactic:
rintro ⟨p, hp⟩

Result:
case right.mk
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
⊢ ∃ a, (esymmAlgHom (Fin n) R n) a = ⟨p, hp⟩

Proof state:
case right.mk.inr.ind.inr.refine_2
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex) p,
    ∀ (p : MvPolynomial (Fin n) R) (hp : p ∈ symmetricSubalgebra (Fin n) R),
      p ≠ 0 → supDegree (⇑toLex) p = y → ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
t : Fin n →₀ ℕ := Finsupp.equivFunOnFinite.symm (invAccumulate n n ⇑(ofLex (supDegree (⇑toLex) p)))
hd : supDegree (⇑toLex) (esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) = supDegree (⇑toLex) p
hne : p ≠ esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)
this : supDegree (⇑toLex) (p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) < supDegree (⇑toLex) p
⊢ ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range

Tactic:
specialize ih _ this _ (Subalgebra.sub_mem _ hp <| isSymmetric_esymmAlgHomMonomial _ _) _ rfl

Result:
case right.mk.inr.ind.inr.refine_2
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
ih :
  ∀ y < supDegree (⇑toLex) p,
    ∀ (p : MvPolynomial (Fin n) R) (hp : p ∈ symmetricSubalgebra (Fin n) R),
      p ≠ 0 → supDegree (⇑toLex) p = y → ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range
t : Fin n →₀ ℕ := Finsupp.equivFunOnFinite.symm (invAccumulate n n ⇑(ofLex (supDegree (⇑toLex) p)))
hd : supDegree (⇑toLex) (esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) = supDegree (⇑toLex) p
hne : p ≠ esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)
this : supDegree (⇑toLex) (p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) < supDegree (⇑toLex) p
⊢ p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p) ≠ 0

case right.mk.inr.ind.inr.refine_2
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
t : Fin n →₀ ℕ := Finsupp.equivFunOnFinite.symm (invAccumulate n n ⇑(ofLex (supDegree (⇑toLex) p)))
hd : supDegree (⇑toLex) (esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) = supDegree (⇑toLex) p
hne : p ≠ esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)
this : supDegree (⇑toLex) (p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) < supDegree (⇑toLex) p
ih : ⟨p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p), ⋯⟩ ∈ (esymmAlgHom (Fin n) R n).range
⊢ ⟨p, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range

Proof state:
case right.mk.inl
R : Type u_3
inst✝ : CommRing R
n : ℕ
hp : 0 ∈ symmetricSubalgebra (Fin n) R
⊢ ⟨0, hp⟩ ∈ (esymmAlgHom (Fin n) R n).range

Tactic:
exact Subalgebra.zero_mem _

Result:
no goals

Proof state:
case h.e'_5.h.e'_3
R : Type u_3
inst✝ : CommRing R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ∈ symmetricSubalgebra (Fin n) R
h0 : p ≠ 0
t : Fin n →₀ ℕ := Finsupp.equivFunOnFinite.symm (invAccumulate n n ⇑(ofLex (supDegree (⇑toLex) p)))
hd : supDegree (⇑toLex) (esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) = supDegree (⇑toLex) p
hne : p ≠ esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)
this : supDegree (⇑toLex) (p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p)) < supDegree (⇑toLex) p
ih : ⟨p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p), ⋯⟩ ∈ (esymmAlgHom (Fin n) R n).range
⊢ ↑(⟨p - esymmAlgHomMonomial (Fin n) t (leadingCoeff (⇑toLex) p), ⋯⟩ +
        (esymmAlgHom (Fin n) R n).toRingHom ((monomial t) (leadingCoeff (⇑toLex) p))) =
    p

Tactic:
apply sub_add_cancel p

Result:
no goals

Proof state:
R : Type u_3
inst✝ : CommRing R
n : ℕ
⊢ Function.Bijective ⇑(esymmAlgHom (Fin n) R n)

Tactic:
use esymmAlgHom_fin_injective R le_rfl

Result:
case right
R : Type u_3
inst✝ : CommRing R
n : ℕ
⊢ Function.Surjective ⇑(esymmAlgHom (Fin n) R n)