awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ 0 = f.coeff (n * p)
have apply : f.natDegree < n * p
Tactic: apply (coeff_eq_zero_of_natDegree_lt _).symm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ n * 1 ≤ n * p
have bc : 1 ≤ p
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
⊢ f.natDegree < n * p
have _ : f.natDegree + 1 ≤ n * 1
Tactic: calc
    f.natDegree < f.natDegree + 1 := Nat.lt_succ_self _
    _ ≤ n * 1 := by simpa only [mul_one] using hn
    _ ≤ n * p := by gcongr; exact hp.bot_lt
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : f.natDegree + 1 ≤ n
_ : f.natDegree + 1 ≤ n * 1
⊢ f.natDegree < n * p
have _₁ : n * 1 ≤ n * p
Tactic: calc
    f.natDegree < f.natDegree + 1 := Nat.lt_succ_self _
    _ ≤ n * 1 := by simpa only [mul_one] using hn
    _ ≤ n * p := by gcongr; exact hp.bot_lt
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
f : R[X]
hp : p ≠ 0
⊢ contract p ((expand R p : (a : R[X]) → R[X]) f) = f
have a : ∀ (n : ℕ), coeff (contract p ((expand R p : (a : R[X]) → R[X]) f)) n = f.coeff n
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n : ℕ
⊢ (contract 1 f).coeff n = f.coeff n
have rw : f.coeff (n * 1) = f.coeff n
Tactic: rw [coeff_contract one_ne_zero, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n : ℕ
rw : f.coeff (n * 1) = f.coeff n
⊢ (contract 1 f).coeff n = f.coeff n
have rw₁ : f.coeff n = f.coeff n
Tactic: rw [coeff_contract one_ne_zero, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
⊢ contract p (f + g) = contract p f + contract p g
have a : ∀ (n : ℕ), (contract p (f + g)).coeff n = (contract p f + contract p g).coeff n
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ (contract p (f + g)).coeff n = (contract p f + contract p g).coeff n
have a : (contract p (f + g)).coeff n = (contract p f).coeff n + (contract p g).coeff n
Tactic: simp_rw [coeff_add, coeff_contract hp, coeff_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
a : (contract p (f + g)).coeff n = (contract p f).coeff n + (contract p g).coeff n
⊢ (contract p (f + g)).coeff n = (contract p f + contract p g).coeff n
have a₁ : (f + g).coeff (n * p) = f.coeff (n * p) + g.coeff (n * p)
Tactic: simp_rw [coeff_add, coeff_contract hp, coeff_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
⊢ contract p (HMul.hMul (β := R[X]) f ((expand R p : (a : R[X]) → R[X]) g : R[X])) = contract p f * g
have a : ∀ (n : ℕ),
  (contract p (HMul.hMul (β := R[X]) f ((expand R p : (a : R[X]) → R[X]) g : R[X]))).coeff n =
    (contract p f * g).coeff n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ (contract p (HMul.hMul (β := R[X]) f ((expand R p : (a : R[X]) → R[X]) g : R[X]))).coeff n =
    (contract p f * g).coeff n
have a : Eq.{u + 1} (α := R)
  (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    f.coeff (x.1 * p, x.2 * p).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x.1 * p, x.2 * p).2)
  (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (contract p f).coeff x.1 * g.coeff x.2)
Tactic: rw [coeff_contract hp, coeff_mul, coeff_mul, ← sum_subset
    (s₁ := (antidiagonal n).image fun x ↦ (x.1 * p, x.2 * p)), sum_image]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
a :
  Eq.{u + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      f.coeff (x.1 * p, x.2 * p).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x.1 * p, x.2 * p).2)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (contract p f).coeff x.1 * g.coeff x.2)
⊢ (contract p (HMul.hMul (β := R[X]) f ((expand R p : (a : R[X]) → R[X]) g : R[X]))).coeff n =
    (contract p f * g).coeff n
have a₁ : Set.InjOn (β := ℕ × ℕ) (fun (x : ℕ × ℕ) ↦ (x.1 * p, x.2 * p)) (↑(@antidiagonal _ Nat.instAddMonoid _ n) : Set (ℕ × ℕ))
Tactic: rw [coeff_contract hp, coeff_mul, coeff_mul, ← sum_subset
    (s₁ := (antidiagonal n).image fun x ↦ (x.1 * p, x.2 * p)), sum_image]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
a :
  Eq.{u + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      f.coeff (x.1 * p, x.2 * p).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x.1 * p, x.2 * p).2)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (contract p f).coeff x.1 * g.coeff x.2)
