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 : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : f = 0
⊢ natDegree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    degreeOf 0 f
have pos : natDegree (R := MvPolynomial (Fin n) R)
    ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) 0) =
  degreeOf.{u, 0} (R := R) (σ := Fin (n + 1)) 0 0
Tactic: rw [c, map_zero, Polynomial.natDegree_zero, degreeOf_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : f = 0
pos :
  natDegree (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) 0) =
    degreeOf.{u, 0} (R := R) (σ := Fin (n + 1)) 0 0
⊢ natDegree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    degreeOf 0 f
have pos₁ : natDegree.{u} (R := MvPolynomial (Fin n) R) 0 = degreeOf.{u, 0} (R := R) (σ := Fin (n + 1)) 0 0
Tactic: rw [c, map_zero, Polynomial.natDegree_zero, degreeOf_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : f = 0
pos :
  natDegree (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) 0) =
    degreeOf.{u, 0} (R := R) (σ := Fin (n + 1)) 0 0
pos₁ : natDegree.{u} (R := MvPolynomial (Fin n) R) 0 = degreeOf.{u, 0} (R := R) (σ := Fin (n + 1)) 0 0
⊢ natDegree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    degreeOf 0 f
have pos₂ : 0 = degreeOf.{u, 0} (R := R) (σ := Fin (n + 1)) 0 0
Tactic: rw [c, map_zero, Polynomial.natDegree_zero, degreeOf_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : f = 0
pos :
  natDegree (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) 0) =
    degreeOf.{u, 0} (R := R) (σ := Fin (n + 1)) 0 0
pos₁ : natDegree.{u} (R := MvPolynomial (Fin n) R) 0 = degreeOf.{u, 0} (R := R) (σ := Fin (n + 1)) 0 0
pos₂ : 0 = degreeOf.{u, 0} (R := R) (σ := Fin (n + 1)) 0 0
⊢ natDegree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    degreeOf 0 f
have pos₃ : Eq (α := ℕ) 0 0
Tactic: rw [c, map_zero, Polynomial.natDegree_zero, degreeOf_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
⊢ natDegree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    degreeOf 0 f
have neg : WithBot.unbotD 0
    (degree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)) =
  degreeOf 0 f
Tactic: rw [Polynomial.natDegree, degree_finSuccEquiv c, Nat.cast_withBot, WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
neg :
  WithBot.unbotD 0
      (degree.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)) =
    degreeOf 0 f
⊢ natDegree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    degreeOf 0 f
have neg₁ : WithBot.unbotD 0 (↑(degreeOf 0 f) : WithBot ℕ) = degreeOf 0 f
Tactic: rw [Polynomial.natDegree, degree_finSuccEquiv c, Nat.cast_withBot, WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
neg :
  WithBot.unbotD 0
      (degree.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)) =
    degreeOf 0 f
neg₁ : WithBot.unbotD 0 (↑(degreeOf 0 f) : WithBot ℕ) = degreeOf 0 f
⊢ natDegree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    degreeOf 0 f
have neg₂ : WithBot.unbotD 0 (↑(degreeOf 0 f) : WithBot ℕ) = degreeOf 0 f
Tactic: rw [Polynomial.natDegree, degree_finSuccEquiv c, Nat.cast_withBot, WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : ¬f = 0
neg :
  WithBot.unbotD 0
      (degree.{u} (R := MvPolynomial (Fin n) R)
        ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f)) =
    degreeOf 0 f
neg₁ : WithBot.unbotD 0 (↑(degreeOf 0 f) : WithBot ℕ) = degreeOf 0 f
neg₂ : WithBot.unbotD 0 (↑(degreeOf 0 f) : WithBot ℕ) = degreeOf 0 f
⊢ natDegree.{u} (R := MvPolynomial (Fin n) R)
      ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) f) =
    degreeOf 0 f
