awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : R[X]
r : R
f g : PolynomialModule R M
e₁ :
  Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) f : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) f : M)
e₂ :
  Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) g : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) g : M)
add :
  HAdd.hAdd (α := M) (β := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) f : M)
      ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) g : M) =
    HAdd.hAdd (α := M) (β := M) ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) f : M)
      ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) g : M)
add₁ :
  HAdd.hAdd (α := M) (β := M) ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) f : M)
      ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) g : M) =
    HAdd.hAdd (α := M) (β := M) ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) f : M)
      ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) g : M)
⊢ Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) (f + g) : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) (f + g) : M)

Tactic:
simp_rw [map_add, e₁, e₂]

Premises used: map_add
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : R[X]
r : R
i : ℕ
m : M
single : Polynomial.eval r p ^ i • HPow.hPow (β := ℕ) r 0 • m = Polynomial.eval r p ^ i • m
⊢ Eq (α := M)
    ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M)
        ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
      M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M)
        ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
      M)

Tactic:
rw [LinearMap.comp_apply, comp_single, eval_single, eval_smul, eval_single, eval_pow]

Premises used: PolynomialModule.comp_single, Polynomial.eval_pow, LinearMap.comp_apply, PolynomialModule.eval_smul, PolynomialModule.eval_single
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : R[X]
r : R
i : ℕ
m : M
⊢ Polynomial.eval r p ^ i • HPow.hPow (β := ℕ) r 0 • m = Polynomial.eval r p ^ i • m

Tactic:
module
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : R[X]
q : PolynomialModule R M
r : R
zero :
  Eq.{u_2 + 1} (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) 0 : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) 0 : M)
add :
  ∀ (f g : PolynomialModule R M)
    (e₁ :
      Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) f : M)
        ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) f : M))
    (e₂ :
      Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) g : M)
        ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) g : M)),
    Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) (f + g) : M)
      ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) (f + g) : M)
single :
  ∀ (i : ℕ) (m : M),
    Eq (α := M)
      ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M)
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
      ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M)
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
        M)
⊢ Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) q : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) q : M)

Tactic:
induction q using induction_linear with
  | zero => simp_rw [map_zero]
  | add _ _ e₁ e₂ => simp_rw [map_add, e₁, e₂]
  | single i m =>
    rw [LinearMap.comp_apply, comp_single, eval_single, eval_smul, eval_single, eval_pow]
    module

