awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
⊢ RingHom.comp (↑(AlgEquiv.symm (finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →+* MvPolynomial (Fin n.succ) R)
      (RingHom.comp Polynomial.C C) =
    C
have refine : ∀ (x : R),
  Eq (α := MvPolynomial (Fin n.succ) R)
    ((RingHom.comp (↑(AlgEquiv.symm (finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →+* MvPolynomial (Fin n.succ) R)
            (RingHom.comp Polynomial.C C) :
          (a : R) → MvPolynomial (Fin n.succ) R)
        x :
      MvPolynomial (Fin n.succ) R)
    ((C : (a : R) → MvPolynomial (Fin n.succ) R) x : MvPolynomial (Fin n.succ) R)
Tactic: refine RingHom.ext fun x => ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
x : R
⊢ Eq (α := MvPolynomial (Fin n.succ) R)
    (((↑(AlgEquiv.symm (finSuccEquiv R n)) : (MvPolynomial (Fin n) R)[X] →+* MvPolynomial (Fin n.succ) R) :
          (a : (MvPolynomial (Fin n) R)[X]) → MvPolynomial (Fin n.succ) R)
        ((RingHom.comp Polynomial.C C : (a : R) → (MvPolynomial (Fin n) R)[X]) x) :
      MvPolynomial (Fin n.succ) R)
    ((C : (a : R) → MvPolynomial (Fin n.succ) R) x : MvPolynomial (Fin n.succ) R)
have R₁ : Eq (α := (MvPolynomial (Fin n) R)[X])
  ((RingHom.comp Polynomial.C C : (a : R) → (MvPolynomial (Fin n) R)[X]) x : (MvPolynomial (Fin n) R)[X])
  ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
      ((C : (a : R) → MvPolynomial (Fin n.succ) R) x) :
    (MvPolynomial (Fin n) R)[X])
Tactic: refine
    (MvPolynomial.finSuccEquiv R n).injective
      (Trans.trans ((MvPolynomial.finSuccEquiv R n).apply_symm_apply _) ?_)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ Eq.{u + 1} (α := R)
    (coeff m
      (Polynomial.coeff
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
          ((monomial j : (a : R) → MvPolynomial (Fin (n + 1)) R) r))
        i))
    (coeff (cons i m) ((monomial j : (a : R) → MvPolynomial (Fin (n + 1)) R) r))
have monomial : r *
    coeff m
      ((HPow.hPow (α := (MvPolynomial (Fin n) R)[X]) (β := ℕ) Polynomial.X ((j : (a : Fin (n + 1)) → ℕ) 0 : ℕ) *
            (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X])
              (∏ x : Fin n,
                HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ))).coeff
        i) =
  if j = cons i m then r else 0
Tactic: simp only [finSuccEquiv_apply, coe_eval₂Hom, eval₂_monomial, RingHom.coe_comp, Finsupp.prod_pow,
      Polynomial.coeff_C_mul, coeff_C_mul, coeff_monomial, Fin.prod_univ_succ, Fin.cases_zero,
      Fin.cases_succ, ← _root_.map_prod, ← map_pow, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r *
      coeff m
        ((HPow.hPow (α := (MvPolynomial (Fin n) R)[X]) (β := ℕ) Polynomial.X ((j : (a : Fin (n + 1)) → ℕ) 0 : ℕ) *
              (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X])
                (∏ x : Fin n,
                  HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x)
                    ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ))).coeff
          i) =
    if j = cons i m then r else 0
have monomial : r *
    coeff m
      (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
        ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0) =
  r * if j = cons i m then 1 else 0
