awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.NormTrace (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Free A B
inst_4 : Module.Finite A B
a : A
x : B
let let₁ let₂ let₃ :
  ∃ (r : A),
    (norm A : (a : B) → A) (1 + a • x) =
      1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
⊢ ∃ (r : A),
    (norm A : (a : B) → A) (1 + a • x) =
      1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
have let₄ : let ι := Free.ChooseBasisIndex A B;
∀ (this : Fintype ι),
  ∃ (r : A),
    (norm A : (a : B) → A) (1 + a • x) =
      1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
Tactic: classical
  let ι := Module.Free.ChooseBasisIndex A B
  let b : Basis ι A B := Module.Free.chooseBasis _ _
  haveI : Fintype ι := inferInstance
  clear_value ι b
  simp_rw [Algebra.norm_eq_matrix_det b, Algebra.trace_eq_matrix_trace b]
  simp only [map_add, map_one, map_smul, Matrix.det_one_add_smul a]
  exact ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.NormTrace (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Free A B
inst_4 : Module.Finite A B
a : A
x : B
let let₁ let₂ let₃ :
  ∃ (r : A),
    (norm A : (a : B) → A) (1 + a • x) =
      1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
let₄ :
  let ι := Free.ChooseBasisIndex A B;
  ∀ (this : Fintype ι),
    ∃ (r : A),
      (norm A : (a : B) → A) (1 + a • x) =
        1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
⊢ ∃ (r : A),
    (norm A : (a : B) → A) (1 + a • x) =
      1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
have let₅ : ∀ (ι : Type u_2) (b : Basis ι A B) (this : Fintype ι),
  ∃ (r : A),
    (norm A : (a : B) → A) (1 + a • x) =
      1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
Tactic: classical
  let ι := Module.Free.ChooseBasisIndex A B
  let b : Basis ι A B := Module.Free.chooseBasis _ _
  haveI : Fintype ι := inferInstance
  clear_value ι b
  simp_rw [Algebra.norm_eq_matrix_det b, Algebra.trace_eq_matrix_trace b]
  simp only [map_add, map_one, map_smul, Matrix.det_one_add_smul a]
  exact ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.NormTrace (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Free A B
inst_4 : Module.Finite A B
a : A
x : B
let let₁ let₂ let₃ :
  ∃ (r : A),
    (norm A : (a : B) → A) (1 + a • x) =
      1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
let₄ :
  let ι := Free.ChooseBasisIndex A B;
  ∀ (this : Fintype ι),
    ∃ (r : A),
      (norm A : (a : B) → A) (1 + a • x) =
        1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
let₅ :
  ∀ (ι : Type u_2) (b : Basis ι A B) (this : Fintype ι),
    ∃ (r : A),
      (norm A : (a : B) → A) (1 + a • x) =
        1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
⊢ ∃ (r : A),
    (norm A : (a : B) → A) (1 + a • x) =
      1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
have let₆ : ∀ (ι : Type u_2) (b : Basis ι A B) (this : Fintype ι),
  ∃ (r : A),
    Matrix.det.{u_1, u_2} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) (1 + a • x)) =
      1 + Matrix.trace.{u_2, u_1} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x) * a +
        r * HPow.hPow (β := ℕ) a 2