Premises used: PolynomialModule.comp_single, Polynomial.eval_pow, LinearMap.comp_apply, map_zero, PolynomialModule.single, map_add, PolynomialModule.eval_smul, PolynomialModule.eval_single
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : R[X]
q : PolynomialModule R M
rw :
  HSMul.hSMul (β := PolynomialModule R M) (eval₂ (algebraMap R R[X]) p p')
      ((eval p : (a : PolynomialModule R[X] (PolynomialModule R M)) → PolynomialModule R M)
          ((map R[X] (lsingle R 0) : (a : PolynomialModule R M) → PolynomialModule R[X] (PolynomialModule R M)) q) :
        PolynomialModule R M) =
    HSMul.hSMul (β := PolynomialModule R M) (eval₂ C p p')
      ((eval p : (a : PolynomialModule R[X] (PolynomialModule R M)) → PolynomialModule R M)
          ((map R[X] (lsingle R 0) : (a : PolynomialModule R M) → PolynomialModule R[X] (PolynomialModule R M)) q) :
        PolynomialModule R M)
⊢ (comp p : (a : PolynomialModule R M) → PolynomialModule R M) (p' • q) =
    HSMul.hSMul (β := PolynomialModule R M) (p'.comp p)
      ((comp p : (a : PolynomialModule R M) → PolynomialModule R M) q : PolynomialModule R M)

Tactic:
rw [comp_apply, map_smul, eval_smul, Polynomial.comp, Polynomial.eval_map, comp_apply]

Premises used: PolynomialModule.map_smul, Polynomial.eval_map, PolynomialModule.comp_apply, PolynomialModule.eval_smul, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : R[X]
q : PolynomialModule R M
⊢ HSMul.hSMul (β := PolynomialModule R M) (eval₂ (algebraMap R R[X]) p p')
      ((eval p : (a : PolynomialModule R[X] (PolynomialModule R M)) → PolynomialModule R M)
          ((map R[X] (lsingle R 0) : (a : PolynomialModule R M) → PolynomialModule R[X] (PolynomialModule R M)) q) :
        PolynomialModule R M) =
    HSMul.hSMul (β := PolynomialModule R M) (eval₂ C p p')
      ((eval p : (a : PolynomialModule R[X] (PolynomialModule R M)) → PolynomialModule R M)
          ((map R[X] (lsingle R 0) : (a : PolynomialModule R M) → PolynomialModule R[X] (PolynomialModule R M)) q) :
        PolynomialModule R M)

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Module.FiniteDimensional
Goal:
R : Type u_1
M : Type u_3
A : Type u_4
a : A
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : AddCommMonoid M
inst_5 : Module A M
inst_6 : Module R M
inst_7 : IsScalarTower R A M
p : R[X]
h : Eq.{u_4 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
h' : p ≠ 0
⊢ Membership.mem (γ := Submonoid R[X]) (nonZeroDivisors R[X]) p

Tactic:
have hp : p ∈ nonZeroDivisors R[X] := mem_nonZeroDivisors_iff_right.mpr
    fun q hq ↦ Or.resolve_right (mul_eq_zero.mp hq) h'
-- Module: Mathlib.Algebra.Polynomial.Module.FiniteDimensional
Goal:
R : Type u_1
M : Type u_3
A : Type u_4
a : A
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : AddCommMonoid M
inst_5 : Module A M
inst_6 : Module R M
inst_7 : IsScalarTower R A M
p : R[X]
h : Eq.{u_4 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
h' : p ≠ 0
hp : Membership.mem (γ := Submonoid R[X]) (nonZeroDivisors R[X]) p
x : AEval R M a
⊢ Eq (α := M)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
        (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) (nonZeroDivisors R[X]) x) p hp • x) :
      M)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) 0 : M)

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Module.FiniteDimensional
Goal:
R : Type u_1
M : Type u_3
A : Type u_4
a : A
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : AddCommMonoid M
inst_5 : Module A M
inst_6 : Module R M
inst_7 : IsScalarTower R A M
p : R[X]
h : Eq.{u_4 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
h' : p ≠ 0
hp : Membership.mem (γ := Submonoid R[X]) (nonZeroDivisors R[X]) p
⊢ IsTorsion.{u_1, u_3} R[X] (AEval R M a)

Tactic:
exact fun x ↦ ⟨⟨p, hp⟩, (of R M a).symm.injective <| by simp [h]⟩
-- Module: Mathlib.Algebra.Polynomial.Module.FiniteDimensional
Goal:
K : Type u_2
M : Type u_3
A : Type u_4
a : A
inst : Field K
inst_1 : Ring A
inst_2 : Algebra K A
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module K M
inst_6 : IsScalarTower K A M
inst_7 : FiniteDimensional K A
⊢ IsTorsion.{u_2, u_3} K[X] (AEval K M a)

Tactic:
isTorsion_of_aeval_eq_zero (minpoly.aeval K a) (minpoly.ne_zero_of_finite K a)

Premises used: Set.Mem, setOf, Module.AEval.isTorsion_of_aeval_eq_zero, minpoly.ne_zero_of_finite, minpoly.aeval
-- Module: Mathlib.Algebra.Polynomial.Module.TensorProduct
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
e : LinearMap (R := R[X]) (RingHom.id R[X]) (R[X] ⊗[R] M) (PolynomialModule R M) := liftBaseChange R[X] (lsingle R 0)
inv : PolynomialModule R M →ₗ[R] R[X] ⊗[R] M :=
  (↑R :
        {S : Type u_1} →
          {M M₂ : Type (max u_1 u_2)} →
            [inst : Semiring R] →
              [inst_3 : Semiring S] →
                [inst_4 : AddCommMonoid M] →
                  [inst_5 : AddCommMonoid M₂] →
                    [inst_6 : Module R M] →
                      [inst_7 : Module R M₂] →
                        [inst_8 : Module S M] →
                          [inst_9 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (eval X) ∘ₗ
    map R[X] ((TensorProduct.mk R R[X] M : (a : R[X]) → M →ₗ[R] R[X] ⊗[R] M) 1)
a :
  ∀ (n : ℕ) (x : M),
    Eq (α := R[X] ⊗[R] M)
      ((((AlgebraTensorModule.curry
                      (inv ∘ₗ
                        (↑R :
                            {S : Type u_1} →
                              {M : Type (max u_1 u_2)} →
                                {M₂ : Type u_2} →
                                  [inst : Semiring R] →
                                    [inst_3 : Semiring S] →
                                      [inst_4 : AddCommMonoid M] →
                                        [inst_5 : AddCommMonoid M₂] →
                                          [inst_6 : Module R M] →
                                            [inst_7 : Module R M₂] →
                                              [inst_8 : Module S M] →
                                                [inst_9 : Module S M₂] →
                                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                          e) ∘ₗ
                    monomial n :
                  R →ₗ[R] M →ₗ[R] R[X] ⊗[R] M) :
                (a : R) → M →ₗ[R] R[X] ⊗[R] M)
              1 :
            (a : M) → R[X] ⊗[R] M)
          x :
        R[X] ⊗[R] M)
      ((((AlgebraTensorModule.curry LinearMap.id ∘ₗ monomial n : R →ₗ[R] M →ₗ[R] R[X] ⊗[R] M) :
                (a : R) → M →ₗ[R] R[X] ⊗[R] M)
              1 :
            (a : M) → R[X] ⊗[R] M)
          x :
        R[X] ⊗[R] M)
⊢ inv ∘ₗ
      (↑R :
          {S : Type u_1} →
            {M : Type (max u_1 u_2)} →
              {M₂ : Type u_2} →
                [inst : Semiring R] →
                  [inst_3 : Semiring S] →
                    [inst_4 : AddCommMonoid M] →
                      [inst_5 : AddCommMonoid M₂] →
                        [inst_6 : Module R M] →
                          [inst_7 : Module R M₂] →
                            [inst_8 : Module S M] →
                              [inst_9 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        e =
    LinearMap.id

Tactic:
ext n x
-- Module: Mathlib.Algebra.Polynomial.Module.TensorProduct
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
e : LinearMap (R := R[X]) (RingHom.id R[X]) (R[X] ⊗[R] M) (PolynomialModule R M) := liftBaseChange R[X] (lsingle R 0)
inv : PolynomialModule R M →ₗ[R] R[X] ⊗[R] M :=
  (↑R :
        {S : Type u_1} →
          {M M₂ : Type (max u_1 u_2)} →
            [inst : Semiring R] →
              [inst_3 : Semiring S] →
                [inst_4 : AddCommMonoid M] →
                  [inst_5 : AddCommMonoid M₂] →
                    [inst_6 : Module R M] →
                      [inst_7 : Module R M₂] →
                        [inst_8 : Module S M] →
                          [inst_9 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (eval X) ∘ₗ
    map R[X] ((TensorProduct.mk R R[X] M : (a : R[X]) → M →ₗ[R] R[X] ⊗[R] M) 1)
n : ℕ
x : M
⊢ Eq (α := R[X] ⊗[R] M)
    ((((AlgebraTensorModule.curry
                    (inv ∘ₗ
                      (↑R :
                          {S : Type u_1} →
                            {M : Type (max u_1 u_2)} →
                              {M₂ : Type u_2} →
                                [inst : Semiring R] →
                                  [inst_3 : Semiring S] →
                                    [inst_4 : AddCommMonoid M] →
                                      [inst_5 : AddCommMonoid M₂] →
                                        [inst_6 : Module R M] →
                                          [inst_7 : Module R M₂] →
                                            [inst_8 : Module S M] →
                                              [inst_9 : Module S M₂] →
                                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                        e) ∘ₗ
                  monomial n :
                R →ₗ[R] M →ₗ[R] R[X] ⊗[R] M) :
              (a : R) → M →ₗ[R] R[X] ⊗[R] M)
            1 :
          (a : M) → R[X] ⊗[R] M)
        x :
      R[X] ⊗[R] M)
    ((((AlgebraTensorModule.curry LinearMap.id ∘ₗ monomial n : R →ₗ[R] M →ₗ[R] R[X] ⊗[R] M) :
              (a : R) → M →ₗ[R] R[X] ⊗[R] M)
            1 :
          (a : M) → R[X] ⊗[R] M)
        x :
      R[X] ⊗[R] M)

Tactic:
simp [inv, e, ← monomial_one_right_eq_X_pow, smul_tmul']

Premises used: TensorProduct.smul_tmul', Polynomial.monomial_one_right_eq_X_pow
-- Module: Mathlib.Algebra.Polynomial.Module.TensorProduct
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
e : LinearMap (R := R[X]) (RingHom.id R[X]) (R[X] ⊗[R] M) (PolynomialModule R M) := liftBaseChange R[X] (lsingle R 0)
inv : PolynomialModule R M →ₗ[R] R[X] ⊗[R] M :=
  (↑R :
        {S : Type u_1} →
          {M M₂ : Type (max u_1 u_2)} →
            [inst : Semiring R] →
              [inst_3 : Semiring S] →
                [inst_4 : AddCommMonoid M] →
                  [inst_5 : AddCommMonoid M₂] →
                    [inst_6 : Module R M] →
                      [inst_7 : Module R M₂] →
                        [inst_8 : Module S M] →
                          [inst_9 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (eval X) ∘ₗ
    map R[X] ((TensorProduct.mk R R[X] M : (a : R[X]) → M →ₗ[R] R[X] ⊗[R] M) 1)
left :
  inv ∘ₗ
      (↑R :
          {S : Type u_1} →
            {M : Type (max u_1 u_2)} →
              {M₂ : Type u_2} →
                [inst : Semiring R] →
                  [inst_3 : Semiring S] →
                    [inst_4 : AddCommMonoid M] →
                      [inst_5 : AddCommMonoid M₂] →
                        [inst_6 : Module R M] →
                          [inst_7 : Module R M₂] →
                            [inst_8 : Module S M] →
                              [inst_9 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        e =
    LinearMap.id
n : ℕ
x : M
⊢ Eq (α := PolynomialModule R M)
    ((((↑R :
                  {S : Type u_1} →
                    {M : Type (max u_1 u_2)} →
                      {M₂ : Type u_2} →
                        [inst : Semiring R] →
                          [inst_3 : Semiring S] →
                            [inst_4 : AddCommMonoid M] →
                              [inst_5 : AddCommMonoid M₂] →
                                [inst_6 : Module R M] →
                                  [inst_7 : Module R M₂] →
                                    [inst_8 : Module S M] →
                                      [inst_9 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                e ∘ₗ
              inv) ∘ₗ
            lsingle R n :
          (a : M) → PolynomialModule R M)
        x :
      PolynomialModule R M)
    ((LinearMap.id ∘ₗ lsingle R n : (a : M) → PolynomialModule R M) x : PolynomialModule R M)

Tactic:
simp [e, inv, ← monomial_one_right_eq_X_pow]

Premises used: Polynomial.monomial_one_right_eq_X_pow
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
⊢ Monic.{u} (R := R) 0 ↔ Subsingleton R

Tactic:
subsingleton_iff_zero_eq_one

Premises used: Polynomial.leadingCoeff, Polynomial.coeff, Polynomial.Monic, subsingleton_iff_zero_eq_one
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
⊢ ¬Monic.{u} (R := R) 0 ↔ Ne.{u + 1} (α := R) 0 1

Tactic:
(monic_zero_iff_subsingleton.trans subsingleton_iff_zero_eq_one.symm).not

Premises used: Iff.not, Iff.trans, subsingleton_iff_zero_eq_one, Polynomial.monic_zero_iff_subsingleton, Iff.symm
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
h : Subsingleton R
⊢ (∀ (f g : R[X]), f = g) ∧ ∀ (a b : R), a = b

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
rw :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) +
    ∑ x ∈ range p.natDegree, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x)
| p

Tactic:
rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]

Premises used: Finset.sum_range_succ_comm, Polynomial.as_sum_range_C_mul_X_pow
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
conv_lhs :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) +
      ∑ x ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x) =
    HPow.hPow (α := R[X]) X p.natDegree +
      ∑ i ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)
⊢ p =
    HPow.hPow (α := R[X]) X p.natDegree +
      ∑ i ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)

Tactic:
conv_lhs => rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]

Premises used: Finset.sum_range_succ_comm, Polynomial.as_sum_range_C_mul_X_pow
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
this : Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) (1 : R[X])
rw :
  1 * HPow.hPow (α := R[X]) X p.natDegree +
      ∑ x ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x) =
    HPow.hPow (α := R[X]) X p.natDegree +
      ∑ i ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)
rw₁ rw₂ :
  HPow.hPow (α := R[X]) X p.natDegree +
      ∑ x ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x) =
    HPow.hPow (α := R[X]) X p.natDegree +
      ∑ i ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) +
      ∑ x ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x) =
    HPow.hPow (α := R[X]) X p.natDegree +
      ∑ i ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)

Tactic:
rw [this, one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
suffices : Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) (1 : R[X])
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) +
      ∑ x ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x) =
    HPow.hPow (α := R[X]) X p.natDegree +
      ∑ i ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)

Tactic:
suffices C (p.coeff p.natDegree) = 1 by rw [this, one_mul]
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
⊢ Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) (1 : R[X])

