awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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:
solve_by_elim
-- 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
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
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
⊢ HSMul.hSMul.{z, u_3, u_3} (α := A) ((aeval a : (a : R[X]) → A) p : 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

Premises used: Polynomial.C, map_add, Polynomial.monomial, mul_left_comm, map_mul, add_smul, SemigroupAction.mul_smul, pow_succ', Polynomial.aeval_X
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
M : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
q : Submodule R M
m : M
hm : m ∈ q
p : R[X]
f : Module.End R M
hq : q ≤ Submodule.comap f q
⊢ Membership.mem (α := M) q ((((aeval f : (a : R[X]) → Module.End R M) p : Module.End R M) : (a : M) → M) m : M)

Tactic:
aeval_apply_smul_mem_of_le_comap' hm p f hq

Premises used: Set.Mem, Polynomial.aeval_apply_smul_mem_of_le_comap'
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
rw : Q.leadingCoeff = 0
⊢ Q = 0

Tactic:
rw [← leadingCoeff_eq_zero]

Premises used: Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
a : Q.leadingCoeff • P = 0
⊢ Q.leadingCoeff = 0

Tactic:
apply h
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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 • P = 0

Tactic:
simpa [ext_iff, mul_comm Q.leadingCoeff] using fun i ↦ congr_arg (·.coeff Q.natDegree) (this i)

Premises used: Polynomial.ext_iff, Polynomial.leadingCoeff, congr_arg, mul_comm
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
suffices : ∀ (i : ℕ), P.coeff i • Q = 0
⊢ 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)
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
step : ∀ (n : ℕ), (∀ m > n, P.coeff m • Q = 0) → P.coeff n • Q = 0
⊢ ∀ (i : ℕ), P.coeff i • Q = 0

Tactic:
apply Nat.strong_decreasing_induction
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
h₁ : ∀ m > P.natDegree, P.coeff m • Q = 0
⊢ ∃ (n : ℕ), ∀ m > n, P.coeff m • Q = 0

Tactic:
use P.natDegree

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
h₂ h₃ : Eq.{u + 1} (α := R[X]) 0 0
⊢ P.coeff i • Q = 0

Tactic:
rw [coeff_eq_zero_of_natDegree_lt hi, zero_smul]

Premises used: zero_smul, Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
step₁ : ∀ (hl : (P.coeff l • Q).natDegree = Q.natDegree), P.coeff l • Q = 0
⊢ P.coeff l • Q = 0

Tactic:
obtain _ | hl := (natDegree_smul_le (P.coeff l) Q).lt_or_eq

Premises used: LE.le.lt_or_eq, Polynomial.coeff, Polynomial.natDegree_smul_le
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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 * P.coeff l • Q = 0
⊢ P.coeff l • Q = 0

Tactic:
apply eq_zero_of_mul_eq_zero_of_smul _ h (P.coeff l • Q)

Premises used: Polynomial.coeff, HSMul.hSMul
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
step₁ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (P.coeff l) : R[X]) (P * Q) = 0
step₂ : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (P.coeff l) : R[X]) (0 : R[X]) = 0
step₃ step₄ : Eq.{u + 1} (α := R[X]) 0 0
⊢ P * P.coeff l • Q = 0

Tactic:
rw [smul_eq_C_mul, mul_left_comm, hQ, mul_zero]

Premises used: Polynomial.smul_eq_C_mul, mul_left_comm, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
hl : (P.coeff l • Q).natDegree = Q.natDegree
this : P.coeff l * Q.leadingCoeff = 0
rwa : (P.coeff l • Q).leadingCoeff = 0
rwa₁ : (P.coeff l • Q).coeff (P.coeff l • Q).natDegree = 0
rwa₂ : P.coeff l • Q.coeff (P.coeff l • Q).natDegree = 0
rwa₃ : P.coeff l • Q.coeff Q.natDegree = 0
rwa₄ : P.coeff l • Q.leadingCoeff = 0
rwa₅ rwa₆ rwa₇ rwa₈ : P.coeff l * Q.leadingCoeff = 0
⊢ P.coeff l • Q = 0

Tactic:
rwa [← leadingCoeff_eq_zero, ← coeff_natDegree, coeff_smul, hl, coeff_natDegree, smul_eq_mul]

Premises used: Polynomial.coeff_natDegree, Polynomial.coeff_smul, smul_eq_mul, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
hl : (P.coeff l • Q).natDegree = Q.natDegree
step : P.coeff l * Q.leadingCoeff = 0
⊢ P.coeff l • Q = 0

