-- Mathlib/RingTheory/Jacobson/Ideal.lean
theorem comap_jacobson_of_surjective {f : R →+* S} (hf : Function.Surjective f) {K : Ideal S} :
    comap f K.jacobson = (comap f K).jacobson

Proof state:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ J.IsMaximal}
this : comap f (map f J) = J
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}

Tactic:
rcases map_eq_top_or_isMaximal_of_surjective _ hf hJ.right with htop | hmax

Result:
case refine_1.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ J.IsMaximal}
this : comap f (map f J) = J
htop : map f J = ⊤
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}

case refine_1.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ J.IsMaximal}
this : comap f (map f J) = J
hmax : (map f J).IsMaximal
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ comap f K.jacobson = (comap f K).jacobson

Tactic:
unfold Ideal.jacobson

Result:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ comap f (sInf {J | K ≤ J ∧ J.IsMaximal}) = sInf {J | comap f K ≤ J ∧ J.IsMaximal}

Proof state:
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K J : Ideal S
hJ : J ∈ {J | K ≤ J ∧ J.IsMaximal}
this : J.IsMaximal
⊢ sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f J

Tactic:
exact sInf_le ⟨comap_mono hJ.left, comap_isMaximal_of_surjective _ hf⟩

Result:
no goals

Proof state:
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K J : Ideal S
hJ : J ∈ {J | K ≤ J ∧ J.IsMaximal}
⊢ sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f J

Tactic:
haveI : J.IsMaximal := hJ.right

Result:
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K J : Ideal S
hJ : J ∈ {J | K ≤ J ∧ J.IsMaximal}
this : J.IsMaximal
⊢ sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f J

Proof state:
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ ∀ i ∈ {J | K ≤ J ∧ J.IsMaximal}, sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f i

Tactic:
intros J hJ

Result:
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K J : Ideal S
hJ : J ∈ {J | K ≤ J ∧ J.IsMaximal}
⊢ sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f J

Proof state:
case refine_1.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ J.IsMaximal}
this : comap f (map f J) = J
htop : map f J = ⊤
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}

Tactic:
exact ⟨⊤, Set.mem_insert ⊤ _, htop ▸ this⟩

Result:
no goals

Proof state:
case refine_1.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ J.IsMaximal}
this : comap f (map f J) = J
hmax : (map f J).IsMaximal
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}

Tactic:
exact ⟨map f J, Set.mem_insert_of_mem _ ⟨le_map_of_comap_le_of_surjective f hf hJ.1, hmax⟩,
  this⟩

Result:
no goals

Proof state:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ J.IsMaximal}
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}

Tactic:
have : comap f (map f J) = J :=
  Trans.trans (comap_map_of_surjective f hf J)
    (le_antisymm (sup_le_iff.2 ⟨le_of_eq rfl, le_trans (comap_mono bot_le) hJ.left⟩)
      le_sup_left)

Result:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ J.IsMaximal}
this : comap f (map f J) = J
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}

Proof state:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ ⨅ I ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}, I ≤ ⨅ a ∈ {J | comap f K ≤ J ∧ J.IsMaximal}, a

Tactic:
refine iInf_le_iInf_of_subset fun J hJ => ?_

Result:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
J : Ideal R
hJ : J ∈ {J | comap f K ≤ J ∧ J.IsMaximal}
⊢ J ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}

Proof state:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ comap f (sInf {J | K ≤ J ∧ J.IsMaximal}) ≤ sInf {J | comap f K ≤ J ∧ J.IsMaximal}

Tactic:
rw [← top_inf_eq (sInf _), ← sInf_insert, comap_sInf', sInf_eq_iInf]

Result:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ ⨅ I ∈ comap f '' insert ⊤ {J | K ≤ J ∧ J.IsMaximal}, I ≤ ⨅ a ∈ {J | comap f K ≤ J ∧ J.IsMaximal}, a

Proof state:
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f (sInf {J | K ≤ J ∧ J.IsMaximal})

Tactic:
simp_rw [comap_sInf, le_iInf_iff]

Result:
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ ∀ i ∈ {J | K ≤ J ∧ J.IsMaximal}, sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f i

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ comap f (sInf {J | K ≤ J ∧ J.IsMaximal}) = sInf {J | comap f K ≤ J ∧ J.IsMaximal}

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ comap f (sInf {J | K ≤ J ∧ J.IsMaximal}) ≤ sInf {J | comap f K ≤ J ∧ J.IsMaximal}

case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
K : Ideal S
⊢ sInf {J | comap f K ≤ J ∧ J.IsMaximal} ≤ comap f (sInf {J | K ≤ J ∧ J.IsMaximal})