a₁ :
  Set.InjOn (β := ℕ × ℕ) (fun (x : ℕ × ℕ) ↦ (x.1 * p, x.2 * p)) (↑(@antidiagonal _ Nat.instAddMonoid _ n) : Set (ℕ × ℕ))
⊢ (contract p (HMul.hMul (β := R[X]) f ((expand R p : (a : R[X]) → R[X]) g : R[X]))).coeff n =
    (contract p f * g).coeff n
have a₂ : image (fun (x : ℕ × ℕ) ↦ (x.1 * p, x.2 * p)) (@antidiagonal _ Nat.instAddMonoid _ n) ⊆
  @antidiagonal _ Nat.instAddMonoid _ (n * p)
Tactic: rw [coeff_contract hp, coeff_mul, coeff_mul, ← sum_subset
    (s₁ := (antidiagonal n).image fun x ↦ (x.1 * p, x.2 * p)), sum_image]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
a :
  Eq.{u + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      f.coeff (x.1 * p, x.2 * p).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x.1 * p, x.2 * p).2)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (contract p f).coeff x.1 * g.coeff x.2)
a₁ :
  Set.InjOn (β := ℕ × ℕ) (fun (x : ℕ × ℕ) ↦ (x.1 * p, x.2 * p)) (↑(@antidiagonal _ Nat.instAddMonoid _ n) : Set (ℕ × ℕ))
a₂ :
  image (fun (x : ℕ × ℕ) ↦ (x.1 * p, x.2 * p)) (@antidiagonal _ Nat.instAddMonoid _ n) ⊆
    @antidiagonal _ Nat.instAddMonoid _ (n * p)
⊢ (contract p (HMul.hMul (β := R[X]) f ((expand R p : (a : R[X]) → R[X]) g : R[X]))).coeff n =
    (contract p f * g).coeff n
have a₃ : ∀ x ∈ @antidiagonal _ Nat.instAddMonoid _ (n * p),
  x ∉ image (fun (x : ℕ × ℕ) ↦ (x.1 * p, x.2 * p)) (@antidiagonal _ Nat.instAddMonoid _ n) →
    f.coeff x.1 * coeff ((expand R p : (a : R[X]) → R[X]) g) x.2 = 0
Tactic: rw [coeff_contract hp, coeff_mul, coeff_mul, ← sum_subset
    (s₁ := (antidiagonal n).image fun x ↦ (x.1 * p, x.2 * p)), sum_image]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ Eq.{u + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      f.coeff (x.1 * p, x.2 * p).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x.1 * p, x.2 * p).2)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (contract p f).coeff x.1 * g.coeff x.2)
have a : Eq.{u + 1} (α := R)
  (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    f.coeff (x.1 * p) * coeff ((expand R p : (a : R[X]) → R[X]) g) (x.2 * p))
  (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (contract p f).coeff x.1 * g.coeff x.2)
Tactic: simp_rw [coeff_expand_mul hp.bot_lt, coeff_contract hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
a a₁ :
  Eq.{u + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      f.coeff (x.1 * p) * coeff ((expand R p : (a : R[X]) → R[X]) g) (x.2 * p))
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (contract p f).coeff x.1 * g.coeff x.2)
⊢ Eq.{u + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      f.coeff (x.1 * p, x.2 * p).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x.1 * p, x.2 * p).2)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (contract p f).coeff x.1 * g.coeff x.2)
have a₂ : Eq.{u + 1} (α := R) (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, f.coeff (x.1 * p) * g.coeff x.2)
  (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, (contract p f).coeff x.1 * g.coeff x.2)
