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.Bijective ↑f
I : Ideal R
H : IsMaximal I
h : map f I = ⊤
⊢ I = ⊤
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.Bijective ↑f
I : Ideal R
H : IsMaximal I
⊢ IsMaximal (map f I)
refine'
  or_iff_not_imp_left.1 (map_eq_top_or_isMaximal_of_surjective f hf.right H) fun h => H.1.1 _
no goals
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.Bijective ↑f
I : Ideal R
H : IsMaximal I
h : map f I = ⊤
⊢ I = ⊤
calc
  I = comap f (map f I) := ((relIsoOfBijective f hf).right_inv I).symm
  _ = comap f ⊤ := by rw [h]
  _ = ⊤ := by rw [comap_top]
no goals
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.Bijective ↑f
I : Ideal R
H : IsMaximal I
h : map f I = ⊤
⊢ comap f (map f I) = comap f ⊤
rw [h]
no goals
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.Bijective ↑f
I : Ideal R
H : IsMaximal I
h : map f I = ⊤
⊢ comap f ⊤ = ⊤
rw [comap_top]