awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
V : Set (σ → K)
x_1 : MvPolynomial σ k
hp : Membership.mem (γ := Ideal (MvPolynomial σ k)) (PrimeSpectrum.vanishingIdeal (pointToPoint '' V)) x_1
x : σ → K
hx : x ∈ V
⊢ IsPrime (α := MvPolynomial σ k) (vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x})

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
K : Type u_2
inst : Field K
σ : Type u_3
I : Ideal (MvPolynomial σ K)
⊢ pointToPoint '' zeroLocus K I ≤ PrimeSpectrum.zeroLocus (↑I : Set (MvPolynomial σ K))

Tactic:
fun J hJ =>
  let ⟨_, hx⟩ := hJ
  (le_trans (le_vanishingIdeal_zeroLocus (K := K) I)
      (hx.2 ▸ vanishingIdeal_anti_mono (Set.singleton_subset_iff.2 hx.1)) :
    I ≤ J.asIdeal)

Premises used: MvPolynomial.vanishingIdeal_anti_mono, Iff.mpr, Set.singleton_subset_iff, MvPolynomial.le_vanishingIdeal_zeroLocus, PrimeSpectrum.zeroLocus, Membership.mem, Eq.rec, _private.0.MvPolynomial.pointToPoint_zeroLocus_le.match_1, Set.Subset, SetLike.coe, And.right, And.left, le_trans
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I : Ideal (MvPolynomial σ k)
hI : I.IsMaximal
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
rw : RingHom.IsIntegral (A := MvPolynomial σ k ⧸ I) (algebraMap k (MvPolynomial σ k ⧸ I))
⊢ Algebra.IsAlgebraic k (MvPolynomial σ k ⧸ I)

Tactic:
rw [Algebra.isAlgebraic_iff_isIntegral, ← algebraMap_isIntegral_iff]

Premises used: algebraMap_isIntegral_iff, Algebra.isAlgebraic_iff_isIntegral
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I : Ideal (MvPolynomial σ k)
hI : I.IsMaximal
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
⊢ RingHom.IsIntegral (A := MvPolynomial σ k ⧸ I) (algebraMap k (MvPolynomial σ k ⧸ I))

Tactic:
MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing
      (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk, Ideal.Quotient.mk_surjective, MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing, MvPolynomial.C
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I : Ideal (MvPolynomial σ k)
hI : I.IsMaximal
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
⊢ RingHom.IsIntegral (A := MvPolynomial σ k ⧸ I) (algebraMap k (MvPolynomial σ k ⧸ I))

Tactic:
exact MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing
      (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk, Ideal.Quotient.mk_surjective, MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I : Ideal (MvPolynomial σ k)
hI : I.IsMaximal
this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
⊢ Algebra.IsAlgebraic k (MvPolynomial σ k ⧸ I)

Tactic:
have : Algebra.IsAlgebraic k (MvPolynomial σ k ⧸ I) := by
    rw [Algebra.isAlgebraic_iff_isIntegral, ← algebraMap_isIntegral_iff]
    exact MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing
      (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I : Ideal (MvPolynomial σ k)
hI : I.IsMaximal
this_1 : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
this : Algebra.IsAlgebraic k (MvPolynomial σ k ⧸ I)
φ : MvPolynomial σ k ⧸ I →ₐ[k] K := IsAlgClosed.lift
x : σ → K :=
  fun (s : σ) ↦
    (φ : (a : MvPolynomial σ k ⧸ I) → K)
      ((Ideal.Quotient.mk I : (a : MvPolynomial σ k) → MvPolynomial σ k ⧸ I) (X s) : MvPolynomial σ k ⧸ I)
hf :
  ∀ (i : σ),
    Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial σ k) → K) (X i) : K)
      ((φ.comp (Quotient.mkₐ k I) : (a : MvPolynomial σ k) → K) (X i) : K)
⊢ aeval x = φ.comp (Quotient.mkₐ k I)

Tactic:
ext
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I : Ideal (MvPolynomial σ k)
hI : I.IsMaximal
this_1 : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
this : Algebra.IsAlgebraic k (MvPolynomial σ k ⧸ I)
φ : MvPolynomial σ k ⧸ I →ₐ[k] K := IsAlgClosed.lift
x : σ → K :=
  fun (s : σ) ↦
    (φ : (a : MvPolynomial σ k ⧸ I) → K)
      ((Ideal.Quotient.mk I : (a : MvPolynomial σ k) → MvPolynomial σ k ⧸ I) (X s) : MvPolynomial σ k ⧸ I)
