awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal S
J : Ideal R
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) J ↔
    Membership.mem (γ := Set (Ideal R)) (comap f '' I.minimalPrimes) J
have h : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) J →
  Membership.mem (γ := Set (Ideal R)) (comap f '' I.minimalPrimes) J
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal S
J : Ideal R
h :
  Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) J →
    Membership.mem (γ := Set (Ideal R)) (comap f '' I.minimalPrimes) J
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) J ↔
    Membership.mem (γ := Set (Ideal R)) (comap f '' I.minimalPrimes) J
have h₁ : Membership.mem (γ := Set (Ideal R)) (comap f '' I.minimalPrimes) J →
  Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) J
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal S
J : Ideal R
H : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) J
⊢ Membership.mem (γ := Set (Ideal R)) (comap f '' I.minimalPrimes) J
have h : ∀ (p : Ideal S) (h : p ∈ I.minimalPrimes)
  (H : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) (comap f p)),
  Membership.mem (γ := Set (Ideal R)) (comap f '' I.minimalPrimes) (comap f p)
Tactic: obtain ⟨p, h, rfl⟩ := Ideal.exists_minimalPrimes_comap_eq f J H
Cleared hypotheses: J, H
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
⊢ Eq.{u_3 + 1} (α := Set (Ideal S)) (Ideal.minimalPrimes (map f I)) (map f '' (I ⊔ RingHom.ker f).minimalPrimes)
have a : Eq (α := Set (Ideal R)) (Set.image (α := Ideal S) (comap f) (Ideal.minimalPrimes (map f I)))
  (Set.image (α := Ideal S) (comap f) (map f '' (I ⊔ RingHom.ker f).minimalPrimes))
Tactic: apply Set.image_injective.mpr (Ideal.comap_injective_of_surjective f hf)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_3
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
⊢ Eq (α := Set (Ideal R)) (Set.image (α := Ideal S) (comap f) (Ideal.minimalPrimes (map f I)))
    (Set.image (α := Ideal S) (comap f) (map f '' (I ⊔ RingHom.ker f).minimalPrimes))
