awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
ι : Type u_2
s : Finset ι
f : ι → Ideal R[X]
⊢ ∏ i ∈ s, (f i).leadingCoeff ≤ (s.prod f).leadingCoeff
have refine : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    ∏ i ∈ s, (f i).leadingCoeff ≤ (s.prod f).leadingCoeff →
      ∏ i ∈ insert a s, (f i).leadingCoeff ≤ ((insert a s).prod f).leadingCoeff
Tactic: classical
  refine Finset.induction_on s (by simp) ?_
  intro i s hi hs
  simpa [hi] using (mul_mono_right hs).trans (leadingCoeff_mul_le (f i) (s.prod f))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (Finset.prod ∅ f).coeff k ∈ I ^ (Finset.sum ∅ n - k)
have empty : Membership.mem (γ := Ideal R) ⊤ (if k = 0 then 1 else 0)
Tactic: rw [sum_empty, prod_empty, coeff_one, zero_tsub, pow_zero, Ideal.one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ ((insert a s).prod f).coeff k ∈ I ^ ((insert a s).sum n - k)
have insert : ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ k, (f a).coeff x.1 * coeff (∏ x ∈ s, f x) x.2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)
Tactic: rw [sum_insert ha, prod_insert ha, coeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ k, (f a).coeff x.1 * coeff (∏ x ∈ s, f x) x.2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)
have insert : ∀ c ∈ @antidiagonal _ Nat.instAddMonoid _ k, (f a).coeff c.1 * coeff (∏ x ∈ s, f x) c.2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)
Tactic: apply sum_mem
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k i j : ℕ
e : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ k
⊢ (f a).coeff (i, j).1 * coeff (∏ x ∈ s, f x) (i, j).2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)
have insert : ∀ (e : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (i + j)),
  (f a).coeff (i, j).1 * coeff (∏ x ∈ s, f x) (i, j).2 ∈ I ^ (n a + ∑ x ∈ s, n x - (i + j))
Tactic: obtain rfl : i + j = k := mem_antidiagonal.mp e
Cleared hypotheses: k, e
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (i + j)
⊢ (f a).coeff (i, j).1 * coeff (∏ x ∈ s, f x) (i, j).2 ∈ I ^ (n a + ∑ x ∈ s, n x - (i + j))
have insert : (f a).coeff (i, j).1 * coeff (∏ x ∈ s, f x) (i, j).2 ∈ I ^ (n a - i + (∑ x ∈ s, n x - j))
Tactic: apply Ideal.pow_le_pow_right add_tsub_add_le_tsub_add_tsub
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
i j : ℕ
e : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (i + j)
⊢ (f a).coeff (i, j).1 * coeff (∏ x ∈ s, f x) (i, j).2 ∈ I ^ (n a - i + (∑ x ∈ s, n x - j))
have insert : (f a).coeff (i, j).1 * coeff (∏ x ∈ s, f x) (i, j).2 ∈ I ^ (n a - i) * I ^ (∑ x ∈ s, n x - j)
Tactic: rw [pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (s.prod f).coeff k ∈ I ^ (s.sum n - k)
have empty : ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ),
  (Finset.prod ∅ f).coeff k ∈ I ^ (Finset.sum ∅ n - k)
Tactic: induction s using Finset.induction generalizing k with
    | empty =>
      rw [sum_empty, prod_empty, coeff_one, zero_tsub, pow_zero, Ideal.one_eq_top]
      exact Submodule.mem_top
    | insert a s ha hs =>
      rw [sum_insert ha, prod_insert ha, coeff_mul]
      apply sum_mem
      rintro ⟨i, j⟩ e
      obtain rfl : i + j = k := mem_antidiagonal.mp e
      apply Ideal.pow_le_pow_right add_tsub_add_le_tsub_add_tsub
      rw [pow_add]
      exact Ideal.mul_mem_mul (by grind) (by grind)
Cleared hypotheses: s, h, k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ),
    (Finset.prod ∅ f).coeff k ∈ I ^ (Finset.sum ∅ n - k)
⊢ (s.prod f).coeff k ∈ I ^ (s.sum n - k)
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k))
  (h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ),
  ((insert a s).prod f).coeff k ∈ I ^ ((insert a s).sum n - k)