Tactic:
suffices P.coeff l * Q.leadingCoeff = 0 by
    rwa [← leadingCoeff_eq_zero, ← coeff_natDegree, coeff_smul, hl, coeff_natDegree, smul_eq_mul]
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
this : (P * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff
rw : (P * Q).coeff (l + m) = 0
rw₁ : Eq.{u + 1} (α := R) (coeff 0 (l + m)) 0
rw₂ rw₃ : Eq.{u + 1} (α := R) 0 0
⊢ P.coeff l * Q.leadingCoeff = 0

Tactic:
rw [← this, hQ, coeff_zero]

Premises used: Polynomial.coeff_zero
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
step : (P * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff
⊢ P.coeff l * Q.leadingCoeff = 0

Tactic:
suffices (P * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff by rw [← this, hQ, coeff_zero]
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
step : ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ (l + m), P.coeff x.1 * Q.coeff x.2 = P.coeff l * Q.leadingCoeff
⊢ (P * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff

Tactic:
rw [coeff_mul]

Premises used: Polynomial.coeff_mul
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
⊢ (l, m) ∉ @antidiagonal _ Nat.instAddMonoid _ (l + m) → P.coeff (l, m).1 * Q.coeff (l, m).2 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
apply : ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (l + m), b ≠ (l, m) → P.coeff b.1 * Q.coeff b.2 = 0
⊢ ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ (l + m), P.coeff x.1 * Q.coeff x.2 = P.coeff l * Q.leadingCoeff

Tactic:
apply Finset.sum_eq_single (l, m) _ (by simp)

Premises used: Prod.mk, Finset.sum_eq_single
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
simp : ∀ (a b : ℕ), a + b = l + m → (a = l → ¬b = m) → P.coeff a * Q.coeff b = 0
⊢ ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (l + m), b ≠ (l, m) → P.coeff b.1 * Q.coeff b.2 = 0

Tactic:
simp only [Finset.mem_antidiagonal, ne_eq, Prod.forall, Prod.mk.injEq, not_and]

Premises used: ne_eq, Finset.HasAntidiagonal.mem_antidiagonal, Prod.mk.injEq, Prod.forall, not_and
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
inl : ∀ (hi : i < l), P.coeff i * Q.coeff j = 0
inr :
  ∀ (IH : ∀ m > i, P.coeff m • Q = 0) (hl : (P.coeff i • Q).natDegree = Q.natDegree) (hij : i + j = i + m)
    (H : i = i → ¬j = m), P.coeff i * Q.coeff j = 0
inr₁ : ∀ (hi : l < i), P.coeff i * Q.coeff j = 0
⊢ P.coeff i * Q.coeff j = 0

Tactic:
obtain hi | rfl | hi := lt_trichotomy i l

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : i < l
⊢ m < j

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : i < l
⊢ m < j

Tactic:
have hj : m < j := by lia
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : i < l
hj : m < j
inl : P.coeff i * 0 = 0
inl₁ inl₂ : Eq.{u + 1} (α := R) 0 0
⊢ P.coeff i * Q.coeff j = 0

Tactic:
rw [coeff_eq_zero_of_natDegree_lt hj, mul_zero]

Premises used: MulZeroClass.mul_zero, Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
m : ℕ := Q.natDegree
i j : ℕ
IH : ∀ m > i, P.coeff m • Q = 0
hl : (P.coeff i • Q).natDegree = Q.natDegree
hij : i + j = i + m
H : i = i → ¬j = m
⊢ P.coeff i * Q.coeff j = 0

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
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
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : l < i
inr : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (P.coeff i) : R[X]) Q).coeff j = 0
inr₁ : (P.coeff i • Q).coeff j = 0
inr₂ : Eq.{u + 1} (α := R) (coeff 0 j) 0
inr₃ inr₄ : Eq.{u + 1} (α := R) 0 0
⊢ P.coeff i * Q.coeff j = 0

Tactic:
rw [← coeff_C_mul, ← smul_eq_C_mul, IH _ hi, coeff_zero]

Premises used: Polynomial.smul_eq_C_mul, Polynomial.coeff_C_mul, Polynomial.coeff_zero
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
⊢ P ∉ R[X]⁰ ↔ ∃ (a : R), a ≠ 0 ∧ a • P = 0

Tactic:
⟨fun hP ↦ ?_, fun ⟨a, ha, h⟩ h1 ↦ ha <| C_eq_zero.1 <| (h1.2 _) <| smul_eq_C_mul a ▸ h⟩

Premises used: Polynomial.C, False, Polynomial.C_eq_zero, Polynomial.smul_eq_C_mul, Eq.rec, And.right, Iff.intro, Iff.mp, _private.0.Polynomial.notMem_nonZeroDivisors_iff.match_1, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
refine : ∀ (hP : P ∉ R[X]⁰), ∃ (a : R), a ≠ 0 ∧ a • P = 0
⊢ P ∉ R[X]⁰ ↔ ∃ (a : R), a ≠ 0 ∧ a • P = 0

Tactic:
refine ⟨fun hP ↦ ?_, fun ⟨a, ha, h⟩ h1 ↦ ha <| C_eq_zero.1 <| (h1.2 _) <| smul_eq_C_mul a ▸ h⟩
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
by_contra! : ∀ (h : ∀ (a : R) (_ : a ≠ 0), a • P ≠ 0), False
⊢ ∃ (a : R), a ≠ 0 ∧ a • P = 0

Tactic:
by_contra! h
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R) (_ : a ≠ 0), a • P ≠ 0
obtain : ∀ (Q : R[X]) (hQ : Membership.mem (γ := Set R[X]) {s : R[X] | s * P = 0 ∧ s ≠ 0} Q), False
⊢ False

Tactic:
obtain ⟨Q, hQ⟩ := notMem_nonZeroDivisors_iff_right.1 hP

Premises used: Iff.mp, notMem_nonZeroDivisors_iff_right
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R) (_ : a ≠ 0), a • P ≠ 0
Q : R[X]
hQ : Membership.mem (γ := Set R[X]) {s : R[X] | s * P = 0 ∧ s ≠ 0} Q
⊢ False

