awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
step₁ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (P.coeff l) : R[X]) (P * Q) = 0
⊢ P * P.coeff l • Q = 0
have step₂ : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (P.coeff l) : R[X]) (0 : R[X]) = 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
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
⊢ P * P.coeff l • Q = 0
have step₃ : Eq.{u + 1} (α := R[X]) 0 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
hl : (P.coeff l • Q).natDegree = Q.natDegree
this : P.coeff l * Q.leadingCoeff = 0
⊢ P.coeff l • Q = 0
have rwa : (P.coeff l • Q).leadingCoeff = 0
Tactic: rwa [← leadingCoeff_eq_zero, ← coeff_natDegree, coeff_smul, hl, coeff_natDegree, smul_eq_mul]
-- 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
hl : (P.coeff l • Q).natDegree = Q.natDegree
this : P.coeff l * Q.leadingCoeff = 0
rwa : (P.coeff l • Q).leadingCoeff = 0
⊢ P.coeff l • Q = 0
have rwa₁ : (P.coeff l • Q).coeff (P.coeff l • Q).natDegree = 0
Tactic: rwa [← leadingCoeff_eq_zero, ← coeff_natDegree, coeff_smul, hl, coeff_natDegree, smul_eq_mul]
-- 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
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
⊢ P.coeff l • Q = 0
have rwa₂ : P.coeff l • Q.coeff (P.coeff l • Q).natDegree = 0
Tactic: rwa [← leadingCoeff_eq_zero, ← coeff_natDegree, coeff_smul, hl, coeff_natDegree, smul_eq_mul]
-- 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
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
⊢ P.coeff l • Q = 0
have rwa₃ : P.coeff l • Q.coeff Q.natDegree = 0
Tactic: rwa [← leadingCoeff_eq_zero, ← coeff_natDegree, coeff_smul, hl, coeff_natDegree, smul_eq_mul]
-- 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
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
⊢ P.coeff l • Q = 0
have rwa₄ : P.coeff l • Q.leadingCoeff = 0
Tactic: rwa [← leadingCoeff_eq_zero, ← coeff_natDegree, coeff_smul, hl, coeff_natDegree, smul_eq_mul]
-- 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
hl : (P.coeff l • Q).natDegree = Q.natDegree
⊢ P.coeff l • Q = 0
have step : P.coeff l * Q.leadingCoeff = 0
Tactic: suffices P.coeff l * Q.leadingCoeff = 0 by
    rwa [← leadingCoeff_eq_zero, ← coeff_natDegree, coeff_smul, hl, coeff_natDegree, smul_eq_mul]
