awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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
⊢ Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I)) f
have h₂ : ∀ (hzero : f.eraseLead = 0),
  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
-- 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
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))
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
have he : f.eraseLead ∈ I
Tactic: have he : f.eraseLead ∈ I := by simpa using I.sub_mem hfI (map_comap_le h)
-- 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))
hzero : f.eraseLead = 0
⊢ 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 (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I))
  (f.eraseLead +
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
Tactic: rwa [← f.eraseLead_add_C_mul_X_pow, hzero, zero_add]
-- 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))
hzero : f.eraseLead = 0
h₁ :
  Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I))
    (f.eraseLead +
      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₂ : Membership.mem (γ := Submodule R[X] R[X]) (map (F := R →+* R[X]) C (comap (F := R →+* R[X]) C I))
  (0 + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
Tactic: rwa [← f.eraseLead_add_C_mul_X_pow, hzero, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
I : Ideal R[X]
cf : ∀ (i : ℕ), Membership.mem (α := R[X]) I ((C : (a : R) → R[X]) (f.coeff i) : R[X])
⊢ Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)} ≤ I
have simp : Ideal.span {g : R[X] | ∃ (i : ℕ), (C : (a : R) → R[X]) (f.coeff i) = g} ≤ I
Tactic: simp only [@eq_comm _ _ (C _)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)}
⊢ Membership.mem (γ := Ideal R[X]) (Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)}) f
have nth_rw : Membership.mem (γ := Ideal R[X]) (Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)})
  (f.sum fun (n : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
Tactic: nth_rw 2 [(sum_C_mul_X_pow_eq f).symm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)}
⊢ Membership.mem (γ := Ideal R[X]) (Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)})
    (f.sum fun (n : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
have refine : ∀ (n : ℕ) (_hn : n ∈ f.support),
  Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)})
    ((fun (n : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) n
      (f.coeff n))
Tactic: refine Submodule.sum_mem _ fun n _hn => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
⊢ Membership.mem (α := R[X]) p ((C : (a : R) → R[X]) (f.coeff n) : R[X])
have a : Membership.mem (α := R[X]) (γ := Set R[X]) {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)}
  ((C : (a : R) → R[X]) (f.coeff n) : R[X])
Tactic: apply subset_span
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
w : ℕ
⊢ ∃ (i : ℕ), Eq (α := R[X]) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) ((C : (a : R) → R[X]) (f.coeff i) : R[X])
have h : Eq (α := R[X]) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) ((C : (a : R) → R[X]) (f.coeff n) : R[X])
Tactic: use n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)})
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
have this : Membership.mem (α := R[X]) p ((C : (a : R) → R[X]) (f.coeff n) : R[X])
Tactic: have : C (coeff f n) ∈ p := by
    apply subset_span
    rw [mem_setOf_eq]
    use n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
this : Membership.mem (α := R[X]) p ((C : (a : R) → R[X]) (f.coeff n) : R[X])
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)})
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
have this₁ : HSMul.hSMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) 1) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) ∈ p
Tactic: have : monomial n (1 : R) • C (coeff f n) ∈ p := p.smul_mem _ this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
this_1 : Membership.mem (α := R[X]) p ((C : (a : R) → R[X]) (f.coeff n) : R[X])
this :
  HSMul.hSMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) 1) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) ∈ p
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)})
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n))
have h : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n) =
  HSMul.hSMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) 1) ((C : (a : R) → R[X]) (f.coeff n) : R[X])
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
this_1 : Membership.mem (α := R[X]) p ((C : (a : R) → R[X]) (f.coeff n) : R[X])
this :
  HSMul.hSMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) 1) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) ∈ p
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n) =
    HSMul.hSMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) 1) ((C : (a : R) → R[X]) (f.coeff n) : R[X])
have h : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n) =
  (monomial n : (a : R) → R[X]) (f.coeff n)
Tactic: simp only [monomial_mul_C, one_mul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : Semiring R
f : R[X]
p : Ideal R[X] := Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)}
n : ℕ
_hn : n ∈ f.support
this_1 : Membership.mem (α := R[X]) p ((C : (a : R) → R[X]) (f.coeff n) : R[X])
this :
  HSMul.hSMul (α := R[X]) (β := R[X]) ((monomial n : (a : R) → R[X]) 1) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) ∈ p
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n) =
    (monomial n : (a : R) → R[X]) (f.coeff n)
