mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case inl
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p q : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨i, q⟩
⊢ ⟨i, p⟩ = ⟨i, q⟩

pp: case inr
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨j, q⟩
ne : i ≠ j
⊢ ⟨i, p⟩ = ⟨j, q⟩

Tactic:
·

Goal state after:
case inl
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p q : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨i, q⟩
⊢ ⟨i, p⟩ = ⟨i, q⟩
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case inr
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨j, q⟩
ne : i ≠ j
⊢ ⟨i, p⟩ = ⟨j, q⟩

Tactic:
·

Goal state after:
case inr
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
x✝¹ x✝ : (i : ι) × PrimeSpectrum (R i)
i : ι
p : PrimeSpectrum (R i)
j : ι
q : PrimeSpectrum (R j)
eq : sigmaToPi R ⟨i, p⟩ = sigmaToPi R ⟨j, q⟩
ne : i ≠ j
⊢ ⟨i, p⟩ = ⟨j, q⟩
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ (∃ i, I.IsMinimalPrime i ∧ x ∈ i) → ∃ y ∉ I.radical, x * y ∈ I.radical

pp: case mpr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ (∃ y ∉ I.radical, x * y ∈ I.radical) → ∃ i, I.IsMinimalPrime i ∧ x ∈ i

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ (∃ i, I.IsMinimalPrime i ∧ x ∈ i) → ∃ y ∉ I.radical, x * y ∈ I.radical
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case pos
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
x : (i : ι) → R i
hx : x ∈ ker (Pi.evalRingHom R i)
j : ι
hj : i = j
⊢ x j = (x * e i) j

pp: case neg
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
x : (i : ι) → R i
hx : x ∈ ker (Pi.evalRingHom R i)
j : ι
hj : ¬i = j
⊢ x j = (x * e i) j

Tactic:
·

Goal state after:
case pos
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
x : (i : ι) → R i
hx : x ∈ ker (Pi.evalRingHom R i)
j : ι
hj : i = j
⊢ x j = (x * e i) j
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case neg
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
x : (i : ι) → R i
hx : x ∈ ker (Pi.evalRingHom R i)
j : ι
hj : ¬i = j
⊢ x j = (x * e i) j

Tactic:
·

Goal state after:
case neg
ι : Type u_3
R : ι → Type u_4
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : _root_.Finite ι
p : PrimeSpectrum ((i : ι) → R i)
val✝ : Fintype ι
e : ι → (i : ι) → R i := fun i ↦ Function.update 1 i 0
H : ∏ i, e i = 0
i : ι
hi : e i ∈ p.asIdeal
h₁ : Function.Surjective ⇑(Pi.evalRingHom R i) := RingHomSurjective.is_surjective
x : (i : ι) → R i
hx : x ∈ ker (Pi.evalRingHom R i)
j : ι
hj : ¬i = j
⊢ x j = (x * e i) j
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Subsingleton R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

pp: case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Subsingleton R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case a
ι : Type u_3
R : ι → Type u_4
inst✝² : (i : ι) → CommRing (R i)
inst✝¹ : _root_.Finite ι
S : Type u_5
inst✝ : CommRing S
f : S →+* (i : ι) → R i
⊢ ⋃ i, Set.range (comap f ∘ comap (Pi.evalRingHom R i)) ⊆ Set.range (comap f)

pp: case a
ι : Type u_3
R : ι → Type u_4
inst✝² : (i : ι) → CommRing (R i)
inst✝¹ : _root_.Finite ι
S : Type u_5
inst✝ : CommRing S
f : S →+* (i : ι) → R i
⊢ Set.range (comap f) ⊆ ⋃ i, Set.range (comap f ∘ comap (Pi.evalRingHom R i))

Tactic:
·

Goal state after:
case a
ι : Type u_3
R : ι → Type u_4
inst✝² : (i : ι) → CommRing (R i)
inst✝¹ : _root_.Finite ι
S : Type u_5
inst✝ : CommRing S
f : S →+* (i : ι) → R i
⊢ ⋃ i, Set.range (comap f ∘ comap (Pi.evalRingHom R i)) ⊆ Set.range (comap f)
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ⊥.IsPrime
⊢ KrullDimLE 1 R

pp: case neg
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ¬⊥.IsPrime
⊢ KrullDimLE 1 R

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
hR : ⊥.IsPrime
⊢ KrullDimLE 1 R
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case a
ι : Type u_3
R : ι → Type u_4
inst✝² : (i : ι) → CommRing (R i)
inst✝¹ : _root_.Finite ι
S : Type u_5
inst✝ : CommRing S
f : S →+* (i : ι) → R i
⊢ Set.range (comap f) ⊆ ⋃ i, Set.range (comap f ∘ comap (Pi.evalRingHom R i))

Tactic:
·

