awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial.{v, u} (↥s) R
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)
⊢ (algebraMap R (MvPolynomial.{v, u} (↥s) R) : (a : R) → MvPolynomial (↥s) R) r ∣ a' * b'
have h : Eq (α := MvPolynomial.{v, u} (↥s) R)
  ((algebraMap R (MvPolynomial.{v, u} (↥s) R) : (a : R) → MvPolynomial (↥s) R) r : MvPolynomial.{v, u} (↥s) R)
  ((killCompl sorry : (a : MvPolynomial σ R) → MvPolynomial (↥s) R)
      ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) r) :
    MvPolynomial.{v, u} (↥s) R)
Tactic: convert! _root_.map_dvd (killCompl Subtype.val_injective) hd
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial.{v, u} (↥s) R
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)
h :
  Eq (α := MvPolynomial.{v, u} (↥s) R)
    ((algebraMap R (MvPolynomial.{v, u} (↥s) R) : (a : R) → MvPolynomial (↥s) R) r : MvPolynomial.{v, u} (↥s) R)
    ((killCompl ⋯ : (a : MvPolynomial σ R) → MvPolynomial (↥s) R)
        ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) r) :
      MvPolynomial.{v, u} (↥s) R)
⊢ (algebraMap R (MvPolynomial.{v, u} (↥s) R) : (a : R) → MvPolynomial (↥s) R) r ∣ a' * b'
have h₁ : a' * b' =
  (killCompl sorry : (a : MvPolynomial σ R) → MvPolynomial (↥s) 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: convert! _root_.map_dvd (killCompl Subtype.val_injective) 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 :
  (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)
⊢ 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 this : (algebraMap R (MvPolynomial.{v, u} (↥s) R) : (a : R) → MvPolynomial (↥s) R) r ∣ a' * b'
Tactic: have : algebraMap R _ r ∣ a' * b' := by
        convert! _root_.map_dvd (killCompl Subtype.val_injective) hd
        · simp
        · simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
r : R
hr : Prime r
s : Finset σ
a' b' : MvPolynomial.{v, u} (↥s) R
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)
this : (algebraMap R (MvPolynomial.{v, u} (↥s) R) : (a : R) → MvPolynomial (↥s) R) r ∣ a' * b'
⊢ 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 rw : Dvd.dvd (α := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R)
        ((C : (a : R) → MvPolynomial (↥s) 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)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R)
        ((C : (a : R) → MvPolynomial (↥s) R) r) :
      MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↥s) R) → MvPolynomial σ R) b' :
      MvPolynomial σ R)
Tactic: rw [← rename_C ((↑) : s → σ)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
s : Set σ
p : MvPolynomial.{v, u} (↑s : Type v) R
⊢ Prime (M := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
          p :
        MvPolynomial σ R) ↔
    Prime p
have symm : Prime p ↔
  Prime (M := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R) p :
      MvPolynomial σ R)
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
s : Set σ
p : MvPolynomial.{v, u} (↑s : Type v) R
eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial.{v, u} (↑s : Type v) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R (↑sᶜ : Type v) (↑s : Type v)))
    (renameEquiv R (Equiv.trans (Equiv.sumComm (↑sᶜ : Type v) (↑s : Type v)) (Equiv.Set.sumCompl s)))
⊢ AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) =
    (↑eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R) →ₐ[R] MvPolynomial σ R).comp C
have hC : ∀ (r : R),
  Eq (α := MvPolynomial σ R)
    ((AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) :
          (a : MvPolynomial (↑s : Type v) R) → MvPolynomial σ R)
        ((C : (a : R) → MvPolynomial (↑s : Type v) R) r) :
      MvPolynomial σ R)
    (((↑eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R) →ₐ[R] MvPolynomial σ R).comp C :
          (a : MvPolynomial (↑s : Type v) R) → MvPolynomial σ R)
        ((C : (a : R) → MvPolynomial (↑s : Type v) R) r) :
      MvPolynomial σ R)
Tactic: apply ringHom_ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
s : Set σ
p : MvPolynomial.{v, u} (↑s : Type v) R
eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial.{v, u} (↑s : Type v) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R (↑sᶜ : Type v) (↑s : Type v)))
    (renameEquiv R (Equiv.trans (Equiv.sumComm (↑sᶜ : Type v) (↑s : Type v)) (Equiv.Set.sumCompl s)))
