-- Mathlib/RingTheory/Valuation/LocalSubring.lean
lemma LocalSubring.map_maximalIdeal_eq_top_of_isMax {R : LocalSubring K}
    (hR : IsMax R) {S : Subring K} (hS : R.toSubring < S) :
    (maximalIdeal R.toSubring).map (Subring.inclusion hS.le) = ⊤

Proof state:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
⊢ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) = ⊤

Tactic:
by_contra h_is_not_top

Result:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) = ⊤
⊢ False

Proof state:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
⊢ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) = ⊤

Tactic:
let mR := (maximalIdeal R.toSubring).map (Subring.inclusion hS.le)

Result:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
⊢ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) = ⊤

Proof state:
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) ≤ M
fSₘ : LocalSubring K := ofPrime S M
⊢ ∀ (a : ↥R.toSubring), IsUnit ((Subring.inclusion ⋯) a) → IsUnit a

Tactic:
rintro ⟨a, h_a_inR⟩ h_fa_isUnit

Result:
case mk
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) ≤ M
fSₘ : LocalSubring K := ofPrime S M
a : K
h_a_inR : a ∈ R.toSubring
h_fa_isUnit : IsUnit ((Subring.inclusion ⋯) ⟨a, h_a_inR⟩)
⊢ IsUnit ⟨a, h_a_inR⟩

Proof state:
case intro.intro
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) ≤ M
⊢ False

Tactic:
let fSₘ : LocalSubring K := LocalSubring.ofPrime S M

Result:
case intro.intro
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) ≤ M
fSₘ : LocalSubring K := ofPrime S M
⊢ False

Proof state:
case mk
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) ≤ M
fSₘ : LocalSubring K := ofPrime S M
a : K
h_a_inR : a ∈ R.toSubring
h_fa_isUnit : IsUnit ((Subring.inclusion ⋯) ⟨a, h_a_inR⟩)
⊢ IsUnit ⟨a, h_a_inR⟩

Tactic:
apply (IsLocalization.AtPrime.isUnit_to_map_iff _ M ⟨a, hS.le h_a_inR⟩).mp at h_fa_isUnit

Result:
case mk
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) ≤ M
fSₘ : LocalSubring K := ofPrime S M
a : K
h_a_inR : a ∈ R.toSubring
h_fa_isUnit : ⟨a, ⋯⟩ ∈ M.primeCompl
⊢ IsUnit ⟨a, h_a_inR⟩

Proof state:
case intro.intro
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) ≤ M
fSₘ : LocalSubring K := ofPrime S M
h_RleSₘ : R ≤ fSₘ
⊢ False

Tactic:
have h_RneSₘ : R ≠ fSₘ :=
  fun e ↦ (hS.trans_le (LocalSubring.le_ofPrime S M)).ne congr(($e).toSubring)

Result:
case intro.intro
K : Type u_3
inst✝ : Field K
R : LocalSubring K
hR : IsMax R
S : Subring K
hS : R.toSubring < S
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) = ⊤
M : Ideal ↥S
h_is_max : M.IsMaximal
h_incl : Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) ≤ M
fSₘ : LocalSubring K := ofPrime S M
h_RleSₘ : R ≤ fSₘ
h_RneSₘ : R ≠ fSₘ
⊢ False