awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hi : i < m
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
have inl : g.coeff (i, j).2 * f.coeff (i, j).1 ∈ P
Tactic: rw [mul_comm]
-- 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
hi : i < m
⊢ g.coeff (i, j).2 * f.coeff (i, j).1 ∈ P
have inl : f.coeff (i, j).1 ∈ P
Tactic: apply P.mul_mem_left
-- 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
hj : j < n
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
have inr : g.coeff (i, j).2 ∈ P
Tactic: apply P.mul_mem_left
-- 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
mpr mpr₁ mpr₂ mpr₃ : ∃ (n : ℕ), (f * g).coeff n ∉ P
⊢ ∃ (n : ℕ), (f * g).coeff n ∉ P
have mpr₄ : let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
(f * g).coeff (m + n) ∉ P
Tactic: classical
        let m := Nat.find hf
        let n := Nat.find hg
        refine ⟨m + n, ?_⟩
        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]
        · apply mt h.2
          rw [not_or]
          exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩
        apply P.sum_mem
        rintro ⟨i, j⟩ hij
        rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij
        simp only [Ne, Prod.mk_inj, not_and_or] at hij
        obtain hi | hj : i < m ∨ j < n := by
          lia
        · rw [mul_comm]
          apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hf hi)
        · apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hg hj)
-- 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
mpr mpr₁ mpr₂ mpr₃ : ∃ (n : ℕ), (f * g).coeff n ∉ P
mpr₄ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  (f * g).coeff (m + n) ∉ P
⊢ ∃ (n : ℕ), (f * g).coeff n ∉ P
have mpr₅ : let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
f.coeff (m, n).1 * g.coeff (m, n).2 ∉ P
Tactic: classical
        let m := Nat.find hf
        let n := Nat.find hg
        refine ⟨m + n, ?_⟩
        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]
        · apply mt h.2
          rw [not_or]
          exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩
        apply P.sum_mem
        rintro ⟨i, j⟩ hij
        rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij
        simp only [Ne, Prod.mk_inj, not_and_or] at hij
        obtain hi | hj : i < m ∨ j < n := by
          lia
        · rw [mul_comm]
          apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hf hi)
        · apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hg hj)
-- 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
mpr mpr₁ mpr₂ mpr₃ : ∃ (n : ℕ), (f * g).coeff n ∉ P
mpr₄ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  (f * g).coeff (m + n) ∉ P
mpr₅ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  f.coeff (m, n).1 * g.coeff (m, n).2 ∉ P
⊢ ∃ (n : ℕ), (f * g).coeff n ∉ P
have let : let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
let 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
Tactic: classical
        let m := Nat.find hf
        let n := Nat.find hg
        refine ⟨m + n, ?_⟩
        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]
        · apply mt h.2
          rw [not_or]
          exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩
        apply P.sum_mem
        rintro ⟨i, j⟩ hij
        rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij
        simp only [Ne, Prod.mk_inj, not_and_or] at hij
        obtain hi | hj : i < m ∨ j < n := by
          lia
        · rw [mul_comm]
          apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hf hi)
        · apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hg hj)
-- 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
mpr mpr₁ mpr₂ mpr₃ : ∃ (n : ℕ), (f * g).coeff n ∉ P
mpr₄ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  (f * g).coeff (m + n) ∉ P
mpr₅ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  f.coeff (m, n).1 * g.coeff (m, n).2 ∉ P
let let₁ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let 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
⊢ ∃ (n : ℕ), (f * g).coeff n ∉ P
have let₂ : let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
∀ c ∈ (@antidiagonal _ Nat.instAddMonoid _ ((m, n).1 + (m, n).2)).erase (m, n), f.coeff c.1 * g.coeff c.2 ∈ P
Tactic: classical
        let m := Nat.find hf
        let n := Nat.find hg
        refine ⟨m + n, ?_⟩
        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]
        · apply mt h.2
          rw [not_or]
          exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩
        apply P.sum_mem
        rintro ⟨i, j⟩ hij
        rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij
        simp only [Ne, Prod.mk_inj, not_and_or] at hij
        obtain hi | hj : i < m ∨ j < n := by
          lia
        · rw [mul_comm]
          apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hf hi)
        · apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hg hj)