i : σ
⊢ Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial σ k) → K) (X i) : K)
    ((φ.comp (Quotient.mkₐ k I) : (a : MvPolynomial σ k) → K) (X i) : K)

Tactic:
simp [x]
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I : Ideal (MvPolynomial σ k)
hI : I.IsMaximal
this_1 : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
this : Algebra.IsAlgebraic k (MvPolynomial σ k ⧸ I)
φ : MvPolynomial σ k ⧸ I →ₐ[k] K := IsAlgClosed.lift
x : σ → K :=
  fun (s : σ) ↦
    (φ : (a : MvPolynomial σ k ⧸ I) → K)
      ((Ideal.Quotient.mk I : (a : MvPolynomial σ k) → MvPolynomial σ k ⧸ I) (X s) : MvPolynomial σ k ⧸ I)
⊢ aeval x = φ.comp (Quotient.mkₐ k I)

Tactic:
have : aeval x = φ.comp (Quotient.mkₐ k I) := by ext; simp [x]
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I : Ideal (MvPolynomial σ k)
hI : I.IsMaximal
this_1 : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
this_2 : Algebra.IsAlgebraic k (MvPolynomial σ k ⧸ I)
φ : MvPolynomial σ k ⧸ I →ₐ[k] K := IsAlgClosed.lift
x : σ → K :=
  fun (s : σ) ↦
    (φ : (a : MvPolynomial σ k ⧸ I) → K)
      ((Ideal.Quotient.mk I : (a : MvPolynomial σ k) → MvPolynomial σ k ⧸ I) (X s) : MvPolynomial σ k ⧸ I)
this : aeval x = φ.comp (Quotient.mkₐ k I)
h : I = vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}
⊢ ∃ (x : σ → K), I = vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}

Tactic:
use x
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I : Ideal (MvPolynomial σ k)
hI : I.IsMaximal
this_1 : Field (MvPolynomial σ k ⧸ I) := Quotient.field I
this_2 : Algebra.IsAlgebraic k (MvPolynomial σ k ⧸ I)
φ : MvPolynomial σ k ⧸ I →ₐ[k] K := IsAlgClosed.lift
x : σ → K :=
  fun (s : σ) ↦
    (φ : (a : MvPolynomial σ k ⧸ I) → K)
      ((Ideal.Quotient.mk I : (a : MvPolynomial σ k) → MvPolynomial σ k ⧸ I) (X s) : MvPolynomial σ k ⧸ I)
this : aeval x = φ.comp (Quotient.mkₐ k I)
⊢ I = vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}

Tactic:
simp [Ideal.ext_iff, this, Ideal.Quotient.eq_zero_iff_mem]

Premises used: Ideal.Quotient.eq_zero_iff_mem, Ideal.ext_iff
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
K : Type u_2
inst : Field K
σ : Type u_3
inst_1 : IsAlgClosed K
inst_2 : Finite σ
I : Ideal (MvPolynomial σ K)
⊢ I.IsMaximal ↔ ∃ (x : σ → K), I = vanishingIdeal K (K := K) {x}

Tactic:
⟨eq_vanishingIdeal_singleton_of_isMaximal K,
    fun ⟨_, hx⟩ => hx ▸ inferInstance⟩

Premises used: Eq.rec, inferInstance, MvPolynomial.eq_vanishingIdeal_singleton_of_isMaximal, Iff.intro, Ideal.IsMaximal, _private.0.MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton.match_1, Eq.symm
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I : Ideal (MvPolynomial σ k)
⊢ vanishingIdeal k (zeroLocus K I) = I.radical

Tactic:
le_antisymm ?_ (radical_le_vanishingIdeal_zeroLocus _)

Premises used: MvPolynomial.radical_le_vanishingIdeal_zeroLocus, le_antisymm
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I : Ideal (MvPolynomial σ k)
refine : vanishingIdeal k (zeroLocus K I) ≤ I.radical
⊢ vanishingIdeal k (zeroLocus K I) = I.radical

Tactic:
refine le_antisymm ?_ (radical_le_vanishingIdeal_zeroLocus _)

Premises used: MvPolynomial.radical_le_vanishingIdeal_zeroLocus, le_antisymm
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I : Ideal (MvPolynomial σ k)
rw : vanishingIdeal k (zeroLocus K I) ≤ I.jacobson
⊢ vanishingIdeal k (zeroLocus K I) ≤ I.radical

Tactic:
rw [I.radical_eq_jacobson]

Premises used: Ideal.radical_eq_jacobson
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I : Ideal (MvPolynomial σ k)
h :
  ∀ (b : Ideal (MvPolynomial σ k)),
    Membership.mem (γ := Set (Ideal (MvPolynomial σ k))) {J : Ideal (MvPolynomial σ k) | I ≤ J ∧ J.IsMaximal} b →
      vanishingIdeal k (zeroLocus K I) ≤ b
