-- 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:
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
h : ¬IsUnit ⟨a, h_a_inR⟩
⊢ False

Tactic:
rw [← mem_nonunits_iff, ← mem_maximalIdeal] at h

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
h : ⟨a, h_a_inR⟩ ∈ maximalIdeal ↥R.toSubring
⊢ 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 : ⟨a, ⋯⟩ ∈ M.primeCompl
h : (Subring.inclusion ⋯) ⟨a, h_a_inR⟩ ∈ Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
⊢ False

Tactic:
exact h_fa_isUnit (h_incl h)

Result:
no goals

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ₘ
h_RneSₘ : R ≠ fSₘ
⊢ False

Tactic:
exact h_RneSₘ (hR.eq_of_le h_RleSₘ)

Result:
no goals

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
⊢ R ≤ fSₘ

Tactic:
refine ⟨hS.le.trans (LocalSubring.le_ofPrime _ _), ⟨?_⟩⟩

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) = ⊤
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

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 : ⟨a, ⋯⟩ ∈ M.primeCompl
h : ⟨a, h_a_inR⟩ ∈ maximalIdeal ↥R.toSubring
⊢ False

Tactic:
apply Ideal.mem_map_of_mem (Subring.inclusion hS.le) at h

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
h : (Subring.inclusion ⋯) ⟨a, h_a_inR⟩ ∈ 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
mR : Ideal ↥S := Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring)
h_is_not_top : ¬Ideal.map (Subring.inclusion ⋯) (maximalIdeal ↥R.toSubring) = ⊤
⊢ False

Tactic:
obtain ⟨M, h_is_max, h_incl⟩ := Ideal.exists_le_maximal _ h_is_not_top

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
⊢ False

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
⊢ False

Tactic:
have h_RleSₘ : R ≤ fSₘ := by
  refine ⟨hS.le.trans (LocalSubring.le_ofPrime _ _), ⟨?_⟩⟩
  rintro ⟨a, h_a_inR⟩ h_fa_isUnit
  apply (IsLocalization.AtPrime.isUnit_to_map_iff _ M ⟨a, hS.le h_a_inR⟩).mp at h_fa_isUnit
  by_contra h
  rw [← mem_nonunits_iff, ← mem_maximalIdeal] at h
  apply Ideal.mem_map_of_mem (Subring.inclusion hS.le) at h
  exact h_fa_isUnit (h_incl h)

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ₘ
⊢ 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 : ⟨a, ⋯⟩ ∈ M.primeCompl
⊢ IsUnit ⟨a, h_a_inR⟩

Tactic:
by_contra h

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
h : ¬IsUnit ⟨a, h_a_inR⟩
⊢ False