hC :
  ∀ (r : R),
    Eq (α := MvPolynomial σ R)
      ((AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) :
            (a : MvPolynomial (↑s : Type v) R) → MvPolynomial σ R)
          ((C : (a : R) → MvPolynomial (↑s : Type v) R) r) :
        MvPolynomial σ R)
      (((↑eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R) →ₐ[R] MvPolynomial σ R).comp C :
            (a : MvPolynomial (↑s : Type v) R) → MvPolynomial σ R)
          ((C : (a : R) → MvPolynomial (↑s : Type v) R) r) :
        MvPolynomial σ R)
⊢ AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) =
    (↑eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R) →ₐ[R] MvPolynomial σ R).comp C
have hX : ∀ (i : (↑s : Type v)),
  Eq (α := MvPolynomial σ R)
    ((AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) :
          (a : MvPolynomial (↑s : Type v) R) → MvPolynomial σ R)
        (X i) :
      MvPolynomial σ R)
    (((↑eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R) →ₐ[R] MvPolynomial σ R).comp C :
          (a : MvPolynomial (↑s : Type v) R) → MvPolynomial σ R)
        (X i) :
      MvPolynomial σ R)
Tactic: apply ringHom_ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
σ : Type v
inst : CommRing R
s : Set σ
p : MvPolynomial.{v, u} (↑s : Type v) R
eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial.{v, u} (↑s : Type v) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R (↑sᶜ : Type v) (↑s : Type v)))
    (renameEquiv R (Equiv.trans (Equiv.sumComm (↑sᶜ : Type v) (↑s : Type v)) (Equiv.Set.sumCompl s)))
⊢ Prime p ↔
    Prime (M := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
          p :
        MvPolynomial σ R)
have this : AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) =
  (↑eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R) →ₐ[R] MvPolynomial σ R).comp C
Tactic: have : (rename (↑)).toRingHom = eqv.toAlgHom.toRingHom.comp C := by
      apply ringHom_ext
      · intro
        simp only [eqv, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, rename_C,
          AlgEquiv.toAlgHom_toRingHom, RingHom.coe_comp, AlgEquiv.coe_trans,
          Function.comp_apply, MvPolynomial.sumAlgEquiv_symm_apply, iterToSum_C_C,
          renameEquiv_apply, Equiv.coe_trans, Equiv.sumComm_apply]
      · intro
        simp only [eqv, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, rename_X,
          AlgEquiv.toAlgHom_toRingHom, RingHom.coe_comp, AlgEquiv.coe_trans,
          Function.comp_apply, MvPolynomial.sumAlgEquiv_symm_apply, iterToSum_C_X,
          renameEquiv_apply, Equiv.coe_trans, Equiv.sumComm_apply, Sum.swap_inr,
          Equiv.Set.sumCompl_apply_inl]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
σ : Type v
inst : CommRing R
s : Set σ
p : MvPolynomial.{v, u} (↑s : Type v) R
eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial.{v, u} (↑s : Type v) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R (↑sᶜ : Type v) (↑s : Type v)))
    (renameEquiv R (Equiv.trans (Equiv.sumComm (↑sᶜ : Type v) (↑s : Type v)) (Equiv.Set.sumCompl s)))
this :
  AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) =
    (↑eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R) →ₐ[R] MvPolynomial σ R).comp C
⊢ Prime p ↔
    Prime (M := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
          p :
        MvPolynomial σ R)
have this₁ : Eq (α := MvPolynomial σ R)
  ((AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) :
        (a : MvPolynomial (↑s : Type v) R) → MvPolynomial σ R)
      p :
    MvPolynomial σ R)
  (((↑eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R) →ₐ[R] MvPolynomial σ R).comp C :
        (a : MvPolynomial (↑s : Type v) R) → MvPolynomial σ R)
      p :
    MvPolynomial σ R)
Tactic: apply_fun (· p) at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
s : Set σ
p : MvPolynomial.{v, u} (↑s : Type v) R
eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial.{v, u} (↑s : Type v) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R (↑sᶜ : Type v) (↑s : Type v)))
    (renameEquiv R (Equiv.trans (Equiv.sumComm (↑sᶜ : Type v) (↑s : Type v)) (Equiv.Set.sumCompl s)))
this :
  Eq (α := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↑s : Type v) R) → MvPolynomial σ R) p :
      MvPolynomial σ R)
    ((eqv : (a : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R)) → MvPolynomial σ R)
        ((C : (a : MvPolynomial (↑s : Type v) R) → MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R)) p) :
      MvPolynomial σ R)
⊢ Prime p ↔
    Prime (M := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
          p :
        MvPolynomial σ R)