Goal state after:
case a
ι : Type u_3
R : ι → Type u_4
inst✝² : (i : ι) → CommRing (R i)
inst✝¹ : _root_.Finite ι
S : Type u_5
inst✝ : CommRing S
f : S →+* (i : ι) → R i
⊢ Set.range (comap f) ⊆ ⋃ i, Set.range (comap f ∘ comap (Pi.evalRingHom R i))
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
⊢ (∃ x, I ≤ x.asIdeal ∧ comap f x = p) → Ideal.comap f I ≤ p.asIdeal

pp: case refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
⊢ ∃ x, I ≤ x.asIdeal ∧ comap f x = p

Tactic:
·

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
⊢ (∃ x, I ≤ x.asIdeal ∧ comap f x = p) → Ideal.comap f I ≤ p.asIdeal
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ ↑a * ↑⟨↑a + ↑b - ↑a * ↑b, ⋯⟩ = ↑a

Tactic:
simp_rw [mul_sub, mul_add]; rw [← mul_assoc, a.2, add_sub_cancel_right]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
⊢ ∃ x, I ≤ x.asIdeal ∧ comap f x = p

Tactic:
·

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
⊢ ∃ x, I ≤ x.asIdeal ∧ comap f x = p
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case refine_2.refine_1
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : S
hx : x ∈ I
⊢ x ∈ { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }.asIdeal

pp: case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
⊢ comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ } = p

Tactic:
·

Goal state after:
case refine_2.refine_1
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : S
hx : x ∈ I
⊢ x ∈ { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ }.asIdeal
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ ↑b * ↑a + ↑b - ↑b * ↑a = ↑b

Tactic:
add_sub_cancel_left

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ ↑b = ↑b
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
⊢ comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ } = p

Tactic:
·

Goal state after:
case refine_2.refine_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
⊢ comap f { asIdeal := Ideal.map f p.asIdeal, isPrime := ⋯ } = p
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ (∃ y ∉ I.radical, x * y ∈ I.radical) → ∃ i, I.IsMinimalPrime i ∧ x ∈ i

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
⊢ (∃ y ∉ I.radical, x * y ∈ I.radical) → ∃ i, I.IsMinimalPrime i ∧ x ∈ i
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
⊢ Set.range (comap f) = zeroLocus ↑(ker f)

Tactic:
rw [← Set.image_univ]
  convert! image_comap_zeroLocus_eq_zeroLocus_comap _ _ hf _
  rw [zeroLocus_bot]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case refine_1
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
⊢ p ∈ Set.range (comap (algebraMap R S))

pp: case refine_2
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : p ∈ Set.range (comap (algebraMap R S))
⊢ Nontrivial (p.asIdeal.ResidueField ⊗[R] S)

Tactic:
·

Goal state after:
case refine_1
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
⊢ p ∈ Set.range (comap (algebraMap R S))
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: case refine_2
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : p ∈ Set.range (comap (algebraMap R S))
⊢ Nontrivial (p.asIdeal.ResidueField ⊗[R] S)

Tactic:
·

Goal state after:
case refine_2
R : Type u
inst✝² : CommRing R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
k : Type u := p.asIdeal.ResidueField
h : p ∈ Set.range (comap (algebraMap R S))
⊢ Nontrivial (p.asIdeal.ResidueField ⊗[R] S)
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I J : Ideal S
h : J ∈ I.minimalPrimes
this✝ : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ (map f K).IsPrime ∧ I ≤ map f K

pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I J : Ideal S
h : J ∈ I.minimalPrimes
this✝ : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ map f K ≤ J

Tactic:
·

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I J : Ideal S
h : J ∈ I.minimalPrimes
this✝ : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ (map f K).IsPrime ∧ I ≤ map f K
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I J : Ideal S
h : J ∈ I.minimalPrimes
this✝ : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ map f K ≤ J

Tactic:
·

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I J : Ideal S
h : J ∈ I.minimalPrimes
this✝ : J.IsPrime
K : Ideal R
hK : K.IsPrime
e₁ : comap f I ≤ K
e₂ : K ≤ comap f J
this : RingHom.ker f ≤ K
⊢ map f K ≤ J
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
⊢ J ∈ (comap f I).minimalPrimes → J ∈ comap f '' I.minimalPrimes

pp: case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
⊢ J ∈ comap f '' I.minimalPrimes → J ∈ (comap f I).minimalPrimes

Tactic:
·

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
⊢ J ∈ (comap f I).minimalPrimes → J ∈ comap f '' I.minimalPrimes
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
⊢ J ∈ comap f '' I.minimalPrimes → J ∈ (comap f I).minimalPrimes

Tactic:
·

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal S
J : Ideal R
⊢ J ∈ comap f '' I.minimalPrimes → J ∈ (comap f I).minimalPrimes
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_3
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
⊢ (map f I).minimalPrimes = map f '' (I ⊔ RingHom.ker f).minimalPrimes

