awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Eval.SMul
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p : R[X]
x : R
rw : eval x (HSMul.hSMul (β := R) s 1 • p) = s • eval x p
rw₁ : eval₂ (RingHom.id R) x (HSMul.hSMul (β := R) s 1 • p) = s • eval x p
rw₂ :
  HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) (HSMul.hSMul (β := R) s 1) : R) (eval₂ (RingHom.id R) x p) =
    s • eval x p
rw₃ : HSMul.hSMul (β := R) s 1 * eval₂ (RingHom.id R) x p = s • eval x p
rw₄ : s • eval₂ (RingHom.id R) x p = s • eval x p
rw₅ rw₆ : s • eval x p = s • eval x p
⊢ eval x (s • p) = s • eval x p

Tactic:
rw [← smul_one_smul R s p, eval, eval₂_smul, RingHom.id_apply, smul_one_mul, eval₂_id]

Premises used: Polynomial.eval, RingHom.id_apply, Polynomial.eval₂_id, smul_one_smul, smul_one_mul, Polynomial.eval₂_smul
-- Module: Mathlib.Algebra.Polynomial.Eval.SMul
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p q : R[X]
rw : (HSMul.hSMul (β := R) s 1 • p).comp q = s • p.comp q
rw₁ : eval₂ C q (HSMul.hSMul (β := R) s 1 • p) = s • p.comp q
rw₂ : eval₂ C q (HSMul.hSMul (β := R) s 1 • p) = s • eval₂ C q p
rw₃ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HSMul.hSMul (β := R) s 1) : R[X]) (eval₂ C q p) = s • eval₂ C q p
rw₄ : HSMul.hSMul (β := R) s 1 • eval₂ C q p = s • eval₂ C q p
rw₅ : s • HSMul.hSMul (α := R) 1 (eval₂ C q p) = s • eval₂ C q p
rw₆ rw₇ : s • eval₂ C q p = s • eval₂ C q p
⊢ (s • p).comp q = s • p.comp q

Tactic:
rw [← smul_one_smul R s p, comp, comp, eval₂_smul, ← smul_eq_C_mul, smul_assoc, one_smul]

Premises used: smul_assoc, Polynomial.smul_eq_C_mul, one_smul, smul_one_smul, Polynomial.eval₂_smul, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Eval.SMul
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
r : R
rw : eval₂ (RingHom.comp C f) X (r • p) = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (eval₂ (RingHom.comp C f) X p)
rw₁ :
  HMul.hMul (α := S[X]) ((RingHom.comp C f : (a : R) → S[X]) r : S[X]) (eval₂ (RingHom.comp C f) X p) =
    HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (eval₂ (RingHom.comp C f) X p)
rw₂ :
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X]) (eval₂ (RingHom.comp C f) X p) =
    HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (eval₂ (RingHom.comp C f) X p)
rw₃ rw₄ :
  HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (eval₂ (RingHom.comp C f) X p) =
    HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (eval₂ (RingHom.comp C f) X p)
⊢ map f (r • p) = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (map f p)

Tactic:
rw [map, eval₂_smul, RingHom.comp_apply, C_mul']

Premises used: Polynomial.C_mul', RingHom.comp_apply, Polynomial.map, Polynomial.eval₂_smul
-- Module: Mathlib.Algebra.Polynomial.Eval.Subring
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
mp : p ∈ (mapRingHom f).rangeS → ∀ (n : ℕ), p.coeff n ∈ f.rangeS
mpr : (∀ (n : ℕ), p.coeff n ∈ f.rangeS) → p ∈ (mapRingHom f).rangeS
⊢ p ∈ (mapRingHom f).rangeS ↔ ∀ (n : ℕ), p.coeff n ∈ f.rangeS

Tactic:
constructor
-- Module: Mathlib.Algebra.Polynomial.Eval.Subring
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
n : ℕ
mp : Membership.mem (α := S) f.rangeS ((f : (a : R) → S) (p.coeff n) : S)
⊢ coeff ((mapRingHom f : (a : R[X]) → S[X]) p) n ∈ f.rangeS

Tactic:
rw [coe_mapRingHom, coeff_map]

Premises used: Polynomial.coeff_map, Polynomial.coe_mapRingHom
-- Module: Mathlib.Algebra.Polynomial.Eval.Subring
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ Membership.mem (α := S) f.rangeS ((f : (a : R) → S) (p.coeff n) : S)

Tactic:
Set.mem_range_self _

Premises used: Set.mem_range_self, Set.Mem, setOf, Set.range
-- Module: Mathlib.Algebra.Polynomial.Eval.Subring
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ Membership.mem (α := S) f.rangeS ((f : (a : R) → S) (p.coeff n) : S)

Tactic:
exact Set.mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.Algebra.Polynomial.Eval.Subring
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
mpr :
  ∑ i ∈ Finset.range (p.natDegree + 1),
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i) ∈
    (mapRingHom f).rangeS