Tactic: rw [← mul_boole, mul_comm (Polynomial.X ^ j 0), Polynomial.coeff_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ r *
      coeff m
        (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
          ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
        else 0) =
    r * if j = cons i m then 1 else 0
have monomial : Eq.{u + 1} (α := R)
  (coeff m
    (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
      ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
    else 0))
  (if j = cons i m then 1 else 0)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
⊢ Eq.{u + 1} (α := R)
    (coeff m
      (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
        ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    (if j = cons i m then 1 else 0)
have monomial : Eq.{u + 1} (α := R)
  (coeff m
    (if i = (cons i m : (a : Fin (n + 1)) → ℕ) 0 then
      ∏ x : Fin n,
        HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((cons i m : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
    else 0))
  (if cons i m = cons i m then 1 else 0)
Tactic: obtain rfl | hjmi := eq_or_ne j (m.cons i)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
monomial :
  Eq.{u + 1} (α := R)
    (coeff m
      (if i = (cons i m : (a : Fin (n + 1)) → ℕ) 0 then
        ∏ x : Fin n,
          HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((cons i m : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    (if cons i m = cons i m then 1 else 0)
⊢ Eq.{u + 1} (α := R)
    (coeff m
      (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
        ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    (if j = cons i m then 1 else 0)
have monomial₁ : ∀ (hjmi : j ≠ cons i m),
  Eq.{u + 1} (α := R)
    (coeff m
      (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
        ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    (if j = cons i m then 1 else 0)
Tactic: obtain rfl | hjmi := eq_or_ne j (m.cons i)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
⊢ Eq.{u + 1} (α := R)
    (coeff m
      (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
        ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    (if j = cons i m then 1 else 0)
have monomial : Eq.{u + 1} (α := R)
  (coeff m
    (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
      ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
    else 0))
  0
Tactic: simp only [hjmi, if_false]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
⊢ Eq.{u + 1} (α := R)
    (coeff m
      (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
        ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    0
have monomial : ∀ (hij : i ≠ (j : (a : Fin (n + 1)) → ℕ) 0),
  Eq.{u + 1} (α := R)
    (coeff m
      (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
        ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    0
Tactic: obtain hij | rfl := ne_or_eq i (j 0)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
i : ℕ
hjmi : j ≠ cons i m
monomial :
  ∀ (hij : i ≠ (j : (a : Fin (n + 1)) → ℕ) 0),
    Eq.{u + 1} (α := R)
      (coeff m
        (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
          ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
        else 0))
      0
⊢ Eq.{u + 1} (α := R)
    (coeff m
      (if i = (j : (a : Fin (n + 1)) → ℕ) 0 then
        ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    0
have monomial₁ : ∀ (hjmi : j ≠ cons ((j : (a : Fin (n + 1)) → ℕ) 0) m),
  Eq.{u + 1} (α := R)
    (coeff m
      (if Eq (α := ℕ) ((j : (a : Fin (n + 1)) → ℕ) 0 : ℕ) ((j : (a : Fin (n + 1)) → ℕ) 0 : ℕ) then
        ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    0
Tactic: obtain hij | rfl := ne_or_eq i (j 0)
Cleared hypotheses: i, hjmi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons ((j : (a : Fin (n + 1)) → ℕ) 0) m
⊢ Eq.{u + 1} (α := R)
    (coeff m
      (if Eq (α := ℕ) ((j : (a : Fin (n + 1)) → ℕ) 0 : ℕ) ((j : (a : Fin (n + 1)) → ℕ) 0 : ℕ) then
        ∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)
      else 0))
    0
have monomial : Eq.{u + 1} (α := R)
  (coeff m
    (∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)))
  0
Tactic: simp only [if_true]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ cons ((j : (a : Fin (n + 1)) → ℕ) 0) j.tail
⊢ False
have hjmi₁ : j ≠ j
Tactic: rw [cons_tail] at hjmi
Cleared hypotheses: hjmi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons ((j : (a : Fin (n + 1)) → ℕ) 0) m
⊢ Eq.{u + 1} (α := R)
    (coeff m
      (∏ x : Fin n, HPow.hPow (α := MvPolynomial (Fin n) R) (β := ℕ) (X x) ((j : (a : Fin (n + 1)) → ℕ) x.succ : ℕ)))
    0
have hmj : m ≠ j.tail
Tactic: have hmj : m ≠ j.tail := by
        rintro rfl
        rw [cons_tail] at hjmi
        contradiction
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
m : Fin n →₀ ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ coeff m
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) =
    coeff (cons i m) f
have add : ∀ (p q : MvPolynomial (Fin (n + 1)) R)
  (hp :
    ∀ (m : Fin n →₀ ℕ) (i : ℕ),
      coeff m
          (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) p)
            i) =
        coeff (cons i m) p)
  (hq :
    ∀ (m : Fin n →₀ ℕ) (i : ℕ),
      coeff m
          (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) q)
            i) =
        coeff (cons i m) q)
  (m : Fin n →₀ ℕ) (i : ℕ),
  coeff m
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) (p + q))
        i) =
    coeff (cons i m) (p + q)
Tactic: induction f using MvPolynomial.induction_on' generalizing i m with
  | add p q hp hq => simp only [map_add, Polynomial.coeff_add, coeff_add, hp, hq]
  | monomial j r =>
    simp only [finSuccEquiv_apply, coe_eval₂Hom, eval₂_monomial, RingHom.coe_comp, Finsupp.prod_pow,
      Polynomial.coeff_C_mul, coeff_C_mul, coeff_monomial, Fin.prod_univ_succ, Fin.cases_zero,
      Fin.cases_succ, ← _root_.map_prod, ← map_pow, Function.comp_apply]
    rw [← mul_boole, mul_comm (Polynomial.X ^ j 0), Polynomial.coeff_C_mul_X_pow]; congr 1
    obtain rfl | hjmi := eq_or_ne j (m.cons i)
    · simpa only [cons_zero, cons_succ, if_pos rfl, monomial_eq, C_1, one_mul,
        Finsupp.prod_pow] using coeff_monomial m m (1 : R)
    · simp only [hjmi, if_false]
      obtain hij | rfl := ne_or_eq i (j 0)
      · simp only [hij, if_false, coeff_zero]
      simp only [if_true]
      have hmj : m ≠ j.tail := by
        rintro rfl
        rw [cons_tail] at hjmi
        contradiction
      simpa only [monomial_eq, C_1, one_mul, Finsupp.prod_pow, tail_apply, if_neg hmj.symm] using
        coeff_monomial m j.tail (1 : R)
Cleared hypotheses: m, f, i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
m : Fin n →₀ ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
add :
  ∀ (p q : MvPolynomial (Fin (n + 1)) R)
    (hp :
      ∀ (m : Fin n →₀ ℕ) (i : ℕ),
        coeff m
            (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) p)
              i) =
          coeff (cons i m) p)
    (hq :
      ∀ (m : Fin n →₀ ℕ) (i : ℕ),
        coeff m
            (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) q)
              i) =
          coeff (cons i m) q)
    (m : Fin n →₀ ℕ) (i : ℕ),
    coeff m
        (Polynomial.coeff
          ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) (p + q)) i) =
      coeff (cons i m) (p + q)
⊢ coeff m
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) =
    coeff (cons i m) f
have monomial : ∀ (j : Fin (n + 1) →₀ ℕ) (r : R) (m : Fin n →₀ ℕ) (i : ℕ),
  Eq.{u + 1} (α := R)
    (coeff m
      (Polynomial.coeff
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
          ((monomial j : (a : R) → MvPolynomial (Fin (n + 1)) R) r))
        i))
    (coeff (cons i m) ((monomial j : (a : R) → MvPolynomial (Fin (n + 1)) R) r))
Tactic: induction f using MvPolynomial.induction_on' generalizing i m with
  | add p q hp hq => simp only [map_add, Polynomial.coeff_add, coeff_add, hp, hq]
  | monomial j r =>
    simp only [finSuccEquiv_apply, coe_eval₂Hom, eval₂_monomial, RingHom.coe_comp, Finsupp.prod_pow,
      Polynomial.coeff_C_mul, coeff_C_mul, coeff_monomial, Fin.prod_univ_succ, Fin.cases_zero,
      Fin.cases_succ, ← _root_.map_prod, ← map_pow, Function.comp_apply]
    rw [← mul_boole, mul_comm (Polynomial.X ^ j 0), Polynomial.coeff_C_mul_X_pow]; congr 1
    obtain rfl | hjmi := eq_or_ne j (m.cons i)
    · simpa only [cons_zero, cons_succ, if_pos rfl, monomial_eq, C_1, one_mul,
        Finsupp.prod_pow] using coeff_monomial m m (1 : R)
    · simp only [hjmi, if_false]
      obtain hij | rfl := ne_or_eq i (j 0)
      · simp only [hij, if_false, coeff_zero]
      simp only [if_true]
      have hmj : m ≠ j.tail := by
        rintro rfl
        rw [cons_tail] at hjmi
        contradiction
      simpa only [monomial_eq, C_1, one_mul, Finsupp.prod_pow, tail_apply, if_neg hmj.symm] using
        coeff_monomial m j.tail (1 : R)
Cleared hypotheses: m, f, i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
r : R
⊢ Eq (α := R[X])
    (OneHom.toFun
      (↑(↑(Polynomial.mapRingHom (eval s)) : (MvPolynomial (Fin n) R)[X] →* R[X]) :
        OneHom (MvPolynomial (Fin n) R)[X] R[X])
      ((algebraMap R (MvPolynomial (Fin n) R)[X] : (a : R) → (MvPolynomial (Fin n) R)[X]) r))
    ((algebraMap R R[X] : (a : R) → R[X]) r)
have h : r =
  (eval s : (a : MvPolynomial (Fin n) R) → R)
    ((algebraMap R (MvPolynomial (Fin n) R) : (a : R) → MvPolynomial (Fin n) R) r : MvPolynomial (Fin n) R)
Tactic: convert! Polynomial.map_C (eval s)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let __src : (MvPolynomial (Fin n) R)[X] →+* R[X] := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ (eval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s) : (a : MvPolynomial (Fin (n + 1)) R) → R) f =
    Polynomial.eval y
      (Polynomial.map (eval s)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f))
have aeval : Eq (α := R) ((aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s) : (a : MvPolynomial (Fin (n + 1)) R) → R) f : R)
  ((AlgHom.comp (Polynomial.aeval y)
          (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])) :
        (a : MvPolynomial (Fin (n + 1)) R) → R)
      f :
    R)
