awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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)
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))
        σ),
    embDomain Embedding.some σ + Finsupp.single none i ∈ p.support
⊢ totalDegree.{u, v} (R := R) (σ := S₁)
      (Polynomial.coeff ((optionEquivLeft R S₁ : (a : MvPolynomial (Option S₁) R) → (MvPolynomial S₁ R)[X]) p) i) ≤
    p.totalDegree

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σ

Premises used: MvPolynomial.mem_support_iff, Finsupp.sum_embDomain, Polynomial.coeff, MvPolynomial.optionEquivLeft_coeff_some_coeff_none, MvPolynomial.totalDegree, Finset.sup_le_iff, MvPolynomial.optionEquivLeft, Finsupp.sum_add_index, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
m : ℕ
d : σ →₀ ℕ
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)))
⊢ coeff d (Polynomial.coeff ((optionEquivLeft R σ : (a : MvPolynomial (Option σ) R) → (MvPolynomial σ R)[X]) p) m) =
    coeff (optionElim m d) p

Tactic:
rw [← optionEquivLeft_coeff_some_coeff_none]

Premises used: MvPolynomial.optionEquivLeft_coeff_some_coeff_none
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
e_p : m = (optionElim m d : (a : Option σ) → ℕ) none
⊢ 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:
congr
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ d = (optionElim m d).some

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial.{u_1, u} (Option σ) R
m : ℕ
d : σ →₀ ℕ
⊢ m = (optionElim m d : (a : Option σ) → ℕ) none

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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])
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)))
⊢ 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]))

Tactic:
ext : 2
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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])
    ((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:
simp only [MvPolynomial.algebraMap_eq, Option.elim, AlgHom.coe_comp, AlgHom.id_comp,
          IsScalarTower.coe_toAlgHom', comp_apply, aevalTower_C, Polynomial.aeval_X, aeval_X,
          aevalTower_X, AlgHom.coe_id, id]

Premises used: MvPolynomial.aeval_X, IsScalarTower.coe_toAlgHom', AlgHom.coe_id, AlgHom.id_comp, MvPolynomial.aevalTower_X, id, MvPolynomial.aevalTower_C, AlgHom.coe_comp, MvPolynomial.algebraMap_eq, Function.comp_apply, Option.elim, Polynomial.aeval_X
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
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:
simp only [MvPolynomial.algebraMap_eq, Option.elim, AlgHom.coe_comp, AlgHom.id_comp,
          IsScalarTower.coe_toAlgHom', comp_apply, aevalTower_C, Polynomial.aeval_X, aeval_X,
          aevalTower_X, AlgHom.coe_id, id]

Premises used: MvPolynomial.aeval_X, IsScalarTower.coe_toAlgHom', AlgHom.coe_id, AlgHom.id_comp, MvPolynomial.aevalTower_X, id, MvPolynomial.aevalTower_C, AlgHom.coe_comp, MvPolynomial.algebraMap_eq, Function.comp_apply, Option.elim, Polynomial.aeval_X
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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)))
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))))
⊢ 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))

Tactic:
ext ⟨i⟩ : 2
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
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:
simp only [Option.elim, AlgHom.coe_comp, comp_apply, aeval_X, aevalTower_C,
          Polynomial.aeval_X, AlgHom.coe_id, id, aevalTower_X]

Premises used: MvPolynomial.aeval_X, AlgHom.coe_id, MvPolynomial.aevalTower_X, id, MvPolynomial.aevalTower_C, AlgHom.coe_comp, Function.comp_apply, Option.elim, Polynomial.aeval_X
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
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:
simp only [Option.elim, AlgHom.coe_comp, comp_apply, aeval_X, aevalTower_C,
          Polynomial.aeval_X, AlgHom.coe_id, id, aevalTower_X]

Premises used: MvPolynomial.aeval_X, AlgHom.coe_id, MvPolynomial.aevalTower_X, id, MvPolynomial.aevalTower_C, AlgHom.coe_comp, Function.comp_apply, Option.elim, Polynomial.aeval_X
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
x : S₁
⊢ Eq (α := MvPolynomial.{v, u} S₁ R[X])
    ((optionEquivRight R S₁ : (a : MvPolynomial (Option S₁) R) → MvPolynomial S₁ R[X]) (X (Option.some x)) :
      MvPolynomial.{v, u} S₁ R[X])
    (X x : MvPolynomial.{v, u} S₁ R[X])

Tactic:
simp [optionEquivRight_apply, aeval_X]

Premises used: MvPolynomial.aeval_X, MvPolynomial.optionEquivRight_apply
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
⊢ Eq (α := MvPolynomial.{v, u} S₁ R[X])
    ((optionEquivRight R S₁ : (a : MvPolynomial (Option S₁) R) → MvPolynomial S₁ R[X]) (X none) :
      MvPolynomial.{v, u} S₁ R[X])
    ((C : (a : R[X]) → MvPolynomial S₁ R[X]) Polynomial.X : MvPolynomial.{v, u} S₁ R[X])

Tactic:
simp [optionEquivRight_apply, aeval_X]

Premises used: MvPolynomial.aeval_X, MvPolynomial.optionEquivRight_apply
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
r : R
⊢ Eq (α := MvPolynomial.{v, u} S₁ R[X])
    ((optionEquivRight R S₁ : (a : MvPolynomial (Option S₁) R) → MvPolynomial S₁ R[X])
        ((C : (a : R) → MvPolynomial (Option S₁) R) r) :
      MvPolynomial.{v, u} S₁ R[X])
    ((C : (a : R[X]) → MvPolynomial S₁ R[X]) ((Polynomial.C : (a : R) → R[X]) r) : MvPolynomial.{v, u} S₁ R[X])

Tactic:
simp only [optionEquivRight_apply, aeval_C, algebraMap_apply, Polynomial.algebraMap_eq]

Premises used: MvPolynomial.algebraMap_apply, MvPolynomial.optionEquivRight_apply, MvPolynomial.aeval_C, Polynomial.algebraMap_eq
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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])
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)
⊢ (↑(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

Tactic:
ext i : 2
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
i : R
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])
⊢ 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:
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]

Premises used: MvPolynomial.optionEquivLeft_apply, RingHom.coe_coe, MvPolynomial.eval₂_C, MvPolynomial.renameEquiv_apply, MvPolynomial.finSuccEquiv, MvPolynomial.coe_eval₂Hom, MvPolynomial.aeval_C, MvPolynomial.rename_C, RingHom.coe_comp, Function.comp_apply, AlgEquiv.coe_trans
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
i : R
⊢ 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:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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)

Tactic:
Fin.cases ?_ ?_ i

Premises used: Fin.cases
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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)
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)
⊢ 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:
refine Fin.cases ?_ ?_ i
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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 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:
simp [optionEquivLeft_apply, finSuccEquiv]

Premises used: MvPolynomial.optionEquivLeft_apply, MvPolynomial.finSuccEquiv
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
n : ℕ
i : Fin (n + 1)
n_1 : ℕ
⊢ ∀ (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:
simp [optionEquivLeft_apply, finSuccEquiv]

Premises used: MvPolynomial.optionEquivLeft_apply, MvPolynomial.finSuccEquiv