have a : ∀ a ∈ (I ⊔ RingHom.ker f).minimalPrimes, Function.comp (β := Ideal S) (comap f) (map f) a = id a
Tactic: rw [← Ideal.comap_minimalPrimes_eq_of_surjective hf, ← Set.image_comp,
    Ideal.comap_map_of_surjective f hf, Set.image_congr, Set.image_id, RingHom.ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
⊢ I.minimalPrimes = Set.image (α := Ideal (R ⧸ I)) (comap (F := R →+* R ⧸ I) (Quotient.mk I)) (minimalPrimes (R ⧸ I))
have rw : I.minimalPrimes =
  Set.image (α := Ideal (R ⧸ I)) (comap (F := R →+* R ⧸ I) (Quotient.mk I)) {p : Ideal (R ⧸ I) | IsMinimalPrime p}
Tactic: rw [minimalPrimes, ← Ideal.comap_minimalPrimes_eq_of_surjective Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
rw :
  I.minimalPrimes =
    Set.image (α := Ideal (R ⧸ I)) (comap (F := R →+* R ⧸ I) (Quotient.mk I)) {p : Ideal (R ⧸ I) | IsMinimalPrime p}
⊢ I.minimalPrimes = Set.image (α := Ideal (R ⧸ I)) (comap (F := R →+* R ⧸ I) (Quotient.mk I)) (minimalPrimes (R ⧸ I))
have rw₁ : I.minimalPrimes = Ideal.minimalPrimes (comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥)
Tactic: rw [minimalPrimes, ← Ideal.comap_minimalPrimes_eq_of_surjective Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
rw :
  I.minimalPrimes =
    Set.image (α := Ideal (R ⧸ I)) (comap (F := R →+* R ⧸ I) (Quotient.mk I)) {p : Ideal (R ⧸ I) | IsMinimalPrime p}
rw₁ : I.minimalPrimes = Ideal.minimalPrimes (comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥)
⊢ I.minimalPrimes = Set.image (α := Ideal (R ⧸ I)) (comap (F := R →+* R ⧸ I) (Quotient.mk I)) (minimalPrimes (R ⧸ I))
have rw₂ : I.minimalPrimes = Ideal.minimalPrimes (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I))
Tactic: rw [minimalPrimes, ← Ideal.comap_minimalPrimes_eq_of_surjective Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
rw :
  I.minimalPrimes =
    Set.image (α := Ideal (R ⧸ I)) (comap (F := R →+* R ⧸ I) (Quotient.mk I)) {p : Ideal (R ⧸ I) | IsMinimalPrime p}
rw₁ : I.minimalPrimes = Ideal.minimalPrimes (comap (F := R →+* R ⧸ I) (Quotient.mk I) ⊥)
rw₂ : I.minimalPrimes = Ideal.minimalPrimes (RingHom.ker (F := R →+* R ⧸ I) (Quotient.mk I))
⊢ I.minimalPrimes = Set.image (α := Ideal (R ⧸ I)) (comap (F := R →+* R ⧸ I) (Quotient.mk I)) (minimalPrimes (R ⧸ I))
have rw₃ : I.minimalPrimes = I.minimalPrimes
Tactic: rw [minimalPrimes, ← Ideal.comap_minimalPrimes_eq_of_surjective Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal R
⊢ Eq.{u_2 + 1} (α := Set (Ideal A)) (Ideal.minimalPrimes (Ideal.map (F := R →+* A) (algebraMap R A) J))
    (Ideal.under R ⁻¹' J.minimalPrimes)
have h : ∀ (p : Ideal A),
  Membership.mem (γ := Set (Ideal A)) (Ideal.minimalPrimes (Ideal.map (F := R →+* A) (algebraMap R A) J)) p ↔
    Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' J.minimalPrimes) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal R
p : Ideal A
⊢ Membership.mem (γ := Set (Ideal A)) (Ideal.minimalPrimes (Ideal.map (F := R →+* A) (algebraMap R A) J)) p ↔
    Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' J.minimalPrimes) p
have h : Membership.mem (γ := Set (Ideal A)) (Ideal.minimalPrimes (Ideal.map (F := R →+* A) (algebraMap R A) J)) p →
  Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' J.minimalPrimes) p
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal R
p : Ideal A
h :
  Membership.mem (γ := Set (Ideal A)) (Ideal.minimalPrimes (Ideal.map (F := R →+* A) (algebraMap R A) J)) p →
    Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' J.minimalPrimes) p
⊢ Membership.mem (γ := Set (Ideal A)) (Ideal.minimalPrimes (Ideal.map (F := R →+* A) (algebraMap R A) J)) p ↔
    Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' J.minimalPrimes) p
have h₁ : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' J.minimalPrimes) p →
  Membership.mem (γ := Set (Ideal A)) (Ideal.minimalPrimes (Ideal.map (F := R →+* A) (algebraMap R A) J)) p
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal R
p : Ideal A
hp : Membership.mem (γ := Set (Ideal A)) (Ideal.minimalPrimes (Ideal.map (F := R →+* A) (algebraMap R A) J)) p
⊢ Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' J.minimalPrimes) p
have this : p.IsPrime
Tactic: have := hp.isPrime
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal R
p : Ideal A
hp : Membership.mem (γ := Set (Ideal A)) (Ideal.minimalPrimes (Ideal.map (F := R →+* A) (algebraMap R A) J)) p
this : p.IsPrime
⊢ Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' J.minimalPrimes) p
have h : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ J ≤ q) y → y ≤ Ideal.under R p → Ideal.under R p ≤ y
Tactic: refine ⟨⟨Ideal.IsPrime.comap _, Ideal.map_le_iff_le_comap.mp hp.le⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal R
p : Ideal A
hp : Membership.mem (γ := Set (Ideal A)) (Ideal.minimalPrimes (Ideal.map (F := R →+* A) (algebraMap R A) J)) p
this : p.IsPrime
I : Ideal R
hI : I.IsPrime ∧ J ≤ I
e : I ≤ Ideal.under R p
⊢ Ideal.under R p ≤ I
have hI' : Disjoint (↑S : Set R) (↑I : Set R)
Tactic: have hI' : Disjoint (S : Set R) I := Set.disjoint_of_subset_right e
      ((IsLocalization.isPrime_iff_isPrime_disjoint S A _).mp hp.isPrime).2
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal R
p : Ideal A
hp : Membership.mem (γ := Set (Ideal A)) (Ideal.minimalPrimes (Ideal.map (F := R →+* A) (algebraMap R A) J)) p
this : p.IsPrime
I : Ideal R
hI : I.IsPrime ∧ J ≤ I
e : I ≤ Ideal.under R p
hI' : Disjoint (↑S : Set R) (↑I : Set R)
⊢ Ideal.under R p ≤ I
have h : Ideal.IsPrime.{u_2} (α := A) (Ideal.map (F := R →+* A) (algebraMap R A) I)
Tactic: refine (Ideal.comap_mono <|
      hp.2 ⟨?_, Ideal.map_mono hI.2⟩ (Ideal.map_le_iff_le_comap.mpr e)).trans_eq ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal R
p : Ideal A
hp : Membership.mem (γ := Set (Ideal A)) (Ideal.minimalPrimes (Ideal.map (F := R →+* A) (algebraMap R A) J)) p
this : p.IsPrime
I : Ideal R
hI : I.IsPrime ∧ J ≤ I
e : I ≤ Ideal.under R p
hI' : Disjoint (↑S : Set R) (↑I : Set R)
h : Ideal.IsPrime.{u_2} (α := A) (Ideal.map (F := R →+* A) (algebraMap R A) I)
⊢ Ideal.under R p ≤ I
have h₁ : Ideal.comap (F := R →+* A) (algebraMap R A) (Ideal.map (F := R →+* A) (algebraMap R A) I) = I
Tactic: refine (Ideal.comap_mono <|
      hp.2 ⟨?_, Ideal.map_mono hI.2⟩ (Ideal.map_le_iff_le_comap.mpr e)).trans_eq ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal R
p : Ideal A
hp : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' J.minimalPrimes) p
⊢ Membership.mem (γ := Set (Ideal A)) (Ideal.minimalPrimes (Ideal.map (F := R →+* A) (algebraMap R A) J)) p
have h : p.IsPrime
Tactic: refine ⟨⟨?_, Ideal.map_le_iff_le_comap.mpr hp.le⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal R
p : Ideal A
hp : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' J.minimalPrimes) p
h : p.IsPrime
⊢ Membership.mem (γ := Set (Ideal A)) (Ideal.minimalPrimes (Ideal.map (F := R →+* A) (algebraMap R A) J)) p
have h₁ : ∀ ⦃y : Ideal A⦄, (fun (q : Ideal A) ↦ q.IsPrime ∧ Ideal.map (F := R →+* A) (algebraMap R A) J ≤ q) y → y ≤ p → p ≤ y
Tactic: refine ⟨⟨?_, Ideal.map_le_iff_le_comap.mpr hp.le⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal R
p : Ideal A
hp : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' J.minimalPrimes) p
⊢ p.IsPrime
have h : Ideal.IsPrime (Ideal.under R p) ∧ p ≠ ⊤
Tactic: rw [IsLocalization.isPrime_iff_isPrime_disjoint S A, IsLocalization.disjoint_under_iff S]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal R
p : Ideal A
hp : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' J.minimalPrimes) p
⊢ Ideal.IsPrime (Ideal.under R p) ∧ p ≠ ⊤
have h : p ≠ ⊤
Tactic: refine ⟨hp.isPrime, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal R
p : Ideal A
hp : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' J.minimalPrimes) p
I : Ideal A
hI : I.IsPrime ∧ Ideal.map (F := R →+* A) (algebraMap R A) J ≤ I
e : I ≤ p
⊢ p ≤ I
have h : LE.le.{u_2} (α := Ideal A) (Ideal.map (F := R →+* A) (algebraMap R A) (Ideal.under R p))
  (Ideal.map (F := R →+* A) (algebraMap R A) (Ideal.under R I))
Tactic: rw [← IsLocalization.map_under S A I, ← IsLocalization.map_under S A p]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal A
| Ideal.comap (F := R →+* A) (algebraMap R A) '' J.minimalPrimes
have rw : Set.image (α := Ideal A) (Ideal.comap (F := R →+* A) (algebraMap R A))
  (Set.preimage (β := Ideal R) (Ideal.under R) (Ideal.minimalPrimes (Ideal.under R J)))
Tactic: rw [← map_under S A J, minimalPrimes_map S]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal A
⊢ Eq (α := Set (Ideal R)) (Ideal.minimalPrimes (Ideal.comap (F := R →+* A) (algebraMap R A) J))
    (Ideal.comap (F := R →+* A) (algebraMap R A) '' J.minimalPrimes)
have conv_rhs : Eq (α := Set (Ideal R)) (Ideal.minimalPrimes (Ideal.comap (F := R →+* A) (algebraMap R A) J))
  (Set.image (α := Ideal A) (Ideal.comap (F := R →+* A) (algebraMap R A))
    (Set.preimage (β := Ideal R) (Ideal.under R) (Ideal.minimalPrimes (Ideal.under R J))))
Tactic: conv_rhs => rw [← map_under S A J, minimalPrimes_map S]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Submonoid R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
J : Ideal A
⊢ Eq (α := Set (Ideal R)) (Ideal.minimalPrimes (Ideal.comap (F := R →+* A) (algebraMap R A) J))
    (Set.image (α := Ideal A) (Ideal.comap (F := R →+* A) (algebraMap R A))
      (Set.preimage (β := Ideal R) (Ideal.under R) (Ideal.minimalPrimes (Ideal.under R J))))
have refine : Subset (α := Set (Ideal R)) (Ideal.minimalPrimes (Ideal.comap (F := R →+* A) (algebraMap R A) J))
  (Set.range (ι := Ideal A) (Ideal.comap (F := R →+* A) (algebraMap R A)))
Tactic: refine (Set.image_preimage_eq_iff.mpr ?_).symm
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
⊢ Eq.{u_2 + 1} (α := Ideal A) (Ideal.radical (Ideal.map (F := R →+* A) (algebraMap R A) I))
    (Ideal.map (F := R →+* A) (algebraMap R A) q)
have this : IsLocalRing A
Tactic: have : IsLocalRing A := AtPrime.isLocalRing A q
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
⊢ Eq.{u_2 + 1} (α := Ideal A) (Ideal.radical (Ideal.map (F := R →+* A) (algebraMap R A) I))
    (Ideal.map (F := R →+* A) (algebraMap R A) q)
have rw : Eq.{u_2 + 1} (α := Ideal A) (sInf (Ideal.under R ⁻¹' I.minimalPrimes)) (Ideal.map (F := R →+* A) (algebraMap R A) q)
Tactic: rw [← Ideal.sInf_minimalPrimes, IsLocalization.minimalPrimes_map q.primeCompl A I]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
⊢ Eq.{u_2 + 1} (α := Ideal A) (sInf (Ideal.under R ⁻¹' I.minimalPrimes)) (Ideal.map (F := R →+* A) (algebraMap R A) q)
have refine_1 : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) (Ideal.map (F := R →+* A) (algebraMap R A) q)
Tactic: refine le_antisymm (sInf_le ?_) (le_sInf fun J hJ ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
refine_1 :
  Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) (Ideal.map (F := R →+* A) (algebraMap R A) q)
⊢ Eq.{u_2 + 1} (α := Ideal A) (sInf (Ideal.under R ⁻¹' I.minimalPrimes)) (Ideal.map (F := R →+* A) (algebraMap R A) q)
have refine_2 : ∀ (J : Ideal A) (hJ : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) J),
  Ideal.map (F := R →+* A) (algebraMap R A) q ≤ J
Tactic: refine le_antisymm (sInf_le ?_) (le_sInf fun J hJ ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
⊢ Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) (Ideal.map (F := R →+* A) (algebraMap R A) q)
have refine_1 : Ideal.under.{u_1, u_2} R (B := A) (Ideal.map (F := R →+* A) (algebraMap R A) q) ∈ I.minimalPrimes
Tactic: rwa [Set.mem_preimage, map_eq_maximalIdeal q A, under_maximalIdeal A q]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
refine_1 : Ideal.under.{u_1, u_2} R (B := A) (Ideal.map (F := R →+* A) (algebraMap R A) q) ∈ I.minimalPrimes
⊢ Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) (Ideal.map (F := R →+* A) (algebraMap R A) q)
have refine_1₁ : Ideal.under R (IsLocalRing.maximalIdeal A) ∈ I.minimalPrimes
Tactic: rwa [Set.mem_preimage, map_eq_maximalIdeal q A, under_maximalIdeal A q]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
J : Ideal A
hJ : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) J
⊢ Ideal.map (F := R →+* A) (algebraMap R A) q ≤ J
have refine_2 : q ≤ Ideal.under R J
Tactic: rw [← IsLocalization.under_le_under_iff q.primeCompl A,
      AtPrime.map_eq_maximalIdeal q A, AtPrime.under_maximalIdeal A q]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (goal)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
J : Ideal A
hJ : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) J
⊢ q ≤ Ideal.under R J
have refine_2 : Ideal.under R J ≤ q
Tactic: apply hIq.2 hJ.1
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
J : Ideal A
hJ : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) J
⊢ Ideal.under R J ≤ q
have this₁ : Ne (α := Ideal R) (Ideal.under R J) ⊤
Tactic: have := hJ.isPrime.ne_top
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.MinimalPrime.Localization (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
A : Type u_2
inst_1 : CommSemiring A
inst_2 : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst_3 : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this_1 : IsLocalRing A
J : Ideal A
hJ : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' I.minimalPrimes) J
this : Ne (α := Ideal R) (Ideal.under R J) ⊤
⊢ Ideal.under R J ≤ q
have this₁ : Disjoint (↑q.primeCompl : Set R) (↑(Ideal.under R J) : Set R)
Tactic: rw [ne_eq, Ideal.comap_eq_top_iff, ← ne_eq, ← disjoint_under_iff q.primeCompl A J] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra B L
inst_10 : IsScalarTower A B L
inst_11 : IsIntegralClosure B A L
⊢ Eq (α := B →ₐ[A] B) (galRestrict' A B B (AlgHom.id K L)) (AlgHom.id A B)
have H : ∀ (x : B), Eq (α := B) ((galRestrict' A B B (AlgHom.id K L) : (a : B) → B) x : B) ((AlgHom.id A B : (a : B) → B) x : B)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IntegralClosure.IntegralRestrict (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : Algebra K L
inst_7 : Algebra A L
inst_8 : IsScalarTower A K L
inst_9 : Algebra B L
inst_10 : IsScalarTower A B L
inst_11 : IsIntegralClosure B A L
x : B
⊢ Eq (α := B) ((galRestrict' A B B (AlgHom.id K L) : (a : B) → B) x : B) ((AlgHom.id A B : (a : B) → B) x : B)
have H : Eq.{u_3 + 1} (α := L) ((algebraMap B L : (a : B) → L) ((galRestrict' A B B (AlgHom.id K L) : (a : B) → B) x : B) : L)
  ((algebraMap B L : (a : B) → L) ((AlgHom.id A B : (a : B) → B) x : B) : L)
Tactic: apply IsIntegralClosure.algebraMap_injective B A L