⊢ vanishingIdeal k (zeroLocus K I) ≤ I.jacobson

Tactic:
apply le_sInf

Premises used: le_sInf
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
h : ∀ (x : σ → K) (hx : J = vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}), vanishingIdeal k (zeroLocus K I) ≤ J
⊢ vanishingIdeal k (zeroLocus K I) ≤ J

Tactic:
obtain ⟨x, hx⟩ := eq_vanishingIdeal_singleton_of_isMaximal K hJ

Premises used: MvPolynomial.eq_vanishingIdeal_singleton_of_isMaximal
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
x : σ → K
hx : J = vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}
⊢ vanishingIdeal k (zeroLocus K I) ≤ J

Tactic:
hx.symm ▸ vanishingIdeal_anti_mono fun y hy p hp => ?_

Premises used: MvPolynomial.vanishingIdeal_anti_mono, Eq.rec, Eq.symm
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
x : σ → K
hx : J = vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}
h :
  ∀ (y : σ → K) (hy : Membership.mem (γ := Set (σ → K)) {x} y) (p : MvPolynomial σ k) (hp : p ∈ I),
    Eq.{u_2 + 1} (α := K) ((aeval y : (a : MvPolynomial σ k) → K) p : K) (0 : K)
⊢ vanishingIdeal k (zeroLocus K I) ≤ J

Tactic:
refine hx.symm ▸ vanishingIdeal_anti_mono fun y hy p hp => ?_
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
x : σ → K
hx : J = vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}
y : σ → K
hy : Membership.mem (γ := Set (σ → K)) {x} y
p : MvPolynomial σ k
hp : p ∈ I
h : p ∈ J
⊢ Eq.{u_2 + 1} (α := K) ((aeval y : (a : MvPolynomial σ k) → K) p : K) (0 : K)

Tactic:
rw [← mem_vanishingIdeal_singleton_iff, Set.mem_singleton_iff.1 hy, ← hx]

Premises used: Set.mem_singleton_iff, Iff.mp, MvPolynomial.mem_vanishingIdeal_singleton_iff
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
x : σ → K
hx : J = vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}
y : σ → K
hy : Membership.mem (γ := Set (σ → K)) {x} y
p : MvPolynomial σ k
hp : p ∈ I
⊢ p ∈ J

Tactic:
hJI hp

Premises used: Set.Mem
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
I J : Ideal (MvPolynomial σ k)
hJI : I ≤ J
hJ : J.IsMaximal
x : σ → K
hx : J = vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}
y : σ → K
hy : Membership.mem (γ := Set (σ → K)) {x} y
p : MvPolynomial σ k
hp : p ∈ I
⊢ p ∈ J

Tactic:
exact hJI hp
-- Module: Mathlib.RingTheory.Nullstellensatz
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
inst_3 : IsAlgClosed K
inst_4 : Finite σ
P : Ideal (MvPolynomial σ k)
h : P.IsPrime
⊢ vanishingIdeal k (zeroLocus K P) = P

Tactic:
Trans.trans (vanishingIdeal_zeroLocus_eq_radical P) h.radical

Premises used: Trans.trans, Ideal.IsPrime.radical, MvPolynomial.vanishingIdeal_zeroLocus_eq_radical
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : Ring R
⊢ ord R 1 = 0

Tactic:
simp_all [ord,
    Ideal.span_singleton_one, Submodule.Quotient.subsingleton_iff]

Premises used: Ring.ord, Ideal.span_singleton_one, Submodule.Quotient.subsingleton_iff
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
simp :
  Eq (α := Submodule R (R ⧸ I))
    (ker (M₂ := R ⧸ a • I) (Submodule.liftQ I (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a) ⋯)) ⊥
⊢ Function.Injective (α := R ⧸ I) (β := R ⧸ a • I) (⇑(mulQuot a I) : (a_1 : R ⧸ I) → R ⧸ a • I)

Tactic:
simp only [mulQuot, Submodule.mapQ, ← ker_eq_bot]

Premises used: LinearMap.ker_eq_bot, Submodule.mapQ, Ideal.mulQuot
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
h : I = ker (M₂ := R ⧸ a • I) (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a)
⊢ Eq (α := Submodule R (R ⧸ I))
    (ker (M₂ := R ⧸ a • I) (Submodule.liftQ I (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a) ⋯)) ⊥

Tactic:
apply Submodule.ker_liftQ_eq_bot'

