awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Basic
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)
⊢ (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

Premises used: MvPolynomial.algebraMap_eq
-- Module: Mathlib.RingTheory.Polynomial.Basic
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.{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)
    ((killCompl ⋯ : (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)) :
      MvPolynomial.{v, u} (↥s) R)

Tactic:
_root_.map_dvd (killCompl Subtype.val_injective) hd

Premises used: MvPolynomial.killCompl, Subtype.val_injective, map_dvd
-- Module: Mathlib.RingTheory.Polynomial.Basic
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)
h₁ :
  a' * b' =
    (killCompl ⋯ : (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))
⊢ (algebraMap R (MvPolynomial.{v, u} (↥s) R) : (a : R) → MvPolynomial (↥s) R) r ∣ a' * b'

Tactic:
convert! _root_.map_dvd (killCompl Subtype.val_injective) hd

Premises used: MvPolynomial.killCompl, Subtype.val_injective, map_dvd
-- Module: Mathlib.RingTheory.Polynomial.Basic
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)
⊢ 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)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Basic
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)
⊢ a' * b' =
    (killCompl ⋯ : (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:
simp
-- Module: Mathlib.RingTheory.Polynomial.Basic
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'

Tactic:
have : algebraMap R _ r ∣ a' * b' := by
        convert! _root_.map_dvd (killCompl Subtype.val_injective) hd
        · simp
        · simp
-- Module: Mathlib.RingTheory.Polynomial.Basic
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'
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)
⊢ 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:
rw [← rename_C ((↑) : s → σ)]

Premises used: MvPolynomial.rename_C, Subtype.val
-- Module: Mathlib.RingTheory.Polynomial.Basic
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'
f : MvPolynomial.{v, u} (↥s) R →+* MvPolynomial σ R :=
  AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)))
⊢ 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:
(((prime_C_iff_of_fintype s).2 hr).2.2 a' b' this).imp (map_dvd f) (map_dvd f)

Premises used: Iff.mpr, _private.0.MvPolynomial.prime_C_iff_of_fintype, Membership.mem, Subtype, map_dvd, And.right, Or.imp
-- Module: Mathlib.RingTheory.Polynomial.Basic
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'
f : MvPolynomial.{v, u} (↥s) R →+* MvPolynomial σ R :=
  AlgHom.toRingHom (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)))
⊢ 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:
exact (((prime_C_iff_of_fintype s).2 hr).2.2 a' b' this).imp (map_dvd f) (map_dvd f)
-- Module: Mathlib.RingTheory.Polynomial.Basic
Goal:
R : Type u
σ : Type v
inst : CommRing R
s : Set σ
p : MvPolynomial.{v, u} (↑s : Type v) R
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)
⊢ 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

Tactic:
symm
-- Module: Mathlib.RingTheory.Polynomial.Basic
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)
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)
⊢ 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:
apply ringHom_ext

Premises used: MvPolynomial.ringHom_ext
-- Module: Mathlib.RingTheory.Polynomial.Basic
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)))
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:
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]

Premises used: AlgEquiv.toAlgHom_toRingHom, RingHom.coe_coe, MvPolynomial.renameEquiv_apply, AlgHom.toRingHom_eq_coe, MvPolynomial.rename_C, MvPolynomial.sumAlgEquiv_symm_apply, RingHom.coe_comp, Equiv.sumComm_apply, Function.comp_apply, MvPolynomial.iterToSum_C_C, Equiv.coe_trans, AlgEquiv.coe_trans
-- Module: Mathlib.RingTheory.Polynomial.Basic
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)))
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:
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]

Premises used: AlgEquiv.toAlgHom_toRingHom, MvPolynomial.iterToSum_C_X, Sum.swap_inr, RingHom.coe_coe, MvPolynomial.renameEquiv_apply, AlgHom.toRingHom_eq_coe, MvPolynomial.sumAlgEquiv_symm_apply, RingHom.coe_comp, MvPolynomial.rename_X, Equiv.sumComm_apply, Function.comp_apply, Equiv.Set.sumCompl_apply_inl, Equiv.coe_trans, AlgEquiv.coe_trans
-- Module: Mathlib.RingTheory.Polynomial.Basic
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

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]
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
⊢ 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
-- Module: Mathlib.RingTheory.Polynomial.Basic
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))
rw₂ rw₃ : Prime p ↔ Prime p
⊢ 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:
rw [this, MulEquiv.prime_iff, prime_C_iff]

Premises used: MulEquiv.prime_iff, MvPolynomial.prime_C_iff
-- Module: Mathlib.RingTheory.Polynomial.Basic
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

Tactic:
WellFounded.not_lt_min inst.wf _ ?_

Premises used: IsNoetherian.wf, WellFounded.not_lt_min
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
refine : I.leadingCoeffNth k ∈ Set.range I.leadingCoeffNth
⊢ ¬M < I.leadingCoeffNth k

Tactic:
refine WellFounded.not_lt_min inst.wf _ ?_

Premises used: IsNoetherian.wf, WellFounded.not_lt_min
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
⊢ I.leadingCoeffNth k ∈ Set.range I.leadingCoeffNth

Tactic:
⟨k, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.RingTheory.Polynomial.Basic
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
⊢ I.leadingCoeffNth k ∈ Set.range I.leadingCoeffNth

Tactic:
exact ⟨k, rfl⟩