awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ 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
have 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)
Tactic: rw [smul_tmul', smul_eq_mul, mul_comm, C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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)
⊢ 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
have 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)
Tactic: rw [smul_tmul', smul_eq_mul, mul_comm, C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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)
⊢ 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
have 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)
Tactic: rw [smul_tmul', smul_eq_mul, mul_comm, C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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)
⊢ 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
have 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)
Tactic: rw [smul_tmul', smul_eq_mul, mul_comm, C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ p ∣ f.coeff i * z ^ i
have pos : ∀ (hi : i ∈ f.support), p ∣ f.coeff i * z ^ i
Tactic: by_cases hi : i ∈ f.support
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ p ∣ f.coeff i * z ^ i
have neg : ∀ (hi : i ∉ f.support), p ∣ f.coeff i * z ^ i
Tactic: by_cases hi : i ∈ f.support
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (hypothesis)
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 ∣ f.coeff i * z ^ i
have dvd_eval₁ : 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
Cleared hypotheses: dvd_eval, dvd_terms, hi
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (hypothesis)
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 ∣ f.coeff i * z ^ i
have 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)
Tactic: rw [← Finset.insert_erase hi, Finset.sum_insert (Finset.notMem_erase _ _)] at dvd_eval
Cleared hypotheses: dvd_eval, dvd_terms, hi
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
have pos : p ∣ ∑ x ∈ f.support.erase i, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff x) : S) (z ^ x)
Tactic: refine (dvd_add_left ?_).mp dvd_eval
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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 ∣ ∑ x ∈ f.support.erase i, HMul.hMul (α := S) ((RingHom.id S : (a : S) → S) (f.coeff x) : S) (z ^ x)
have 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)
Tactic: apply Finset.dvd_sum
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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 ∣ f.coeff i * z ^ i
have h : f.coeff i * z ^ i = 0
Tactic: convert! dvd_zero p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (hypothesis)
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 * z ^ i = 0
have hi₁ : f.coeff i = 0
Tactic: rw [notMem_support_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
r : R
⊢ eval r (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) = 0
have rw : eval r p * r - eval r p * r = 0
Tactic: rw [mul_sub, eval_sub, eval_mul_X, eval_mul_C_of_commute]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
r : R
rw : eval r p * r - eval r p * r = 0
⊢ eval r (p * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) = 0
have rw₁ : Commute r r
Tactic: rw [mul_sub, eval_sub, eval_mul_X, eval_mul_C_of_commute]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ Eq.{u + 1} (α := R) 0 1
have rw : eval r (g * HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])) = 1
Tactic: rw [← eval_mul_X_sub_C, hgf, eval_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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]
⊢ Eq.{u + 1} (α := R) 0 1
have rw₃ : eval r 1 = 1
Tactic: rw [← eval_mul_X_sub_C, hgf, eval_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ Eq.{u + 1} (α := R) 0 1
have rw₄ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [← eval_mul_X_sub_C, hgf, eval_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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) ((((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)
have 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)
Tactic: rw [aeval_def, eval₂_eq_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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 ↔
    HPow.hPow (α := R[X]) X n ∣ p.comp (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]))
have 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)
Tactic: convert! (map_dvd_iff <| algEquivAevalXAddC t).symm using 2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommRing R
p q : R[X]
a b : R
inst_1 : Invertible a
⊢ 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
have 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]))))
Tactic: convert! map_dvd_iff <| algEquivCMulXAddC a b using 2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
c : R[X]ˣ
p : R[X]
⊢ (↑c : R[X]).coeff 0 • p = (↑c : R[X]) * p
have rw : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ((↑c : R[X]).coeff 0) : R[X]) p = (↑c : R[X]) * p
Tactic: rw [← Polynomial.C_mul', ← Polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ (↑c : R[X]).coeff 0 • p = (↑c : R[X]) * p
have rw₁ : (↑c : R[X]) * p = (↑c : R[X]) * p
Tactic: rw [← Polynomial.C_mul', ← Polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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₁ + f₂) : A) m ∈ q
have 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
Tactic: simp_rw [map_add, add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ 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
have 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
Tactic: rw [pow_succ', mul_left_comm, map_mul, aeval_X, mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
p : R[X]
a : A
hq : q ≤ Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R M : (a : A) → Module.End R M) a) q
⊢ HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) p : A) m ∈ q
have C : ∀ (a_1 : R), HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) ((C : (a : R) → R[X]) a_1 : R[X]) : A) m ∈ q
Tactic: induction p using Polynomial.induction_on with
  | C a => simpa using SMulMemClass.smul_mem a hm
  | add f₁ f₂ h₁ h₂ =>
    simp_rw [map_add, add_smul]
    exact Submodule.add_mem q h₁ h₂
  | monomial n t hmq =>
    dsimp only at hmq ⊢
    rw [pow_succ', mul_left_comm, map_mul, aeval_X, mul_smul]
    solve_by_elim
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
p : R[X]
a : A
hq : q ≤ Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R M : (a : A) → Module.End R M) a) q
C :
  ∀ (a_1 : R),
    HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) ((Polynomial.C : (a : R) → R[X]) a_1 : R[X]) : A) m ∈
      q
