R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I✝ : Ideal R
hf : Function.Surjective ↑f
I : Ideal R
H : IsMaximal I
ne_top : ¬map f I = ⊤
J : Ideal S
hJ : map f I < J
⊢ J = ⊤
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I✝ : Ideal R
hf : Function.Surjective ↑f
I : Ideal R
H : IsMaximal I
⊢ map f I = ⊤ ∨ IsMaximal (map f I)
refine' or_iff_not_imp_left.2 fun ne_top => ⟨⟨fun h => ne_top h, fun J hJ => _⟩⟩
case refine'_1
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I✝ : Ideal R
hf : Function.Surjective ↑f
I : Ideal R
H : IsMaximal I
ne_top : ¬map f I = ⊤
J : Ideal S
hJ : map f I < J
⊢ I ≤ comap f J

case refine'_2
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I✝ : Ideal R
hf : Function.Surjective ↑f
I : Ideal R
H : IsMaximal I
ne_top : ¬map f I = ⊤
J : Ideal S
hJ : map f I < J
⊢ I ≠ comap f J
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I✝ : Ideal R
hf : Function.Surjective ↑f
I : Ideal R
H : IsMaximal I
ne_top : ¬map f I = ⊤
J : Ideal S
hJ : map f I < J
⊢ J = ⊤
refine'
  (relIsoOfSurjective f hf).injective
    (Subtype.ext_iff.2 (Eq.trans (H.1.2 (comap f J) (lt_of_le_of_ne _ _)) comap_top.symm))
no goals
case refine'_1
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I✝ : Ideal R
hf : Function.Surjective ↑f
I : Ideal R
H : IsMaximal I
ne_top : ¬map f I = ⊤
J : Ideal S
hJ : map f I < J
⊢ I ≤ comap f J
exact map_le_iff_le_comap.1 (le_of_lt hJ)
no goals
case refine'_2
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : RingHomClass F R S
f : F
I✝ : Ideal R
hf : Function.Surjective ↑f
I : Ideal R
H : IsMaximal I
ne_top : ¬map f I = ⊤
J : Ideal S
hJ : map f I < J
⊢ I ≠ comap f J
exact fun h => hJ.right (le_map_of_comap_le_of_surjective f hf (le_of_eq h.symm))