awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
h₁ :
  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)) (Ideal.minimalPrimes (comap f I)) J ↔
    Membership.mem (γ := Set (Ideal R)) (comap f '' I.minimalPrimes) J

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
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)
⊢ Membership.mem (γ := Set (Ideal R)) (comap f '' I.minimalPrimes) J

Tactic:
obtain ⟨p, h, rfl⟩ := Ideal.exists_minimalPrimes_comap_eq f J H

Premises used: Ideal.exists_minimalPrimes_comap_eq, rfl
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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 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:
⟨p, h, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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 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:
exact ⟨p, h, rfl⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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 J : Ideal S
hJ : J ∈ I.minimalPrimes
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) (comap f J)

Tactic:
Ideal.minimalPrimes_comap_of_surjective hf hJ

Premises used: Ideal.minimalPrimes_comap_of_surjective
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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 J : Ideal S
hJ : J ∈ I.minimalPrimes
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (comap f I)) (comap f J)

Tactic:
exact Ideal.minimalPrimes_comap_of_surjective hf hJ

Premises used: Ideal.minimalPrimes_comap_of_surjective
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
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))
⊢ Eq.{u_3 + 1} (α := Set (Ideal S)) (Ideal.minimalPrimes (map f I)) (map f '' (I ⊔ RingHom.ker f).minimalPrimes)

Tactic:
apply Set.image_injective.mpr (Ideal.comap_injective_of_surjective f hf)

Premises used: Iff.mpr, Set.image_injective, Ideal.comap_injective_of_surjective
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
a : ∀ a ∈ (I ⊔ RingHom.ker f).minimalPrimes, Function.comp (β := Ideal S) (comap f) (map f) a = id 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:
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]

Premises used: Ideal.comap_map_of_surjective, Set.image_congr, Ideal.comap_minimalPrimes_eq_of_surjective, Set.image_comp, Set.image_id, RingHom.ker
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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 x : Ideal R
hx : x ∈ (I ⊔ RingHom.ker f).minimalPrimes
⊢ Function.comp (β := Ideal S) (comap f) (map f) x = id x

Tactic:
(Ideal.comap_map_of_surjective f hf _).trans (sup_eq_left.mpr <| le_sup_right.trans hx.le)

Premises used: Iff.mpr, Set.Mem, Ideal.IsMinimalPrime.le, setOf, sup_eq_left, le_sup_right, Ideal.comap_map_of_surjective, Ideal.comap, LE.le.trans, Eq.trans
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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 x : Ideal R
hx : x ∈ (I ⊔ RingHom.ker f).minimalPrimes
⊢ Function.comp (β := Ideal S) (comap f) (map f) x = id x

Tactic:
exact (Ideal.comap_map_of_surjective f hf _).trans (sup_eq_left.mpr <| le_sup_right.trans hx.le)

Premises used: Iff.mpr, Ideal.IsMinimalPrime.le, sup_eq_left, le_sup_right, Ideal.comap_map_of_surjective, LE.le.trans, Eq.trans
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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))
rw₃ rw₄ : I.minimalPrimes = I.minimalPrimes
⊢ I.minimalPrimes = Set.image (α := Ideal (R ⧸ I)) (comap (F := R →+* R ⧸ I) (Quotient.mk I)) (minimalPrimes (R ⧸ I))

Tactic:
rw [minimalPrimes, ← Ideal.comap_minimalPrimes_eq_of_surjective Ideal.Quotient.mk_surjective,
    ← RingHom.ker_eq_comap_bot, Ideal.mk_ker]

Premises used: Ideal.Quotient.mk_surjective, RingHom.ker_eq_comap_bot, Ideal.comap_minimalPrimes_eq_of_surjective, minimalPrimes, Ideal.mk_ker
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
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
⊢ Eq.{u_2 + 1} (α := Set (Ideal A)) (Ideal.minimalPrimes (Ideal.map (F := R →+* A) (algebraMap R A) J))
    (Ideal.under R ⁻¹' J.minimalPrimes)

Tactic:
ext p
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
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
⊢ 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
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
⊢ p.IsPrime

Tactic:
have := hp.isPrime
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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

Tactic:
⟨⟨Ideal.IsPrime.comap _, Ideal.map_le_iff_le_comap.mp hp.le⟩, ?_⟩

Premises used: Set.Mem, Ideal.IsMinimalPrime.le, setOf, Ideal.IsPrime.comap, Ideal.map_le_iff_le_comap, Set.preimage, Ideal.IsMinimalPrime, And.intro, Iff.mp, Minimal
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
h : ∀ ⦃y : Ideal R⦄, (fun (q : Ideal R) ↦ q.IsPrime ∧ J ≤ q) y → y ≤ Ideal.under R p → Ideal.under R p ≤ y
⊢ Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' J.minimalPrimes) p

Tactic:
refine ⟨⟨Ideal.IsPrime.comap _, Ideal.map_le_iff_le_comap.mp hp.le⟩, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
⊢ 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
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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

Tactic:
(Ideal.comap_mono <|
      hp.2 ⟨?_, Ideal.map_mono hI.2⟩ (Ideal.map_le_iff_le_comap.mpr e)).trans_eq ?_

Premises used: Iff.mpr, LE.le.trans_eq, Set.Mem, Ideal.comap_mono, Ideal.map_le_iff_le_comap, And.right, And.intro, Ideal.map_mono
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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)
h₁ : Ideal.comap (F := R →+* A) (algebraMap R A) (Ideal.map (F := R →+* A) (algebraMap R A) I) = I
⊢ Ideal.under R p ≤ I

Tactic:
refine (Ideal.comap_mono <|
      hp.2 ⟨?_, Ideal.map_mono hI.2⟩ (Ideal.map_le_iff_le_comap.mpr e)).trans_eq ?_

