awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
k : ℕ
s : S
n : N
tmul :
  Eq (α := TensorProduct.{u, v, u_3} R S[X] N)
    (HSMul.hSMul (β := S[X]) (HPow.hPow (α := S[X]) X k) ((C : (a : S) → S[X]) s : S[X]) ⊗ₜ[R] n)
    ((monomial k : (a : S) → S[X]) s ⊗ₜ[R] n)
tmul₁ :
  Eq (α := TensorProduct.{u, v, u_3} R S[X] N)
    (HMul.hMul (β := S[X]) (HPow.hPow (α := S[X]) X k) ((C : (a : S) → S[X]) s : S[X]) ⊗ₜ[R] n)
    ((monomial k : (a : S) → S[X]) s ⊗ₜ[R] n)
tmul₂ :
  Eq (α := TensorProduct.{u, v, u_3} R S[X] N)
    (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) s : S[X]) (HPow.hPow (α := S[X]) X k) ⊗ₜ[R] n)
    ((monomial k : (a : S) → S[X]) s ⊗ₜ[R] n)
tmul₃ tmul₄ :
  Eq (α := TensorProduct.{u, v, u_3} R S[X] N)
    ((monomial k : (a : S) → S[X]) s ⊗ₜ[R] n : TensorProduct.{u, v, u_3} R S[X] N)
    ((monomial k : (a : S) → S[X]) s ⊗ₜ[R] n : TensorProduct.{u, v, u_3} R S[X] N)
⊢ HSMul.hSMul (β := TensorProduct.{u, v, u_3} R S[X] N) (HPow.hPow (α := S[X]) X k)
      ((C : (a : S) → S[X]) s ⊗ₜ[R] n : TensorProduct.{u, v, u_3} R S[X] N) =
    (monomial k : (a : S) → S[X]) s ⊗ₜ[R] n

Tactic:
rw [smul_tmul', smul_eq_mul, mul_comm, C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, TensorProduct.smul_tmul', mul_comm, smul_eq_mul
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
pos : ∀ (hi : i ∈ f.support), p ∣ f.coeff i * z ^ i
neg : ∀ (hi : i ∉ f.support), p ∣ f.coeff i * z ^ i
⊢ p ∣ f.coeff i * z ^ i

Tactic:
by_cases hi : i ∈ f.support

Premises used: Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
⊢ p ∣ ∑ n ∈ f.support, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff n) : S) (z ^ n)

Tactic:
rw [eval, eval₂_eq_sum, sum_def] at dvd_eval

Premises used: Polynomial.eval, Polynomial.sum_def, Polynomial.eval₂_eq_sum
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
dvd_eval₁ : p ∣ ∑ n ∈ f.support, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff n) : S) (z ^ n)
⊢ ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j

Tactic:
rw [eval, eval₂_eq_sum, sum_def] at dvd_eval

Premises used: Polynomial.eval, Polynomial.sum_def, Polynomial.eval₂_eq_sum
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
dvd_eval₁ : p ∣ ∑ n ∈ f.support, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff n) : S) (z ^ n)
dvd_terms₁ : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
⊢ i ∈ f.support

Tactic:
rw [eval, eval₂_eq_sum, sum_def] at dvd_eval

Premises used: Polynomial.eval, Polynomial.sum_def, Polynomial.eval₂_eq_sum
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ ∑ n ∈ f.support, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff n) : S) (z ^ n)
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
⊢ p ∣
    HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff i) : S) (z ^ i) +
      ∑ x ∈ f.support.erase i, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff x) : S) (z ^ x)

Tactic:
rw [← Finset.insert_erase hi, Finset.sum_insert (Finset.notMem_erase _ _)] at dvd_eval

Premises used: Finset.notMem_erase, Finset.sum_insert, Finset.insert_erase
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ ∑ n ∈ f.support, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff n) : S) (z ^ n)
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
dvd_eval₁ :
  p ∣
    HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff i) : S) (z ^ i) +
      ∑ x ∈ f.support.erase i, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff x) : S) (z ^ x)