have rw : Prime p ↔
  Prime (M := MvPolynomial σ R)
    ((eqv : (a : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R)) → MvPolynomial σ R)
        ((C : (a : MvPolynomial (↑s : Type v) R) → MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R)) p) :
      MvPolynomial σ R)
Tactic: rw [this, MulEquiv.prime_iff, prime_C_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
s : Set σ
p : MvPolynomial.{v, u} (↑s : Type v) R
eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial.{v, u} (↑s : Type v) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R (↑sᶜ : Type v) (↑s : Type v)))
    (renameEquiv R (Equiv.trans (Equiv.sumComm (↑sᶜ : Type v) (↑s : Type v)) (Equiv.Set.sumCompl s)))
this :
  Eq (α := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↑s : Type v) R) → MvPolynomial σ R) p :
      MvPolynomial σ R)
    ((eqv : (a : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R)) → MvPolynomial σ R)
        ((C : (a : MvPolynomial (↑s : Type v) R) → MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R)) p) :
      MvPolynomial σ R)
rw :
  Prime p ↔
    Prime (M := MvPolynomial σ R)
      ((eqv : (a : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R)) → MvPolynomial σ R)
          ((C : (a : MvPolynomial (↑s : Type v) R) → MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R)) p) :
        MvPolynomial σ R)
⊢ Prime p ↔
    Prime (M := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
          p :
        MvPolynomial σ R)
have rw₁ : Prime p ↔
  Prime (M := MvPolynomial (↑sᶜ : Type v) (MvPolynomial.{v, u} (↑s : Type v) R))
    ((C : (a : MvPolynomial (↑s : Type v) R) → MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R)) p :
      MvPolynomial (↑sᶜ : Type v) (MvPolynomial.{v, u} (↑s : Type v) R))
Tactic: rw [this, MulEquiv.prime_iff, prime_C_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
s : Set σ
p : MvPolynomial.{v, u} (↑s : Type v) R
eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial.{v, u} (↑s : Type v) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R (↑sᶜ : Type v) (↑s : Type v)))
    (renameEquiv R (Equiv.trans (Equiv.sumComm (↑sᶜ : Type v) (↑s : Type v)) (Equiv.Set.sumCompl s)))
this :
  Eq (α := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial (↑s : Type v) R) → MvPolynomial σ R) p :
      MvPolynomial σ R)
    ((eqv : (a : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R)) → MvPolynomial σ R)
        ((C : (a : MvPolynomial (↑s : Type v) R) → MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R)) p) :
      MvPolynomial σ R)
rw :
  Prime p ↔
    Prime (M := MvPolynomial σ R)
      ((eqv : (a : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R)) → MvPolynomial σ R)
          ((C : (a : MvPolynomial (↑s : Type v) R) → MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R)) p) :
        MvPolynomial σ R)
rw₁ :
  Prime p ↔
    Prime (M := MvPolynomial (↑sᶜ : Type v) (MvPolynomial.{v, u} (↑s : Type v) R))
      ((C : (a : MvPolynomial (↑s : Type v) R) → MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R)) p :
        MvPolynomial (↑sᶜ : Type v) (MvPolynomial.{v, u} (↑s : Type v) R))
⊢ Prime p ↔
    Prime (M := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
          p :
        MvPolynomial σ R)
have rw₂ : Prime p ↔ Prime p
Tactic: rw [this, MulEquiv.prime_iff, prime_C_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
s : Set σ
p : MvPolynomial.{v, u} (↑s : Type v) R
⊢ Prime (M := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
          p :
        MvPolynomial σ R) ↔
    Prime p
have let : Prime p ↔
  Prime (M := MvPolynomial σ R)
    ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R) p :
      MvPolynomial σ R)
