awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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 (α := ℕ) ((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:
Finset.le_sup
    (f := fun (g : Fin (Nat.succ n) →₀ ℕ) => g (Fin.succ j))
    (mem_support_coeff_finSuccEquiv.1 hm)

Premises used: Iff.mp, MvPolynomial.mem_support_coeff_finSuccEquiv, Finset.le_sup
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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 (α := ℕ) ((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:
exact Finset.le_sup
    (f := fun (g : Fin (Nat.succ n) →₀ ℕ) => g (Fin.succ j))
    (mem_support_coeff_finSuccEquiv.1 hm)

Premises used: Iff.mp, MvPolynomial.mem_support_coeff_finSuccEquiv, Finset.le_sup
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial.{u_1, u} (Option σ) R
this :
  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])
⊢ 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])

Tactic:
DFunLike.congr_fun this φ

Premises used: Multiset.sum, Multiset.foldr, DFunLike.congr_fun, Finsupp.sum, MvPolynomial.eval₂, Polynomial.map, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial.{u_1, u} (Option σ) R
this :
  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])
⊢ 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])

Tactic:
exact DFunLike.congr_fun this φ

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial.{u_1, u} (Option σ) R
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])
⊢ 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])

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 φ
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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])
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])
⊢ 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:
apply ringHom_ext

Premises used: MvPolynomial.ringHom_ext
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial.{u_1, u} (Option σ) R
⊢ ∀ (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:
simp [Polynomial.algebraMap_apply, algebraMap_eq, finSuccEquiv_apply, optionEquivLeft_apply]

Premises used: MvPolynomial.optionEquivLeft_apply, Polynomial.algebraMap_apply, MvPolynomial.finSuccEquiv_apply, MvPolynomial.algebraMap_eq
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial.{u_1, u} (Option σ) 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])
        (X none) :
      (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 none) :
      (MvPolynomial (Fin n) R)[X])

Tactic:
simp [finSuccEquiv_apply, optionEquivLeft_apply]

Premises used: MvPolynomial.optionEquivLeft_apply, MvPolynomial.finSuccEquiv_apply
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial.{u_1, u} (Option σ) R
i : σ
⊢ 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 (Option.some 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 (Option.some i)) :
      (MvPolynomial (Fin n) R)[X])

Tactic:
simp [finSuccEquiv_apply, optionEquivLeft_apply]

Premises used: MvPolynomial.optionEquivLeft_apply, MvPolynomial.finSuccEquiv_apply
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [← aeval_algHom_apply, rename_X]

Premises used: MvPolynomial.rename_X, Polynomial.aeval_algHom_apply
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_1
σ : Type u_3
inst : CommSemiring R
i : σ
r : R
⊢ Eq (α := MvPolynomial σ R)
    ((toMvPolynomial i : (a : R[X]) → MvPolynomial σ R) ((C : (a : R) → R[X]) r) : MvPolynomial σ R)
    ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)

Tactic:
simp [toMvPolynomial]

Premises used: Polynomial.toMvPolynomial
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_1
σ : Type u_3
inst : CommSemiring R
i : σ
⊢ Eq (α := MvPolynomial σ R) ((toMvPolynomial i : (a : R[X]) → MvPolynomial σ R) X : MvPolynomial σ R)
    (MvPolynomial.X i : MvPolynomial σ R)

Tactic:
simp [toMvPolynomial]

Premises used: Polynomial.toMvPolynomial
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_1
σ : Type u_3
inst : CommSemiring R
i : σ
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))
⊢ 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))

Tactic:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_1
σ : Type u_3
inst : CommSemiring R
i : σ
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:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_1
σ : Type u_3
inst : CommSemiring R
i : σ
simp :
  Injective (α := MvPolynomial Unit R) (β := MvPolynomial σ R)
    (⇑(MvPolynomial.rename fun (x : Unit) ↦ i) : (a : MvPolynomial Unit R) → MvPolynomial σ R)
⊢ Injective (α := R[X]) (β := MvPolynomial σ R) (⇑(toMvPolynomial i) : (a : R[X]) → MvPolynomial σ R)

Tactic:
simp only [toMvPolynomial_eq_rename_comp, AlgHom.coe_comp, AlgEquiv.coe_algHom,
    EquivLike.injective_comp]

Premises used: EquivLike.injective_comp, Polynomial.toMvPolynomial_eq_rename_comp, AlgHom.coe_comp, AlgEquiv.coe_algHom
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_1
σ : Type u_3
inst : CommSemiring R
i : σ
⊢ Injective (α := MvPolynomial Unit R) (β := MvPolynomial σ R)
    (⇑(MvPolynomial.rename fun (x : Unit) ↦ i) : (a : MvPolynomial Unit R) → MvPolynomial σ R)

Tactic:
MvPolynomial.rename_injective (fun x ↦ i) fun _ _ _ ↦ rfl

Premises used: MvPolynomial.rename_injective, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_1
σ : Type u_3
inst : CommSemiring R
i : σ
⊢ Injective (α := MvPolynomial Unit R) (β := MvPolynomial σ R)
    (⇑(MvPolynomial.rename fun (x : Unit) ↦ i) : (a : MvPolynomial Unit R) → MvPolynomial σ R)

Tactic:
exact MvPolynomial.rename_injective (fun x ↦ i) fun _ _ _ ↦ rfl

Premises used: MvPolynomial.rename_injective
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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)
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)
⊢ RingHom.comp (eval f) (↑(toMvPolynomial i) : R[X] →+* MvPolynomial σ R) = evalRingHom (f i)

