refine ⟨fun H ↦ ⟨H.1.1, H.2⟩, fun H ↦ ⟨⟨H.1, ?_⟩, H.2⟩⟩
case neg.h.a
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝ : NoZeroSMulDivisors R S
hIbot : ¬I = ⊥
h1 : Algebra.IsIntegral R S
hIbot' : Ideal.comap (algebraMap R S) I ≠ ⊥
𝔓 : (p : Ideal R) → p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p → Ideal S
h𝔓 : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ≥ I
h𝔓' : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ∈ primesOver S p
p : Ideal R
hp : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p
hpbot : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
this : p.IsPrime
P : Ideal S
⊢ (P.IsPrime ∧ I ≤ P) ∧ Ideal.comap (algebraMap R S) P = p ↔ P ∈ primesOver S p
case neg.h.a
R : Type u_1
K : Type u_2
L : Type u_3
S : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra R L
inst✝⁵ : IsScalarTower R S L
inst✝⁴ : IsScalarTower R K L
inst✝³ : IsIntegralClosure S R L
inst✝² : FiniteDimensional K L
inst✝¹ : IsGalois K L
inst✝ : IsUnramified R S
I : Ideal S
hI : ∀ (σ : L ≃ₐ[K] L), Ideal.comap ((galRestrict R K L S) σ) I = I
this✝² : IsDomain S
this✝¹ : IsDedekindDomain S
hRS : Function.Injective ⇑(algebraMap R S)
this✝ : NoZeroSMulDivisors R S
hIbot : ¬I = ⊥
h1 : Algebra.IsIntegral R S
hIbot' : Ideal.comap (algebraMap R S) I ≠ ⊥
𝔓 : (p : Ideal R) → p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p → Ideal S
h𝔓 : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ≥ I
h𝔓' : ∀ (p : Ideal R) (a : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p), 𝔓 p a ∈ primesOver S p
p : Ideal R
hp : p.IsPrime ∧ Ideal.comap (algebraMap R S) I ≤ p
hpbot : p ≠ ⊥
hpbot' : Ideal.map (algebraMap R S) p ≠ ⊥
this : p.IsPrime
P : Ideal S
H : P ∈ primesOver S p
⊢ I ≤ P