-- Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
lemma esymmAlgHom_fin_surjective (h : m ≤ n) :
    Function.Surjective (esymmAlgHom (Fin m) R n)

Proof state:
case intro.h_X
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R n) (X ⟨↑i, ⋯⟩) = (esymmAlgHom (Fin m) R m) (X i)

Tactic:
simp_rw [esymmAlgHom, aeval_X]

Result:
no goals

Proof state:
case intro.h_add
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p q : MvPolynomial (Fin m) R
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
hq : (esymmAlgHom (Fin m) R m) q ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R m) p + (esymmAlgHom (Fin m) R m) q ∈ (esymmAlgHom (Fin m) R n).range

Tactic:
exact Subalgebra.add_mem _ hp hq

Result:
no goals

Proof state:
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : ↥(symmetricSubalgebra (Fin m) R)
⊢ ∃ a, (esymmAlgHom (Fin m) R n) a = p

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

Result:
case intro
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
q : MvPolynomial (Fin m) R
⊢ ∃ a, (esymmAlgHom (Fin m) R n) a = (esymmAlgHom (Fin m) R m) q

Proof state:
case intro
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
q : MvPolynomial (Fin m) R
⊢ ∃ a, (esymmAlgHom (Fin m) R n) a = (esymmAlgHom (Fin m) R m) q

Tactic:
rw [← AlgHom.mem_range]

Result:
case intro
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
q : MvPolynomial (Fin m) R
⊢ (esymmAlgHom (Fin m) R m) q ∈ (esymmAlgHom (Fin m) R n).range

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

Tactic:
intro p

Result:
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : ↥(symmetricSubalgebra (Fin m) R)
⊢ ∃ a, (esymmAlgHom (Fin m) R n) a = p

Proof state:
case intro
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
q : MvPolynomial (Fin m) R
⊢ (esymmAlgHom (Fin m) R m) q ∈ (esymmAlgHom (Fin m) R n).range

Tactic:
induction q using MvPolynomial.induction_on with
| h_C r => rw [← algebraMap_eq, AlgHom.commutes]; apply Subalgebra.algebraMap_mem
| h_add p q hp hq => rw [map_add]; exact Subalgebra.add_mem _ hp hq
| h_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]

Result:
no goals

Proof state:
case intro.h_C
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
r : R
⊢ (algebraMap R ↥(symmetricSubalgebra (Fin m) R)) r ∈ (esymmAlgHom (Fin m) R n).range

Tactic:
apply Subalgebra.algebraMap_mem

Result:
no goals

Proof state:
case intro.h_X
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R m) (X i) ∈ (esymmAlgHom (Fin m) R n).range

Tactic:
rw [AlgHom.mem_range]

Result:
case intro.h_X
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
⊢ ∃ x, (esymmAlgHom (Fin m) R n) x = (esymmAlgHom (Fin m) R m) (X i)

Proof state:
case intro.h_X
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
⊢ ∃ x, (esymmAlgHom (Fin m) R n) x = (esymmAlgHom (Fin m) R m) (X i)

Tactic:
refine ⟨X ⟨i, i.2.trans_le h⟩, ?_⟩

Result:
case intro.h_X
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R n) (X ⟨↑i, ⋯⟩) = (esymmAlgHom (Fin m) R m) (X i)

Proof state:
case intro.h_C
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
r : R
⊢ (esymmAlgHom (Fin m) R m) (C r) ∈ (esymmAlgHom (Fin m) R n).range

Tactic:
rw [← algebraMap_eq, AlgHom.commutes]

Result:
case intro.h_C
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
r : R
⊢ (algebraMap R ↥(symmetricSubalgebra (Fin m) R)) r ∈ (esymmAlgHom (Fin m) R n).range

Proof state:
case intro.h_X
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R m) (p * X i) ∈ (esymmAlgHom (Fin m) R n).range

Tactic:
rw [map_mul]

Result:
case intro.h_X
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R m) p * (esymmAlgHom (Fin m) R m) (X i) ∈ (esymmAlgHom (Fin m) R n).range

Proof state:
case intro.h_X
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R m) p * (esymmAlgHom (Fin m) R m) (X i) ∈ (esymmAlgHom (Fin m) R n).range

Tactic:
apply Subalgebra.mul_mem _ hp

Result:
case intro.h_X
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p : MvPolynomial (Fin m) R
i : Fin m
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R m) (X i) ∈ (esymmAlgHom (Fin m) R n).range

Proof state:
case intro.h_add
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p q : MvPolynomial (Fin m) R
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
hq : (esymmAlgHom (Fin m) R m) q ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R m) (p + q) ∈ (esymmAlgHom (Fin m) R n).range

Tactic:
rw [map_add]

Result:
case intro.h_add
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : m ≤ n
p q : MvPolynomial (Fin m) R
hp : (esymmAlgHom (Fin m) R m) p ∈ (esymmAlgHom (Fin m) R n).range
hq : (esymmAlgHom (Fin m) R m) q ∈ (esymmAlgHom (Fin m) R n).range
⊢ (esymmAlgHom (Fin m) R m) p + (esymmAlgHom (Fin m) R m) q ∈ (esymmAlgHom (Fin m) R n).range