Tactic:
hQ.2 (eq_zero_of_mul_eq_zero_of_smul P (fun a ha ↦ ?_) Q (mul_comm P _ ▸ hQ.1))

Premises used: Eq.rec, And.right, And.left, mul_comm, Eq.symm, Polynomial.eq_zero_of_mul_eq_zero_of_smul
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R) (_ : a ≠ 0), a • P ≠ 0
Q : R[X]
hQ : Membership.mem (γ := Set R[X]) {s : R[X] | s * P = 0 ∧ s ≠ 0} Q
refine : ∀ (a : R) (ha : a • P = 0), a = 0
⊢ False

Tactic:
refine hQ.2 (eq_zero_of_mul_eq_zero_of_smul P (fun a ha ↦ ?_) Q (mul_comm P _ ▸ hQ.1))

Premises used: Eq.rec, And.right, And.left, mul_comm, Eq.symm, Polynomial.eq_zero_of_mul_eq_zero_of_smul
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R) (_ : a ≠ 0), a • P ≠ 0
Q : R[X]
hQ : Membership.mem (γ := Set R[X]) {s : R[X] | s * P = 0 ∧ s ≠ 0} Q
a : R
ha : a • P = 0
contrapose! : ∀ (ha : a ≠ 0), a • P ≠ 0
⊢ a = 0

Tactic:
contrapose! ha
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R) (_ : a ≠ 0), a • P ≠ 0
Q : R[X]
hQ : Membership.mem (γ := Set R[X]) {s : R[X] | s * P = 0 ∧ s ≠ 0} Q
a : R
ha : a ≠ 0
⊢ a • P ≠ 0

Tactic:
h a ha
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R) (_ : a ≠ 0), a • P ≠ 0
Q : R[X]
hQ : Membership.mem (γ := Set R[X]) {s : R[X] | s * P = 0 ∧ s ≠ 0} Q
a : R
ha : a ≠ 0
⊢ a • P ≠ 0

Tactic:
exact h a ha
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
⊢ Membership.mem (γ := Submonoid R[X]) R[X]⁰ P ↔ ∀ (a : R), a • P = 0 → a = 0

Tactic:
simpa [not_imp_not] using (notMem_nonZeroDivisors_iff (P := P)).not

Premises used: Polynomial.notMem_nonZeroDivisors_iff, Iff.not, not_imp_not
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
n : ℕ
hp : Membership.mem (γ := Submonoid R) R⁰ (p.coeff n)
r : R
hr : r • p = 0
⊢ r * p.coeff n = 0

Tactic:
simpa using congr(coeff $hr n)
-- Module: Mathlib.Algebra.Polynomial.AlgebraMap
Goal:
R : Type u
inst : CommSemiring R
⊢ Membership.mem (γ := Submonoid R) R⁰ (coeff X 1)

Tactic:
simp [one_mem]

Premises used: OneMemClass.one_mem
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X] → Prop
⊢ (∀ (p : R[X]), P p) ↔ ∀ (q : R[ℕ]), P { toFinsupp := q }

Tactic:
⟨fun h q => h ⟨q⟩, fun h ⟨p⟩ => h p⟩

Premises used: _private.0.Polynomial.forall_iff_forall_finsupp.match_1, Iff.intro, Polynomial.ofFinsupp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
P : R[X] → Prop
⊢ (∃ (p : R[X]), P p) ↔ ∃ (q : R[ℕ]), P { toFinsupp := q }

Tactic:
⟨fun ⟨⟨p⟩, hp⟩ => ⟨p, hp⟩, fun ⟨q, hq⟩ => ⟨⟨q⟩, hq⟩⟩

