-- Mathlib/RingTheory/Jacobson/Ideal.lean
theorem map_jacobson_of_surjective {f : R →+* S} (hf : Function.Surjective f) :
    RingHom.ker f ≤ I → map f I.jacobson = (map f I).jacobson

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

Tactic:
have : ∀ J ∈ { J : Ideal R | I ≤ J ∧ J.IsMaximal }, RingHom.ker f ≤ J :=
  fun J hJ => le_trans h hJ.left

Result:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
⊢ map f (sInf {J | I ≤ J ∧ J.IsMaximal}) = sInf {J | map f I ≤ J ∧ J.IsMaximal}

Proof state:
case refine_2.inr
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
hmax : (map f J).IsMaximal
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}

Tactic:
exact Set.mem_insert_of_mem ⊤ ⟨map_mono hJ.1.1, hmax⟩

Result:
no goals

Proof state:
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
⊢ sInf {J | map f I ≤ J ∧ J.IsMaximal} ≤ sInf (map f '' {J | I ≤ J ∧ J.IsMaximal})

Tactic:
refine sInf_le_sInf_of_subset_insert_top fun j hj => hj.recOn fun J hJ => ?_

Result:
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
⊢ j ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}

Proof state:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
⊢ sInf (map f '' {J | I ≤ J ∧ J.IsMaximal}) ≤ sInf {J | map f I ≤ J ∧ J.IsMaximal}

Tactic:
refine
  sInf_le_sInf fun J hJ =>
    ⟨comap f J, ⟨⟨le_comap_of_map_le hJ.1, ?_⟩, map_comap_of_surjective f hf J⟩⟩

Result:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
J : Ideal S
hJ : J ∈ {J | map f I ≤ J ∧ J.IsMaximal}
⊢ (comap f J).IsMaximal

Proof state:
case refine_2.inl
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
htop : map f J = ⊤
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}

Tactic:
exact htop.symm ▸ Set.mem_insert ⊤ _

Result:
no goals

Proof state:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
J : Ideal S
hJ : J ∈ {J | map f I ≤ J ∧ J.IsMaximal}
⊢ (comap f J).IsMaximal

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

Result:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this✝ : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
J : Ideal S
hJ : J ∈ {J | map f I ≤ J ∧ J.IsMaximal}
this : J.IsMaximal
⊢ (comap f J).IsMaximal

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
⊢ map f (sInf {J | I ≤ J ∧ J.IsMaximal}) = sInf {J | map f I ≤ J ∧ J.IsMaximal}

Tactic:
refine Trans.trans (map_sInf hf this) (le_antisymm ?_ ?_)

Result:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
⊢ sInf (map f '' {J | I ≤ J ∧ J.IsMaximal}) ≤ sInf {J | map f I ≤ J ∧ J.IsMaximal}

case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
⊢ sInf {J | map f I ≤ J ∧ J.IsMaximal} ≤ sInf (map f '' {J | I ≤ J ∧ J.IsMaximal})

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
⊢ map f I.jacobson = (map f I).jacobson

Tactic:
unfold Ideal.jacobson

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

Proof state:
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
⊢ j ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}

Tactic:
rw [← hJ.2]

Result:
case refine_2
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
j : Ideal S
hj : j ∈ map f '' {J | I ≤ J ∧ J.IsMaximal}
J : Ideal R
hJ : J ∈ {J | I ≤ J ∧ J.IsMaximal} ∧ map f J = j
⊢ map f J ∈ insert ⊤ {J | map f I ≤ J ∧ J.IsMaximal}

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
⊢ RingHom.ker f ≤ I → map f I.jacobson = (map f I).jacobson

Tactic:
intro h

Result:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
⊢ map f I.jacobson = (map f I).jacobson

Proof state:
case refine_1
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
I : Ideal R
f : R →+* S
hf : Function.Surjective ⇑f
h : RingHom.ker f ≤ I
this✝ : ∀ J ∈ {J | I ≤ J ∧ J.IsMaximal}, RingHom.ker f ≤ J
J : Ideal S
hJ : J ∈ {J | map f I ≤ J ∧ J.IsMaximal}
this : J.IsMaximal
⊢ (comap f J).IsMaximal

Tactic:
exact comap_isMaximal_of_surjective f hf

Result:
no goals