Tactic: induction s using Finset.induction generalizing k with
    | empty =>
      rw [sum_empty, prod_empty, coeff_one, zero_tsub, pow_zero, Ideal.one_eq_top]
      exact Submodule.mem_top
    | insert a s ha hs =>
      rw [sum_insert ha, prod_insert ha, coeff_mul]
      apply sum_mem
      rintro ⟨i, j⟩ e
      obtain rfl : i + j = k := mem_antidiagonal.mp e
      apply Ideal.pow_le_pow_right add_tsub_add_le_tsub_add_tsub
      rw [pow_add]
      exact Ideal.mul_mem_mul (by grind) (by grind)
Cleared hypotheses: s, h, k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ (s.prod f).coeff k ∈ I ^ (s.sum n - k)
have empty : ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ),
  (Finset.prod ∅ f).coeff k ∈ I ^ (Finset.sum ∅ n - k)
Tactic: classical
    induction s using Finset.induction generalizing k with
    | empty =>
      rw [sum_empty, prod_empty, coeff_one, zero_tsub, pow_zero, Ideal.one_eq_top]
      exact Submodule.mem_top
    | insert a s ha hs =>
      rw [sum_insert ha, prod_insert ha, coeff_mul]
      apply sum_mem
      rintro ⟨i, j⟩ e
      obtain rfl : i + j = k := mem_antidiagonal.mp e
      apply Ideal.pow_le_pow_right add_tsub_add_le_tsub_add_tsub
      rw [pow_add]
      exact Ideal.mul_mem_mul (by grind) (by grind)
Cleared hypotheses: s, h, k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → R[X]
I : Ideal R
n : ι → ℕ
h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
empty :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ),
    (Finset.prod ∅ f).coeff k ∈ I ^ (Finset.sum ∅ n - k)
⊢ (s.prod f).coeff k ∈ I ^ (s.sum n - k)
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (hs : ∀ (h : ∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k))
  (h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ),
  ((insert a s).prod f).coeff k ∈ I ^ ((insert a s).sum n - k)
Tactic: classical
    induction s using Finset.induction generalizing k with
    | empty =>
      rw [sum_empty, prod_empty, coeff_one, zero_tsub, pow_zero, Ideal.one_eq_top]
      exact Submodule.mem_top
    | insert a s ha hs =>
      rw [sum_insert ha, prod_insert ha, coeff_mul]
      apply sum_mem
      rintro ⟨i, j⟩ e
      obtain rfl : i + j = k := mem_antidiagonal.mp e
      apply Ideal.pow_le_pow_right add_tsub_add_le_tsub_add_tsub
      rw [pow_add]
      exact Ideal.mul_mem_mul (by grind) (by grind)