Tactic: classical
  let ι := Module.Free.ChooseBasisIndex A B
  let b : Basis ι A B := Module.Free.chooseBasis _ _
  haveI : Fintype ι := inferInstance
  clear_value ι b
  simp_rw [Algebra.norm_eq_matrix_det b, Algebra.trace_eq_matrix_trace b]
  simp only [map_add, map_one, map_smul, Matrix.det_one_add_smul a]
  exact ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.NormTrace (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Free A B
inst_4 : Module.Finite A B
a : A
x : B
let let₁ let₂ let₃ :
  ∃ (r : A),
    (norm A : (a : B) → A) (1 + a • x) =
      1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
let₄ :
  let ι := Free.ChooseBasisIndex A B;
  ∀ (this : Fintype ι),
    ∃ (r : A),
      (norm A : (a : B) → A) (1 + a • x) =
        1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
let₅ :
  ∀ (ι : Type u_2) (b : Basis ι A B) (this : Fintype ι),
    ∃ (r : A),
      (norm A : (a : B) → A) (1 + a • x) =
        1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
let₆ :
  ∀ (ι : Type u_2) (b : Basis ι A B) (this : Fintype ι),
    ∃ (r : A),
      Matrix.det.{u_1, u_2} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) (1 + a • x)) =
        1 + Matrix.trace.{u_2, u_1} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x) * a +
          r * HPow.hPow (β := ℕ) a 2
⊢ ∃ (r : A),
    (norm A : (a : B) → A) (1 + a • x) =
      1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
have let₇ : ∀ (ι : Type u_2) (b : Basis ι A B) (this : Fintype ι),
  ∃ (r : A),
    1 + Matrix.trace.{u_2, u_1} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x) * a +
        Polynomial.eval a
            (1 +
                    HSMul.hSMul (α := Polynomial A) (β := Matrix.{u_2, u_2, u_1} ι ι (Polynomial A)) Polynomial.X
                      (Matrix.map (α := A) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x)
                        (⇑Polynomial.C : (a : A) → Polynomial A))).det.divX.divX *
          HPow.hPow (β := ℕ) a 2 =
      1 + Matrix.trace.{u_2, u_1} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x) * a +
        r * HPow.hPow (β := ℕ) a 2
Tactic: classical
  let ι := Module.Free.ChooseBasisIndex A B
  let b : Basis ι A B := Module.Free.chooseBasis _ _
  haveI : Fintype ι := inferInstance
  clear_value ι b
  simp_rw [Algebra.norm_eq_matrix_det b, Algebra.trace_eq_matrix_trace b]
  simp only [map_add, map_one, map_smul, Matrix.det_one_add_smul a]
  exact ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.NormalClosure (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
inst_6 : Module.Finite R S
inst_7 : PerfectField.{u_1} K
⊢ IsGalois.{u_1, u_2} K (FractionRing T)
have refine : Eq (α := RingHom.{u_1, u_2} K (FractionRing T))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K (FractionRing T))
    (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv R K))) : K →+* K))
  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
    (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv T ↥E))) : ↥E →+* FractionRing T) (algebraMap K ↥E))
Tactic: refine IsGalois.of_equiv_equiv (F := K) («E» := E)
    (f := (FractionRing.algEquiv R K).symm.toRingEquiv)
    (g := (FractionRing.algEquiv T E).symm.toRingEquiv) ?_
-- Lean 4 proof step from Mathlib.RingTheory.NormalClosure (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
inst_6 : Module.Finite R S
inst_7 : PerfectField.{u_1} K
⊢ Eq (α := RingHom.{u_1, u_2} K (FractionRing T))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K (FractionRing T))
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv R K))) : K →+* K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv T ↥E))) : ↥E →+* FractionRing T) (algebraMap K ↥E))
have a : ∀ (x : K),
  Eq.{u_2 + 1} (α := FractionRing T)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K (FractionRing T))
            (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv R K))) : K →+* K) :
          (a : K) → FractionRing T)
        x :
      FractionRing T)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(AlgEquiv.toRingEquiv (AlgEquiv.symm (FractionRing.algEquiv T ↥E))) : ↥E →+* FractionRing T)
            (algebraMap K ↥E) :
          (a : K) → FractionRing T)
        x :
      FractionRing T)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
⊢ IsPrime (α := MvPolynomial σ k) (vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x})
have h : vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x} = RingHom.ker (F := MvPolynomial σ k →ₐ[k] K) (aeval x)
Tactic: convert! RingHom.ker_isPrime (aeval (R := k) x)
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
⊢ vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x} = RingHom.ker (F := MvPolynomial σ k →ₐ[k] K) (aeval x)
have h : ∀ (x_1 : MvPolynomial σ k),
  Membership.mem (γ := Ideal (MvPolynomial σ k)) (vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}) x_1 ↔
    Membership.mem (γ := Ideal (MvPolynomial σ k)) (RingHom.ker (F := MvPolynomial σ k →ₐ[k] K) (aeval x)) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