⊢ ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j

Tactic:
rw [← Finset.insert_erase hi, Finset.sum_insert (Finset.notMem_erase _ _)] at dvd_eval

Premises used: Finset.notMem_erase, Finset.sum_insert, Finset.insert_erase
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ ∑ n ∈ f.support, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff n) : S) (z ^ n)
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
dvd_eval₁ :
  p ∣
    HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff i) : S) (z ^ i) +
      ∑ x ∈ f.support.erase i, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff x) : S) (z ^ x)
dvd_terms₁ : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
⊢ i ∈ f.support

Tactic:
rw [← Finset.insert_erase hi, Finset.sum_insert (Finset.notMem_erase _ _)] at dvd_eval

Premises used: Finset.notMem_erase, Finset.sum_insert, Finset.insert_erase
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval :
  p ∣
    HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff i) : S) (z ^ i) +
      ∑ x ∈ f.support.erase i, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff x) : S) (z ^ x)
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
⊢ p ∣ f.coeff i * z ^ i

Tactic:
(dvd_add_left ?_).mp dvd_eval

Premises used: dvd_add_left, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval :
  p ∣
    HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff i) : S) (z ^ i) +
      ∑ x ∈ f.support.erase i, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff x) : S) (z ^ x)
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
pos : p ∣ ∑ x ∈ f.support.erase i, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff x) : S) (z ^ x)
⊢ p ∣ f.coeff i * z ^ i

Tactic:
refine (dvd_add_left ?_).mp dvd_eval

Premises used: dvd_add_left, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval :
  p ∣
    HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff i) : S) (z ^ i) +
      ∑ x ∈ f.support.erase i, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff x) : S) (z ^ x)
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
pos : ∀ i_1 ∈ f.support.erase i, p ∣ HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff i_1) : S) (z ^ i_1)
⊢ p ∣ ∑ x ∈ f.support.erase i, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff x) : S) (z ^ x)

Tactic:
apply Finset.dvd_sum

Premises used: Finset.dvd_sum
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval :
  p ∣
    HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff i) : S) (z ^ i) +
      ∑ x ∈ f.support.erase i, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff x) : S) (z ^ x)
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
j : ℕ
hj : j ∈ f.support.erase i
⊢ p ∣ HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff j) : S) (z ^ j)

Tactic:
dvd_terms j (Finset.ne_of_mem_erase hj)

Premises used: Finset.ne_of_mem_erase, Polynomial.coeff
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval :
  p ∣
    HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff i) : S) (z ^ i) +
      ∑ x ∈ f.support.erase i, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff x) : S) (z ^ x)
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
j : ℕ
hj : j ∈ f.support.erase i
⊢ p ∣ HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff j) : S) (z ^ j)

Tactic:
exact dvd_terms j (Finset.ne_of_mem_erase hj)

Premises used: Finset.ne_of_mem_erase
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∉ f.support
⊢ p ∣ 0

Tactic:
dvd_zero p

Premises used: dvd_zero
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∉ f.support
h : f.coeff i * z ^ i = 0
⊢ p ∣ f.coeff i * z ^ i

Tactic:
convert! dvd_zero p

Premises used: dvd_zero
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∉ f.support
⊢ f.coeff i = 0

Tactic:
rw [notMem_support_iff] at hi

Premises used: Polynomial.notMem_support_iff
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ eval z f
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : f.coeff i = 0
⊢ f.coeff i * z ^ i = 0

Tactic:
simp [hi]
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
S : Type v
inst : CommRing S
r p : S
f : S[X]
i : ℕ
hr : f.IsRoot r
h : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * r ^ j
⊢ p ∣ f.coeff i * r ^ i

Tactic:
dvd_term_of_dvd_eval_of_dvd_terms i (Eq.symm hr ▸ dvd_zero p) h