Cleared hypotheses: s, h, k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : Ring R
⊢ ¬IsField.{u} R[X]
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
h : Nontrivial R
hR : IsField.{u} R[X]
⊢ False
have obtain : ∀ (p : R[X]) (hp : X * p = 1), False
Tactic: obtain ⟨p, hp⟩ := hR.mul_inv_cancel X_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : Ring R
h : Nontrivial R
hR : IsField.{u} R[X]
p : R[X]
hp : X * p = 1
⊢ False
have hp0 : p ≠ 0
Tactic: have hp0 : p ≠ 0 := right_ne_zero_of_mul_eq_one hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : Ring R
h : Nontrivial R
hR : IsField.{u} R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
⊢ False
have this : p.degree < (p * X).degree
Tactic: have := degree_lt_degree_mul_X hp0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : Ring R
h : Nontrivial R
hR : IsField.{u} R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p.degree < (p * X).degree
⊢ False
have this₁ : p = 0
Tactic: rw [← X_mul, congr_arg degree hp, degree_one, Nat.WithBot.lt_zero_iff, degree_eq_bot] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) x : R[X])
⊢ x = 0
have refine : ∀ (hx0 : ¬x = 0), 1 ∈ I
Tactic: refine Classical.by_contradiction fun hx0 => hI.ne_top ((eq_top_iff_one I).2 ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) x : R[X])
hx0 : ¬x = 0
⊢ 1 ∈ I
have obtain : ∀ (y : R) (hy : x * y = 1), 1 ∈ I
Tactic: obtain ⟨y, hy⟩ := hR.mul_inv_cancel hx0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) x : R[X])
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 ∈ I
have h : 1 = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) ((C : (a : R) → R[X]) x : R[X])
Tactic: convert! I.mul_mem_left (C y) hx
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) x : R[X])
hx0 : ¬x = 0
y : R
hy : x * y = 1
⊢ 1 = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) ((C : (a : R) → R[X]) x : R[X])
have h : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (y * x) : R[X])
Tactic: rw [← C.map_mul, hR.mul_comm y x, hy, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) x : R[X])
hx0 : ¬x = 0
y : R
hy : x * y = 1
h : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (y * x) : R[X])
⊢ 1 = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) ((C : (a : R) → R[X]) x : R[X])
have h₁ : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (x * y) : R[X])
Tactic: rw [← C.map_mul, hR.mul_comm y x, hy, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) x : R[X])
hx0 : ¬x = 0
y : R
hy : x * y = 1
h : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (y * x) : R[X])
h₁ : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (x * y) : R[X])
⊢ 1 = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) ((C : (a : R) → R[X]) x : R[X])
have h₂ : Eq.{u + 1} (α := R[X]) 1 ((C : (a : R) → R[X]) 1)
Tactic: rw [← C.map_mul, hR.mul_comm y x, hy, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Ring R
hR : IsField R
I : Ideal R[X]
hI : I.IsMaximal
x : R
hx : Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) x : R[X])
hx0 : ¬x = 0
y : R
hy : x * y = 1
h : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (y * x) : R[X])
h₁ : Eq (α := R[X]) (1 : R[X]) ((C : (a : R) → R[X]) (x * y) : R[X])
h₂ : Eq.{u + 1} (α := R[X]) 1 ((C : (a : R) → R[X]) 1)
⊢ 1 = HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) y : R[X]) ((C : (a : R) → R[X]) x : R[X])
have h₃ : Eq.{u + 1} (α := R[X]) 1 1
Tactic: rw [← C.map_mul, hR.mul_comm y x, hy, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
⊢ IsPrime (α := R[X]) (map (F := R →+* R[X]) C P) ↔ P.IsPrime
have mp : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P) → P.IsPrime
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
mp : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P) → P.IsPrime
⊢ IsPrime (α := R[X]) (map (F := R →+* R[X]) C P) ↔ P.IsPrime
have mpr : P.IsPrime → IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
H : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
⊢ P.IsPrime
have this : IsPrime (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P))
Tactic: have := comap_isPrime C (map C P)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
H : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
this : IsPrime (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P))
⊢ P.IsPrime
have h : P = comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P)
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
H : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
this : IsPrime (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P))
⊢ P = comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P)
have h : ∀ (x : R), x ∈ P ↔ Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
H : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
this : IsPrime (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P))
x : R
⊢ x ∈ P ↔ Membership.mem (γ := Ideal R) (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P)) x
have h : x ∈ P ↔ ∀ (n : ℕ), coeff ((C : (a : R) → R[X]) x) n ∈ P
Tactic: simp only [mem_comap, mem_map_C_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
H : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
this : IsPrime (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P))
x : R
⊢ x ∈ P ↔ ∀ (n : ℕ), coeff ((C : (a : R) → R[X]) x) n ∈ P
have h : x ∈ P → ∀ (n : ℕ), coeff ((C : (a : R) → R[X]) x) n ∈ P
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
H : IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
this : IsPrime (comap (F := R →+* R[X]) C (map (F := R →+* R[X]) C P))
x : R
h : x ∈ P → ∀ (n : ℕ), coeff ((C : (a : R) → R[X]) x) n ∈ P
⊢ x ∈ P ↔ ∀ (n : ℕ), coeff ((C : (a : R) → R[X]) x) n ∈ P
have h₁ : (∀ (n : ℕ), coeff ((C : (a : R) → R[X]) x) n ∈ P) → x ∈ P
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
⊢ IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
have mpr : Ne (α := Ideal R[X]) (map (F := R →+* R[X]) C P) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
mpr : Ne (α := Ideal R[X]) (map (F := R →+* R[X]) C P) ⊤
⊢ IsPrime (α := R[X]) (map (F := R →+* R[X]) C P)
have mpr₁ : ∀ {x y : R[X]},
  Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C P) (x * y) →
    Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C P) x ∨
      Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C P) y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
