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

Proof state:
case refine_2
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : coeff t p ≠ 0
s : Fin n →₀ ℕ
hs : coeff s p ≠ 0
he :
  supDegree ⇑toLex ↑((esymmAlgHom (Fin m) R n) ((monomial t) (coeff t p))) =
    supDegree ⇑toLex ↑((esymmAlgHom (Fin m) R n) ((monomial s) (coeff s p)))
⊢ (accumulate n m) ⇑t = (accumulate n m) ⇑s

Tactic:
rwa [← esymmAlgHomMonomial, ← esymmAlgHomMonomial, ← ofLex_inj, DFunLike.ext'_iff,
     supDegree_esymmAlgHomMonomial ht t h, supDegree_esymmAlgHomMonomial hs s h] at he

Result:
no goals

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

Tactic:
rw [injective_iff_map_eq_zero]

Result:
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
⊢ ∀ (a : MvPolynomial (Fin n) R), (esymmAlgHom (Fin m) R n) a = 0 → a = 0

Proof state:
case refine_1
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : t ∈ p.support
⊢ ↑((esymmAlgHom (Fin m) R n) ((monomial t) (coeff t p))) ≠ 0

Tactic:
rw [← esymmAlgHomMonomial, Ne, ← leadingCoeff_eq_zero toLex.injective,
  leadingCoeff_esymmAlgHomMonomial t h]

Result:
case refine_1
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : t ∈ p.support
⊢ ¬coeff t p = 0

Proof state:
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
⊢ ∀ (a : MvPolynomial (Fin n) R), (esymmAlgHom (Fin m) R n) a = 0 → a = 0

Tactic:
refine fun p ↦ (fun hp ↦ ?_).mtr

Result:
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
⊢ ¬(esymmAlgHom (Fin m) R n) p = 0

Proof state:
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
⊢ ¬∑ i ∈ p.support, ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p))) = 0

Tactic:
refine sum_ne_zero_of_injOn_supDegree (D := toLex) (support_eq_empty.not.2 hp) (fun t ht ↦ ?_)
  (fun t ht s hs he ↦ DFunLike.ext' <| accumulate_injective h ?_)

Result:
case refine_1
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : t ∈ p.support
⊢ ↑((esymmAlgHom (Fin m) R n) ((monomial t) (coeff t p))) ≠ 0

case refine_2
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : t ∈ ↑p.support
s : Fin n →₀ ℕ
hs : s ∈ ↑p.support
he :
  (supDegree ⇑toLex ∘ fun i => ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p)))) t =
    (supDegree ⇑toLex ∘ fun i => ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p)))) s
⊢ (accumulate n m) ⇑t = (accumulate n m) ⇑s

Proof state:
case refine_2
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : t ∈ ↑p.support
s : Fin n →₀ ℕ
hs : s ∈ ↑p.support
he :
  (supDegree ⇑toLex ∘ fun i => ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p)))) t =
    (supDegree ⇑toLex ∘ fun i => ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p)))) s
⊢ (accumulate n m) ⇑t = (accumulate n m) ⇑s

Tactic:
rw [mem_coe, mem_support_iff] at ht hs

Result:
case refine_2
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : coeff t p ≠ 0
s : Fin n →₀ ℕ
hs : coeff s p ≠ 0
he :
  (supDegree ⇑toLex ∘ fun i => ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p)))) t =
    (supDegree ⇑toLex ∘ fun i => ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p)))) s
⊢ (accumulate n m) ⇑t = (accumulate n m) ⇑s

Proof state:
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
⊢ ¬(esymmAlgHom (Fin m) R n) p = 0

Tactic:
rw [p.as_sum, map_sum (esymmAlgHom (Fin m) R n), ← Subalgebra.coe_eq_zero,
  AddSubmonoidClass.coe_finset_sum]

Result:
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
⊢ ¬∑ i ∈ p.support, ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p))) = 0

Proof state:
case refine_1
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : t ∈ p.support
⊢ ¬coeff t p = 0

Tactic:
rwa [mem_support_iff] at ht

Result:
no goals

Proof state:
case refine_2
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : coeff t p ≠ 0
s : Fin n →₀ ℕ
hs : coeff s p ≠ 0
he :
  (supDegree ⇑toLex ∘ fun i => ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p)))) t =
    (supDegree ⇑toLex ∘ fun i => ↑((esymmAlgHom (Fin m) R n) ((monomial i) (coeff i p)))) s
⊢ (accumulate n m) ⇑t = (accumulate n m) ⇑s

Tactic:
dsimp only [Function.comp] at he

Result:
case refine_2
R : Type u_3
n m : ℕ
inst✝ : CommRing R
h : n ≤ m
p : MvPolynomial (Fin n) R
hp : ¬p = 0
t : Fin n →₀ ℕ
ht : coeff t p ≠ 0
s : Fin n →₀ ℕ
hs : coeff s p ≠ 0
he :
  supDegree ⇑toLex ↑((esymmAlgHom (Fin m) R n) ((monomial t) (coeff t p))) =
    supDegree ⇑toLex ↑((esymmAlgHom (Fin m) R n) ((monomial s) (coeff s p)))
⊢ (accumulate n m) ⇑t = (accumulate n m) ⇑s