Premises used: Submodule.ker_liftQ_eq_bot'
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
h : I ≤ ker (M₂ := R ⧸ a • I) (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a)
h₁ : ker (M₂ := R ⧸ a • I) (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a) ≤ I
⊢ I = ker (M₂ := R ⧸ a • I) (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
⊢ Submodule.map (σ₁₂ := RingHom.id R) ((mul R R : (a : R) → R →ₗ[R] R) a) I = a • I

Tactic:
have : Submodule.map (mul R R a) I = a • I := rfl
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
this : Submodule.map (σ₁₂ := RingHom.id R) ((mul R R : (a : R) → R →ₗ[R] R) a) I = a • I
h : Eq (α := Submodule R (R ⧸ a • I)) (Submodule.map (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a) I) ⊥
h₁ :
  Eq (α := Submodule R (R ⧸ a • I))
    (Submodule.map (Submodule.mkQ (a • I)) (Submodule.map (σ₁₂ := RingHom.id R) ((mul R R : (a : R) → R →ₗ[R] R) a) I))
    ⊥
h₂ : Eq.{u_1 + 1} (α := Submodule R (R ⧸ a • I)) (Submodule.map (Submodule.mkQ (a • I)) (a • I)) ⊥
h₃ h₄ : Eq.{u_1 + 1} (α := Submodule R (R ⧸ a • I)) ⊥ ⊥
⊢ I ≤ ker (M₂ := R ⧸ a • I) (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a)

Tactic:
rw [le_ker_iff_map, Submodule.map_comp, this, Submodule.mkQ_map_self]

Premises used: Submodule.map_comp, Submodule.mkQ_map_self, LinearMap.le_ker_iff_map
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
h :
  ∀ (b : R),
    b ∈ I ↔
      Membership.mem (γ := Ideal R) (Submodule.comap (σ₁₂ := RingHom.id R) ((mul R R : (a : R) → R →ₗ[R] R) a) (a • I))
        b
⊢ I = Submodule.comap (σ₁₂ := RingHom.id R) ((mul R R : (a : R) → R →ₗ[R] R) a) (a • I)

Tactic:
ext b
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
b : R
⊢ b ∈ I ↔
    Membership.mem (γ := Ideal R) (Submodule.comap (σ₁₂ := RingHom.id R) ((mul R R : (a : R) → R →ₗ[R] R) a) (a • I)) b

Tactic:
(Submodule.mul_mem_smul_iff ha).symm

Premises used: Set.Mem, Submodule.mul_mem_smul_iff, setOf, Set.preimage, Set.image, Iff.symm
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
b : R
⊢ b ∈ I ↔
    Membership.mem (γ := Ideal R) (Submodule.comap (σ₁₂ := RingHom.id R) ((mul R R : (a : R) → R →ₗ[R] R) a) (a • I)) b

Tactic:
exact (Submodule.mul_mem_smul_iff ha).symm

Premises used: Submodule.mul_mem_smul_iff, Iff.symm
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
⊢ I = Submodule.comap (σ₁₂ := RingHom.id R) ((mul R R : (a : R) → R →ₗ[R] R) a) (a • I)

Tactic:
have m : I = Submodule.comap (mul R R a) (a • I) := by
      ext b
      exact (Submodule.mul_mem_smul_iff ha).symm
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
m : I = Submodule.comap (σ₁₂ := RingHom.id R) ((mul R R : (a : R) → R →ₗ[R] R) a) (a • I)
⊢ ker (M₂ := R ⧸ a • I) (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a) ≤ I

Tactic:
simp [← m, ker_comp]

Premises used: LinearMap.ker_comp
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := R ⧸ a • I) (β := HasQuotient.Quotient R (B := Ideal R) (span {a}))
    (⇑(Submodule.factor ⋯) : (a_1 : R ⧸ a • I) → R ⧸ span {a})

Tactic:
Submodule.factor_surjective <|
    Submodule.singleton_set_smul I a ▸ Submodule.smul_le_span {a} I

Premises used: Submodule.factor_surjective
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := R ⧸ a • I) (β := HasQuotient.Quotient R (B := Ideal R) (span {a}))
    (⇑(Submodule.factor ⋯) : (a_1 : R ⧸ a • I) → R ⧸ span {a})

Tactic:
exact Submodule.factor_surjective <|
    Submodule.singleton_set_smul I a ▸ Submodule.smul_le_span {a} I