-- 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
mpr mpr₁ mpr₂ mpr₃ : ∃ (n : ℕ), (f * g).coeff n ∉ P
mpr₄ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  (f * g).coeff (m + n) ∉ P
mpr₅ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  f.coeff (m, n).1 * g.coeff (m, n).2 ∉ P
let let₁ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let 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
let₂ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  ∀ c ∈ (@antidiagonal _ Nat.instAddMonoid _ ((m, n).1 + (m, n).2)).erase (m, n), f.coeff c.1 * g.coeff c.2 ∈ P
⊢ ∃ (n : ℕ), (f * g).coeff n ∉ P
have let₃ : let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
let 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
Tactic: classical
        let m := Nat.find hf
        let n := Nat.find hg
        refine ⟨m + n, ?_⟩
        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]
        · apply mt h.2
          rw [not_or]
          exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩
        apply P.sum_mem
        rintro ⟨i, j⟩ hij
        rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij
        simp only [Ne, Prod.mk_inj, not_and_or] at hij
        obtain hi | hj : i < m ∨ j < n := by
          lia
        · rw [mul_comm]
          apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hf hi)
        · apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hg hj)
-- 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
mpr mpr₁ mpr₂ mpr₃ : ∃ (n : ℕ), (f * g).coeff n ∉ P
mpr₄ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  (f * g).coeff (m + n) ∉ P
mpr₅ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  f.coeff (m, n).1 * g.coeff (m, n).2 ∉ P
let let₁ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let 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
let₂ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  ∀ c ∈ (@antidiagonal _ Nat.instAddMonoid _ ((m, n).1 + (m, n).2)).erase (m, n), f.coeff c.1 * g.coeff c.2 ∈ P
let₃ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let 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
⊢ ∃ (n : ℕ), (f * g).coeff n ∉ P
have let₄ : let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
let 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
Tactic: classical
        let m := Nat.find hf
        let n := Nat.find hg
        refine ⟨m + n, ?_⟩
        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]
        · apply mt h.2
          rw [not_or]
          exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩
        apply P.sum_mem
        rintro ⟨i, j⟩ hij
        rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij
        simp only [Ne, Prod.mk_inj, not_and_or] at hij
        obtain hi | hj : i < m ∨ j < n := by
          lia
        · rw [mul_comm]
          apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hf hi)
        · apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hg hj)
-- 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
mpr mpr₁ mpr₂ mpr₃ : ∃ (n : ℕ), (f * g).coeff n ∉ P
mpr₄ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  (f * g).coeff (m + n) ∉ P
mpr₅ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  f.coeff (m, n).1 * g.coeff (m, n).2 ∉ P
let let₁ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let 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
let₂ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  ∀ c ∈ (@antidiagonal _ Nat.instAddMonoid _ ((m, n).1 + (m, n).2)).erase (m, n), f.coeff c.1 * g.coeff c.2 ∈ P
let₃ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let 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
let₄ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let 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
⊢ ∃ (n : ℕ), (f * g).coeff n ∉ P
have let₅ : let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
let 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
Tactic: classical
        let m := Nat.find hf
        let n := Nat.find hg
        refine ⟨m + n, ?_⟩
        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]
        · apply mt h.2
          rw [not_or]
          exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩
        apply P.sum_mem
        rintro ⟨i, j⟩ hij
        rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij
        simp only [Ne, Prod.mk_inj, not_and_or] at hij
        obtain hi | hj : i < m ∨ j < n := by
          lia
        · rw [mul_comm]
          apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hf hi)
        · apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hg hj)
-- 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
mpr mpr₁ mpr₂ mpr₃ : ∃ (n : ℕ), (f * g).coeff n ∉ P
mpr₄ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  (f * g).coeff (m + n) ∉ P
mpr₅ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  f.coeff (m, n).1 * g.coeff (m, n).2 ∉ P
let let₁ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let 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
let₂ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  ∀ c ∈ (@antidiagonal _ Nat.instAddMonoid _ ((m, n).1 + (m, n).2)).erase (m, n), f.coeff c.1 * g.coeff c.2 ∈ P
let₃ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let 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
let₄ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let 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
let₅ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let 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
⊢ ∃ (n : ℕ), (f * g).coeff n ∉ P
have inl : let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
∀ (i j : ℕ) (hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n) (hi : i < m), f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
Tactic: classical
        let m := Nat.find hf
        let n := Nat.find hg
        refine ⟨m + n, ?_⟩
        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]
        · apply mt h.2
          rw [not_or]
          exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩
        apply P.sum_mem
        rintro ⟨i, j⟩ hij
        rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij
        simp only [Ne, Prod.mk_inj, not_and_or] at hij
        obtain hi | hj : i < m ∨ j < n := by
          lia
        · rw [mul_comm]
          apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hf hi)
        · apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hg hj)