-- 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
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
this : (P * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff
⊢ P.coeff l * Q.leadingCoeff = 0
have rw : (P * Q).coeff (l + m) = 0
Tactic: rw [← this, hQ, coeff_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
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
⊢ P.coeff l * Q.leadingCoeff = 0
have rw₁ : Eq.{u + 1} (α := R) (coeff 0 (l + m)) 0
Tactic: rw [← this, hQ, coeff_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
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
⊢ P.coeff l * Q.leadingCoeff = 0
have rw₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [← this, hQ, coeff_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
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
⊢ P.coeff l * Q.leadingCoeff = 0
have step : (P * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff
Tactic: suffices (P * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff by rw [← this, hQ, coeff_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
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
⊢ (P * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff
have step : ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ (l + m), P.coeff x.1 * Q.coeff x.2 = P.coeff l * Q.leadingCoeff
Tactic: rw [coeff_mul]
-- 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
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
⊢ ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ (l + m), P.coeff x.1 * Q.coeff x.2 = P.coeff l * Q.leadingCoeff
have apply : ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (l + m), b ≠ (l, m) → P.coeff b.1 * Q.coeff b.2 = 0
Tactic: apply Finset.sum_eq_single (l, m) _ (by simp)
-- 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
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
⊢ ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (l + m), b ≠ (l, m) → P.coeff b.1 * Q.coeff b.2 = 0
have simp : ∀ (a b : ℕ), a + b = l + m → (a = l → ¬b = m) → P.coeff a * Q.coeff b = 0
Tactic: simp only [Finset.mem_antidiagonal, ne_eq, Prod.forall, Prod.mk.injEq, not_and]
-- 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
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
⊢ P.coeff i * Q.coeff j = 0
have inl : ∀ (hi : i < l), P.coeff i * Q.coeff j = 0
Tactic: obtain hi | rfl | hi := lt_trichotomy i l
-- 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
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
⊢ P.coeff i * Q.coeff j = 0
have 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
Tactic: obtain hi | rfl | hi := lt_trichotomy i l
Cleared hypotheses: l, IH, hl, hij, 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
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
⊢ P.coeff i * Q.coeff j = 0
have inr₁ : ∀ (hi : l < i), P.coeff i * Q.coeff j = 0
Tactic: obtain hi | rfl | hi := lt_trichotomy i l
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (hypothesis)
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
⊢ P.coeff i * Q.coeff j = 0
have hj : m < j
Tactic: have hj : m < j := by lia
-- 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
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
⊢ P.coeff i * Q.coeff j = 0
have inl : P.coeff i * 0 = 0
Tactic: rw [coeff_eq_zero_of_natDegree_lt hj, 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
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
⊢ P.coeff i * Q.coeff j = 0
have inl₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [coeff_eq_zero_of_natDegree_lt hj, 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
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
⊢ P.coeff i * Q.coeff j = 0
have inr : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (P.coeff i) : R[X]) Q).coeff j = 0
Tactic: rw [← coeff_C_mul, ← smul_eq_C_mul, IH _ hi, coeff_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
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
⊢ P.coeff i * Q.coeff j = 0
have inr₁ : (P.coeff i • Q).coeff j = 0
Tactic: rw [← coeff_C_mul, ← smul_eq_C_mul, IH _ hi, coeff_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
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
⊢ P.coeff i * Q.coeff j = 0
have inr₂ : Eq.{u + 1} (α := R) (coeff 0 j) 0
Tactic: rw [← coeff_C_mul, ← smul_eq_C_mul, IH _ hi, coeff_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
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
⊢ P.coeff i * Q.coeff j = 0
have inr₃ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [← coeff_C_mul, ← smul_eq_C_mul, IH _ hi, coeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
⊢ P ∉ R[X]⁰ ↔ ∃ (a : R), a ≠ 0 ∧ a • P = 0
have refine : ∀ (hP : 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⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
⊢ ∃ (a : R), a ≠ 0 ∧ a • P = 0
have by_contra! : ∀ (h : ∀ (a : R) (_ : a ≠ 0), a • P ≠ 0), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
Goal:
R : Type u
inst : CommSemiring R
P : R[X]
hP : P ∉ R[X]⁰
h : ∀ (a : R) (_ : a ≠ 0), a • P ≠ 0
⊢ False
have obtain : ∀ (Q : R[X]) (hQ : Membership.mem (γ := Set R[X]) {s : R[X] | s * P = 0 ∧ s ≠ 0} Q), False
Tactic: obtain ⟨Q, hQ⟩ := notMem_nonZeroDivisors_iff_right.1 hP
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
have refine : ∀ (a : R) (ha : a • P = 0), a = 0
Tactic: refine hQ.2 (eq_zero_of_mul_eq_zero_of_smul P (fun a ha ↦ ?_) Q (mul_comm P _ ▸ hQ.1))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.AlgebraMap (goal)
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
⊢ a = 0
have contrapose! : ∀ (ha : a ≠ 0), a • P ≠ 0
Tactic: contrapose! ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
a b : R[ℕ]
⊢ { toFinsupp := a - b : R[X] } = { toFinsupp := a : R[X] } - { toFinsupp := b : R[X] }
have rw : { toFinsupp := a + -b : R[X] } = { toFinsupp := a : R[X] } - { toFinsupp := b : R[X] }
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
a : R[ℕ]
n : ℕ
⊢ { toFinsupp := a ^ n : R[X] } = npowRec n { toFinsupp := a }
have zero : { toFinsupp := HPow.hPow (β := ℕ) a 0 : R[X] } = npowRec 0 { toFinsupp := a }
Tactic: induction n with
  | zero        => simp [npowRec]
  | succ n n_ih => simp [npowRec, n_ih, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
a : R[ℕ]
n : ℕ
zero : { toFinsupp := HPow.hPow (β := ℕ) a 0 : R[X] } = npowRec 0 { toFinsupp := a }
⊢ { toFinsupp := a ^ n : R[X] } = npowRec n { toFinsupp := a }
have succ : ∀ (n : ℕ) (n_ih : { toFinsupp := a ^ n : R[X] } = npowRec n { toFinsupp := a }),
  { toFinsupp := a ^ (n + 1) : R[X] } = npowRec (n + 1) { toFinsupp := a }
Tactic: induction n with
  | zero        => simp [npowRec]
  | succ n n_ih => simp [npowRec, n_ih, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
a b : R[X]
⊢ (a - b).toFinsupp = a.toFinsupp - b.toFinsupp
have rw : (a - b).toFinsupp = a.toFinsupp + -b.toFinsupp
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
a : R[X]
n : ℕ
⊢ (a ^ n).toFinsupp = a.toFinsupp ^ n
have rw : { toFinsupp := a.toFinsupp ^ n : R[X] }.toFinsupp = a.toFinsupp ^ n
Tactic: rw [← ofFinsupp_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
a : R[X]
⊢ a.toFinsupp = 0 ↔ a = 0
have rw : a.toFinsupp = toFinsupp 0 ↔ a = 0
Tactic: rw [← toFinsupp_zero, toFinsupp_inj]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
a : R[X]
rw : a.toFinsupp = toFinsupp 0 ↔ a = 0
⊢ a.toFinsupp = 0 ↔ a = 0
have rw₁ : a = 0 ↔ a = 0
Tactic: rw [← toFinsupp_zero, toFinsupp_inj]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
a : R[X]
⊢ a.toFinsupp = 1 ↔ a = 1
have rw : a.toFinsupp = toFinsupp 1 ↔ a = 1
Tactic: rw [← toFinsupp_one, toFinsupp_inj]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
a : R[X]
rw : a.toFinsupp = toFinsupp 1 ↔ a = 1
⊢ a.toFinsupp = 1 ↔ a = 1
have rw₁ : a = 1 ↔ a = 1
Tactic: rw [← toFinsupp_one, toFinsupp_inj]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
a : R[ℕ]
⊢ { toFinsupp := a : R[X] } = 0 ↔ a = 0
have rw : { toFinsupp := a : R[X] } = { toFinsupp := 0 } ↔ a = 0
Tactic: rw [← ofFinsupp_zero, ofFinsupp_inj]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
a : R[ℕ]
rw : { toFinsupp := a : R[X] } = { toFinsupp := 0 } ↔ a = 0
⊢ { toFinsupp := a : R[X] } = 0 ↔ a = 0
have rw₁ : a = 0 ↔ a = 0
Tactic: rw [← ofFinsupp_zero, ofFinsupp_inj]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
a : R[ℕ]
⊢ { toFinsupp := a : R[X] } = 1 ↔ a = 1
have rw : { toFinsupp := a : R[X] } = { toFinsupp := 1 } ↔ a = 1
Tactic: rw [← ofFinsupp_one, ofFinsupp_inj]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
a : R[ℕ]
rw : { toFinsupp := a : R[X] } = { toFinsupp := 1 } ↔ a = 1
⊢ { toFinsupp := a : R[X] } = 1 ↔ a = 1
have rw₁ : a = 1 ↔ a = 1
Tactic: rw [← ofFinsupp_one, ofFinsupp_inj]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
S : Type u_1
inst_1 : SMulZeroClass S R
inst_2 : FaithfulSMul S R
_s₁ _s₂ : S
h : ∀ (a : R[X]), _s₁ • a = _s₂ • a
⊢ _s₁ = _s₂
have apply : ∀ (a : ℕ →₀ R), _s₁ • a = _s₂ • a
Tactic: apply eq_of_smul_eq_smul (α := ℕ →₀ R)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a b : R
m_1 n_1 : ℕ
inst : Semiring R
p q : R[X]
S₁ : Type u_1
S₂ : Type u_2
inst_1 : SMulZeroClass S₁ R
inst_2 : SMulZeroClass S₂ R
inst_3 : SMulCommClass S₁ S₂ R
m : S₁
n : S₂
f : R[ℕ]
⊢ m • n • { toFinsupp := f : R[X] } = n • m • { toFinsupp := f : R[X] }
have simp_rw : { toFinsupp := m • n • f : R[X] } = { toFinsupp := n • m • f }
Tactic: simp_rw [← ofFinsupp_smul, smul_comm m n f]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
S₁ : Type u_1
S₂ : Type u_2
inst_1 : SMul S₁ S₂
inst_2 : SMulZeroClass S₁ R
inst_3 : SMulZeroClass S₂ R
inst_4 : IsScalarTower S₁ S₂ R
x : S₁
y : S₂
toFinsupp : R[ℕ]
⊢ (x • y) • { toFinsupp := toFinsupp : R[X] } = x • y • { toFinsupp := toFinsupp : R[X] }
have simp_rw : { toFinsupp := (x • y) • toFinsupp : R[X] } = { toFinsupp := x • y • toFinsupp }
Tactic: simp_rw [← ofFinsupp_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
α : Type u_1
K : Type u_2
inst_1 : Semiring K
inst_2 : DistribSMul α K
inst_3 : IsScalarTower α K K
x : α
toFinsupp toFinsupp_1 : K[ℕ]
⊢ (x • { toFinsupp := toFinsupp : K[X] }) • { toFinsupp := toFinsupp_1 : K[X] } =
    x • { toFinsupp := toFinsupp : K[X] } • { toFinsupp := toFinsupp_1 : K[X] }
have simp_rw : x • { toFinsupp := toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] } =
  x • ({ toFinsupp := toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] })
Tactic: simp_rw [smul_eq_mul, ← ofFinsupp_smul, ← ofFinsupp_mul, ← ofFinsupp_smul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
α : Type u_1
K : Type u_2
inst_1 : Semiring K
inst_2 : DistribSMul α K
inst_3 : IsScalarTower α K K
x : α
toFinsupp toFinsupp_1 : K[ℕ]
simp_rw :
  x • { toFinsupp := toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] } =
    x • ({ toFinsupp := toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] })
⊢ (x • { toFinsupp := toFinsupp : K[X] }) • { toFinsupp := toFinsupp_1 : K[X] } =
    x • { toFinsupp := toFinsupp : K[X] } • { toFinsupp := toFinsupp_1 : K[X] }
have simp_rw₁ : { toFinsupp := x • toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] } =
  x • ({ toFinsupp := toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] })
Tactic: simp_rw [smul_eq_mul, ← ofFinsupp_smul, ← ofFinsupp_mul, ← ofFinsupp_smul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
α : Type u_1
K : Type u_2
inst_1 : Semiring K
inst_2 : DistribSMul α K
inst_3 : IsScalarTower α K K
x : α
toFinsupp toFinsupp_1 : K[ℕ]
simp_rw :
  x • { toFinsupp := toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] } =
    x • ({ toFinsupp := toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] })
simp_rw₁ :
  { toFinsupp := x • toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] } =
    x • ({ toFinsupp := toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] })
⊢ (x • { toFinsupp := toFinsupp : K[X] }) • { toFinsupp := toFinsupp_1 : K[X] } =
    x • { toFinsupp := toFinsupp : K[X] } • { toFinsupp := toFinsupp_1 : K[X] }
have simp_rw₂ : { toFinsupp := x • toFinsupp * toFinsupp_1 : K[X] } = x • { toFinsupp := toFinsupp * toFinsupp_1 : K[X] }
Tactic: simp_rw [smul_eq_mul, ← ofFinsupp_smul, ← ofFinsupp_mul, ← ofFinsupp_smul, smul_mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Basic (goal)
Goal:
R : Type u
a b : R
m n : ℕ
inst : Semiring R
p q : R[X]
α : Type u_1
K : Type u_2
inst_1 : Semiring K
inst_2 : DistribSMul α K
inst_3 : IsScalarTower α K K
x : α
toFinsupp toFinsupp_1 : K[ℕ]
simp_rw :
  x • { toFinsupp := toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] } =
    x • ({ toFinsupp := toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] })
simp_rw₁ :
  { toFinsupp := x • toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] } =
    x • ({ toFinsupp := toFinsupp : K[X] } * { toFinsupp := toFinsupp_1 : K[X] })
simp_rw₂ : { toFinsupp := x • toFinsupp * toFinsupp_1 : K[X] } = x • { toFinsupp := toFinsupp * toFinsupp_1 : K[X] }
⊢ (x • { toFinsupp := toFinsupp : K[X] }) • { toFinsupp := toFinsupp_1 : K[X] } =
    x • { toFinsupp := toFinsupp : K[X] } • { toFinsupp := toFinsupp_1 : K[X] }
have simp_rw₃ : { toFinsupp := x • toFinsupp * toFinsupp_1 : K[X] } = { toFinsupp := x • (toFinsupp * toFinsupp_1) }
Tactic: simp_rw [smul_eq_mul, ← ofFinsupp_smul, ← ofFinsupp_mul, ← ofFinsupp_smul, smul_mul_assoc]