⊢ IsMaximal (α := MvPolynomial σ K) (vanishingIdeal K (K := K) {x})
have h : Eq (α := Semiring (MvPolynomial σ K)) AddMonoidAlgebra.semiring Ring.toSemiring →
  vanishingIdeal K (K := K) {x} = RingHom.ker (F := MvPolynomial σ K →ₐ[K] K) (aeval x)
Tactic: convert! RingHom.ker_isMaximal_of_surjective (aeval (R := K) x) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
h :
  Eq (α := Semiring (MvPolynomial σ K)) AddMonoidAlgebra.semiring Ring.toSemiring →
    vanishingIdeal K (K := K) {x} = RingHom.ker (F := MvPolynomial σ K →ₐ[K] K) (aeval x)
⊢ IsMaximal (α := MvPolynomial σ K) (vanishingIdeal K (K := K) {x})
have convert! : Function.Surjective (α := MvPolynomial σ K) (β := K) (⇑(aeval x) : (a : MvPolynomial σ K) → K)
Tactic: convert! RingHom.ker_isMaximal_of_surjective (aeval (R := K) x) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
e_2 : Eq (α := Semiring (MvPolynomial σ K)) AddMonoidAlgebra.semiring Ring.toSemiring
⊢ vanishingIdeal K (K := K) {x} = RingHom.ker (F := MvPolynomial σ K →ₐ[K] K) (aeval x)
have h : ∀ (x_1 : MvPolynomial σ K),
  Membership.mem (γ := Ideal (MvPolynomial σ K)) (vanishingIdeal K (K := K) {x}) x_1 ↔
    Membership.mem (γ := Ideal (MvPolynomial σ K)) (RingHom.ker (F := MvPolynomial σ K →ₐ[K] K) (aeval x)) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
x : σ → K
z : K
⊢ ∃ (a : MvPolynomial σ K), (aeval x : (a : MvPolynomial σ K) → K) a = z
have h : (aeval x : (a : MvPolynomial σ K) → K) ((C : (a : K) → MvPolynomial σ K) z : MvPolynomial σ K) = z
Tactic: use C z
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ I.radical
x : σ → K
hx : x ∈ zeroLocus K I
⊢ Eq.{u_2 + 1} (α := K) ((aeval x : (a : MvPolynomial σ k) → K) p : K) (0 : K)
have rw : Membership.mem (γ := Ideal (MvPolynomial σ k)) (vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}) p
Tactic: rw [← mem_vanishingIdeal_singleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (goal)
Goal:
k : Type u_1
K : Type u_2
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
σ : Type u_3
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ I.radical
x : σ → K
hx : x ∈ zeroLocus K I
⊢ Membership.mem (γ := Ideal (MvPolynomial σ k)) (vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}) p
have rw : ∀
  (hp :
    Membership.mem (γ := Submodule (MvPolynomial σ k) (MvPolynomial σ k))
      (sInf {J : Ideal (MvPolynomial σ k) | I ≤ J ∧ J.IsPrime}) p)
  (x : σ → K) (hx : x ∈ zeroLocus K I),
  Membership.mem (γ := Ideal (MvPolynomial σ k)) (vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}) p