Tactic: change
    aeval (Fin.cons y s : Fin (n + 1) → R) f =
      (Polynomial.aeval y).comp (φ.comp (finSuccEquiv R n).toAlgHom) f
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let __src : (MvPolynomial (Fin n) R)[X] →+* R[X] := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ Eq (α := R) ((aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s) : (a : MvPolynomial (Fin (n + 1)) R) → R) f : R)
    ((AlgHom.comp (Polynomial.aeval y)
            (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])) :
          (a : MvPolynomial (Fin (n + 1)) R) → R)
        f :
      R)
have e_a : Eq (α := MvPolynomial (Fin (n + 1)) R →ₐ[R] R) (aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s))
  (AlgHom.comp (Polynomial.aeval y)
    (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let __src : (MvPolynomial (Fin n) R)[X] →+* R[X] := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ Eq (α := MvPolynomial (Fin (n + 1)) R →ₐ[R] R) (aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s))
    (AlgHom.comp (Polynomial.aeval y)
      (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])))
have e_a : ∀ (i : Fin (n + 1)),
  Eq (α := R)
    ((aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s) : (a : MvPolynomial (Fin (n + 1)) R) → R) (X i) : R)
    ((AlgHom.comp (Polynomial.aeval y)
            (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])) :
          (a : MvPolynomial (Fin (n + 1)) R) → R)
        (X i) :
      R)