Premises used: dvd_zero, Eq.rec, Polynomial.dvd_term_of_dvd_eval_of_dvd_terms, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : Ring R
p : R[X]
r : R
rw : eval r p * r - eval r p * r = 0
rw₁ : Commute r r
⊢ eval r (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) = 0

Tactic:
rw [mul_sub, eval_sub, eval_mul_X, eval_mul_C_of_commute]

Premises used: mul_sub, Polynomial.eval_mul_X, Polynomial.eval_mul_C_of_commute, Polynomial.eval_sub
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : Ring R
p : R[X]
r : R
⊢ eval r p * r - eval r p * r = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : Ring R
p : R[X]
r : R
⊢ Commute r r

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
r : R
h : IsUnit (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]))
g : R[X]
_hfg : HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) * g = 1
hgf : g * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) = 1
rw : eval r (g * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) = 1
rw₁ : R
rw₂ : R[X]
rw₃ : eval r 1 = 1
rw₄ rw₅ : Eq.{u + 1} (α := R) 1 1
⊢ Eq.{u + 1} (α := R) 0 1

Tactic:
rw [← eval_mul_X_sub_C, hgf, eval_one]

Premises used: Polynomial.eval_one, Polynomial.eval_mul_X_sub_C
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
inst : CommRing R
p : R[X]
inst_1 : Ring A
inst_2 : Algebra R A
x : A
⊢ Eq.{z + 1} (α := A) ((aeval x : (a : R[X]) → A) (-p) : A) (-(aeval x : (a : R[X]) → A) p : A)

Tactic:
map_neg ..

Premises used: map_neg
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
inst : CommRing R
p q : R[X]
inst_1 : Ring A
inst_2 : Algebra R A
x : A
⊢ (aeval x : (a : R[X]) → A) (p - q) =
    HSub.hSub (α := A) (β := A) ((aeval x : (a : R[X]) → A) p : A) ((aeval x : (a : R[X]) → A) q : A)

Tactic:
map_sub ..

Premises used: map_sub
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
v : M
p : R[X]
rw :
  Eq (α := M)
    ((p.sum fun (e : ℕ) (a : R) ↦
            HMul.hMul (α := M →ₗ[R] M) ((algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) a : M →ₗ[R] M) (f ^ e) :
          (a : M) → M)
        v :
      M)
    (p.sum fun (n : ℕ) (b : R) ↦ HSMul.hSMul (β := M) b ((f ^ n : (a : M) → M) v : M) : M)
⊢ Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) p : M →ₗ[R] M) : (a : M) → M) v : M)
    (p.sum fun (n : ℕ) (b : R) ↦ HSMul.hSMul (β := M) b ((f ^ n : (a : M) → M) v : M) : M)

Tactic:
rw [aeval_def, eval₂_eq_sum]

Premises used: Polynomial.aeval_def, Polynomial.eval₂_eq_sum
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
v : M
p : R[X]
⊢ Eq (α := M)
    ((p.sum fun (e : ℕ) (a : R) ↦
            HMul.hMul (α := M →ₗ[R] M) ((algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) a : M →ₗ[R] M) (f ^ e) :
          (a : M) → M)
        v :
      M)
    (p.sum fun (n : ℕ) (b : R) ↦ HSMul.hSMul (β := M) b ((f ^ n : (a : M) → M) v : M) : M)

Tactic:
map_sum (LinearMap.applyₗ v) _ _

Premises used: LinearMap.applyₗ, Polynomial.sum, map_sum, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
v : M
p : R[X]
⊢ Eq (α := M)
    ((p.sum fun (e : ℕ) (a : R) ↦
            HMul.hMul (α := M →ₗ[R] M) ((algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) a : M →ₗ[R] M) (f ^ e) :
          (a : M) → M)
        v :
      M)
    (p.sum fun (n : ℕ) (b : R) ↦ HSMul.hSMul (β := M) b ((f ^ n : (a : M) → M) v : M) : M)

Tactic:
exact map_sum (LinearMap.applyₗ v) _ _