-- 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
mpr mpr₁ mpr₂ mpr₃ : ∃ (n : ℕ), (f * g).coeff n ∉ P
mpr₄ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  (f * g).coeff (m + n) ∉ P
mpr₅ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  f.coeff (m, n).1 * g.coeff (m, n).2 ∉ P
let let₁ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let 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
let₂ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  ∀ c ∈ (@antidiagonal _ Nat.instAddMonoid _ ((m, n).1 + (m, n).2)).erase (m, n), f.coeff c.1 * g.coeff c.2 ∈ P
let₃ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let 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
let₄ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let 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
let₅ :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let 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
inl :
  let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
  let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
  ∀ (i j : ℕ) (hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n) (hi : i < m), f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
⊢ ∃ (n : ℕ), (f * g).coeff n ∉ P
have inr : let m := Nat.find (p := fun (n : ℕ) ↦ f.coeff n ∉ P) hf;
let n := Nat.find (p := fun (n : ℕ) ↦ g.coeff n ∉ P) hg;
∀ (i j : ℕ) (hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n) (hj : j < n), f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P
Tactic: classical
        let m := Nat.find hf
        let n := Nat.find hg
        refine ⟨m + n, ?_⟩
        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]
        · apply mt h.2
          rw [not_or]
          exact ⟨Nat.find_spec hf, Nat.find_spec hg⟩
        apply P.sum_mem
        rintro ⟨i, j⟩ hij
        rw [Finset.mem_erase, Finset.mem_antidiagonal] at hij
        simp only [Ne, Prod.mk_inj, not_and_or] at hij
        obtain hi | hj : i < m ∨ j < n := by
          lia
        · rw [mul_comm]
          apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hf hi)
        · apply P.mul_mem_left
          exact Classical.not_not.1 (Nat.find_min hg hj)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R[X]
hI : comap (F := R →+* R[X]) C I = I.leadingCoeff
⊢ map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I) = I
have refine : ∀ (f : R[X]) (hfI : f ∈ I),
  Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
Tactic: refine le_antisymm map_comap_le (fun f hfI ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R[X]
hI : comap (F := R →+* R[X]) C I = I.leadingCoeff
f : R[X]
hfI : f ∈ I
⊢ Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
have h : ∀ (n : ℕ)
  (ih :
    ∀ m < n,
      ∀ (f : R[X]) (hfI : f ∈ I) (hn : f.natDegree = m),
        Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f)
  (f : R[X]) (hfI : f ∈ I) (hn : f.natDegree = n),
  Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
Tactic: induction hn : f.natDegree using Nat.strong_induction_on generalizing f with | _ _ ih
Cleared hypotheses: f, hfI
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
I : Ideal R[X]
hI : comap (F := R →+* R[X]) C I = I.leadingCoeff
n : ℕ
ih :
  ∀ m < n,
    ∀ (f : R[X]) (hfI : f ∈ I) (hn : f.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n
⊢ Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
have h : Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I))
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
Tactic: have h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I) :=
    (map C (comap C I)).mul_mem_right (X ^ f.natDegree) <| mem_map_of_mem C <| by
      simpa [hI] using (I.mem_leadingCoeff f.leadingCoeff).2 ⟨f, hfI, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
I : Ideal R[X]
hI : comap (F := R →+* R[X]) C I = I.leadingCoeff
n : ℕ
ih :
  ∀ m < n,
    ∀ (f : R[X]) (hfI : f ∈ I) (hn : f.natDegree = m),
      Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
f : R[X]
hfI : f ∈ I
hn : f.natDegree = n
h :
  Membership.mem (γ := Ideal R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I))
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
⊢ Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
have h₁ : ∀ (hlt : f.eraseLead.natDegree < f.natDegree),
  Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
Tactic: rcases f.eraseLead_natDegree_lt_or_eraseLead_eq_zero with hlt | hzero