Tactic:
congr_arg C hp

Premises used: Polynomial.C, congr_arg, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
⊢ Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) (1 : R[X])

Tactic:
exact congr_arg C hp

Premises used: Polynomial.C, congr_arg, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
hp : p.Monic
⊢ (Polynomial.map f p).Monic

Tactic:
subsingleton_or_nontrivial S |>.elim (·.elim ..) fun _ ↦
    f.map_one ▸ hp ▸ leadingCoeff_map_eq_of_isUnit_leadingCoeff _ <| isUnit_one

Premises used: subsingleton_or_nontrivial, Polynomial.leadingCoeff, Polynomial.map, Subsingleton.elim, Or.elim, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
⊢ Nontrivial R

Tactic:
nontriviality
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
h : Nontrivial R
rw : leadingCoeff ((C : (a : R) → R[X]) b) * p.leadingCoeff = 1
rw₁ : leadingCoeff ((C : (a : R) → R[X]) b) * p.leadingCoeff ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) p).leadingCoeff = 1

Tactic:
rw [leadingCoeff_mul' _]

Premises used: Polynomial.leadingCoeff_mul'
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
h : Nontrivial R
⊢ leadingCoeff ((C : (a : R) → R[X]) b) * p.leadingCoeff = 1

Tactic:
simp [leadingCoeff_C b, hp]

Premises used: Polynomial.leadingCoeff_C
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
h : Nontrivial R
⊢ leadingCoeff ((C : (a : R) → R[X]) b) * p.leadingCoeff ≠ 0

Tactic:
simp [leadingCoeff_C b, hp]

Premises used: Polynomial.leadingCoeff_C
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
⊢ Nontrivial R

Tactic:
nontriviality
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
h : Nontrivial R
rw : p.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) b) = 1
rw₁ : p.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) b) ≠ 0
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) b : R[X])).leadingCoeff = 1

Tactic:
rw [leadingCoeff_mul' _]

Premises used: Polynomial.leadingCoeff_mul'
-- Module: Mathlib.Algebra.Polynomial.Monic
Goal:
R : Type u
inst : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
h : Nontrivial R
⊢ p.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) b) = 1

Tactic:
simp [leadingCoeff_C b, hp]

Premises used: Polynomial.leadingCoeff_C