have neg₃ : degreeOf 0 f = degreeOf 0 f
Tactic: rw [Polynomial.natDegree, degree_finSuccEquiv c, Nat.cast_withBot, WithBot.unbotD_coe]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
a : σ
p : MvPolynomial σ R
⊢ degreeOf a p =
    natDegree (R := MvPolynomial.{u_1, u} { b : σ // b ≠ a } R)
      ((optionEquivLeft R { b : σ // b ≠ a } :
          (a_1 : MvPolynomial (Option { b : σ // b ≠ a }) R) → (MvPolynomial { b : σ // b ≠ a } R)[X])
        ((rename (⇑(Equiv.optionSubtypeNe a).symm : (a_1 : σ) → Option { b : σ // b ≠ a }) :
            (a_1 : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ a }) R)
          p))
have rw : degreeOf.{u, u_1} (R := R) (σ := Option { b : σ // b ≠ a }) none
    ((rename (⇑(Equiv.optionSubtypeNe a).symm : (a_1 : σ) → Option { b : σ // b ≠ a }) :
        (a_1 : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ a }) R)
      p) =
  degreeOf a p
Tactic: rw [natDegree_optionEquivLeft, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
a : σ
p : MvPolynomial σ R
⊢ degreeOf.{u, u_1} (R := R) (σ := Option { b : σ // b ≠ a }) none
      ((rename (⇑(Equiv.optionSubtypeNe a).symm : (a_1 : σ) → Option { b : σ // b ≠ a }) :
          (a_1 : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ a }) R)
        p) =
    degreeOf a p
have h : Eq.{u_1 + 1} (α := Option { b : σ // b ≠ a }) none
  (((Equiv.optionSubtypeNe a).symm : (a_1 : σ) → Option { b : σ // b ≠ a }) a)
Tactic: convert! degreeOf_rename_of_injective (Equiv.injective (Equiv.optionSubtypeNe a).symm) a
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
a : σ
p : MvPolynomial σ R
⊢ Eq.{u_1 + 1} (α := Option { b : σ // b ≠ a }) none
    (((Equiv.optionSubtypeNe a).symm : (a_1 : σ) → Option { b : σ // b ≠ a }) a)
have h : Eq.{u_1 + 1} (α := Option { b : σ // b ≠ a }) none
  (if h : a = a then none else Option.some (Subtype.mk (p := fun (y : σ) ↦ ¬y = a) a h))
Tactic: rw [Equiv.optionSubtypeNe_symm_apply, dif_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
a : σ
p : MvPolynomial σ R
h :
  Eq.{u_1 + 1} (α := Option { b : σ // b ≠ a }) none
    (if h : a = a then none else Option.some (Subtype.mk (p := fun (y : σ) ↦ ¬y = a) a h))
⊢ Eq.{u_1 + 1} (α := Option { b : σ // b ≠ a }) none
    (((Equiv.optionSubtypeNe a).symm : (a_1 : σ) → Option { b : σ // b ≠ a }) a)
have h₁ : Eq.{u_1 + 1} (α := Option { b : σ // b ≠ a }) none none
Tactic: rw [Equiv.optionSubtypeNe_symm_apply, dif_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ degreeOf.{u, 0} (R := R) j
      (Polynomial.coeff ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) p) i) ≤
    degreeOf j.succ p
have rw : ∀ (b : 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]) p) i))
      b →
    LE.le (α := ℕ) ((b : (a : Fin n) → ℕ) j : ℕ)
      (p.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) j.succ : ℕ)
Tactic: rw [degreeOf_eq_sup, degreeOf_eq_sup, Finset.sup_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm :
  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]) p) i))
    m
⊢ LE.le (α := ℕ) ((m : (a : Fin n) → ℕ) j : ℕ)
    (p.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) j.succ : ℕ)
have rw : LE.le (α := ℕ) ((cons i m : (a : Fin (n + 1)) → ℕ) j.succ : ℕ)
  (p.support.sup fun (m : Fin (n + 1) →₀ ℕ) ↦ (m : (a : Fin (n + 1)) → ℕ) j.succ : ℕ)
Tactic: rw [← Finsupp.cons_succ j i m]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial.{u_1, u} (Option σ) R
⊢ Eq (α := (MvPolynomial (Fin n) R)[X])
    ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        ((rename (⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm) : (a : Option σ) → Fin (n + 1)) :
            (a : MvPolynomial (Option σ) R) → MvPolynomial (Fin (n + 1)) R)
          φ) :
      (MvPolynomial (Fin n) R)[X])
    (Polynomial.map (R := MvPolynomial σ R) (AlgHom.toRingHom (rename (⇑e : (a : σ) → Fin n)))
        ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) φ) :
      (MvPolynomial (Fin n) R)[X])
have suffices : RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (finSuccEquiv R n)))
    (AlgHom.toRingHom (rename (⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm) : (a : Option σ) → Fin (n + 1)))) =
  RingHom.comp (Polynomial.mapRingHom (AlgHom.toRingHom (rename (⇑e : (a : σ) → Fin n))))
    (↑(optionEquivLeft R σ) : MvPolynomial (Option σ) R →+* (MvPolynomial σ R)[X])
Tactic: suffices (finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ((Equiv.optionCongr e).trans
        (_root_.finSuccEquiv n).symm)).toRingHom =
      (Polynomial.mapRingHom (rename e).toRingHom).comp (optionEquivLeft R σ) by
    exact DFunLike.congr_fun this φ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial.{u_1, u} (Option σ) R
⊢ RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (finSuccEquiv R n)))
      (AlgHom.toRingHom (rename (⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm) : (a : Option σ) → Fin (n + 1)))) =
    RingHom.comp (Polynomial.mapRingHom (AlgHom.toRingHom (rename (⇑e : (a : σ) → Fin n))))
      (↑(optionEquivLeft R σ) : MvPolynomial (Option σ) R →+* (MvPolynomial σ R)[X])
have hC : ∀ (r : R),
  Eq.{u + 1} (α := (MvPolynomial (Fin n) R)[X])
    ((RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (finSuccEquiv R n)))
            (AlgHom.toRingHom
              (rename (⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm) : (a : Option σ) → Fin (n + 1)))) :
          (a : MvPolynomial (Option σ) R) → (MvPolynomial (Fin n) R)[X])
        ((C : (a : R) → MvPolynomial (Option σ) R) r) :
      (MvPolynomial (Fin n) R)[X])
    ((RingHom.comp (Polynomial.mapRingHom (AlgHom.toRingHom (rename (⇑e : (a : σ) → Fin n))))
            (↑(optionEquivLeft R σ) : MvPolynomial (Option σ) R →+* (MvPolynomial σ R)[X]) :
          (a : MvPolynomial (Option σ) R) → (MvPolynomial (Fin n) R)[X])
        ((C : (a : R) → MvPolynomial (Option σ) R) r) :
      (MvPolynomial (Fin n) R)[X])
Tactic: apply ringHom_ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial.{u_1, u} (Option σ) R
hC :
  ∀ (r : R),
    Eq.{u + 1} (α := (MvPolynomial (Fin n) R)[X])
      ((RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (finSuccEquiv R n)))
              (AlgHom.toRingHom
                (rename (⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm) : (a : Option σ) → Fin (n + 1)))) :
            (a : MvPolynomial (Option σ) R) → (MvPolynomial (Fin n) R)[X])
          ((C : (a : R) → MvPolynomial (Option σ) R) r) :
        (MvPolynomial (Fin n) R)[X])
      ((RingHom.comp (Polynomial.mapRingHom (AlgHom.toRingHom (rename (⇑e : (a : σ) → Fin n))))
              (↑(optionEquivLeft R σ) : MvPolynomial (Option σ) R →+* (MvPolynomial σ R)[X]) :
            (a : MvPolynomial (Option σ) R) → (MvPolynomial (Fin n) R)[X])
          ((C : (a : R) → MvPolynomial (Option σ) R) r) :
        (MvPolynomial (Fin n) R)[X])
⊢ RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (finSuccEquiv R n)))
      (AlgHom.toRingHom (rename (⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm) : (a : Option σ) → Fin (n + 1)))) =
    RingHom.comp (Polynomial.mapRingHom (AlgHom.toRingHom (rename (⇑e : (a : σ) → Fin n))))
      (↑(optionEquivLeft R σ) : MvPolynomial (Option σ) R →+* (MvPolynomial σ R)[X])
have hX : ∀ (i : Option σ),
  Eq.{u + 1} (α := (MvPolynomial (Fin n) R)[X])
    ((RingHom.comp (RingEquiv.toRingHom (AlgEquiv.toRingEquiv (finSuccEquiv R n)))
            (AlgHom.toRingHom
              (rename (⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm) : (a : Option σ) → Fin (n + 1)))) :
          (a : MvPolynomial (Option σ) R) → (MvPolynomial (Fin n) R)[X])
        (X i) :
      (MvPolynomial (Fin n) R)[X])
    ((RingHom.comp (Polynomial.mapRingHom (AlgHom.toRingHom (rename (⇑e : (a : σ) → Fin n))))
            (↑(optionEquivLeft R σ) : MvPolynomial (Option σ) R →+* (MvPolynomial σ R)[X]) :
          (a : MvPolynomial (Option σ) R) → (MvPolynomial (Fin n) R)[X])
        (X i) :
      (MvPolynomial (Fin n) R)[X])
Tactic: apply ringHom_ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_2
τ : Type u_3
f : σ → τ
i : σ
p : R[X]
⊢ Eq (α := MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
        ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) p) :
      MvPolynomial τ R)
    ((Polynomial.aeval (X (f i)) : (a : R[X]) → MvPolynomial τ R) p : MvPolynomial τ R)
have rw : Eq (α := MvPolynomial τ R)
  (((Polynomial.aeval ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) : R[X] →ₐ[R] MvPolynomial τ R) :
        (a : R[X]) → MvPolynomial τ R)
      p :
    MvPolynomial τ R)
  ((Polynomial.aeval (X (f i)) : (a : R[X]) → MvPolynomial τ R) p : MvPolynomial τ R)
Tactic: rw [← aeval_algHom_apply, rename_X]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_2
τ : Type u_3
f : σ → τ
i : σ
p : R[X]
rw :
  Eq (α := MvPolynomial τ R)
    (((Polynomial.aeval ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) : R[X] →ₐ[R] MvPolynomial τ R) :
          (a : R[X]) → MvPolynomial τ R)
        p :
      MvPolynomial τ R)
    ((Polynomial.aeval (X (f i)) : (a : R[X]) → MvPolynomial τ R) p : MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R)
        ((Polynomial.aeval (X i) : (a : R[X]) → MvPolynomial σ R) p) :
      MvPolynomial τ R)
    ((Polynomial.aeval (X (f i)) : (a : R[X]) → MvPolynomial τ R) p : MvPolynomial τ R)
have rw₁ : Eq (α := MvPolynomial τ R) ((Polynomial.aeval (X (f i)) : (a : R[X]) → MvPolynomial τ R) p : MvPolynomial τ R)
  ((Polynomial.aeval (X (f i)) : (a : R[X]) → MvPolynomial τ R) p : MvPolynomial τ R)
Tactic: rw [← aeval_algHom_apply, rename_X]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u_1
σ : Type u_3
inst : CommSemiring R
i : σ
⊢ Eq (α := R[X] →ₐ[R] MvPolynomial σ R) (toMvPolynomial i)
    (AlgHom.comp (MvPolynomial.rename fun (x : Unit) ↦ i)
      (↑(AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit)) : R[X] →ₐ[R] MvPolynomial Unit R))