Tactic:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_1
σ : Type u_3
inst : CommSemiring R
f : σ → R
i : σ
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:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_1
σ : Type u_3
inst : CommSemiring R
f : σ → R
i : σ
⊢ 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:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_1
σ : Type u_3
inst : CommSemiring R
f : σ → R
i : σ
p : R[X]
⊢ (eval f : (a : MvPolynomial σ R) → R) ((toMvPolynomial i : (a : R[X]) → MvPolynomial σ R) p : MvPolynomial σ R) =
    Polynomial.eval (f i) p

Tactic:
DFunLike.congr_fun (eval_comp_toMvPolynomial ..) p

Premises used: Multiset.sum, Polynomial.eval, Multiset.foldr, DFunLike.congr_fun, MvPolynomial.eval_comp_toMvPolynomial, Finsupp.sum, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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 : σ
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)
⊢ Eq (α := R[X] →ₐ[R] S) (AlgHom.comp (aeval f) (toMvPolynomial i)) (Polynomial.aeval (f i))

Tactic:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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.{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:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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 : σ
p : R[X]
⊢ Eq.{u_2 + 1} (α := S)
    ((aeval f : (a : MvPolynomial σ R) → S) ((toMvPolynomial i : (a : R[X]) → MvPolynomial σ R) p : MvPolynomial σ R) :
      S)
    ((Polynomial.aeval (f i) : (a : R[X]) → S) p : S)

Tactic:
DFunLike.congr_fun (aeval_comp_toMvPolynomial ..) p

Premises used: Multiset.sum, Multiset.foldr, DFunLike.congr_fun, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.aeval_comp_toMvPolynomial, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_1
σ : Type u_3
τ : Type u_4
inst : CommSemiring R
f : σ → τ
a : σ
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))
⊢ Eq (α := R[X] →ₐ[R] MvPolynomial τ R) (AlgHom.comp (rename f) (toMvPolynomial a)) (toMvPolynomial (f a))

Tactic:
ext
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_1
σ : Type u_3
τ : Type u_4
inst : CommSemiring R
f : σ → τ
a : σ
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:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u_1
σ : Type u_3
τ : Type u_4
inst : CommSemiring R
f : σ → τ
a : σ
p : R[X]
⊢ Eq (α := MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((toMvPolynomial a : (a : R[X]) → MvPolynomial σ R) p) :
      MvPolynomial τ R)
    ((toMvPolynomial (f a) : (a : R[X]) → MvPolynomial τ R) p : MvPolynomial τ R)

Tactic:
DFunLike.congr_fun (rename_comp_toMvPolynomial ..) p

Premises used: Multiset.sum, Multiset.foldr, DFunLike.congr_fun, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.rename_comp_toMvPolynomial, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
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 ∈ d.support, HPow.hPow (β := ℕ) (X i) ((d : (a : σ) → ℕ) i : ℕ) : S₁)

Tactic:
rfl

Premises used: Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.support, MvPolynomial.coeff, Finsupp.prod, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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
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₁))
⊢ 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₁)

Tactic:
simp only [eval₂_eq, ← Finsupp.prod_pow]

Premises used: Finsupp.prod_pow, MvPolynomial.eval₂_eq
-- Module: Mathlib.Algebra.MvPolynomial.Eval
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
⊢ 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:
rfl
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
⊢ eval₂ f g 0 = 0

Tactic:
Finsupp.sum_zero_index

Premises used: MvPolynomial.eval₂, AddMonoidAlgebra.coeff, Finsupp.sum_zero_index
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ a ∈ p.support ∪ q.support,
    HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) 0 : S₁) (a.prod fun (n : σ) (e : ℕ) ↦ g n ^ e : S₁) = 0

Tactic:
simp [f.map_zero]

Premises used: RingHom.map_zero
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ ∀ a ∈ p.support ∪ q.support,
    ∀ (b₁ b₂ : R),
      HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) (b₁ + b₂) : S₁) (a.prod fun (n : σ) (e : ℕ) ↦ g n ^ e : S₁) =
        HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) b₁ : S₁) (a.prod fun (n : σ) (e : ℕ) ↦ g n ^ e : S₁) +
          HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) b₂ : S₁) (a.prod fun (n : σ) (e : ℕ) ↦ g n ^ e : S₁)

Tactic:
simp [add_mul, f.map_add]

Premises used: add_mul, RingHom.map_add
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ eval₂ f g (p + q) = eval₂ f g p + eval₂ f g q

Tactic:
exact Finsupp.sum_add_index (by simp [f.map_zero]) (by simp [add_mul, f.map_add])

Premises used: Finsupp.sum_add_index
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
p q : MvPolynomial σ R
f : R →+* S₁
g : σ → S₁
⊢ eval₂ f g (p + q) = eval₂ f g p + eval₂ f g q

Tactic:
classical exact Finsupp.sum_add_index (by simp [f.map_zero]) (by simp [add_mul, f.map_add])

Premises used: Finsupp.sum_add_index
-- Module: Mathlib.Algebra.MvPolynomial.Eval
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
a : R
s : σ →₀ ℕ
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
⊢ HMul.hMul (α := S₁) (β := S₁) ((f : (a : R) → S₁) 0 : S₁) (s.prod fun (n : σ) (e : ℕ) ↦ g n ^ e : S₁) = 0

Tactic:
simp [f.map_zero]

Premises used: RingHom.map_zero