have h : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n) =
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n)
Tactic: rw [← C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
r : R
hr : Prime r
⊢ Prime (M := R[X]) ((C : (a : R) → R[X]) r : R[X])
have this : r ≠ 0
Tactic: have := hr.1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
r : R
hr : Prime r
this : r ≠ 0
⊢ Prime (M := R[X]) ((C : (a : R) → R[X]) r : R[X])
have rw : ∀ (hr : Ideal.IsPrime (α := R) (Ideal.span {r})) (this : r ≠ 0),
  Ideal.IsPrime (α := R[X]) (Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) r : R[X])))
Tactic: rw [← Ideal.span_singleton_prime] at hr ⊢
Cleared hypotheses: hr, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
r : R
hr : Prime r
this : r ≠ 0
rw :
  ∀ (hr : Ideal.IsPrime (α := R) (Ideal.span {r})) (this : r ≠ 0),
    Ideal.IsPrime (α := R[X]) (Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) r : R[X])))
⊢ Prime (M := R[X]) ((C : (a : R) → R[X]) r : R[X])
have rw₁ : ∀ (hr : Ideal.IsPrime (α := R) (Ideal.span {r})) (this : r ≠ 0),
  Ne (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])
Tactic: rw [← Ideal.span_singleton_prime] at hr ⊢
Cleared hypotheses: hr, this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst : CommRing R
r : R
hr : Ideal.IsPrime (α := R) (Ideal.span {r})
this : r ≠ 0
⊢ Ideal.IsPrime (α := R[X]) (Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) r : R[X])))
have rw : Ideal.IsPrime (α := R[X]) (Ideal.map (R := R) (F := R →+* R[X]) C (Ideal.span {r}))
Tactic: rw [← Set.image_singleton, ← Ideal.map_span]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
r : R
inst : CommRing R
inst_1 : Finite σ
⊢ Prime (M := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔ Prime r
have have : ∀ (this : Fintype σ), Prime (M := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔ Prime r
Tactic: have := Fintype.ofFinite σ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
r : R
inst : CommRing R
inst_1 : Finite σ
this : Fintype σ
⊢ Prime (M := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔ Prime r
have rw : Prime.{u} (M := MvPolynomial (Fin (Fintype.card σ)) R)
    ((renameEquiv R (Fintype.equivFin σ) : (a : MvPolynomial σ R) → MvPolynomial (Fin (Fintype.card σ)) R)
        ((C : (a : R) → MvPolynomial σ R) r) :
      MvPolynomial (Fin (Fintype.card σ)) R) ↔
  Prime r
Tactic: rw [← MulEquiv.prime_iff (renameEquiv R (Fintype.equivFin σ))]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
r : R
inst : CommRing R
inst_1 : Finite σ
this : Fintype σ
⊢ Prime.{u} (M := MvPolynomial (Fin (Fintype.card σ)) R)
      ((renameEquiv R (Fintype.equivFin σ) : (a : MvPolynomial σ R) → MvPolynomial (Fin (Fintype.card σ)) R)
          ((C : (a : R) → MvPolynomial σ R) r) :
        MvPolynomial (Fin (Fintype.card σ)) R) ↔
    Prime r
have h : Prime.{u} (M := MvPolynomial (Fin (Fintype.card σ)) R)
    ((renameEquiv R (Fintype.equivFin σ) : (a : MvPolynomial σ R) → MvPolynomial (Fin (Fintype.card σ)) R)
        ((C : (a : R) → MvPolynomial σ R) r) :
      MvPolynomial (Fin (Fintype.card σ)) R) ↔
  Prime (M := MvPolynomial (Fin (Fintype.card σ)) R)
    ((C : (a : R) → MvPolynomial (Fin (Fintype.card σ)) R) r : MvPolynomial (Fin (Fintype.card σ)) R)
Tactic: convert_to Prime (C r) ↔ _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
r : R
inst : CommRing R
inst_1 : Finite σ
this : Fintype σ
h :
  Prime.{u} (M := MvPolynomial (Fin (Fintype.card σ)) R)
      ((renameEquiv R (Fintype.equivFin σ) : (a : MvPolynomial σ R) → MvPolynomial (Fin (Fintype.card σ)) R)
          ((C : (a : R) → MvPolynomial σ R) r) :
        MvPolynomial (Fin (Fintype.card σ)) R) ↔
    Prime (M := MvPolynomial (Fin (Fintype.card σ)) R)
      ((C : (a : R) → MvPolynomial (Fin (Fintype.card σ)) R) r : MvPolynomial (Fin (Fintype.card σ)) R)
⊢ Prime.{u} (M := MvPolynomial (Fin (Fintype.card σ)) R)
      ((renameEquiv R (Fintype.equivFin σ) : (a : MvPolynomial σ R) → MvPolynomial (Fin (Fintype.card σ)) R)
          ((C : (a : R) → MvPolynomial σ R) r) :
        MvPolynomial (Fin (Fintype.card σ)) R) ↔
    Prime r
have convert_1 : Type
Tactic: convert_to Prime (C r) ↔ _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
r : R
inst : CommRing R
inst_1 : Finite σ
this : Fintype σ
h :
  Prime.{u} (M := MvPolynomial (Fin (Fintype.card σ)) R)
      ((renameEquiv R (Fintype.equivFin σ) : (a : MvPolynomial σ R) → MvPolynomial (Fin (Fintype.card σ)) R)
          ((C : (a : R) → MvPolynomial σ R) r) :
        MvPolynomial (Fin (Fintype.card σ)) R) ↔
    Prime (M := MvPolynomial (Fin (Fintype.card σ)) R)
      ((C : (a : R) → MvPolynomial (Fin (Fintype.card σ)) R) r : MvPolynomial (Fin (Fintype.card σ)) R)
convert_1 : Type
⊢ Prime.{u} (M := MvPolynomial (Fin (Fintype.card σ)) R)
      ((renameEquiv R (Fintype.equivFin σ) : (a : MvPolynomial σ R) → MvPolynomial (Fin (Fintype.card σ)) R)
          ((C : (a : R) → MvPolynomial σ R) r) :
        MvPolynomial (Fin (Fintype.card σ)) R) ↔
    Prime r
have convert_3 : Prime (M := MvPolynomial (Fin (Fintype.card σ)) R)
    ((C : (a : R) → MvPolynomial (Fin (Fintype.card σ)) R) r : MvPolynomial (Fin (Fintype.card σ)) R) ↔
  Prime r
Tactic: convert_to Prime (C r) ↔ _
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
r : R
inst : CommRing R
inst_1 : Finite σ
this : Fintype σ
⊢ Prime.{u} (M := MvPolynomial (Fin (Fintype.card σ)) R)
      ((renameEquiv R (Fintype.equivFin σ) : (a : MvPolynomial σ R) → MvPolynomial (Fin (Fintype.card σ)) R)
          ((C : (a : R) → MvPolynomial σ R) r) :
        MvPolynomial (Fin (Fintype.card σ)) R) ↔
    Prime (M := MvPolynomial (Fin (Fintype.card σ)) R)
      ((C : (a : R) → MvPolynomial (Fin (Fintype.card σ)) R) r : MvPolynomial (Fin (Fintype.card σ)) R)
have h : Eq.{u + 1} (α := MvPolynomial (Fin (Fintype.card σ)) R)
  ((renameEquiv R (Fintype.equivFin σ) : (a : MvPolynomial σ R) → MvPolynomial (Fin (Fintype.card σ)) R)
      ((C : (a : R) → MvPolynomial σ R) r) :
    MvPolynomial (Fin (Fintype.card σ)) R)
  ((C : (a : R) → MvPolynomial (Fin (Fintype.card σ)) R) r : MvPolynomial (Fin (Fintype.card σ)) R)
Tactic: congr!
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
r : R
inst : CommRing R
inst_1 : Finite σ
this : Fintype σ
d : ℕ
hd : Prime (M := MvPolynomial (Fin d) R) ((C : (a : R) → MvPolynomial (Fin d) R) r : MvPolynomial (Fin d) R) ↔ Prime r
⊢ Prime (M := MvPolynomial (Fin (d + 1)) R)
      ((C : (a : R) → MvPolynomial (Fin (d + 1)) R) r : MvPolynomial (Fin (d + 1)) R) ↔
    Prime r
have h : Eq (α := MvPolynomial (Fin (d + 1)) R) ((C : (a : R) → MvPolynomial (Fin (d + 1)) R) r : MvPolynomial (Fin (d + 1)) R)
  ((AlgEquiv.symm (finSuccEquiv R d) : (a : (MvPolynomial (Fin d) R)[X]) → MvPolynomial (Fin (d + 1)) R)
      ((Polynomial.C : (a : MvPolynomial (Fin d) R) → (MvPolynomial (Fin d) R)[X])
        ((C : (a : R) → MvPolynomial (Fin d) R) r)) :
    MvPolynomial (Fin (d + 1)) R)
Tactic: convert! MulEquiv.prime_iff (finSuccEquiv R d).symm (p := Polynomial.C (C r))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
r : R
inst : CommRing R
inst_1 : Finite σ
this : Fintype σ
d : ℕ
hd : Prime (M := MvPolynomial (Fin d) R) ((C : (a : R) → MvPolynomial (Fin d) R) r : MvPolynomial (Fin d) R) ↔ Prime r
h :
  Eq (α := MvPolynomial (Fin (d + 1)) R) ((C : (a : R) → MvPolynomial (Fin (d + 1)) R) r : MvPolynomial (Fin (d + 1)) R)
    ((AlgEquiv.symm (finSuccEquiv R d) : (a : (MvPolynomial (Fin d) R)[X]) → MvPolynomial (Fin (d + 1)) R)
        ((Polynomial.C : (a : MvPolynomial (Fin d) R) → (MvPolynomial (Fin d) R)[X])
          ((C : (a : R) → MvPolynomial (Fin d) R) r)) :
      MvPolynomial (Fin (d + 1)) R)
⊢ Prime (M := MvPolynomial (Fin (d + 1)) R)
      ((C : (a : R) → MvPolynomial (Fin (d + 1)) R) r : MvPolynomial (Fin (d + 1)) R) ↔
    Prime r
have h₁ : Prime r ↔
  Prime (M := (MvPolynomial (Fin d) R)[X])
    ((Polynomial.C : (a : MvPolynomial (Fin d) R) → (MvPolynomial (Fin d) R)[X])
        ((C : (a : R) → MvPolynomial (Fin d) R) r) :
      (MvPolynomial (Fin d) R)[X])
Tactic: convert! MulEquiv.prime_iff (finSuccEquiv R d).symm (p := Polynomial.C (C r))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
r : R
inst : CommRing R
inst_1 : Finite σ
this : Fintype σ
⊢ Prime (M := MvPolynomial (Fin (Fintype.card σ)) R)
      ((C : (a : R) → MvPolynomial (Fin (Fintype.card σ)) R) r : MvPolynomial (Fin (Fintype.card σ)) R) ↔
    Prime r
have convert_3 : ∀ (x : ℕ),
  Prime (M := MvPolynomial (Fin x) R) ((C : (a : R) → MvPolynomial (Fin x) R) r : MvPolynomial (Fin x) R) ↔ Prime r
Tactic: induction Fintype.card σ with
    | zero => exact MulEquiv.prime_iff (isEmptyAlgEquiv R (Fin 0)).symm (p := r)
    | succ d hd =>
      convert! MulEquiv.prime_iff (finSuccEquiv R d).symm (p := Polynomial.C (C r))
      · simp [← finSuccEquiv_comp_C_eq_C]
      · simp [← hd, Polynomial.prime_C_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
r : R
hr : Prime r
h : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) (0 : MvPolynomial σ R)
⊢ r = 0
have rw : Eq (α := MvPolynomial σ R) 0 ((C : (a : R) → MvPolynomial σ R) 0)
Tactic: rw [← C_inj, h]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
r : R
hr : Prime r
h : IsUnit (M := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
⊢ IsUnit r
have rw : IsUnit.{u} (M := R)
  ((constantCoeff : (a : MvPolynomial σ R) → R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : R)
Tactic: rw [← constantCoeff_C _ r]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
r : R
hr : Prime r
a b : MvPolynomial σ R
hd : (C : (a : R) → MvPolynomial σ R) r ∣ a * b
⊢ (C : (a : R) → MvPolynomial σ R) r ∣ a ∨ (C : (a : R) → MvPolynomial σ R) r ∣ b
have obtain : ∀ (s : Finset σ) (a' b' : MvPolynomial.{v, u} (↥s) R)
  (hd :
    (C : (a : R) → MvPolynomial σ R) r ∣
      HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) a' :
          MvPolynomial σ R)
        ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) b' :
          MvPolynomial σ R)),
  Dvd.dvd (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) a' :
        MvPolynomial σ R) ∨
    Dvd.dvd (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) b' :
        MvPolynomial σ R)
Tactic: obtain ⟨s, a', b', rfl, rfl⟩ := exists_finset_rename₂ a b
Cleared hypotheses: a, b, hd
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
σ : Type v
inst : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial.{v, u} (↥s) R
hd :
  (C : (a : R) → MvPolynomial σ R) r ∣
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) a' :
        MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) b' :
        MvPolynomial σ R)
⊢ Dvd.dvd (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) a' :
        MvPolynomial σ R) ∨
    Dvd.dvd (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) b' :
        MvPolynomial σ R)
have hd₁ : (algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) r ∣
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) a' :
      MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) b' :
      MvPolynomial σ R)
Tactic: rw [← algebraMap_eq] at hd
Cleared hypotheses: hd