Premises used: Exists, _private.0.Polynomial.exists_iff_exists_finsupp.match_2, Iff.intro, Exists.intro, _private.0.Polynomial.exists_iff_exists_finsupp.match_1, Polynomial.ofFinsupp
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
f : R[X]
⊢ { toFinsupp := f.toFinsupp : R[X] } = f

Tactic:
constructor
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R[X]) { toFinsupp := 0 } 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R[X]) { toFinsupp := 1 } 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a b : R[ℕ]
⊢ { toFinsupp := a + b : R[X] } = { toFinsupp := a : R[X] } + { toFinsupp := b : R[X] }

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
a : R[ℕ]
⊢ { toFinsupp := -a : R[X] } = -{ toFinsupp := a }

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
a b : R[ℕ]
rw : { toFinsupp := a + -b : R[X] } = { toFinsupp := a : R[X] } - { toFinsupp := b : R[X] }
⊢ { toFinsupp := a - b : R[X] } = { toFinsupp := a : R[X] } - { toFinsupp := b : R[X] }

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
a b : R[ℕ]
⊢ { toFinsupp := a + -b : R[X] } = { toFinsupp := a : R[X] } - { toFinsupp := b : R[X] }

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a b : R[ℕ]
⊢ { toFinsupp := a * b : R[X] } = { toFinsupp := a : R[X] } * { toFinsupp := b : R[X] }

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : ℕ
b : R[ℕ]
⊢ { toFinsupp := a • b : R[X] } = a • { toFinsupp := b : R[X] }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
a : S
b : R[ℕ]
⊢ { toFinsupp := a • b : R[X] } = a • { toFinsupp := b : R[X] }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : R[ℕ]
⊢ { toFinsupp := HPow.hPow (β := ℕ) a 0 : R[X] } = npowRec 0 { toFinsupp := a }

Tactic:
simp [npowRec]

Premises used: npowRec
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : R[ℕ]
n : ℕ
n_ih : { toFinsupp := a ^ n : R[X] } = npowRec n { toFinsupp := a }
⊢ { toFinsupp := a ^ (n + 1) : R[X] } = npowRec (n + 1) { toFinsupp := a }

Tactic:
simp [npowRec, n_ih, pow_succ]

Premises used: pow_succ, npowRec
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : R[ℕ]
n : ℕ
zero : { toFinsupp := HPow.hPow (β := ℕ) a 0 : R[X] } = npowRec 0 { toFinsupp := a }
succ :
  ∀ (n : ℕ) (n_ih : { toFinsupp := a ^ n : R[X] } = npowRec n { toFinsupp := a }),
    { toFinsupp := a ^ (n + 1) : R[X] } = npowRec (n + 1) { toFinsupp := a }
⊢ { toFinsupp := a ^ n : R[X] } = npowRec n { toFinsupp := a }

Tactic:
induction n with
  | zero        => simp [npowRec]
  | succ n n_ih => simp [npowRec, n_ih, pow_succ]

Premises used: pow_succ, npowRec, AddMonoidAlgebra.zero
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R[ℕ]) (toFinsupp 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R[ℕ]) (toFinsupp 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a b : R[X]
⊢ (a + b).toFinsupp = a.toFinsupp + b.toFinsupp

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
a : R[X]
⊢ (-a).toFinsupp = -a.toFinsupp

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
a b : R[X]
rw : (a - b).toFinsupp = a.toFinsupp + -b.toFinsupp
⊢ (a - b).toFinsupp = a.toFinsupp - b.toFinsupp

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Ring R
a b : R[X]
⊢ (a - b).toFinsupp = a.toFinsupp + -b.toFinsupp

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a b : R[X]
⊢ (a * b).toFinsupp = a.toFinsupp * b.toFinsupp

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : ℕ
b : R[X]
⊢ (a • b).toFinsupp = a • b.toFinsupp

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
S : Type u_1
inst_1 : SMulZeroClass S R
a : S
b : R[X]
⊢ (a • b).toFinsupp = a • b.toFinsupp

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
a : R[X]
n : ℕ
rw rw₁ : { toFinsupp := a.toFinsupp ^ n : R[X] }.toFinsupp = a.toFinsupp ^ n
⊢ (a ^ n).toFinsupp = a.toFinsupp ^ n

Tactic:
rw [← ofFinsupp_pow]

Premises used: Polynomial.ofFinsupp_pow
-- Module: Mathlib.Algebra.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
⊢ Injective.{u + 1, u + 1} (α := R[X]) toFinsupp

Tactic:
fun ⟨_x⟩ ⟨_y⟩ => congr_arg _

Premises used: _private.0.Polynomial.forall_iff_forall_finsupp.match_1, congr_arg, Function.Injective, Polynomial.ofFinsupp