⊢ p ∈ (mapRingHom f).rangeS

Tactic:
rw [p.as_sum_range_C_mul_X_pow]

Premises used: Polynomial.as_sum_range_C_mul_X_pow
-- Module: Mathlib.Algebra.Polynomial.Eval.Subring
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
⊢ ∑ i ∈ Finset.range (p.natDegree + 1),
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i) ∈
    (mapRingHom f).rangeS

Tactic:
(mapRingHom f).rangeS.sum_mem ?_

Premises used: Polynomial.mapRingHom, RingHom.rangeS, Subsemiring.sum_mem
-- Module: Mathlib.Algebra.Polynomial.Eval.Subring
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
mpr :
  ∀ c ∈ Finset.range (p.natDegree + 1),
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff c) : S[X]) (HPow.hPow (α := S[X]) X c) ∈ (mapRingHom f).rangeS
⊢ ∑ i ∈ Finset.range (p.natDegree + 1),
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i) ∈
    (mapRingHom f).rangeS

Tactic:
refine (mapRingHom f).rangeS.sum_mem ?_

Premises used: Polynomial.mapRingHom, RingHom.rangeS, Subsemiring.sum_mem
-- Module: Mathlib.Algebra.Polynomial.Eval.Subring
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
mpr :
  ∀ (c : R) (hc : (f : (a : R) → S) c = p.coeff i),
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i) ∈ (mapRingHom f).rangeS
⊢ HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i) ∈ (mapRingHom f).rangeS

Tactic:
rcases h i with ⟨c, hc⟩
-- Module: Mathlib.Algebra.Polynomial.Eval.Subring
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : (f : (a : R) → S) c = p.coeff i
h₁ :
  (mapRingHom f : (a : R[X]) → S[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
⊢ HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i) ∈ (mapRingHom f).rangeS

Tactic:
use C c * X ^ i

Premises used: Polynomial.C, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.Eval.Subring
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : (f : (a : R) → S) c = p.coeff i
h₁ :
  map f (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
h₂ :
  map f ((C : (a : R) → R[X]) c) * map f (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
h₃ :
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) c) : S[X]) (map f (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
h₄ :
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (map f (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
h₅ :
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (map f X ^ i) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
h₆ h₇ :
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
⊢ (mapRingHom f : (a : R[X]) → S[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)

Tactic:
rw [coe_mapRingHom, Polynomial.map_mul, map_C, hc, Polynomial.map_pow, map_X]

Premises used: Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_X, Polynomial.coe_mapRingHom, Polynomial.map_C
-- Module: Mathlib.Algebra.Polynomial.Eval.Subring
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
⊢ p ∉ (mapRingHom f).rangeS ↔ ∃ (n : ℕ), p.coeff n ∉ f.rangeS

Tactic:
(mem_map_rangeS f (p := p)).not.trans not_forall

Premises used: Iff.not, Iff.trans, Classical.not_forall, Polynomial.mem_map_rangeS
-- Module: Mathlib.Algebra.Polynomial.Eval.Subring
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
p : S[X]
⊢ p ∈ (mapRingHom f).range ↔
    ∀ (n : ℕ), Membership.mem (γ := Subring S) (RingHom.range.{u_1, u_2} (R := R) f) (p.coeff n)

Tactic:
mem_map_rangeS f

Premises used: Set.Mem, Polynomial.mem_map_rangeS
-- Module: Mathlib.Algebra.Polynomial.Eval.Subring
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
f : R →+* S
p : S[X]
⊢ p ∉ (mapRingHom f).range ↔ ∃ (n : ℕ), p.coeff n ∉ RingHom.range.{u_1, u_2} (R := R) f

Tactic:
notMem_map_rangeS f

Premises used: Set.Mem, Polynomial.notMem_map_rangeS
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
⊢ (⇑(expand R p) : (a : R[X]) → R[X]) = eval₂ C (HPow.hPow (α := R[X]) X p)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
⊢ (expand R p : (a : R[X]) → R[X]) f = f.comp (HPow.hPow (α := R[X]) X p)

Tactic:
rfl

Premises used: Polynomial.comp, rfl
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
    (f.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X p ^ e) :
      R[X])

Tactic:
simp [expand, eval₂]

Premises used: Polynomial.eval₂, Polynomial.expand
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
r : R
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X]) ((C : (a : R) → R[X]) r : R[X])

Tactic:
eval₂_C _ _

Premises used: Polynomial.eval₂_C
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
⊢ (expand R p : (a : R[X]) → R[X]) X = HPow.hPow (α := R[X]) X p

Tactic:
eval₂_X _ _

Premises used: Polynomial.eval₂_X
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
r : R
simp_rw : (expand R p : (a : R[X]) → R[X]) (r • HPow.hPow (α := R[X]) X q) = r • HPow.hPow (α := R[X]) X (q * p)
simp_rw₁ :
  HSMul.hSMul (β := R[X]) r ((expand R p : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X q) : R[X]) =
    r • HPow.hPow (α := R[X]) X (q * p)
simp_rw₂ : r • HPow.hPow (α := R[X]) ((expand R p : (a : R[X]) → R[X]) X : R[X]) q = r • HPow.hPow (α := R[X]) X (q * p)
simp_rw₃ : r • HPow.hPow (α := R[X]) X p ^ q = r • HPow.hPow (α := R[X]) X (q * p)
simp_rw₄ : r • HPow.hPow (α := R[X]) X p ^ q = r • HPow.hPow (α := R[X]) X (p * q)
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((monomial q : (a : R) → R[X]) r) : R[X])
    ((monomial (q * p) : (a : R) → R[X]) r : R[X])

Tactic:
simp_rw [← smul_X_eq_monomial, map_smul, map_pow, expand_X, mul_comm, pow_mul]

Premises used: map_pow, pow_mul, Polynomial.expand_X, mul_comm, Polynomial.smul_X_eq_monomial, map_smul
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
r : R
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)) : R[X])
    ((expand R (p * q) : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X])