⊢ Ne (α := Ideal R[X]) (map (F := R →+* R[X]) C P) ⊤
have mpr : ∃ (x : ℕ), coeff 1 x ∉ P
Tactic: rw [Ne, eq_top_iff_one, mem_map_C_iff, not_forall]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
⊢ ∃ (x : ℕ), coeff 1 x ∉ P
have h₁ : coeff 1 0 ∉ P
Tactic: use 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
⊢ coeff 1 0 ∉ P
have h₁ : ¬P = ⊤
Tactic: rw [coeff_one_zero, ← eq_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
⊢ Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C P) (f * g) →
    Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C P) f ∨
      Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C P) g
have mpr : (∀ (n : ℕ), (f * g).coeff n ∈ P) → (∀ (n : ℕ), f.coeff n ∈ P) ∨ ∀ (n : ℕ), g.coeff n ∈ P
Tactic: simp only [mem_map_C_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
⊢ (∀ (n : ℕ), (f * g).coeff n ∈ P) → (∀ (n : ℕ), f.coeff n ∈ P) ∨ ∀ (n : ℕ), g.coeff n ∈ P
have mpr : ((∃ (n : ℕ), f.coeff n ∉ P) ∧ ∃ (n : ℕ), g.coeff n ∉ P) → ∃ (n : ℕ), (f * g).coeff n ∉ P
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
⊢ ∃ (n : ℕ), (f * g).coeff n ∉ P
have mpr : (f * g).coeff (m + n) ∉ P
Tactic: refine ⟨m + n, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
⊢ (f * g).coeff (m + n) ∉ P
have mpr : f.coeff (m, n).1 * g.coeff (m, n).2 ∉ P
Tactic: rw [coeff_mul, ← Finset.insert_erase ((Finset.mem_antidiagonal (a := (m, n))).mpr rfl),
          Finset.sum_insert (Finset.notMem_erase _ _), (P.add_mem_iff_left _).not]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
mpr : f.coeff (m, n).1 * g.coeff (m, n).2 ∉ P
⊢ (f * g).coeff (m + n) ∉ P
have rw : ∑ x ∈ (@antidiagonal _ Nat.instAddMonoid _ ((m, n).1 + (m, n).2)).erase (m, n), f.coeff x.1 * g.coeff x.2 ∈ P
Tactic: rw [coeff_mul, ← Finset.insert_erase ((Finset.mem_antidiagonal (a := (m, n))).mpr rfl),
          Finset.sum_insert (Finset.notMem_erase _ _), (P.add_mem_iff_left _).not]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
⊢ f.coeff (m, n).1 * g.coeff (m, n).2 ∉ P
have mpr : ¬(f.coeff (m, n).1 ∈ P ∨ g.coeff (m, n).2 ∈ P)
Tactic: apply mt h.2
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
⊢ ¬(f.coeff (m, n).1 ∈ P ∨ g.coeff (m, n).2 ∈ P)
have mpr : f.coeff (m, n).1 ∉ P ∧ g.coeff (m, n).2 ∉ P
Tactic: rw [not_or]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
⊢ ∑ x ∈ (@antidiagonal _ Nat.instAddMonoid _ ((m, n).1 + (m, n).2)).erase (m, n), f.coeff x.1 * g.coeff x.2 ∈ P
have apply : ∀ c ∈ (@antidiagonal _ Nat.instAddMonoid _ ((m, n).1 + (m, n).2)).erase (m, n), f.coeff c.1 * g.coeff c.2 ∈ P
Tactic: apply P.sum_mem
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
i j : ℕ
hij : (i, j) ∈ (@antidiagonal _ Nat.instAddMonoid _ ((m, n).1 + (m, n).2)).erase (m, n)
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
have hij₁ : (i, j) ≠ (m, n) ∧ (i, j).1 + (i, j).2 = (m, n).1 + (m, n).2
Tactic: rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
i j : ℕ
hij : (i, j) ≠ (m, n) ∧ (i, j).1 + (i, j).2 = (m, n).1 + (m, n).2
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
have hij₁ : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
Tactic: simp only [Ne, Prod.mk_inj, not_and_or] at hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
have inl : ∀ (hi : i < m), f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
Tactic: obtain hi | hj : i < m ∨ j < n := by
          lia
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ (n : ℕ), f.coeff n ∉ P
hg : ∃ (n : ℕ), g.coeff n ∉ P
m : ℕ := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf
n : ℕ := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
inl : ∀ (hi : i < m), f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
have inr : ∀ (hj : j < n), f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
Tactic: obtain hi | hj : i < m ∨ j < n := by
          lia