-- Mathlib/RingTheory/Valuation/LocalSubring.lean
lemma bijective_rangeRestrict_comp_of_valuationRing [IsDomain R] [ValuationRing R]
    [IsLocalRing S] [Algebra R K] [IsFractionRing R K]
    (f : R →+* S) (g : S →+* K) (h : g.comp f = algebraMap R K) [IsLocalHom f] :
    Function.Bijective (g.rangeRestrict.comp f)

Proof state:
case refine_2.a.mk.intro
R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
V : ValuationSubring K := { toSubring := (algebraMap R K).range, mem_or_inv_mem' := ⋯ }
H : (algebraMap R K).range ≤ g.range
a : R
ha : IsUnit ⟨(algebraMap R K) a, ⋯⟩
⊢ IsUnit ⟨(algebraMap R K) a, ⋯⟩

Tactic:
suffices IsUnit a from this.map (algebraMap R K).rangeRestrict

Result:
case refine_2.a.mk.intro
R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
V : ValuationSubring K := { toSubring := (algebraMap R K).range, mem_or_inv_mem' := ⋯ }
H : (algebraMap R K).range ≤ g.range
a : R
ha : IsUnit ⟨(algebraMap R K) a, ⋯⟩
⊢ IsUnit a

Proof state:
case h.e'_3
R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
⊢ Subtype.val ∘ ⇑(g.rangeRestrict.comp f) = ⇑(g.comp f)

Tactic:
rfl

Result:
no goals

Proof state:
case refine_2
R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
V : ValuationSubring K := { toSubring := (algebraMap R K).range, mem_or_inv_mem' := ⋯ }
⊢ LocalSubring.range g ≤ V.toLocalSubring

Tactic:
apply V.isMax_toLocalSubring

Result:
case refine_2.a
R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
V : ValuationSubring K := { toSubring := (algebraMap R K).range, mem_or_inv_mem' := ⋯ }
⊢ V.toLocalSubring ≤ LocalSubring.range g

Proof state:
case refine_2
R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
V : ValuationSubring K := { toSubring := (algebraMap R K).range, mem_or_inv_mem' := ⋯ }
⊢ Function.Surjective ⇑(g.rangeRestrict.comp f)

Tactic:
suffices LocalSubring.range g ≤ V.toLocalSubring by
  rintro ⟨_, x, rfl⟩
  obtain ⟨y, hy⟩ := this.1 ⟨x, rfl⟩
  exact ⟨y, Subtype.ext (by simpa [← h] using hy)⟩

Result:
case refine_2
R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
V : ValuationSubring K := { toSubring := (algebraMap R K).range, mem_or_inv_mem' := ⋯ }
⊢ LocalSubring.range g ≤ V.toLocalSubring

Proof state:
R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
⊢ Function.Bijective ⇑(g.rangeRestrict.comp f)

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
⊢ Function.Injective ⇑(g.rangeRestrict.comp f)

case refine_2
R : Type u_1
S : Type u_2
K : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : ValuationRing R
inst✝³ : IsLocalRing S
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
f : R →+* S
g : S →+* K
h : g.comp f = algebraMap R K
inst✝ : IsLocalHom f
⊢ Function.Surjective ⇑(g.rangeRestrict.comp f)