-- Mathlib/RingTheory/Ideal/Maps.lean
theorem comap_isMaximal_of_surjective (hf : Function.Surjective f) {K : Ideal S} [H : IsMaximal K] :
    IsMaximal (comap f K)

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
h : K = map f J
⊢ comap f ⊥ ≤ J

Tactic:
exact le_trans (comap_mono bot_le) (le_of_lt hJ)

Result:
no goals

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
this : map f J = ⊤
⊢ J = ⊤

Tactic:
have := congr_arg (comap f) this

Result:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
this✝ : map f J = ⊤
this : comap f (map f J) = comap f ⊤
⊢ J = ⊤

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
⊢ (comap f K).IsMaximal

Tactic:
refine ⟨⟨comap_ne_top _ H.1.1, fun J hJ => ?_⟩⟩

Result:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
⊢ J = ⊤

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
⊢ J = ⊤

Tactic:
suffices map f J = ⊤ by
  have := congr_arg (comap f) this
  rw [comap_top, comap_map_of_surjective _ hf, eq_top_iff] at this
  rw [eq_top_iff]
  exact le_trans this (sup_le (le_of_eq rfl) (le_trans (comap_mono bot_le) (le_of_lt hJ)))

Result:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
⊢ map f J = ⊤

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
this✝ : map f J = ⊤
this : ⊤ ≤ J ⊔ comap f ⊥
⊢ J = ⊤

Tactic:
rw [eq_top_iff]

Result:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
this✝ : map f J = ⊤
this : ⊤ ≤ J ⊔ comap f ⊥
⊢ ⊤ ≤ J

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
⊢ map f J = ⊤

Tactic:
refine
  H.1.2 (map f J)
    (lt_of_le_of_ne (le_map_of_comap_le_of_surjective _ hf (le_of_lt hJ)) fun h =>
      ne_of_lt hJ (_root_.trans (congr_arg (comap f) h) ?_))

Result:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
h : K = map f J
⊢ comap f (map f J) = J

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
this✝ : map f J = ⊤
this : ⊤ ≤ J ⊔ comap f ⊥
⊢ ⊤ ≤ J

Tactic:
exact le_trans this (sup_le (le_of_eq rfl) (le_trans (comap_mono bot_le) (le_of_lt hJ)))

Result:
no goals

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
h : K = map f J
⊢ comap f (map f J) = J

Tactic:
rw [comap_map_of_surjective _ hf, sup_eq_left]

Result:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
h : K = map f J
⊢ comap f ⊥ ≤ J

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
this✝ : map f J = ⊤
this : comap f (map f J) = comap f ⊤
⊢ J = ⊤

Tactic:
rw [comap_top, comap_map_of_surjective _ hf, eq_top_iff] at this

Result:
R : Type u
S : Type v
F : Type u_1
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
K : Ideal S
H : K.IsMaximal
J : Ideal R
hJ : comap f K < J
this✝ : map f J = ⊤
this : ⊤ ≤ J ⊔ comap f ⊥
⊢ J = ⊤