⊢ HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) p : A) m ∈ q
have add : ∀ (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₁ + f₂) : A) m ∈ q
Tactic: induction p using Polynomial.induction_on with
  | C a => simpa using SMulMemClass.smul_mem a hm
  | add f₁ f₂ h₁ h₂ =>
    simp_rw [map_add, add_smul]
    exact Submodule.add_mem q h₁ h₂
  | monomial n t hmq =>
    dsimp only at hmq ⊢
    rw [pow_succ', mul_left_comm, map_mul, aeval_X, mul_smul]
    solve_by_elim
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
p : R[X]
a : A
hq : q ≤ Submodule.comap (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R M : (a : A) → Module.End R M) a) q
C :
  ∀ (a_1 : R),
    HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) ((Polynomial.C : (a : R) → R[X]) a_1 : R[X]) : A) m ∈
      q
add :
  ∀ (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₁ + f₂) : A) m ∈ q
⊢ HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) p : A) m ∈ q
have monomial : ∀ (n : ℕ) (t : R)
  (hmq :
    HSMul.hSMul.{z, u_3, u_3} (α := A)
        ((aeval a : (a : R[X]) → A)
            (HMul.hMul (α := R[X]) ((Polynomial.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]) ((Polynomial.C : (a : R) → R[X]) t : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
        A)
      m ∈
    q
Tactic: induction p using Polynomial.induction_on with
  | C a => simpa using SMulMemClass.smul_mem a hm
  | add f₁ f₂ h₁ h₂ =>
    simp_rw [map_add, add_smul]
    exact Submodule.add_mem q h₁ h₂
  | monomial n t hmq =>
    dsimp only at hmq ⊢
    rw [pow_succ', mul_left_comm, map_mul, aeval_X, mul_smul]
    solve_by_elim
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
this : ∀ (i : ℕ), P.coeff i • Q = 0
⊢ Q = 0
have rw : Q.leadingCoeff = 0
Tactic: rw [← leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
this : ∀ (i : ℕ), P.coeff i • Q = 0
⊢ Q.leadingCoeff = 0
have a : Q.leadingCoeff • P = 0
Tactic: apply h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
⊢ Q = 0
have suffices : ∀ (i : ℕ), P.coeff i • Q = 0
Tactic: suffices ∀ i, P.coeff i • Q = 0 by
    rw [← leadingCoeff_eq_zero]
    apply h
    simpa [ext_iff, mul_comm Q.leadingCoeff] using fun i ↦ congr_arg (·.coeff Q.natDegree) (this i)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
⊢ ∀ (i : ℕ), P.coeff i • Q = 0
have base : ∃ (n : ℕ), ∀ m > n, P.coeff m • Q = 0
Tactic: apply Nat.strong_decreasing_induction
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
base : ∃ (n : ℕ), ∀ m > n, P.coeff m • Q = 0
⊢ ∀ (i : ℕ), P.coeff i • Q = 0
have step : ∀ (n : ℕ), (∀ m > n, P.coeff m • Q = 0) → P.coeff n • Q = 0
Tactic: apply Nat.strong_decreasing_induction
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
⊢ ∃ (n : ℕ), ∀ m > n, P.coeff m • Q = 0
have h₁ : ∀ m > P.natDegree, P.coeff m • Q = 0
Tactic: use P.natDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
i : ℕ
hi : i > P.natDegree
⊢ P.coeff i • Q = 0
have h₁ : HSMul.hSMul (α := R) 0 Q = 0
Tactic: rw [coeff_eq_zero_of_natDegree_lt hi, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
i : ℕ
hi : i > P.natDegree
h₁ : HSMul.hSMul (α := R) 0 Q = 0
⊢ P.coeff i • Q = 0
have h₂ : Eq.{u + 1} (α := R[X]) 0 0
Tactic: rw [coeff_eq_zero_of_natDegree_lt hi, zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
⊢ P.coeff l • Q = 0
have step : (P.coeff l • Q).natDegree < Q.natDegree → P.coeff l • Q = 0
Tactic: obtain _ | hl := (natDegree_smul_le (P.coeff l) Q).lt_or_eq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
step : (P.coeff l • Q).natDegree < Q.natDegree → P.coeff l • Q = 0
⊢ P.coeff l • Q = 0
have step₁ : ∀ (hl : (P.coeff l • Q).natDegree = Q.natDegree), P.coeff l • Q = 0
Tactic: obtain _ | hl := (natDegree_smul_le (P.coeff l) Q).lt_or_eq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
h_1 : (P.coeff l • Q).natDegree < Q.natDegree
⊢ P.coeff l • Q = 0
have step : P * P.coeff l • Q = 0
Tactic: apply eq_zero_of_mul_eq_zero_of_smul _ h (P.coeff l • Q)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
h_1 : (P.coeff l • Q).natDegree < Q.natDegree
⊢ P * P.coeff l • Q = 0
have step : P * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (P.coeff l) : R[X]) Q = 0
Tactic: rw [smul_eq_C_mul, mul_left_comm, hQ, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
h_1 : (P.coeff l • Q).natDegree < Q.natDegree
step : P * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (P.coeff l) : R[X]) Q = 0
⊢ P * P.coeff l • Q = 0
have step₁ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (P.coeff l) : R[X]) (P * Q) = 0
Tactic: rw [smul_eq_C_mul, mul_left_comm, hQ, mul_zero]