Tactic:
simp_rw [expand_C]

Premises used: Polynomial.expand_C
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f_1 f g : R[X]
ihf :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) f) : R[X])
    ((expand R (p * q) : (a : R[X]) → R[X]) f : R[X])
ihg :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) g) : R[X])
    ((expand R (p * q) : (a : R[X]) → R[X]) g : R[X])
simp_rw :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) f) : R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) g) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) f : R[X])
      ((expand R (p * q) : (a : R[X]) → R[X]) g : R[X])
simp_rw₁ :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) f : R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) g) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) f : R[X])
      ((expand R (p * q) : (a : R[X]) → R[X]) g : R[X])
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) (f + g)) : R[X])
    ((expand R (p * q) : (a : R[X]) → R[X]) (f + g) : R[X])

Tactic:
simp_rw [map_add, ihf, ihg]

Premises used: map_add
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
h :
  Eq (α := R[X])
    ((expand R p : (a : R[X]) → R[X])
        ((expand R q : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) :
      R[X])
    ((expand R (p * q) : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) :
      R[X])
simp_rw :
  HMul.hMul (α := R[X]) (β := R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)) : R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1))) : R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X])
      ((expand R (p * q) : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X])
simp_rw₁ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1))) : R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
      ((expand R (p * q) : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X])
simp_rw₂ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) X) : R[X]) (n + 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) X : R[X]) (n + 1))
simp_rw₃ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := R[X]) ((expand R p : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X q) : R[X]) (n + 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (p * q) ^ (n + 1))
simp_rw₄ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := R[X]) ((expand R p : (a : R[X]) → R[X]) X : R[X]) q ^ (n + 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (p * q) ^ (n + 1))
simp_rw₅ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ((HPow.hPow (α := R[X]) X p ^ q) ^ (n + 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (p * q) ^ (n + 1))
⊢ Eq (α := R[X])
    ((expand R p : (a : R[X]) → R[X])
        ((expand R q : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))) :
      R[X])
    ((expand R (p * q) : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
      R[X])

Tactic:
simp_rw [map_mul, expand_C, map_pow, expand_X, map_pow, expand_X, pow_mul]

Premises used: Polynomial.expand_C, map_pow, pow_mul, Polynomial.expand_X, map_mul
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
⊢ Eq (α := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) f : R[X])
    ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) f) : R[X])

Tactic:
(expand_expand p q f).symm

Premises used: Polynomial.expand_expand, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
⊢ Eq (α := R[X]) ((expand R 0 : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) (eval 1 f) : R[X])

Tactic:
simp [expand]

Premises used: Polynomial.expand
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
r : R
rw rw₁ : Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) ((C : (a : R) → R[X]) r : R[X])
⊢ Eq (α := R[X]) ((expand R 1 : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X]) ((C : (a : R) → R[X]) r : R[X])

Tactic:
rw [expand_C]

Premises used: Polynomial.expand_C
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
f_1 f g : R[X]
ihf : (expand R 1 : (a : R[X]) → R[X]) f = f
ihg : (expand R 1 : (a : R[X]) → R[X]) g = g
rw :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R 1 : (a : R[X]) → R[X]) f : R[X])
      ((expand R 1 : (a : R[X]) → R[X]) g : R[X]) =
    f + g