Premises used: Submodule.factor_surjective
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
simp : (quotOfMul a I).ker = (mulQuot a I).range
⊢ Function.Exact (M := R ⧸ I) (N := R ⧸ a • I) (P := HasQuotient.Quotient R (B := Ideal R) (span {a}))
    (⇑(mulQuot a I) : (a_1 : R ⧸ I) → R ⧸ a • I) (⇑(quotOfMul a I) : (a_1 : R ⧸ a • I) → R ⧸ span {a})

Tactic:
simp only [exact_iff]

Premises used: LinearMap.exact_iff
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
⊢ (quotOfMul a I).ker = HSMul.hSMul (β := Submodule R (R ⧸ a • I)) a ⊤

Tactic:
simp only [← submodule_span_eq, quotOfMul, Submodule.factor, Submodule.mapQ, comp_id,
      Submodule.ker_liftQ, Submodule.ker_mkQ, Submodule.map_span, Submodule.mkQ_apply,
      Quotient.mk_eq_mk, Set.image_singleton, Quotient.smul_top]

Premises used: Ideal.submodule_span_eq, Set.image_singleton, Ideal.Quotient.smul_top, Submodule.mkQ_apply, Ideal.quotOfMul, Submodule.mapQ, Submodule.factor, Ideal.Quotient.mk_eq_mk, LinearMap.comp_id, Submodule.ker_mkQ, Submodule.map_span, Submodule.ker_liftQ
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
⊢ (quotOfMul a I).ker = HSMul.hSMul (β := Submodule R (R ⧸ a • I)) a ⊤

Tactic:
have : ker (Ideal.quotOfMul a I) = a • ⊤ := by
    simp only [← submodule_span_eq, quotOfMul, Submodule.factor, Submodule.mapQ, comp_id,
      Submodule.ker_liftQ, Submodule.ker_mkQ, Submodule.map_span, Submodule.mkQ_apply,
      Quotient.mk_eq_mk, Set.image_singleton, Quotient.smul_top]
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
this : (quotOfMul a I).ker = HSMul.hSMul (β := Submodule R (R ⧸ a • I)) a ⊤
⊢ (quotOfMul a I).ker = (mulQuot a I).range

Tactic:
simp [this, Ideal.mulQuot, Submodule.mapQ.eq_1, Submodule.range_liftQ,
    range_comp, Ideal.Quotient.smul_top, ← Ideal.submodule_span_eq, LinearMap.map_span]

Premises used: Ideal.submodule_span_eq, LinearMap.range_comp, Ideal.Quotient.smul_top, Submodule.mapQ.eq_1, LinearMap.map_span, Ideal.mulQuot, Submodule.range_liftQ
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a b : R
hb : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) b
⊢ Module.length R (R ⧸ HSMul.hSMul (β := Ideal R) b (span {a})) =
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a})) +
      Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {b}))

Tactic:
have := Module.length_eq_add_of_exact (Ideal.mulQuot b (Ideal.span {a}))
          (Ideal.quotOfMul b (Ideal.span {a})) (Ideal.mulQuot_injective (Ideal.span {a}) hb)
          (Ideal.quotOfMul_surjective (Ideal.span {a}))
          (Ideal.exact_mulQuot_quotOfMul (Ideal.span {a}))
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a b : R
hb : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) b
this :
  Module.length R (R ⧸ HSMul.hSMul (β := Ideal R) b (span {a})) =
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a})) +
      Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {b}))
simp :
  Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a * b})) =
    Module.length R (R ⧸ HSMul.hSMul (β := Ideal R) b (span {a}))
⊢ ord R (a * b) = ord R a + ord R b

Tactic:
simp only [Ring.ord, ← this]

Premises used: Ring.ord
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a b : R
hb : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) b
this :
  Module.length R (R ⧸ HSMul.hSMul (β := Ideal R) b (span {a})) =
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a})) +
      Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {b}))
⊢ HSMul.hSMul (α := Set R) (β := Ideal R) {b} (span {a}) = span {b * a}

Tactic:
simp [← Ideal.submodule_span_eq, Submodule.set_smul_span]

Premises used: Submodule.set_smul_span, Ideal.submodule_span_eq
-- Module: Mathlib.RingTheory.OrderOfVanishing.Basic
Goal:
R : Type u_1
inst : CommRing R
a b : R
hb : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) b
this :
  Module.length R (R ⧸ HSMul.hSMul (β := Ideal R) b (span {a})) =
    Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {a})) +
      Module.length R (HasQuotient.Quotient R (B := Ideal R) (span {b}))
⊢ HSMul.hSMul (α := Set R) (β := Ideal R) {b} (span {a}) = span {b * a}

Tactic:
have lem : (({b} : Set R) • Ideal.span {a}) = Ideal.span {b * a} := by
    simp [← Ideal.submodule_span_eq, Submodule.set_smul_span]