Tactic:
apply Set.image_injective.mpr (Ideal.comap_injective_of_surjective f hf)
  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]
  intro x hx
  exact (Ideal.comap_map_of_surjective f hf _).trans (sup_eq_left.mpr <| le_sup_right.trans hx.le)

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
⊢ p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes → p ∈ Ideal.under R ⁻¹' J.minimalPrimes

pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
⊢ p ∈ Ideal.under R ⁻¹' J.minimalPrimes → p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
⊢ p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes → p ∈ Ideal.under R ⁻¹' J.minimalPrimes
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp.refine_1
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
this : p.IsPrime
I : Ideal R
hI : I.IsPrime ∧ J ≤ I
e : I ≤ Ideal.under R p
hI' : Disjoint ↑S ↑I
⊢ (Ideal.map (algebraMap R A) I).IsPrime

pp: case mp.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
this : p.IsPrime
I : Ideal R
hI : I.IsPrime ∧ J ≤ I
e : I ≤ Ideal.under R p
hI' : Disjoint ↑S ↑I
⊢ Ideal.comap (algebraMap R A) (Ideal.map (algebraMap R A) I) = I

Tactic:
·

Goal state after:
case mp.refine_1
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
this : p.IsPrime
I : Ideal R
hI : I.IsPrime ∧ J ≤ I
e : I ≤ Ideal.under R p
hI' : Disjoint ↑S ↑I
⊢ (Ideal.map (algebraMap R A) I).IsPrime
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
this : p.IsPrime
I : Ideal R
hI : I.IsPrime ∧ J ≤ I
e : I ≤ Ideal.under R p
hI' : Disjoint ↑S ↑I
⊢ Ideal.comap (algebraMap R A) (Ideal.map (algebraMap R A) I) = I

Tactic:
·

Goal state after:
case mp.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
this : p.IsPrime
I : Ideal R
hI : I.IsPrime ∧ J ≤ I
e : I ≤ Ideal.under R p
hI' : Disjoint ↑S ↑I
⊢ Ideal.comap (algebraMap R A) (Ideal.map (algebraMap R A) I) = I
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
⊢ p ∈ Ideal.under R ⁻¹' J.minimalPrimes → p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes

Tactic:
·

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
⊢ p ∈ Ideal.under R ⁻¹' J.minimalPrimes → p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mpr.refine_1
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ Ideal.under R ⁻¹' J.minimalPrimes
⊢ p.IsPrime

pp: case mpr.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ Ideal.under R ⁻¹' J.minimalPrimes
⊢ ∀ ⦃y : Ideal A⦄, (fun q ↦ q.IsPrime ∧ Ideal.map (algebraMap R A) J ≤ q) y → y ≤ p → p ≤ y

Tactic:
·

Goal state after:
case mpr.refine_1
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ Ideal.under R ⁻¹' J.minimalPrimes
⊢ p.IsPrime
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mpr.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ Ideal.under R ⁻¹' J.minimalPrimes
⊢ ∀ ⦃y : Ideal A⦄, (fun q ↦ q.IsPrime ∧ Ideal.map (algebraMap R A) J ≤ q) y → y ≤ p → p ≤ y

Tactic:
·

Goal state after:
case mpr.refine_2
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ Ideal.under R ⁻¹' J.minimalPrimes
⊢ ∀ ⦃y : Ideal A⦄, (fun q ↦ q.IsPrime ∧ Ideal.map (algebraMap R A) J ≤ q) y → y ≤ p → p ≤ y
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
⊢ Ideal.map (algebraMap R A) q ∈ Ideal.under R ⁻¹' I.minimalPrimes

pp: case refine_2
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
J : Ideal A
hJ : J ∈ Ideal.under R ⁻¹' I.minimalPrimes
⊢ Ideal.map (algebraMap R A) q ≤ J

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
⊢ Ideal.map (algebraMap R A) q ∈ Ideal.under R ⁻¹' I.minimalPrimes
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
J : Ideal A
hJ : J ∈ Ideal.under R ⁻¹' I.minimalPrimes
⊢ Ideal.map (algebraMap R A) q ≤ J

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
J : Ideal A
hJ : J ∈ Ideal.under R ⁻¹' I.minimalPrimes
⊢ Ideal.map (algebraMap R A) q ≤ J
Module: Mathlib.Topology.Compactness.Bases

Goal state before:
pp: case refine_1
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : Y → ι
e : U = ⋃ i, (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ U ⊆ ⋃ i ∈ ↑(Finset.image f' t), b i

pp: case refine_2
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : Y → ι
e : U = ⋃ i, (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ⋃ i ∈ ↑(Finset.image f' t), b i ⊆ U

Tactic:
·

Goal state after:
case refine_1
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : Y → ι
e : U = ⋃ i, (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ U ⊆ ⋃ i ∈ ↑(Finset.image f' t), b i