-- Mathlib/RingTheory/NoetherNormalization.lean
private lemma leadingCoeff_finSuccEquiv_t  :
    (finSuccEquiv k n ((T f) ((monomial v) (coeff v f)))).leadingCoeff =
    algebraMap k _ (coeff v f)

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
this : ∀ (j : Fin (n + 1)), ((MvPolynomial.finSuccEquiv k n) ((T1 f 1) (MvPolynomial.X j))).leadingCoeff = 1
⊢ MvPolynomial.C (MvPolynomial.coeff v f) *
      ∏ x : Fin (n + 1), ((MvPolynomial.finSuccEquiv k n) ((T1 f 1) (MvPolynomial.X x))).leadingCoeff ^ v x =
    MvPolynomial.C (MvPolynomial.coeff v f)

Tactic:
simp only [this, one_pow, Finset.prod_const_one, mul_one]

Result:
no goals

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((⇑Polynomial.C ∘ ⇑MvPolynomial.C) (MvPolynomial.coeff v f)).leadingCoeff *
      ∏ i : Fin (n + 1),
        ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (MvPolynomial.X i ^ v i))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)

Tactic:
simp only [AlgEquiv.ofAlgHom_apply, Function.comp_apply, leadingCoeff_C, map_pow,
  leadingCoeff_pow, algebraMap_eq]

Result:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ MvPolynomial.C (MvPolynomial.coeff v f) *
      ∏ x : Fin (n + 1), ((MvPolynomial.finSuccEquiv k n) ((T1 f 1) (MvPolynomial.X x))).leadingCoeff ^ v x =
    MvPolynomial.C (MvPolynomial.coeff v f)

Proof state:
case neg
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
j : Fin (n + 1)
h : ¬j = 0
⊢ ((MvPolynomial.finSuccEquiv k n) (MvPolynomial.X j) +
        (MvPolynomial.finSuccEquiv k n) (MvPolynomial.X 0) ^ up ^ ↑j).leadingCoeff =
    1

Tactic:
obtain ⟨i, rfl⟩ := Fin.exists_succ_eq.mpr h

Result:
case neg.intro
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
i : Fin n
h : ¬i.succ = 0
⊢ ((MvPolynomial.finSuccEquiv k n) (MvPolynomial.X i.succ) +
        (MvPolynomial.finSuccEquiv k n) (MvPolynomial.X 0) ^ up ^ ↑i.succ).leadingCoeff =
    1

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((MvPolynomial.finSuccEquiv k n)
        ((NoetherNormalization.T f) ((MvPolynomial.monomial v) (MvPolynomial.coeff v f)))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)

Tactic:
rw [monomial_eq, Finsupp.prod_fintype]

Result:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((MvPolynomial.finSuccEquiv k n)
        ((NoetherNormalization.T f)
          (MvPolynomial.C (MvPolynomial.coeff v f) * ∏ i : Fin (n + 1), MvPolynomial.X i ^ v i))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)

case h
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ∀ (i : Fin (n + 1)), MvPolynomial.X i ^ 0 = 1

Proof state:
case pos
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
j : Fin (n + 1)
h : j = 0
⊢ ((MvPolynomial.finSuccEquiv k n) ((T1 f 1) (MvPolynomial.X j))).leadingCoeff = 1

Tactic:
simp [h, finSuccEquiv_apply]

Result:
no goals

Proof state:
case neg.intro
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
i : Fin n
h : ¬i.succ = 0
⊢ ((MvPolynomial.finSuccEquiv k n) (MvPolynomial.X i.succ) +
        (MvPolynomial.finSuccEquiv k n) (MvPolynomial.X 0) ^ up ^ ↑i.succ).leadingCoeff =
    1

Tactic:
simp [finSuccEquiv_X_succ, finSuccEquiv_X_zero, add_comm]

Result:
no goals

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((MvPolynomial.finSuccEquiv k n)
        ((NoetherNormalization.T f)
          (MvPolynomial.C (MvPolynomial.coeff v f) * ∏ i : Fin (n + 1), MvPolynomial.X i ^ v i))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)

Tactic:
simp only [_root_.map_mul, map_prod, leadingCoeff_mul, leadingCoeff_prod]

Result:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((MvPolynomial.finSuccEquiv k n)
          ((NoetherNormalization.T f) (MvPolynomial.C (MvPolynomial.coeff v f)))).leadingCoeff *
      ∏ i : Fin (n + 1),
        ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (MvPolynomial.X i ^ v i))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)

Proof state:
case neg
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
j : Fin (n + 1)
h : ¬j = 0
⊢ ((MvPolynomial.finSuccEquiv k n) ((T1 f 1) (MvPolynomial.X j))).leadingCoeff = 1

Tactic:
simp only [aeval_eq_bind₁, bind₁_X_right, if_neg h, one_smul, map_add, map_pow]

Result:
case neg
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
j : Fin (n + 1)
h : ¬j = 0
⊢ ((MvPolynomial.finSuccEquiv k n) (MvPolynomial.X j) +
        (MvPolynomial.finSuccEquiv k n) (MvPolynomial.X 0) ^ up ^ ↑j).leadingCoeff =
    1

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
j : Fin (n + 1)
⊢ ((MvPolynomial.finSuccEquiv k n) ((T1 f 1) (MvPolynomial.X j))).leadingCoeff = 1

Tactic:
by_cases h : j = 0

Result:
case pos
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
j : Fin (n + 1)
h : j = 0
⊢ ((MvPolynomial.finSuccEquiv k n) ((T1 f 1) (MvPolynomial.X j))).leadingCoeff = 1

case neg
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
j : Fin (n + 1)
h : ¬j = 0
⊢ ((MvPolynomial.finSuccEquiv k n) ((T1 f 1) (MvPolynomial.X j))).leadingCoeff = 1

Proof state:
case h
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ∀ (i : Fin (n + 1)), MvPolynomial.X i ^ 0 = 1

Tactic:
exact fun i ↦ pow_zero _

Result:
no goals

Proof state:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((MvPolynomial.finSuccEquiv k n)
          ((NoetherNormalization.T f) (MvPolynomial.C (MvPolynomial.coeff v f)))).leadingCoeff *
      ∏ i : Fin (n + 1),
        ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (MvPolynomial.X i ^ v i))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)

Tactic:
rw [AlgEquiv.ofAlgHom_apply, algHom_C, algebraMap_eq, finSuccEquiv_apply,
  eval₂Hom_C, coe_comp]

Result:
k : Type u_1
inst✝ : Field k
n : ℕ
f : MvPolynomial (Fin (n + 1)) k
v : Fin (n + 1) →₀ ℕ
⊢ ((⇑Polynomial.C ∘ ⇑MvPolynomial.C) (MvPolynomial.coeff v f)).leadingCoeff *
      ∏ i : Fin (n + 1),
        ((MvPolynomial.finSuccEquiv k n) ((NoetherNormalization.T f) (MvPolynomial.X i ^ v i))).leadingCoeff =
    (algebraMap k (MvPolynomial (Fin n) k)) (MvPolynomial.coeff v f)