Tactic: simp_rw [coeff_expand_mul hp.bot_lt, coeff_contract hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ image (fun (x : ℕ × ℕ) ↦ (x.1 * p, x.2 * p)) (@antidiagonal _ Nat.instAddMonoid _ n) ⊆
    @antidiagonal _ Nat.instAddMonoid _ (n * p)
have a : ∀ ⦃x : ℕ × ℕ⦄, (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = x) → x.1 + x.2 = n * p
Tactic: simp_rw [subset_iff, mem_image, mem_antidiagonal]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
x : ℕ × ℕ
⊢ (x.1 * p, x.2 * p).1 + (x.1 * p, x.2 * p).2 = (x.1 + x.2) * p
have a : x.1 * p + x.2 * p = (x.1 + x.2) * p
Tactic: simp_rw [add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n : ℕ
⊢ ∀ x ∈ @antidiagonal _ Nat.instAddMonoid _ (n * p),
    x ∉ image (fun (x : ℕ × ℕ) ↦ (x.1 * p, x.2 * p)) (@antidiagonal _ Nat.instAddMonoid _ n) →
      f.coeff x.1 * coeff ((expand R p : (a : R[X]) → R[X]) g) x.2 = 0
have a : ∀ (x : ℕ × ℕ),
  x.1 + x.2 = n * p →
    (¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = x) →
      f.coeff x.1 * coeff ((expand R p : (a : R[X]) → R[X]) g) x.2 = 0
Tactic: simp_rw [mem_image, mem_antidiagonal]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
⊢ f.coeff (x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x, y).2 = 0
have pos : ∀ (h : p ∣ y), f.coeff (x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x, y).2 = 0
Tactic: by_cases h : p ∣ y
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
pos : ∀ (h : p ∣ y), f.coeff (x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x, y).2 = 0
⊢ f.coeff (x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x, y).2 = 0
have neg : ∀ (h : ¬p ∣ y), f.coeff (x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x, y).2 = 0
Tactic: by_cases h : p ∣ y
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : p ∣ y
⊢ f.coeff (x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x, y).2 = 0
have pos : ∀ (x : ℕ) (eq : (p * x, y).1 + (p * x, y).2 = n * p)
  (nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, y)),
  f.coeff (p * x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (p * x, y).2 = 0
Tactic: obtain ⟨x, rfl⟩ : p ∣ x := (Nat.dvd_add_iff_left h).mpr (eq ▸ dvd_mul_left p n)
Cleared hypotheses: x, eq, nex
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n y : ℕ
h : p ∣ y
x : ℕ
eq : (p * x, y).1 + (p * x, y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, y)
⊢ f.coeff (p * x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (p * x, y).2 = 0
have pos : ∀ (y : ℕ) (eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p)
  (nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)),
  f.coeff (p * x, p * y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (p * x, p * y).2 = 0
Tactic: obtain ⟨y, rfl⟩ := h
Cleared hypotheses: y, h, eq, nex
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ ((x, y).1 * p, (x, y).2 * p) = (p * x, p * y)
have simp_rw : (x * p, y * p) = (p * x, p * y)
Tactic: simp_rw [mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ f.coeff (p * x, p * y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (p * x, p * y).2 = 0
have pos : ((x, y).1 + (x, y).2) * p = n * p
Tactic: refine (nex ⟨⟨x, y⟩, (Nat.mul_right_cancel_iff hp.bot_lt).mp ?_, by simp_rw [mul_comm]⟩).elim
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
⊢ ((x, y).1 + (x, y).2) * p = n * p
have pos : ((x, y).1 + (x, y).2) * p = (p * x, p * y).1 + (p * x, p * y).2
Tactic: rw [← eq, mul_comm, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
pos : ((x, y).1 + (x, y).2) * p = (p * x, p * y).1 + (p * x, p * y).2
⊢ ((x, y).1 + (x, y).2) * p = n * p
have pos₁ : p * ((x, y).1 + (x, y).2) = (p * x, p * y).1 + (p * x, p * y).2
Tactic: rw [← eq, mul_comm, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (p * x, p * y).1 + (p * x, p * y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (p * x, p * y)
pos : ((x, y).1 + (x, y).2) * p = (p * x, p * y).1 + (p * x, p * y).2
pos₁ : p * ((x, y).1 + (x, y).2) = (p * x, p * y).1 + (p * x, p * y).2
⊢ ((x, y).1 + (x, y).2) * p = n * p
have pos₂ : p * (x, y).1 + p * (x, y).2 = (p * x, p * y).1 + (p * x, p * y).2
Tactic: rw [← eq, mul_comm, mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : ¬p ∣ y
⊢ f.coeff (x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x, y).2 = 0
have neg : (f.coeff (x, y).1 * if p ∣ (x, y).2 then g.coeff ((x, y).2 / p) else 0) = 0
Tactic: rw [coeff_expand hp.bot_lt, if_neg h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : ¬p ∣ y
neg : (f.coeff (x, y).1 * if p ∣ (x, y).2 then g.coeff ((x, y).2 / p) else 0) = 0
⊢ f.coeff (x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x, y).2 = 0
have neg₁ : f.coeff (x, y).1 * 0 = 0
Tactic: rw [coeff_expand hp.bot_lt, if_neg h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
hp : p ≠ 0
f g : R[X]
n x y : ℕ
eq : (x, y).1 + (x, y).2 = n * p
nex : ¬∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1 * p, a.2 * p) = (x, y)
h : ¬p ∣ y
neg : (f.coeff (x, y).1 * if p ∣ (x, y).2 then g.coeff ((x, y).2 / p) else 0) = 0
neg₁ : f.coeff (x, y).1 * 0 = 0
⊢ f.coeff (x, y).1 * coeff ((expand R p : (a : R[X]) → R[X]) g) (x, y).2 = 0
have neg₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [coeff_expand hp.bot_lt, if_neg h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
p : ℕ
hp : p ≠ 0
h : IsCoprime (R := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((expand R p : (a : R[X]) → R[X]) g : R[X])
a b : R[X]
eq :
  HMul.hMul (β := R[X]) a ((expand R p : (a : R[X]) → R[X]) f : R[X]) +
      HMul.hMul (β := R[X]) b ((expand R p : (a : R[X]) → R[X]) g : R[X]) =
    1
⊢ contract p a * f + contract p b * g = 1
have simp_rw : contract p (HMul.hMul (β := R[X]) a ((expand R p : (a : R[X]) → R[X]) f : R[X])) +
    contract p (HMul.hMul (β := R[X]) b ((expand R p : (a : R[X]) → R[X]) g : R[X])) =
  1
Tactic: simp_rw [← contract_mul_expand hp, ← contract_add hp, eq, ← C_1, contract_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
p : ℕ
hp : p ≠ 0
h : IsCoprime (R := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((expand R p : (a : R[X]) → R[X]) g : R[X])
a b : R[X]
eq :
  HMul.hMul (β := R[X]) a ((expand R p : (a : R[X]) → R[X]) f : R[X]) +
      HMul.hMul (β := R[X]) b ((expand R p : (a : R[X]) → R[X]) g : R[X]) =
    1
simp_rw :
  contract p (HMul.hMul (β := R[X]) a ((expand R p : (a : R[X]) → R[X]) f : R[X])) +
      contract p (HMul.hMul (β := R[X]) b ((expand R p : (a : R[X]) → R[X]) g : R[X])) =
    1
⊢ contract p a * f + contract p b * g = 1
have simp_rw₁ : contract p
    (HMul.hMul (β := R[X]) a ((expand R p : (a : R[X]) → R[X]) f : R[X]) +
      HMul.hMul (β := R[X]) b ((expand R p : (a : R[X]) → R[X]) g : R[X])) =
  1
Tactic: simp_rw [← contract_mul_expand hp, ← contract_add hp, eq, ← C_1, contract_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
p : ℕ
hp : p ≠ 0
h : IsCoprime (R := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((expand R p : (a : R[X]) → R[X]) g : R[X])
a b : R[X]
eq :
  HMul.hMul (β := R[X]) a ((expand R p : (a : R[X]) → R[X]) f : R[X]) +
      HMul.hMul (β := R[X]) b ((expand R p : (a : R[X]) → R[X]) g : R[X]) =
    1
simp_rw :
  contract p (HMul.hMul (β := R[X]) a ((expand R p : (a : R[X]) → R[X]) f : R[X])) +
      contract p (HMul.hMul (β := R[X]) b ((expand R p : (a : R[X]) → R[X]) g : R[X])) =
    1
simp_rw₁ :
  contract p
      (HMul.hMul (β := R[X]) a ((expand R p : (a : R[X]) → R[X]) f : R[X]) +
        HMul.hMul (β := R[X]) b ((expand R p : (a : R[X]) → R[X]) g : R[X])) =
    1
⊢ contract p a * f + contract p b * g = 1
have simp_rw₂ : Eq.{u + 1} (α := R[X]) (contract p 1) 1
Tactic: simp_rw [← contract_mul_expand hp, ← contract_add hp, eq, ← C_1, contract_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
p : ℕ
hp : p ≠ 0
h : IsCoprime (R := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((expand R p : (a : R[X]) → R[X]) g : R[X])
a b : R[X]
eq :
  HMul.hMul (β := R[X]) a ((expand R p : (a : R[X]) → R[X]) f : R[X]) +
      HMul.hMul (β := R[X]) b ((expand R p : (a : R[X]) → R[X]) g : R[X]) =
    1
simp_rw :
  contract p (HMul.hMul (β := R[X]) a ((expand R p : (a : R[X]) → R[X]) f : R[X])) +
      contract p (HMul.hMul (β := R[X]) b ((expand R p : (a : R[X]) → R[X]) g : R[X])) =
    1
simp_rw₁ :
  contract p
      (HMul.hMul (β := R[X]) a ((expand R p : (a : R[X]) → R[X]) f : R[X]) +
        HMul.hMul (β := R[X]) b ((expand R p : (a : R[X]) → R[X]) g : R[X])) =
    1
simp_rw₂ : Eq.{u + 1} (α := R[X]) (contract p 1) 1
⊢ contract p a * f + contract p b * g = 1
have simp_rw₃ : Eq.{u + 1} (α := R[X]) (contract p ((C : (a : R) → R[X]) 1)) ((C : (a : R) → R[X]) 1)
Tactic: simp_rw [← contract_mul_expand hp, ← contract_add hp, eq, ← C_1, contract_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
⊢ (expand R p : (a : R[X]) → R[X]) (contract p f) = f
have a : ∀ (n : ℕ), coeff ((expand R p : (a : R[X]) → R[X]) (contract p f)) n = f.coeff n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
⊢ coeff ((expand R p : (a : R[X]) → R[X]) (contract p f)) n = f.coeff n
have a : (if p ∣ n then f.coeff (n / p * p) else 0) = f.coeff n
Tactic: rw [coeff_expand hp.bot_lt, coeff_contract hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
⊢ (if p ∣ n then f.coeff (n / p * p) else 0) = f.coeff n
have pos : ∀ (h : p ∣ n), f.coeff (n / p * p) = f.coeff n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
pos : ∀ (h : p ∣ n), f.coeff (n / p * p) = f.coeff n
⊢ (if p ∣ n then f.coeff (n / p * p) else 0) = f.coeff n
have neg : ∀ (h : ¬p ∣ n), 0 = f.coeff n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : p ∣ n
⊢ f.coeff (n / p * p) = f.coeff n
have pos : f.coeff n = f.coeff n
Tactic: rw [Nat.div_mul_cancel h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n
⊢ 0 = f.coeff n
have neg : ∀ (h : ¬p ∣ 0), 0 = f.coeff 0
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n
neg : ∀ (h : ¬p ∣ 0), 0 = f.coeff 0
⊢ 0 = f.coeff n
have neg₁ : ∀ (n : ℕ) (h : ¬p ∣ n + 1), 0 = f.coeff (n + 1)
Tactic: rcases n with - | n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
⊢ 0 = f.coeff (n + 1)
have this : coeff ((derivative : (a : R[X]) → R[X]) f) n = f.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
Tactic: have := coeff_derivative f n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
this : coeff ((derivative : (a : R[X]) → R[X]) f) n = f.coeff (n + 1) * HAdd.hAdd (α := R) (↑n : R) 1
⊢ 0 = f.coeff (n + 1)
have this₁ : f.coeff (n + 1) = 0 ∨ HAdd.hAdd (α := R) (↑n : R) 1 = 0
Tactic: rw [hf, coeff_zero, zero_eq_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : CharP R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n + 1
this : f.coeff (n + 1) = 0 ∨ HAdd.hAdd (α := R) (↑n : R) 1 = 0
⊢ 0 = f.coeff (n + 1)
have neg : ∀ (h' : f.coeff (n + 1) = 0), 0 = f.coeff (n + 1)
Tactic: rcases this with h' | _
Cleared hypotheses: this