Tactic: apply MvPolynomial.algHom_ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
φ : (MvPolynomial (Fin n) R)[X] →ₐ[R] R[X] :=
  let __src : (MvPolynomial (Fin n) R)[X] →+* R[X] := Polynomial.mapRingHom (eval s);
  { toRingHom := __src, commutes' := ⋯ }
⊢ ∀ (i : Fin (n + 1)),
    Eq (α := R)
      ((aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s) : (a : MvPolynomial (Fin (n + 1)) R) → R) (X i) : R)
      ((AlgHom.comp (Polynomial.aeval y)
              (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])) :
            (a : MvPolynomial (Fin (n + 1)) R) → R)
          (X i) :
        R)
have e_a : Eq (α := R) ((aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s) : (a : MvPolynomial (Fin (n + 1)) R) → R) (X 0) : R)
    ((AlgHom.comp (Polynomial.aeval y)
            (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])) :
          (a : MvPolynomial (Fin (n + 1)) R) → R)
        (X 0) :
      R) ∧
  ∀ (i : Fin n),
    Eq (α := R)
      ((aeval (Fin.cons (α := fun (a : Fin (n + 1)) ↦ R) y s) : (a : MvPolynomial (Fin (n + 1)) R) → R) (X i.succ) : R)
      ((AlgHom.comp (Polynomial.aeval y)
              (φ.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →ₐ[R] (MvPolynomial (Fin n) R)[X])) :
            (a : MvPolynomial (Fin (n + 1)) R) → R)
          (X i.succ) :
        R)
Tactic: rw [Fin.forall_iff_succ]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ Membership.mem (γ := Finset (Fin n →₀ ℕ))
      (support.{u, 0} (R := R)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
      m ↔
    cons i m ∈ f.support
have mp : Membership.mem (γ := Finset (Fin n →₀ ℕ))
    (support.{u, 0} (R := R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
    m →
  cons i m ∈ f.support
Tactic: apply Iff.intro
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
mp :
  Membership.mem (γ := Finset (Fin n →₀ ℕ))
      (support.{u, 0} (R := R)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
      m →
    cons i m ∈ f.support
⊢ Membership.mem (γ := Finset (Fin n →₀ ℕ))
      (support.{u, 0} (R := R)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
      m ↔
    cons i m ∈ f.support
have mpr : cons i m ∈ f.support →
  Membership.mem (γ := Finset (Fin n →₀ ℕ))
    (support.{u, 0} (R := R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
    m
Tactic: apply Iff.intro
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi :
  Ne.{u + 1} (α := MvPolynomial (Fin n) R)
    (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) 0
⊢ Finset.Nonempty (α := Fin n →₀ ℕ)
    (support.{u, 0} (R := R)
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
have rw : ¬Eq.{max (u + 1) 1} (α := MvPolynomial (Fin n) R)
    (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) 0
Tactic: rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi :
  Ne.{u + 1} (α := MvPolynomial (Fin n) R)
    (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) 0
⊢ totalDegree.{u, 0} (R := R) (σ := Fin n)
        (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i) +
      i ≤
    f.totalDegree
have hf'_sup : Finset.Nonempty (α := Fin n →₀ ℕ)
  (support.{u, 0} (R := R)
    (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) i))
Tactic: have hf'_sup : ((finSuccEquiv R n f).coeff i).support.Nonempty := by
    rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty]
    exact hi