awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Basic
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))
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))
h₃ h₄ h₅ h₆ :
  Membership.mem (γ := Submodule R[X] 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

Tactic:
rwa [← f.eraseLead_add_C_mul_X_pow, hzero, zero_add]

Premises used: Polynomial.eraseLead_add_C_mul_X_pow, zero_add
-- Module: Mathlib.RingTheory.Polynomial.Basic
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])
simp : Ideal.span {g : R[X] | ∃ (i : ℕ), (C : (a : R) → R[X]) (f.coeff i) = g} ≤ I
⊢ Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)} ≤ I

Tactic:
simp only [@eq_comm _ _ (C _)]

Premises used: eq_comm
-- Module: Mathlib.RingTheory.Polynomial.Basic
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 : ℕ), (C : (a : R) → R[X]) (f.coeff i) = g} ≤ I

Tactic:
(Ideal.span_le.trans range_subset_iff).mpr cf

Premises used: Ideal.span_le, Iff.mpr, Set.Mem, setOf, Iff.trans, Set.range, Set.range_subset_iff
-- Module: Mathlib.RingTheory.Polynomial.Basic
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 : ℕ), (C : (a : R) → R[X]) (f.coeff i) = g} ≤ I

Tactic:
exact (Ideal.span_le.trans range_subset_iff).mpr cf

Premises used: Ideal.span_le, Iff.mpr, Iff.trans, Set.range_subset_iff
-- Module: Mathlib.RingTheory.Polynomial.Basic
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)}
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))
⊢ Membership.mem (γ := Ideal R[X]) (Ideal.span {g : R[X] | ∃ (i : ℕ), g = (C : (a : R) → R[X]) (f.coeff i)}) f

Tactic:
nth_rw 2 [(sum_C_mul_X_pow_eq f).symm]

Premises used: Polynomial.sum_C_mul_X_pow_eq, Eq.symm
-- Module: Mathlib.RingTheory.Polynomial.Basic
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))

Tactic:
Submodule.sum_mem _ fun n _hn => ?_

Premises used: Set.Mem, Polynomial.sum, Submodule.sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
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)}
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))
⊢ 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:
refine Submodule.sum_mem _ fun n _hn => ?_

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
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])
⊢ Membership.mem (α := R[X]) p ((C : (a : R) → R[X]) (f.coeff n) : R[X])

Tactic:
apply subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.RingTheory.Polynomial.Basic
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 : ℕ
h : Eq (α := R[X]) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) ((C : (a : R) → R[X]) (f.coeff n) : R[X])
⊢ ∃ (i : ℕ), Eq (α := R[X]) ((C : (a : R) → R[X]) (f.coeff n) : R[X]) ((C : (a : R) → R[X]) (f.coeff i) : R[X])

Tactic:
use n
-- Module: Mathlib.RingTheory.Polynomial.Basic
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])

Tactic:
have : C (coeff f n) ∈ p := by
    apply subset_span
    rw [mem_setOf_eq]
    use n
-- Module: Mathlib.RingTheory.Polynomial.Basic
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])
⊢ 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
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
⊢ 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:
this
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
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])
⊢ 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))

Tactic:
convert! this using 1
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
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)
⊢ 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:
simp only [monomial_mul_C, one_mul, smul_eq_mul]

Premises used: Polynomial.monomial_mul_C, smul_eq_mul, one_mul
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
h 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)
⊢ 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:
rw [← C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : Semiring R
f : R[X]
I : Ideal R[X]
⊢ f ∉ I → ∃ (i : ℕ), ((C : (a : R) → R[X]) (f.coeff i) : R[X]) ∉ I

Tactic:
Not.imp_symm fun cf => span_le_of_C_coeff_mem (not_exists_not.mp cf) mem_span_C_coeff

Premises used: span_le_of_C_coeff_mem, Not.imp_symm, mem_span_C_coeff, Iff.mp, Classical.not_exists_not
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
r : R
hr : Prime r
⊢ r ≠ 0

Tactic:
have := hr.1
-- Module: Mathlib.RingTheory.Polynomial.Basic
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])))
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])
rw₂ : r ≠ 0
⊢ Prime (M := R[X]) ((C : (a : R) → R[X]) r : R[X])

