awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
pos :
  ∀
    (hpi :
      Eq (α := MvPolynomial S₁ R)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0),
    totalDegree.{u, v} (R := R) (σ := S₁)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
      p.totalDegree
neg neg₁ :
  ∀
    (hpi :
      ¬Eq (α := MvPolynomial S₁ R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i)
          0),
    totalDegree.{u, v} (R := R) (σ := S₁)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
      p.totalDegree
neg₂ neg₃ :
  ∀
    (hpi :
      ¬Eq (α := MvPolynomial S₁ R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0)
    (σ : S₁ →₀ ℕ)
    (hσ :
      Membership.mem (γ := Finset (S₁ →₀ ℕ))
        (support.{u, v} (R := R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
        σ),
    (σ.sum fun (x : S₁) (e : ℕ) ↦ e) ≤ p.totalDegree
⊢ totalDegree.{u, v} (R := R) (σ := S₁)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
    p.totalDegree
have neg₄ : ∀
  (hpi :
    ¬Eq (α := MvPolynomial S₁ R)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0)
  (σ : S₁ →₀ ℕ)
  (hσ :
    Membership.mem (γ := Finset (S₁ →₀ ℕ))
      (support.{u, v} (R := R)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
      σ),
  LE.le (α := ℕ) (σ.sum fun (x : S₁) (e : ℕ) ↦ e)
    ((embDomain Embedding.some σ + Finsupp.single none i).sum fun (x : Option S₁) (e : ℕ) ↦ e)
Tactic: classical
  by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
  · rw [hpi]; simp
  rw [totalDegree, Finset.sup_le_iff]
  intro σ hσ
  refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
  · simp [Finsupp.sum_add_index, Finsupp.sum_embDomain]
  · simpa [mem_support_iff, ← optionEquivLeft_coeff_some_coeff_none R S₁] using hσ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
p : MvPolynomial.{v, u} (Option S₁) R
i : ℕ
pos :
  ∀
    (hpi :
      Eq (α := MvPolynomial S₁ R)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0),
    totalDegree.{u, v} (R := R) (σ := S₁)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
      p.totalDegree
neg neg₁ :
  ∀
    (hpi :
      ¬Eq (α := MvPolynomial S₁ R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i)
          0),
    totalDegree.{u, v} (R := R) (σ := S₁)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
      p.totalDegree
neg₂ neg₃ :
  ∀
    (hpi :
      ¬Eq (α := MvPolynomial S₁ R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0)
    (σ : S₁ →₀ ℕ)
    (hσ :
      Membership.mem (γ := Finset (S₁ →₀ ℕ))
        (support.{u, v} (R := R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
        σ),
    (σ.sum fun (x : S₁) (e : ℕ) ↦ e) ≤ p.totalDegree
neg₄ :
  ∀
    (hpi :
      ¬Eq (α := MvPolynomial S₁ R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0)
    (σ : S₁ →₀ ℕ)
    (hσ :
      Membership.mem (γ := Finset (S₁ →₀ ℕ))
        (support.{u, v} (R := R)
          (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
        σ),
    LE.le (α := ℕ) (σ.sum fun (x : S₁) (e : ℕ) ↦ e)
      ((embDomain Embedding.some σ + Finsupp.single none i).sum fun (x : Option S₁) (e : ℕ) ↦ e)
⊢ totalDegree.{u, v} (R := R) (σ := S₁)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
    p.totalDegree
have neg₅ : ∀
  (hpi :
    ¬Eq (α := MvPolynomial S₁ R)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) 0)
  (σ : S₁ →₀ ℕ)
  (hσ :
    Membership.mem (γ := Finset (S₁ →₀ ℕ))
      (support.{u, v} (R := R)
        (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i))
      σ),
  embDomain Embedding.some σ + Finsupp.single none i ∈ p.support
Tactic: classical
  by_cases hpi : (optionEquivLeft R S₁ p).coeff i = 0
  · rw [hpi]; simp
  rw [totalDegree, Finset.sup_le_iff]
  intro σ hσ
  refine le_trans ?_ (Finset.le_sup (b := σ.embDomain .some + .single .none i) ?_)
  · simp [Finsupp.sum_add_index, Finsupp.sum_embDomain]
  · simpa [mem_support_iff, ← optionEquivLeft_coeff_some_coeff_none R S₁] using hσ
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ coeff d (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) m) =
    coeff (optionElim m d) p
have rw : Eq.{u + 1} (α := R)
  (coeff d (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) m))
  (coeff (optionElim m d).some
    (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
      ((optionElim m d : (a : Option σ) → ℕ) none)))
Tactic: rw [← optionEquivLeft_coeff_some_coeff_none]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ Eq.{u + 1} (α := R)
    (coeff d (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) m))
    (coeff (optionElim m d).some
      (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
        ((optionElim m d : (a : Option σ) → ℕ) none)))
have e_m : d = (optionElim m d).some
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
m : ℕ
d : σ →₀ ℕ
e_m : d = (optionElim m d).some
⊢ Eq.{u + 1} (α := R)
    (coeff d (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) m))
    (coeff (optionElim m d).some
      (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p)
        ((optionElim m d : (a : Option σ) → ℕ) none)))
have e_p : m = (optionElim m d : (a : Option σ) → ℕ) none
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
⊢ Eq (α := MvPolynomial.{v, u} S₁ R[X] →ₐ[R] MvPolynomial.{v, u} S₁ R[X])
    (AlgHom.comp (B := MvPolynomial.{v, u} (Option S₁) R)
      (aeval fun (o : Option S₁) ↦ o.elim ((C : (a : R[X]) → MvPolynomial S₁ R[X]) Polynomial.X) X)
      (aevalTower (Polynomial.aeval (X none)) fun (i : S₁) ↦ X (Option.some i)))
    (AlgHom.id R (MvPolynomial.{v, u} S₁ R[X]))
have h₁ : Eq (α := MvPolynomial.{v, u} S₁ R[X])
  ((AlgHom.comp (B := MvPolynomial.{v, u} S₁ R[X])
          (AlgHom.comp (B := MvPolynomial.{v, u} (Option S₁) R)
            (aeval fun (o : Option S₁) ↦ o.elim ((C : (a : R[X]) → MvPolynomial S₁ R[X]) Polynomial.X) X)
            (aevalTower (Polynomial.aeval (X none)) fun (i : S₁) ↦ X (Option.some i)))
          (IsScalarTower.toAlgHom R R[X] (MvPolynomial.{v, u} S₁ R[X])) :
        (a : R[X]) → MvPolynomial S₁ R[X])
      Polynomial.X :
    MvPolynomial.{v, u} S₁ R[X])
  ((AlgHom.comp (AlgHom.id R (MvPolynomial.{v, u} S₁ R[X]))
          (IsScalarTower.toAlgHom R R[X] (MvPolynomial.{v, u} S₁ R[X])) :
        (a : R[X]) → MvPolynomial S₁ R[X])
      Polynomial.X :
    MvPolynomial.{v, u} S₁ R[X])
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
h₁ :
  Eq (α := MvPolynomial.{v, u} S₁ R[X])
    ((AlgHom.comp (B := MvPolynomial.{v, u} S₁ R[X])
            (AlgHom.comp (B := MvPolynomial.{v, u} (Option S₁) R)
              (aeval fun (o : Option S₁) ↦ o.elim ((C : (a : R[X]) → MvPolynomial S₁ R[X]) Polynomial.X) X)
              (aevalTower (Polynomial.aeval (X none)) fun (i : S₁) ↦ X (Option.some i)))
            (IsScalarTower.toAlgHom R R[X] (MvPolynomial.{v, u} S₁ R[X])) :
          (a : R[X]) → MvPolynomial S₁ R[X])
        Polynomial.X :
      MvPolynomial.{v, u} S₁ R[X])
    ((AlgHom.comp (AlgHom.id R (MvPolynomial.{v, u} S₁ R[X]))
            (IsScalarTower.toAlgHom R R[X] (MvPolynomial.{v, u} S₁ R[X])) :
          (a : R[X]) → MvPolynomial S₁ R[X])
        Polynomial.X :
      MvPolynomial.{v, u} S₁ R[X])
⊢ Eq (α := MvPolynomial.{v, u} S₁ R[X] →ₐ[R] MvPolynomial.{v, u} S₁ R[X])
    (AlgHom.comp (B := MvPolynomial.{v, u} (Option S₁) R)
      (aeval fun (o : Option S₁) ↦ o.elim ((C : (a : R[X]) → MvPolynomial S₁ R[X]) Polynomial.X) X)
      (aevalTower (Polynomial.aeval (X none)) fun (i : S₁) ↦ X (Option.some i)))
    (AlgHom.id R (MvPolynomial.{v, u} S₁ R[X]))
have h₂ : ∀ (i : S₁) (m : S₁ →₀ ℕ),
  Eq.{u + 1} (α := R[X])
    (coeff m
      ((AlgHom.comp (B := MvPolynomial.{v, u} (Option S₁) R)
            (aeval fun (o : Option S₁) ↦ o.elim ((C : (a : R[X]) → MvPolynomial S₁ R[X]) Polynomial.X) X)
            (aevalTower (Polynomial.aeval (X none)) fun (i : S₁) ↦ X (Option.some i)) :
          (a : MvPolynomial S₁ R[X]) → MvPolynomial S₁ R[X])
        (X i)))
    (coeff m ((AlgHom.id R (MvPolynomial.{v, u} S₁ R[X]) : (a : MvPolynomial S₁ R[X]) → MvPolynomial S₁ R[X]) (X i)))
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
⊢ Eq (α := MvPolynomial.{v, u} (Option S₁) R →ₐ[R] MvPolynomial.{v, u} (Option S₁) R)
    (AlgHom.comp (B := MvPolynomial.{v, u} S₁ R[X])
      (aevalTower (Polynomial.aeval (X none)) fun (i : S₁) ↦ X (Option.some i))
      (aeval fun (o : Option S₁) ↦ o.elim ((C : (a : R[X]) → MvPolynomial S₁ R[X]) Polynomial.X) X))
    (AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R))
have hf : ∀ (m : Option S₁ →₀ ℕ),
  Eq.{u + 1} (α := R)
    (coeff m
      ((AlgHom.comp (B := MvPolynomial.{v, u} S₁ R[X])
            (aevalTower (Polynomial.aeval (X none)) fun (i : S₁) ↦ X (Option.some i))
            (aeval fun (o : Option S₁) ↦ o.elim ((C : (a : R[X]) → MvPolynomial S₁ R[X]) Polynomial.X) X) :
          (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X none)))
    (coeff m
      ((AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R) : (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X none)))
Tactic: ext ⟨i⟩ : 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst : CommSemiring R
hf :
  ∀ (m : Option S₁ →₀ ℕ),
    Eq.{u + 1} (α := R)
      (coeff m
        ((AlgHom.comp (B := MvPolynomial.{v, u} S₁ R[X])
              (aevalTower (Polynomial.aeval (X none)) fun (i : S₁) ↦ X (Option.some i))
              (aeval fun (o : Option S₁) ↦ o.elim ((C : (a : R[X]) → MvPolynomial S₁ R[X]) Polynomial.X) X) :
            (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
          (X none)))
      (coeff m
        ((AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R) :
            (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
          (X none)))
⊢ Eq (α := MvPolynomial.{v, u} (Option S₁) R →ₐ[R] MvPolynomial.{v, u} (Option S₁) R)
    (AlgHom.comp (B := MvPolynomial.{v, u} S₁ R[X])
      (aevalTower (Polynomial.aeval (X none)) fun (i : S₁) ↦ X (Option.some i))
      (aeval fun (o : Option S₁) ↦ o.elim ((C : (a : R[X]) → MvPolynomial S₁ R[X]) Polynomial.X) X))
    (AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R))
have hf₁ : ∀ (val : S₁) (m : Option S₁ →₀ ℕ),
  Eq.{u + 1} (α := R)
    (coeff m
      ((AlgHom.comp (B := MvPolynomial.{v, u} S₁ R[X])
            (aevalTower (Polynomial.aeval (X none)) fun (i : S₁) ↦ X (Option.some i))
            (aeval fun (o : Option S₁) ↦ o.elim ((C : (a : R[X]) → MvPolynomial S₁ R[X]) Polynomial.X) X) :
          (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X (Option.some val))))
    (coeff m
      ((AlgHom.id R (MvPolynomial.{v, u} (Option S₁) R) : (a : MvPolynomial (Option S₁) R) → MvPolynomial (Option S₁) R)
        (X (Option.some val))))
Tactic: ext ⟨i⟩ : 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
⊢ (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →+* (MvPolynomial (Fin n) R)[X]) =
    eval₂Hom (RingHom.comp Polynomial.C C) fun (i : Fin (n + 1)) ↦
      Fin.cases (motive := fun (x : Fin (n + 1)) ↦ (MvPolynomial (Fin n) R)[X]) Polynomial.X
        (fun (k : Fin n) ↦ (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X]) (X k)) i
have hC : ∀ (i : R),
  Eq (α := (MvPolynomial (Fin n) R)[X])
    ((RingHom.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →+* (MvPolynomial (Fin n) R)[X]) C :
          (a : R) → (MvPolynomial (Fin n) R)[X])
        i :
      (MvPolynomial (Fin n) R)[X])
    ((RingHom.comp (β := MvPolynomial (Fin (n + 1)) R)
            (eval₂Hom (RingHom.comp Polynomial.C C) fun (i : Fin (n + 1)) ↦
              Fin.cases (motive := fun (x : Fin (n + 1)) ↦ (MvPolynomial (Fin n) R)[X]) Polynomial.X
                (fun (k : Fin n) ↦ (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X]) (X k)) i)
            C :
          (a : R) → (MvPolynomial (Fin n) R)[X])
        i :
      (MvPolynomial (Fin n) R)[X])
Tactic: ext i : 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
hC :
  ∀ (i : R),
    Eq (α := (MvPolynomial (Fin n) R)[X])
      ((RingHom.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →+* (MvPolynomial (Fin n) R)[X]) C :
            (a : R) → (MvPolynomial (Fin n) R)[X])
          i :
        (MvPolynomial (Fin n) R)[X])
      ((RingHom.comp (β := MvPolynomial (Fin (n + 1)) R)
              (eval₂Hom (RingHom.comp Polynomial.C C) fun (i : Fin (n + 1)) ↦
                Fin.cases (motive := fun (x : Fin (n + 1)) ↦ (MvPolynomial (Fin n) R)[X]) Polynomial.X
                  (fun (k : Fin n) ↦ (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X]) (X k))
                  i)
              C :
            (a : R) → (MvPolynomial (Fin n) R)[X])
          i :
        (MvPolynomial (Fin n) R)[X])
⊢ (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →+* (MvPolynomial (Fin n) R)[X]) =
    eval₂Hom (RingHom.comp Polynomial.C C) fun (i : Fin (n + 1)) ↦
      Fin.cases (motive := fun (x : Fin (n + 1)) ↦ (MvPolynomial (Fin n) R)[X]) Polynomial.X
        (fun (k : Fin n) ↦ (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X]) (X k)) i
have hX : ∀ (i : Fin (n + 1)) (n_1 : ℕ),
  Eq.{u + 1} (α := MvPolynomial (Fin n) R)
    (Polynomial.coeff
      (((↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →+* (MvPolynomial (Fin n) R)[X]) :
          (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        (X i))
      n_1)
    (Polynomial.coeff
      ((eval₂Hom (RingHom.comp Polynomial.C C) fun (i : Fin (n + 1)) ↦
            Fin.cases (motive := fun (x : Fin (n + 1)) ↦ (MvPolynomial (Fin n) R)[X]) Polynomial.X
              (fun (k : Fin n) ↦ (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X]) (X k)) i :
          (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        (X i))
      n_1)
Tactic: ext i : 2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
i : R
⊢ Eq (α := (MvPolynomial (Fin n) R)[X])
    ((RingHom.comp (↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →+* (MvPolynomial (Fin n) R)[X]) C :
          (a : R) → (MvPolynomial (Fin n) R)[X])
        i :
      (MvPolynomial (Fin n) R)[X])
    ((RingHom.comp (β := MvPolynomial (Fin (n + 1)) R)
            (eval₂Hom (RingHom.comp Polynomial.C C) fun (i : Fin (n + 1)) ↦
              Fin.cases (motive := fun (x : Fin (n + 1)) ↦ (MvPolynomial (Fin n) R)[X]) Polynomial.X
                (fun (k : Fin n) ↦ (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X]) (X k)) i)
            C :
          (a : R) → (MvPolynomial (Fin n) R)[X])
        i :
      (MvPolynomial (Fin n) R)[X])
have hC : Eq (α := (MvPolynomial (Fin n) R)[X])
  ((algebraMap R (MvPolynomial (Fin n) R)[X] : (a : R) → (MvPolynomial (Fin n) R)[X]) i : (MvPolynomial (Fin n) R)[X])
  ((Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X])
      ((C : (a : R) → MvPolynomial (Fin n) R) i) :
    (MvPolynomial (Fin n) R)[X])
Tactic: simp only [finSuccEquiv, optionEquivLeft_apply, aeval_C, AlgEquiv.coe_trans, RingHom.coe_coe,
      coe_eval₂Hom, comp_apply, renameEquiv_apply, eval₂_C, RingHom.coe_comp, rename_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
i : Fin (n + 1)
n_1 : ℕ
⊢ Eq.{u + 1} (α := MvPolynomial (Fin n) R)
    (Polynomial.coeff
      (((↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →+* (MvPolynomial (Fin n) R)[X]) :
          (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        (X i))
      n_1)
    (Polynomial.coeff
      ((eval₂Hom (RingHom.comp Polynomial.C C) fun (i : Fin (n + 1)) ↦
            Fin.cases (motive := fun (x : Fin (n + 1)) ↦ (MvPolynomial (Fin n) R)[X]) Polynomial.X
              (fun (k : Fin n) ↦ (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X]) (X k)) i :
          (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        (X i))
      n_1)
have hX : Eq.{u + 1} (α := MvPolynomial (Fin n) R)
  (Polynomial.coeff
    (((↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →+* (MvPolynomial (Fin n) R)[X]) :
        (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
      (X 0))
    n_1)
  (Polynomial.coeff
    ((eval₂Hom (RingHom.comp Polynomial.C C) fun (i : Fin (n + 1)) ↦
          Fin.cases (motive := fun (x : Fin (n + 1)) ↦ (MvPolynomial (Fin n) R)[X]) Polynomial.X
            (fun (k : Fin n) ↦ (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X]) (X k)) i :
        (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
      (X 0))
    n_1)
Tactic: refine Fin.cases ?_ ?_ i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
i : Fin (n + 1)
n_1 : ℕ
hX :
  Eq.{u + 1} (α := MvPolynomial (Fin n) R)
    (Polynomial.coeff
      (((↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →+* (MvPolynomial (Fin n) R)[X]) :
          (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        (X 0))
      n_1)
    (Polynomial.coeff
      ((eval₂Hom (RingHom.comp Polynomial.C C) fun (i : Fin (n + 1)) ↦
            Fin.cases (motive := fun (x : Fin (n + 1)) ↦ (MvPolynomial (Fin n) R)[X]) Polynomial.X
              (fun (k : Fin n) ↦ (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X]) (X k)) i :
          (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        (X 0))
      n_1)
⊢ Eq.{u + 1} (α := MvPolynomial (Fin n) R)
    (Polynomial.coeff
      (((↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →+* (MvPolynomial (Fin n) R)[X]) :
          (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        (X i))
      n_1)
    (Polynomial.coeff
      ((eval₂Hom (RingHom.comp Polynomial.C C) fun (i : Fin (n + 1)) ↦
            Fin.cases (motive := fun (x : Fin (n + 1)) ↦ (MvPolynomial (Fin n) R)[X]) Polynomial.X
              (fun (k : Fin n) ↦ (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X]) (X k)) i :
          (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        (X i))
      n_1)
have hX₁ : ∀ (i : Fin n),
  Eq.{u + 1} (α := MvPolynomial (Fin n) R)
    (Polynomial.coeff
      (((↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →+* (MvPolynomial (Fin n) R)[X]) :
          (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        (X i.succ))
      n_1)
    (Polynomial.coeff
      ((eval₂Hom (RingHom.comp Polynomial.C C) fun (i : Fin (n + 1)) ↦
            Fin.cases (motive := fun (x : Fin (n + 1)) ↦ (MvPolynomial (Fin n) R)[X]) Polynomial.X
              (fun (k : Fin n) ↦ (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X]) (X k)) i :
          (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        (X i.succ))
      n_1)
Tactic: refine Fin.cases ?_ ?_ i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
⊢ Eq (α := (MvPolynomial (Fin n) R)[X])
    ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) p :
      (MvPolynomial (Fin n) R)[X])
    ((eval₂Hom (RingHom.comp Polynomial.C C) fun (i : Fin (n + 1)) ↦
            Fin.cases (motive := fun (x : Fin (n + 1)) ↦ (MvPolynomial (Fin n) R)[X]) Polynomial.X
              (fun (k : Fin n) ↦ (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X]) (X k)) i :
          (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        p :
      (MvPolynomial (Fin n) R)[X])
have rw : Eq (α := (MvPolynomial (Fin n) R)[X])
  ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) p :
    (MvPolynomial (Fin n) R)[X])
  (((↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →+* (MvPolynomial (Fin n) R)[X]) :
        (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
      p :
    (MvPolynomial (Fin n) R)[X])
Tactic: rw [← finSuccEquiv_eq, RingHom.coe_coe]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
rw :
  Eq (α := (MvPolynomial (Fin n) R)[X])
    ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) p :
      (MvPolynomial (Fin n) R)[X])
    (((↑(finSuccEquiv R n) : MvPolynomial (Fin (n + 1)) R →+* (MvPolynomial (Fin n) R)[X]) :
          (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        p :
      (MvPolynomial (Fin n) R)[X])
⊢ Eq (α := (MvPolynomial (Fin n) R)[X])
    ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) p :
      (MvPolynomial (Fin n) R)[X])
    ((eval₂Hom (RingHom.comp Polynomial.C C) fun (i : Fin (n + 1)) ↦
            Fin.cases (motive := fun (x : Fin (n + 1)) ↦ (MvPolynomial (Fin n) R)[X]) Polynomial.X
              (fun (k : Fin n) ↦ (Polynomial.C : (a : MvPolynomial (Fin n) R) → (MvPolynomial (Fin n) R)[X]) (X k)) i :
          (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X])
        p :
      (MvPolynomial (Fin n) R)[X])
have rw₁ : Eq (α := (MvPolynomial (Fin n) R)[X])
  ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) p :
    (MvPolynomial (Fin n) R)[X])
  ((finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → (MvPolynomial (Fin n) R)[X]) p :
    (MvPolynomial (Fin n) R)[X])
Tactic: rw [← finSuccEquiv_eq, RingHom.coe_coe]