Premises used: LinearMap.applyₗ, map_sum, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ n ∣ p ↔
    Dvd.dvd (α := R[X])
      ((algEquivAevalXAddC t : (a : R[X]) → R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ n) :
        R[X])
      ((algEquivAevalXAddC t : (a : R[X]) → R[X]) p : R[X])

Tactic:
(map_dvd_iff <| algEquivAevalXAddC t).symm

Premises used: map_dvd_iff, Polynomial.algEquivAevalXAddC, Iff.symm
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
h :
  HPow.hPow (α := R[X]) X n =
    (algEquivAevalXAddC t : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ n)
⊢ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ n ∣ p ↔
    HPow.hPow (α := R[X]) X n ∣ p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))

Tactic:
convert! (map_dvd_iff <| algEquivAevalXAddC t).symm using 2

Premises used: map_dvd_iff, Polynomial.algEquivAevalXAddC, Iff.symm
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
n : ℕ
⊢ HPow.hPow (α := R[X]) X n =
    (algEquivAevalXAddC t : (a : R[X]) → R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ n)

Tactic:
simp [C_eq_algebraMap]

Premises used: Polynomial.C_eq_algebraMap
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
⊢ p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) = 0 ↔ p = 0

Tactic:
EmbeddingLike.map_eq_zero_iff (f := algEquivAevalXAddC t)

Premises used: Polynomial.C, MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Polynomial.comp, EmbeddingLike.map_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
⊢ p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X])) ≠ 0 ↔ p ≠ 0

Tactic:
comp_X_add_C_eq_zero_iff.not

Premises used: Iff.not, Polynomial.comp_X_add_C_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommRing R
p q : R[X]
a b : R
inst_1 : Invertible a
⊢ Dvd.dvd (α := R[X])
      ((algEquivCMulXAddC a b : (a : R[X]) → R[X])
          (p.comp
            (HMul.hMul (α := R[X])
              ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _) : R[X])
              (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X])))) :
        R[X])
      ((algEquivCMulXAddC a b : (a : R[X]) → R[X]) q : R[X]) ↔
    p.comp
        (HMul.hMul (α := R[X])
          ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _) : R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))) ∣
      q

Tactic:
map_dvd_iff <| algEquivCMulXAddC a b

Premises used: map_dvd_iff, Polynomial.algEquivCMulXAddC
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommRing R
p q : R[X]
a b : R
inst_1 : Invertible a
h :
  p =
    (algEquivCMulXAddC a b : (a : R[X]) → R[X])
      (p.comp
        (HMul.hMul (α := R[X])
          ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _) : R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))))
⊢ p ∣
      q.comp
        (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
          ((C : (a : R) → R[X]) b : R[X])) ↔
    p.comp
        (HMul.hMul (α := R[X])
          ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _) : R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))) ∣
      q

Tactic:
convert! map_dvd_iff <| algEquivCMulXAddC a b using 2

Premises used: map_dvd_iff, Polynomial.algEquivCMulXAddC
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommRing R
p q : R[X]
a b : R
inst_1 : Invertible a
⊢ p =
    (algEquivCMulXAddC a b : (a : R[X]) → R[X])
      (p.comp
        (HMul.hMul (α := R[X])
          ((C : (a : R) → R[X]) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _) : R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) b : R[X]))))

Tactic:
simp [← comp_eq_aeval, comp_assoc, ← mul_assoc, ← C_mul]