Tactic: rw [radical_eq_sInf] at hp
Cleared hypotheses: hp, x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (goal)
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)
have rw : RingHom.IsIntegral (A := MvPolynomial σ k ⧸ I) (algebraMap k (MvPolynomial σ k ⧸ I))
Tactic: rw [Algebra.isAlgebraic_iff_isIntegral, ← algebraMap_isIntegral_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (hypothesis)
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
⊢ ∃ (x : σ → K), I = vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (goal)
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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (hypothesis)
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)
⊢ ∃ (x : σ → K), I = vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}
have this₁ : aeval x = φ.comp (Quotient.mkₐ k I)
Tactic: have : aeval x = φ.comp (Quotient.mkₐ k I) := by ext; simp [x]
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (goal)
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)
⊢ ∃ (x : σ → K), I = vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}
have h : I = vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}
Tactic: use x
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (goal)
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
have refine : vanishingIdeal k (zeroLocus K I) ≤ I.radical
Tactic: refine le_antisymm ?_ (radical_le_vanishingIdeal_zeroLocus _)
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (goal)
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
have rw : vanishingIdeal k (zeroLocus K I) ≤ I.jacobson
Tactic: rw [I.radical_eq_jacobson]
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (goal)
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.jacobson
have 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
Tactic: apply le_sInf
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (goal)
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
⊢ vanishingIdeal k (zeroLocus K I) ≤ J
have h : ∀ (x : σ → K) (hx : J = vanishingIdeal.{u_1, u_2, u_3} k (K := K) {x}), vanishingIdeal k (zeroLocus K I) ≤ J
Tactic: obtain ⟨x, hx⟩ := eq_vanishingIdeal_singleton_of_isMaximal K hJ
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (goal)
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
have 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)
Tactic: refine hx.symm ▸ vanishingIdeal_anti_mono fun y hy p hp => ?_
-- Lean 4 proof step from Mathlib.RingTheory.Nullstellensatz (goal)
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
⊢ Eq.{u_2 + 1} (α := K) ((aeval y : (a : MvPolynomial σ k) → K) p : K) (0 : K)
have h : p ∈ J
Tactic: rw [← mem_vanishingIdeal_singleton_iff, Set.mem_singleton_iff.1 hy, ← hx]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
⊢ Function.Injective (α := R ⧸ I) (β := R ⧸ a • I) (⇑(mulQuot a I) : (a_1 : R ⧸ I) → R ⧸ a • I)
have 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) sorry)) ⊥
Tactic: simp only [mulQuot, Submodule.mapQ, ← ker_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors 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) ⋯)) ⊥
have h : I = ker (M₂ := R ⧸ a • I) (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a)
Tactic: apply Submodule.ker_liftQ_eq_bot'
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
⊢ I = ker (M₂ := R ⧸ a • I) (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a)
have h : I ≤ ker (M₂ := R ⧸ a • I) (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
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)
⊢ I = ker (M₂ := R ⧸ a • I) (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a)
have h₁ : ker (M₂ := R ⧸ a • I) (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a) ≤ I
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
a : R
I : Ideal R
ha : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) a
⊢ I ≤ ker (M₂ := R ⧸ a • I) (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a)
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
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
⊢ I ≤ ker (M₂ := R ⧸ a • I) (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a)
have h : Eq (α := Submodule R (R ⧸ a • I)) (Submodule.map (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a) I) ⊥
Tactic: rw [le_ker_iff_map, Submodule.map_comp, this, Submodule.mkQ_map_self]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
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) ⊥
⊢ I ≤ ker (M₂ := R ⧸ a • I) (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a)
have 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)) ⊥
Tactic: rw [le_ker_iff_map, Submodule.map_comp, this, Submodule.mkQ_map_self]
-- Lean 4 proof step from Mathlib.RingTheory.OrderOfVanishing.Basic (goal)
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))
    ⊥
⊢ I ≤ ker (M₂ := R ⧸ a • I) (Submodule.mkQ (a • I) ∘ₗ (mul R R : (a : R) → R →ₗ[R] R) a)
have h₂ : Eq.{u_1 + 1} (α := Submodule R (R ⧸ a • I)) (Submodule.map (Submodule.mkQ (a • I)) (a • I)) ⊥
Tactic: rw [le_ker_iff_map, Submodule.map_comp, this, Submodule.mkQ_map_self]