-- Mathlib/RingTheory/Ideal/GoingUp.lean
lemma map_eq_top_iff_of_ker_le {R S} [CommRing R] [CommRing S]
    (f : R →+* S) {I : Ideal R} (hf₁ : RingHom.ker f ≤ I) (hf₂ : f.IsIntegral) :
    I.map f = ⊤ ↔ I = ⊤

Proof state:
case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ ¬I = ⊤ → ¬map f I = ⊤

Tactic:
intro h

Result:
case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
⊢ ¬map f I = ⊤

Proof state:
case mp.intro.intro.intro.intro
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
x✝ : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
m' : Ideal S
left✝¹ : m'.IsMaximal
left✝ : (comap (algebraMap R S) m').IsMaximal
hm : I ≤ comap (algebraMap R S) m'
⊢ ¬map f I = ⊤

Tactic:
rw [← map_le_iff_le_comap] at hm

Result:
case mp.intro.intro.intro.intro
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
x✝ : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
m' : Ideal S
left✝¹ : m'.IsMaximal
left✝ : (comap (algebraMap R S) m').IsMaximal
hm : map (algebraMap R S) I ≤ m'
⊢ ¬map f I = ⊤

Proof state:
case mpr
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ I = ⊤ → map f I = ⊤

Tactic:
rintro rfl

Result:
case mpr
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf₂ : f.IsIntegral
hf₁ : RingHom.ker f ≤ ⊤
⊢ map f ⊤ = ⊤

Proof state:
case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
⊢ ¬map f I = ⊤

Tactic:
obtain ⟨m, _, hm⟩ := Ideal.exists_le_maximal I h

Result:
case mp.intro.intro
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
m : Ideal R
left✝ : m.IsMaximal
hm : I ≤ m
⊢ ¬map f I = ⊤

Proof state:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ map f I = ⊤ ↔ I = ⊤

Tactic:
constructor

Result:
case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ map f I = ⊤ → I = ⊤

case mpr
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ I = ⊤ → map f I = ⊤

Proof state:
case mp.intro.intro
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
m : Ideal R
left✝ : m.IsMaximal
hm : I ≤ m
x✝ : Algebra R S := f.toAlgebra
⊢ ¬map f I = ⊤

Tactic:
have : Algebra.IsIntegral _ _ := ⟨hf₂⟩

Result:
case mp.intro.intro
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
m : Ideal R
left✝ : m.IsMaximal
hm : I ≤ m
x✝ : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
⊢ ¬map f I = ⊤

Proof state:
case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ map f I = ⊤ → I = ⊤

case mpr
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ I = ⊤ → map f I = ⊤

Tactic:
swap

Result:
case mpr
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ I = ⊤ → map f I = ⊤

case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ map f I = ⊤ → I = ⊤

Proof state:
case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ map f I = ⊤ → I = ⊤

Tactic:
contrapose

Result:
case mp
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
⊢ ¬I = ⊤ → ¬map f I = ⊤

Proof state:
case mp.intro.intro.intro.intro
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
x✝ : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
m' : Ideal S
left✝¹ : m'.IsMaximal
left✝ : (comap (algebraMap R S) m').IsMaximal
hm : map (algebraMap R S) I ≤ m'
⊢ ¬map f I = ⊤

Tactic:
exact (hm.trans_lt (lt_top_iff_ne_top.mpr (IsMaximal.ne_top ‹_›))).ne

Result:
no goals

Proof state:
case mpr
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf₂ : f.IsIntegral
hf₁ : RingHom.ker f ≤ ⊤
⊢ map f ⊤ = ⊤

Tactic:
exact Ideal.map_top _

Result:
no goals

Proof state:
case mp.intro.intro
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
m : Ideal R
left✝ : m.IsMaximal
hm : I ≤ m
x✝ : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
⊢ ¬map f I = ⊤

Tactic:
obtain ⟨m', _, rfl⟩ := exists_ideal_over_maximal_of_isIntegral m (hf₁.trans hm)

Result:
case mp.intro.intro.intro.intro
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
x✝ : Algebra R S := f.toAlgebra
this : Algebra.IsIntegral R S
m' : Ideal S
left✝¹ : m'.IsMaximal
left✝ : (comap (algebraMap R S) m').IsMaximal
hm : I ≤ comap (algebraMap R S) m'
⊢ ¬map f I = ⊤

Proof state:
case mp.intro.intro
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
m : Ideal R
left✝ : m.IsMaximal
hm : I ≤ m
⊢ ¬map f I = ⊤

Tactic:
let _ := f.toAlgebra

Result:
case mp.intro.intro
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hf₁ : RingHom.ker f ≤ I
hf₂ : f.IsIntegral
h : ¬I = ⊤
m : Ideal R
left✝ : m.IsMaximal
hm : I ≤ m
x✝ : Algebra R S := f.toAlgebra
⊢ ¬map f I = ⊤