Tactic:
rw [← Ideal.span_singleton_prime] at hr ⊢

Premises used: Ideal.span_singleton_prime
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
r : R
hr : Ideal.IsPrime (α := R) (Ideal.span {r})
this : r ≠ 0
rw : Ideal.IsPrime (α := R[X]) (Ideal.map (R := R) (F := R →+* R[X]) C (Ideal.span {r}))
⊢ Ideal.IsPrime (α := R[X]) (Ideal.span (singleton (α := R[X]) ((C : (a : R) → R[X]) r : R[X])))

Tactic:
rw [← Set.image_singleton, ← Ideal.map_span]

Premises used: Set.image_singleton, Ideal.map_span
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
r : R
hr : Ideal.IsPrime (α := R) (Ideal.span {r})
this : r ≠ 0
⊢ Ideal.IsPrime (α := R[X]) (Ideal.map (R := R) (F := R →+* R[X]) C (Ideal.span {r}))

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
r : R
hr : Ideal.IsPrime (α := R) (Ideal.span {r})
this : r ≠ 0
h : Eq (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X])
⊢ False

Tactic:
apply (this (C_eq_zero.mp h))

Premises used: Polynomial.C_eq_zero, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
inst : CommRing R
r : R
hr : Prime r
this : r ≠ 0
⊢ r ≠ 0

Tactic:
assumption
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R_1 : Type u
S : Type u_1
σ : Type v
M : Type w
inst : CommRing R_1
inst_1 : CommRing S
inst_2 : AddCommGroup M
inst_3 : Module R_1 M
r : R_1
ι : Type u_2
R : Type u_3
inst_4 : CommSemiring R
inst_5 : IsEmpty ι
⊢ Module.Finite R (MvPolynomial ι R)

Tactic:
Module.Finite.equiv (MvPolynomial.isEmptyAlgEquiv R ι).toLinearEquiv.symm

Premises used: LinearEquiv.symm, MvPolynomial.isEmptyAlgEquiv, AlgEquiv.toLinearEquiv, Module.Finite.equiv
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
r : R
inst : CommRing R
inst_1 : Finite σ
have :
  ∀ (this : Fintype σ), Prime (M := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔ Prime r
⊢ Prime (M := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔ Prime r

Tactic:
have := Fintype.ofFinite σ
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
r : R
inst : CommRing R
inst_1 : Finite σ
this : Fintype σ
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
⊢ Prime (M := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔ Prime r

Tactic:
rw [← MulEquiv.prime_iff (renameEquiv R (Fintype.equivFin σ))]

Premises used: MulEquiv.prime_iff, Fintype.equivFin, MvPolynomial.renameEquiv
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
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
⊢ 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:
convert_to Prime (C r) ↔ _

Premises used: Prime, MvPolynomial.C, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
r : R
inst : CommRing R
inst_1 : Finite σ
this : Fintype σ
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)
⊢ 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:
congr!
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
r : R
inst : CommRing R
inst_1 : Finite σ
this : Fintype σ
⊢ 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:
simp only [renameEquiv_apply, algHom_C, algebraMap_eq]

Premises used: MvPolynomial.renameEquiv_apply, MvPolynomial.algHom_C, MvPolynomial.algebraMap_eq
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
r : R
inst : CommRing R
inst_1 : Finite σ
this : Fintype σ
⊢ Prime (M := MvPolynomial (Fin 0) R) ((C : (a : R) → MvPolynomial (Fin 0) R) r : MvPolynomial (Fin 0) R) ↔ Prime r

Tactic:
MulEquiv.prime_iff (isEmptyAlgEquiv R (Fin 0)).symm (p := r)

Premises used: AlgEquiv.symm, MulEquiv.prime_iff, MvPolynomial.isEmptyAlgEquiv, OfNat.ofNat, Fin, Finsupp.single
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
r : R
inst : CommRing R
inst_1 : Finite σ
this : Fintype σ
⊢ Prime (M := MvPolynomial (Fin 0) R) ((C : (a : R) → MvPolynomial (Fin 0) R) r : MvPolynomial (Fin 0) R) ↔ Prime r

Tactic:
exact MulEquiv.prime_iff (isEmptyAlgEquiv R (Fin 0)).symm (p := r)

Premises used: AlgEquiv.symm, MulEquiv.prime_iff, MvPolynomial.isEmptyAlgEquiv, OfNat.ofNat, Fin
-- Module: Mathlib.RingTheory.Polynomial.Basic
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)
      ((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) 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:
MulEquiv.prime_iff (finSuccEquiv R d).symm (p := Polynomial.C (C r))

Premises used: AlgEquiv.symm, MulEquiv.prime_iff, MvPolynomial.finSuccEquiv
-- Module: Mathlib.RingTheory.Polynomial.Basic
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)
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])
⊢ Prime (M := MvPolynomial (Fin (d + 1)) R)
      ((C : (a : R) → MvPolynomial (Fin (d + 1)) R) r : MvPolynomial (Fin (d + 1)) R) ↔
    Prime r