rw₁ : HAdd.hAdd (β := R[X]) f ((expand R 1 : (a : R[X]) → R[X]) g : R[X]) = f + g
rw₂ rw₃ : f + g = f + g
⊢ (expand R 1 : (a : R[X]) → R[X]) (f + g) = f + g

Tactic:
rw [map_add, ihf, ihg]

Premises used: map_add
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n : ℕ
r : R
h :
  (expand R 1 : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)
rw :
  HMul.hMul (α := R[X]) (β := R[X]) ((expand R 1 : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X])
      ((expand R 1 : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
rw₁ :
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
      ((expand R 1 : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X]) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
rw₂ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X])
      (HPow.hPow (α := R[X]) ((expand R 1 : (a : R[X]) → R[X]) X : R[X]) (n + 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
rw₃ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 1 ^ (n + 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
rw₄ rw₅ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))
⊢ (expand R 1 : (a : R[X]) → R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))

Tactic:
rw [map_mul, expand_C, map_pow, expand_X, pow_one]

Premises used: Polynomial.expand_C, map_pow, Polynomial.expand_X, map_mul, pow_one
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
rw : (expand R 1 : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[Nat.zero] f
rw₁ : f = (⇑(expand R p) : (a : R[X]) → R[X])^[Nat.zero] f
rw₂ : f = id f
rw₃ rw₄ : f = f
⊢ (expand R (p ^ Nat.zero) : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[Nat.zero] f

Tactic:
rw [pow_zero, expand_one, Function.iterate_zero, id]

Premises used: Function.iterate_zero, Polynomial.expand_one, id, pow_zero
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
ih : (expand R (p ^ n) : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[n] f
rw :
  Eq (α := R[X]) ((expand R (p ^ n.succ) : (a : R[X]) → R[X]) f : R[X])
    ((expand R p : (a : R[X]) → R[X]) ((⇑(expand R p) : (a : R[X]) → R[X])^[n] f) : R[X])
rw₁ :
  Eq (α := R[X]) ((expand R (p * p ^ n) : (a : R[X]) → R[X]) f : R[X])
    ((expand R p : (a : R[X]) → R[X]) ((⇑(expand R p) : (a : R[X]) → R[X])^[n] f) : R[X])
rw₂ :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R (p ^ n) : (a : R[X]) → R[X]) f) : R[X])
    ((expand R p : (a : R[X]) → R[X]) ((⇑(expand R p) : (a : R[X]) → R[X])^[n] f) : R[X])
rw₃ rw₄ :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((⇑(expand R p) : (a : R[X]) → R[X])^[n] f) : R[X])
    ((expand R p : (a : R[X]) → R[X]) ((⇑(expand R p) : (a : R[X]) → R[X])^[n] f) : R[X])
⊢ (expand R (p ^ n.succ) : (a : R[X]) → R[X]) f = (⇑(expand R p) : (a : R[X]) → R[X])^[n.succ] f

Tactic:
rw [Function.iterate_succ_apply', pow_succ', expand_mul, ih]

Premises used: Function.iterate_succ_apply', Polynomial.expand_mul, pow_succ'
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
rw :
  (derivative : (a : R[X]) → R[X]) (eval₂ C (HPow.hPow (α := R[X]) X p) f) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
rw₁ :
  HMul.hMul (β := R[X]) (eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f))
      ((derivative : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X p) : R[X]) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
rw₂ :
  eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      HMul.hMul (β := R[X]) ((C : (a : R) → R[X]) (↑p : R) * HPow.hPow (α := R[X]) X (p - 1))
        ((derivative : (a : R[X]) → R[X]) X : R[X]) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
rw₃ :
  eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      HMul.hMul (β := R[X]) ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
        ((derivative : (a : R[X]) → R[X]) X : R[X]) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
rw₄ :
  eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1) * 1) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
rw₅ rw₆ :
  eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1)) =
    eval₂ C (HPow.hPow (α := R[X]) X p) ((derivative : (a : R[X]) → R[X]) f) *
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))
⊢ (derivative : (a : R[X]) → R[X]) ((expand R p : (a : R[X]) → R[X]) f) =
    HMul.hMul (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((derivative : (a : R[X]) → R[X]) f) : R[X])
      ((↑p : R[X]) * HPow.hPow (α := R[X]) X (p - 1))

Tactic:
rw [coe_expand, derivative_eval₂_C, derivative_pow, C_eq_natCast, derivative_X, mul_one]

Premises used: Polynomial.derivative_X, Polynomial.C_eq_natCast, Polynomial.derivative_eval₂_C, Polynomial.derivative_pow, Polynomial.coe_expand, mul_one