Premises used: Polynomial.comp_assoc, mul_assoc, Polynomial.comp_eq_aeval, Polynomial.C_mul
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommRing R
p q : R[X]
a : R
x : Invertible (α := R) 1 := invertibleOne
⊢ p ∣ q.comp (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ↔
    p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ∣ q

Tactic:
simpa using dvd_comp_C_mul_X_add_C_iff p q 1 (-a)

Premises used: Polynomial.dvd_comp_C_mul_X_add_C_iff, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommRing R
p q : R[X]
a : R
⊢ p ∣ q.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ↔
    p.comp (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) ∣ q

Tactic:
simpa using dvd_comp_X_sub_C_iff p q (-a)

Premises used: Polynomial.dvd_comp_X_sub_C_iff, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommRing R
p q : R[X]
x : Invertible (α := R) 1 := invertibleOne
x_1 : Invertible (α := R) (-1) := invertibleNeg 1
⊢ p ∣ q.comp (-X) ↔ p.comp (-X) ∣ q

Tactic:
simpa using dvd_comp_C_mul_X_add_C_iff p q (-1) 0

Premises used: Polynomial.dvd_comp_C_mul_X_add_C_iff, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
c : R[X]ˣ
p : R[X]
rw : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑c : R[X]).coeff 0) : R[X]) p = (↑c : R[X]) * p
rw₁ rw₂ : (↑c : R[X]) * p = (↑c : R[X]) * p
⊢ (↑c : R[X]).coeff 0 • p = (↑c : R[X]) * p

Tactic:
rw [← Polynomial.C_mul', ← Polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)]

Premises used: Polynomial.eq_C_of_degree_eq_zero, Polynomial.C_mul', Polynomial.degree_coe_units
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
q : Submodule R M
m : M
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
hm : m ∈ q
a_1 : A
hq : q ≤ Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R M : (a : A) → Module.End R M) a_1) q
a : R
⊢ HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a_1 : (a : R[X]) → A) ((C : (a : R) → R[X]) a : R[X]) : A) m ∈ q

Tactic:
simpa using SMulMemClass.smul_mem a hm

Premises used: SMulMemClass.smul_mem
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
q : Submodule R M
m : M
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
hm : m ∈ q
a : A
hq : q ≤ Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R M : (a : A) → Module.End R M) a) q
f₁ f₂ : R[X]
h₁ : HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) f₁ : A) m ∈ q
h₂ : HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) f₂ : A) m ∈ q
add :
  HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) f₁ : A) m +
      HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) f₂ : A) m ∈
    q
⊢ HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) (f₁ + f₂) : A) m ∈ q

Tactic:
simp_rw [map_add, add_smul]

Premises used: map_add, add_smul
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
q : Submodule R M
m : M
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
hm : m ∈ q
a : A
hq : q ≤ Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R M : (a : A) → Module.End R M) a) q
f₁ f₂ : R[X]
h₁ : HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) f₁ : A) m ∈ q
h₂ : HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) f₂ : A) m ∈ q
⊢ HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) f₁ : A) m +
      HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) f₂ : A) m ∈
    q

Tactic:
Submodule.add_mem q h₁ h₂

Premises used: Submodule.add_mem
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
q : Submodule R M
m : M
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
hm : m ∈ q
a : A
hq : q ≤ Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R M : (a : A) → Module.End R M) a) q
f₁ f₂ : R[X]
h₁ : HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) f₁ : A) m ∈ q
h₂ : HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) f₂ : A) m ∈ q
⊢ HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) f₁ : A) m +
      HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) f₂ : A) m ∈
    q

Tactic:
exact Submodule.add_mem q h₁ h₂

Premises used: Submodule.add_mem
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
A : Type z
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
q : Submodule R M
m : M
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
hm : m ∈ q
a : A
hq : q ≤ Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R M : (a : A) → Module.End R M) a) q
n : ℕ
t : R
hmq :
  HSMul.hSMul.{z, u_3, u_3} (α := A)
      ((aeval a : (a : R[X]) → A) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X n)) :
        A)
      m ∈
    q
monomial :
  a •
      HSMul.hSMul.{z, u_3, u_3} (α := A)
        ((aeval a : (a : R[X]) → A)
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X n)) :
          A)
        m ∈
    q
⊢ HSMul.hSMul.{z, u_3, u_3} (α := A)
      ((aeval a : (a : R[X]) → A)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
        A)
      m ∈
    q

Tactic:
rw [pow_succ', mul_left_comm, map_mul, aeval_X, mul_smul]

Premises used: mul_left_comm, map_mul, SemigroupAction.mul_smul, pow_succ', Polynomial.aeval_X