Premises used: Iff.mpr, LE.le.trans_eq, Ideal.comap_mono, Ideal.map_le_iff_le_comap, And.right, And.intro, Ideal.map_mono
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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.IsPrime.{u_2} (α := A) (Ideal.map (F := R →+* A) (algebraMap R A) I)

Tactic:
IsLocalization.isPrime_of_isPrime_disjoint S A I hI.1 hI'

Premises used: IsLocalization.isPrime_of_isPrime_disjoint, And.left
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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.IsPrime.{u_2} (α := A) (Ideal.map (F := R →+* A) (algebraMap R A) I)

Tactic:
exact IsLocalization.isPrime_of_isPrime_disjoint S A I hI.1 hI'

Premises used: IsLocalization.isPrime_of_isPrime_disjoint, And.left
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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.comap (F := R →+* A) (algebraMap R A) (Ideal.map (F := R →+* A) (algebraMap R A) I) = I

Tactic:
IsLocalization.under_map_of_isPrime_disjoint S A hI.1 hI'

Premises used: And.left, IsLocalization.under_map_of_isPrime_disjoint
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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.comap (F := R →+* A) (algebraMap R A) (Ideal.map (F := R →+* A) (algebraMap R A) I) = I

Tactic:
exact IsLocalization.under_map_of_isPrime_disjoint S A hI.1 hI'

Premises used: And.left, IsLocalization.under_map_of_isPrime_disjoint
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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

Tactic:
⟨⟨?_, Ideal.map_le_iff_le_comap.mpr hp.le⟩, ?_⟩

Premises used: Iff.mpr, Set.Mem, Ideal.IsMinimalPrime.le, setOf, Ideal.map_le_iff_le_comap, Ideal.IsMinimalPrime, And.intro, Minimal
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
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
⊢ Membership.mem (γ := Set (Ideal A)) (Ideal.minimalPrimes (Ideal.map (F := R →+* A) (algebraMap R A) J)) p

Tactic:
refine ⟨⟨?_, Ideal.map_le_iff_le_comap.mpr hp.le⟩, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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 : Ideal.IsPrime (Ideal.under R p) ∧ p ≠ ⊤
⊢ p.IsPrime

Tactic:
rw [IsLocalization.isPrime_iff_isPrime_disjoint S A, IsLocalization.disjoint_under_iff S]

Premises used: IsLocalization.isPrime_iff_isPrime_disjoint, IsLocalization.disjoint_under_iff
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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 ≠ ⊤

Tactic:
⟨hp.isPrime, ?_⟩

Premises used: Ideal.IsMinimalPrime.isPrime, And.intro
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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 ≠ ⊤
⊢ Ideal.IsPrime (Ideal.under R p) ∧ p ≠ ⊤

Tactic:
refine ⟨hp.isPrime, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
hp : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' J.minimalPrimes) ⊤
⊢ False

Tactic:
hp.isPrime.ne_top rfl

Premises used: Ideal.IsMinimalPrime.isPrime, Ideal.IsPrime.ne_top, rfl
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
hp : Membership.mem (γ := Set (Ideal A)) (Ideal.under R ⁻¹' J.minimalPrimes) ⊤
⊢ False

Tactic:
exact hp.isPrime.ne_top rfl

Premises used: Ideal.IsMinimalPrime.isPrime, Ideal.IsPrime.ne_top, rfl
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
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))
⊢ p ≤ I

Tactic:
rw [← IsLocalization.map_under S A I, ← IsLocalization.map_under S A p]

Premises used: IsLocalization.map_under
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
⊢ 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:
Ideal.map_mono (hp.2 ⟨hI.1.comap _, Ideal.map_le_iff_le_comap.mp hI.2⟩
        (Ideal.comap_mono e))

Premises used: Ideal.IsPrime.comap, Ideal.comap_mono, Ideal.map_le_iff_le_comap, And.right, And.intro, Iff.mp, Ideal.map_mono
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
⊢ 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:
exact Ideal.map_mono (hp.2 ⟨hI.1.comap _, Ideal.map_le_iff_le_comap.mp hI.2⟩
        (Ideal.comap_mono e))

Premises used: Ideal.IsPrime.comap, Ideal.comap_mono, Ideal.map_le_iff_le_comap, And.right, And.intro, Iff.mp, Ideal.map_mono
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
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)))
| Ideal.comap (F := R →+* A) (algebraMap R A) '' J.minimalPrimes

Tactic:
rw [← map_under S A J, minimalPrimes_map S]

Premises used: IsLocalization.minimalPrimes_map, IsLocalization.map_under
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
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))))
⊢ 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)

Tactic:
conv_rhs => rw [← map_under S A J, minimalPrimes_map S]

Premises used: IsLocalization.minimalPrimes_map, IsLocalization.map_under
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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))))

Tactic:
(Set.image_preimage_eq_iff.mpr ?_).symm

Premises used: Iff.mpr, setOf, Set.image_preimage_eq_iff, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
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)))
⊢ 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:
refine (Set.image_preimage_eq_iff.mpr ?_).symm

Premises used: Iff.mpr, Set.image_preimage_eq_iff, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
⊢ Subset (α := Set (Ideal R)) (Ideal.comap (F := R →+* A) (algebraMap R A) '' J.minimalPrimes)
    (Set.range (ι := Ideal A) (Ideal.comap (F := R →+* A) (algebraMap R A)))

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization
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
⊢ 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:
exact subset_trans (Ideal.minimalPrimes_comap_subset (algebraMap R A) J) (by simp)

Premises used: Algebra.algebraMap, subset_trans, Ideal.minimalPrimes_comap_subset