Tactic: classical
    symm
    let eqv :=
      (sumAlgEquiv R (↥sᶜ) s).symm.trans
        (renameEquiv R <| (Equiv.sumComm (↥sᶜ) s).trans <| Equiv.Set.sumCompl s)
    have : (rename (↑)).toRingHom = eqv.toAlgHom.toRingHom.comp C := by
      apply ringHom_ext
      · intro
        simp only [eqv, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, rename_C,
          AlgEquiv.toAlgHom_toRingHom, RingHom.coe_comp, AlgEquiv.coe_trans,
          Function.comp_apply, MvPolynomial.sumAlgEquiv_symm_apply, iterToSum_C_C,
          renameEquiv_apply, Equiv.coe_trans, Equiv.sumComm_apply]
      · intro
        simp only [eqv, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, rename_X,
          AlgEquiv.toAlgHom_toRingHom, RingHom.coe_comp, AlgEquiv.coe_trans,
          Function.comp_apply, MvPolynomial.sumAlgEquiv_symm_apply, iterToSum_C_X,
          renameEquiv_apply, Equiv.coe_trans, Equiv.sumComm_apply, Sum.swap_inr,
          Equiv.Set.sumCompl_apply_inl]
    apply_fun (· p) at this
    simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, AlgEquiv.toAlgHom_toRingHom,
      RingHom.coe_comp, Function.comp_apply] at this
    rw [this, MulEquiv.prime_iff, prime_C_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
σ : Type v
inst : CommRing R
s : Set σ
p : MvPolynomial.{v, u} (↑s : Type v) R
let :
  Prime p ↔
    Prime (M := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
          p :
        MvPolynomial σ R)
let₁ :
  Prime p ↔
    Prime (M := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
          p :
        MvPolynomial σ R)
⊢ Prime (M := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
          p :
        MvPolynomial σ R) ↔
    Prime p
have let₂ : let eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial.{v, u} (↑s : Type v) R) ≃ₐ[R] MvPolynomial σ R :=
  AlgEquiv.trans (AlgEquiv.symm (sumAlgEquiv R (↑sᶜ : Type v) (↑s : Type v)))
    (renameEquiv R (Equiv.trans (Equiv.sumComm (↑sᶜ : Type v) (↑s : Type v)) (Equiv.Set.sumCompl s)));
∀
  (this :
    AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))) =
      (↑eqv : MvPolynomial (↑sᶜ : Type v) (MvPolynomial (↑s : Type v) R) →ₐ[R] MvPolynomial σ R).comp C),
  Prime p ↔
    Prime (M := MvPolynomial σ R)
      ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
          p :
        MvPolynomial σ R)
Tactic: classical
    symm
    let eqv :=
      (sumAlgEquiv R (↥sᶜ) s).symm.trans
        (renameEquiv R <| (Equiv.sumComm (↥sᶜ) s).trans <| Equiv.Set.sumCompl s)
    have : (rename (↑)).toRingHom = eqv.toAlgHom.toRingHom.comp C := by
      apply ringHom_ext
      · intro
        simp only [eqv, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, rename_C,
          AlgEquiv.toAlgHom_toRingHom, RingHom.coe_comp, AlgEquiv.coe_trans,
          Function.comp_apply, MvPolynomial.sumAlgEquiv_symm_apply, iterToSum_C_C,
          renameEquiv_apply, Equiv.coe_trans, Equiv.sumComm_apply]
      · intro
        simp only [eqv, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, rename_X,
          AlgEquiv.toAlgHom_toRingHom, RingHom.coe_comp, AlgEquiv.coe_trans,
          Function.comp_apply, MvPolynomial.sumAlgEquiv_symm_apply, iterToSum_C_X,
          renameEquiv_apply, Equiv.coe_trans, Equiv.sumComm_apply, Sum.swap_inr,
          Equiv.Set.sumCompl_apply_inl]
    apply_fun (· p) at this
    simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, AlgEquiv.toAlgHom_toRingHom,
      RingHom.coe_comp, Function.comp_apply] at this
    rw [this, MulEquiv.prime_iff, prime_C_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
k : ℕ
h : N < k
x : R
hx : x ∈ I.leadingCoeffNth k
hxm : x ∉ M
this : IsNoetherian R R
⊢ ¬M < I.leadingCoeffNth k
have refine : I.leadingCoeffNth k ∈ Set.range I.leadingCoeffNth
Tactic: refine WellFounded.not_lt_min inst.wf _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (hypothesis)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
⊢ I ≤ Submodule.span R[X] (↑s : Set R[X])
have this : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
Tactic: have : Submodule.span R[X] ↑s = Ideal.span ↑s := rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Basic (goal)
Goal:
R : Type u
inst_1 : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (r := fun (x1 x2 : Submodule R R) ↦ x1 > x2) (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R (↑s : Set R[X]) = I.degreeLE (↑N : WithBot ℕ)
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE (↑N : WithBot ℕ) → Membership.mem (γ := Ideal R[X]) (Ideal.span (↑s : Set R[X])) x
this : Eq (α := Submodule R[X] R[X]) (Submodule.span R[X] (↑s : Set R[X])) (Ideal.span (↑s : Set R[X]))
p : R[X]
hp : p ∈ I
⊢ Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
have generalize : ∀ (k : ℕ) (hn : p.natDegree = k), Membership.mem (γ := Submodule R[X] R[X]) (Ideal.span (↑s : Set R[X])) p
Tactic: generalize hn : p.natDegree = k