Tactic:
convert! MulEquiv.prime_iff (finSuccEquiv R d).symm (p := Polynomial.C (C r))

Premises used: AlgEquiv.symm, MulEquiv.prime_iff, MvPolynomial.finSuccEquiv
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
⊢ 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:
simp [← finSuccEquiv_comp_C_eq_C]

Premises used: MvPolynomial.finSuccEquiv_comp_C_eq_C
-- Module: Mathlib.RingTheory.Polynomial.Basic
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 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:
simp [← hd, Polynomial.prime_C_iff]

Premises used: Polynomial.prime_C_iff
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
r : R
inst : CommRing R
inst_1 : Finite σ
this : Fintype σ
convert_3 :
  ∀ (x : ℕ),
    Prime (M := MvPolynomial (Fin x) R) ((C : (a : R) → MvPolynomial (Fin x) R) r : MvPolynomial (Fin x) R) ↔ Prime r
⊢ Prime (M := MvPolynomial (Fin (Fintype.card σ)) R)
      ((C : (a : R) → MvPolynomial (Fin (Fintype.card σ)) R) r : MvPolynomial (Fin (Fintype.card σ)) 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]

Premises used: Polynomial.prime_C_iff, AlgEquiv.symm, MulEquiv.prime_iff, Fintype.card, MvPolynomial.isEmptyAlgEquiv, MvPolynomial.finSuccEquiv_comp_C_eq_C, OfNat.ofNat, Fin
-- Module: Mathlib.RingTheory.Polynomial.Basic
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)
rw : Eq (α := MvPolynomial σ R) 0 ((C : (a : R) → MvPolynomial σ R) 0)
⊢ r = 0

Tactic:
rw [← C_inj, h]

Premises used: MvPolynomial.C_inj
-- Module: Mathlib.RingTheory.Polynomial.Basic
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)
⊢ Eq (α := MvPolynomial σ R) 0 ((C : (a : R) → MvPolynomial σ R) 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Basic
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)
rw :
  IsUnit.{u} (M := R)
    ((constantCoeff : (a : MvPolynomial σ R) → R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : R)
rw₁ : Type v
⊢ IsUnit r

Tactic:
rw [← constantCoeff_C _ r]

Premises used: MvPolynomial.constantCoeff_C
-- Module: Mathlib.RingTheory.Polynomial.Basic
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.{u} (M := R)
    ((constantCoeff : (a : MvPolynomial σ R) → R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : R)

Tactic:
h.map _

Premises used: IsUnit.map
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
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)
⊢ (C : (a : R) → MvPolynomial σ R) r ∣ a ∨ (C : (a : R) → MvPolynomial σ R) r ∣ b

Tactic:
obtain ⟨s, a', b', rfl, rfl⟩ := exists_finset_rename₂ a b

Premises used: MvPolynomial.exists_finset_rename₂, rfl