have hX : ∀ (m : σ →₀ ℕ),
  Eq.{u_1 + 1} (α := R) (MvPolynomial.coeff m ((toMvPolynomial i : (a : R[X]) → MvPolynomial σ R) X))
    (MvPolynomial.coeff m
      ((AlgHom.comp (MvPolynomial.rename fun (x : Unit) ↦ i)
            (↑(AlgEquiv.symm (MvPolynomial.uniqueAlgEquiv R Unit)) : R[X] →ₐ[R] MvPolynomial Unit R) :
          (a : R[X]) → MvPolynomial σ R)
        X))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u_1
σ : Type u_3
inst : CommSemiring R
i : σ
⊢ Injective (α := R[X]) (β := MvPolynomial σ R) (⇑(toMvPolynomial i) : (a : R[X]) → MvPolynomial σ R)
have simp : Injective (α := MvPolynomial Unit R) (β := MvPolynomial σ R)
  (⇑(MvPolynomial.rename fun (x : Unit) ↦ i) : (a : MvPolynomial Unit R) → MvPolynomial σ R)
Tactic: simp only [toMvPolynomial_eq_rename_comp, AlgHom.coe_comp, AlgEquiv.coe_algHom,
    EquivLike.injective_comp]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u_1
σ : Type u_3
inst : CommSemiring R
f : σ → R
i : σ
⊢ RingHom.comp (eval f) (↑(toMvPolynomial i) : R[X] →+* MvPolynomial σ R) = evalRingHom (f i)
have h₁ : ∀ (x : R),
  Eq (α := R)
    ((RingHom.comp (RingHom.comp (eval f) (↑(toMvPolynomial i) : R[X] →+* MvPolynomial σ R)) Polynomial.C : (a : R) → R)
        x :
      R)
    ((RingHom.comp (evalRingHom (f i)) Polynomial.C : (a : R) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u_1
σ : Type u_3
inst : CommSemiring R
f : σ → R
i : σ
h₁ :
  ∀ (x : R),
    Eq (α := R)
      ((RingHom.comp (RingHom.comp (eval f) (↑(toMvPolynomial i) : R[X] →+* MvPolynomial σ R)) Polynomial.C :
            (a : R) → R)
          x :
        R)
      ((RingHom.comp (evalRingHom (f i)) Polynomial.C : (a : R) → R) x : R)
⊢ RingHom.comp (eval f) (↑(toMvPolynomial i) : R[X] →+* MvPolynomial σ R) = evalRingHom (f i)
have h₂ : Eq (α := R)
  ((RingHom.comp (eval f) (↑(toMvPolynomial i) : R[X] →+* MvPolynomial σ R) : (a : R[X]) → R) Polynomial.X : R)
  ((evalRingHom (f i) : (a : R[X]) → R) Polynomial.X : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u_1
S : Type u_2
σ : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
f : σ → S
i : σ
⊢ Eq (α := R[X] →ₐ[R] S) (AlgHom.comp (aeval f) (toMvPolynomial i)) (Polynomial.aeval (f i))
have hX : Eq.{u_2 + 1} (α := S) ((AlgHom.comp (aeval f) (toMvPolynomial i) : (a : R[X]) → S) Polynomial.X : S)
  ((Polynomial.aeval (f i) : (a : R[X]) → S) Polynomial.X : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u_1
σ : Type u_3
τ : Type u_4
inst : CommSemiring R
f : σ → τ
a : σ
⊢ Eq (α := R[X] →ₐ[R] MvPolynomial τ R) (AlgHom.comp (rename f) (toMvPolynomial a)) (toMvPolynomial (f a))
have hX : ∀ (m : τ →₀ ℕ),
  Eq.{u_1 + 1} (α := R)
    (coeff m ((AlgHom.comp (rename f) (toMvPolynomial a) : (a : R[X]) → MvPolynomial τ R) Polynomial.X))
    (coeff m ((toMvPolynomial (f a) : (a : R[X]) → MvPolynomial τ R) Polynomial.X))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Fintype σ
g : R →+* S₁
X : σ → S₁
f : MvPolynomial σ R
⊢ eval₂ g X f =
    ∑ d ∈ f.support,
      HMul.hMul (α := S₁) (β := S₁) ((g : (a : R) → S₁) (coeff d f) : S₁)
        (∏ i : σ, HPow.hPow (β := ℕ) (X i) ((d : (a : σ) → ℕ) i : ℕ) : S₁)
have simp : Eq.{v + 1} (α := S₁)
  (∑ d ∈ f.support,
    HMul.hMul (α := S₁) (β := S₁) ((g : (a : R) → S₁) (coeff d f) : S₁)
      (∏ i ∈ d.support, HPow.hPow (β := ℕ) (X i) ((d : (a : σ) → ℕ) i : ℕ) : S₁))
  (∑ x ∈ f.support,
    HMul.hMul (α := S₁) (β := S₁) ((g : (a : R) → S₁) (coeff x f) : S₁) (x.prod fun (a : σ) (b : ℕ) ↦ X a ^ b : S₁))
Tactic: simp only [eval₂_eq, ← Finsupp.prod_pow]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
a : R
⊢ eval₂ f g ((C : (a : R) → MvPolynomial σ R) a) = (f : (a : R) → S₁) a
have rw : eval₂ f g ((monomial 0 : (a : R) → MvPolynomial σ R) a) = (f : (a : R) → S₁) a
Tactic: rw [C_apply, eval₂_monomial, prod_zero_index, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
a : R
rw : eval₂ f g ((monomial 0 : (a : R) → MvPolynomial σ R) a) = (f : (a : R) → S₁) a
⊢ eval₂ f g ((C : (a : R) → MvPolynomial σ R) a) = (f : (a : R) → S₁) a
have rw₁ : HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) a : S₁) (Finsupp.prod 0 fun (n : σ) (e : ℕ) ↦ g n ^ e : S₁) =
  (f : (a : R) → S₁) a
Tactic: rw [C_apply, eval₂_monomial, prod_zero_index, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
a : R
rw : eval₂ f g ((monomial 0 : (a : R) → MvPolynomial σ R) a) = (f : (a : R) → S₁) a
rw₁ :
  HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) a : S₁) (Finsupp.prod 0 fun (n : σ) (e : ℕ) ↦ g n ^ e : S₁) =
    (f : (a : R) → S₁) a
⊢ eval₂ f g ((C : (a : R) → MvPolynomial σ R) a) = (f : (a : R) → S₁) a
have rw₂ : HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) a : S₁) (1 : S₁) = (f : (a : R) → S₁) a
Tactic: rw [C_apply, eval₂_monomial, prod_zero_index, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
a : R
rw : eval₂ f g ((monomial 0 : (a : R) → MvPolynomial σ R) a) = (f : (a : R) → S₁) a
rw₁ :
  HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) a : S₁) (Finsupp.prod 0 fun (n : σ) (e : ℕ) ↦ g n ^ e : S₁) =
    (f : (a : R) → S₁) a
rw₂ : HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) a : S₁) (1 : S₁) = (f : (a : R) → S₁) a
⊢ eval₂ f g ((C : (a : R) → MvPolynomial σ R) a) = (f : (a : R) → S₁) a
have rw₃ : Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) a : S₁) ((f : (a : R) → S₁) a : S₁)
Tactic: rw [C_apply, eval₂_monomial, prod_zero_index, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ {s : σ →₀ ℕ} {a : R},
    eval₂ f g (HMul.hMul (β := MvPolynomial σ R) p ((monomial s : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)) =
      HMul.hMul (β := S₁) (eval₂ f g p) ((f : (a : R) → S₁) a : S₁) * s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e
have C : ∀ (a : R) {s : σ →₀ ℕ} {a_1 : R},
  eval₂ f g
      (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
        ((monomial s : (a : R) → MvPolynomial σ R) a_1 : MvPolynomial σ R)) =
    HMul.hMul (β := S₁) (eval₂ f g ((C : (a : R) → MvPolynomial σ R) a)) ((f : (a : R) → S₁) a_1 : S₁) *
      s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e
Tactic: apply MvPolynomial.induction_on p