-- Mathlib/RingTheory/SurjectiveOnStalks.lean
lemma surjectiveOnStalks_iff_of_isLocalHom [IsLocalRing S] [IsLocalHom f] :
    f.SurjectiveOnStalks ↔ Function.Surjective f

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
H : f.SurjectiveOnStalks
x : S
⊢ ∃ a, f a = x

Tactic:
obtain ⟨y, r, c, hc, hr, e⟩ :=
  (surjective_localRingHom_iff _).mp (H (IsLocalRing.maximalIdeal _) inferInstance) x

Result:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
hc : c ∉ IsLocalRing.maximalIdeal S
hr : f r ∉ IsLocalRing.maximalIdeal S
e : c * f r * x = c * f y
⊢ ∃ a, f a = x

Proof state:
case intro.intro.intro.intro.intro.a
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
e : c * f r * x = c * f y
hc : IsUnit c
hr : IsUnit (f r)
⊢ (fun x => f r * x) (f (↑⋯.unit⁻¹ * y)) = (fun x => f r * x) x

Tactic:
apply hc.mul_right_injective

Result:
case intro.intro.intro.intro.intro.a.a
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
e : c * f r * x = c * f y
hc : IsUnit c
hr : IsUnit (f r)
⊢ (fun x => c * x) ((fun x => f r * x) (f (↑⋯.unit⁻¹ * y))) = (fun x => c * x) ((fun x => f r * x) x)

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
⊢ f.SurjectiveOnStalks ↔ Function.Surjective ⇑f

Tactic:
refine ⟨fun H x ↦ ?_, fun h ↦ surjectiveOnStalks_of_surjective h⟩

Result:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
H : f.SurjectiveOnStalks
x : S
⊢ ∃ a, f a = x

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
hc : c ∉ IsLocalRing.maximalIdeal S
hr : f r ∉ IsLocalRing.maximalIdeal S
e : c * f r * x = c * f y
⊢ ∃ a, f a = x

Tactic:
simp only [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, not_not] at hc hr

Result:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
e : c * f r * x = c * f y
hc : IsUnit c
hr : IsUnit (f r)
⊢ ∃ a, f a = x

Proof state:
case intro.intro.intro.intro.intro.a.a
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
e : c * f r * x = c * f y
hc : IsUnit c
hr : IsUnit (f r)
⊢ (fun x => c * x) ((fun x => f r * x) (f (↑⋯.unit⁻¹ * y))) = (fun x => c * x) ((fun x => f r * x) x)

Tactic:
simp only [← _root_.map_mul, ← mul_assoc, IsUnit.mul_val_inv, one_mul, e]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
e : c * f r * x = c * f y
hc : IsUnit c
hr : IsUnit (f r)
⊢ ∃ a, f a = x

Tactic:
refine ⟨(isUnit_of_map_unit f r hr).unit⁻¹ * y, ?_⟩

Result:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
e : c * f r * x = c * f y
hc : IsUnit c
hr : IsUnit (f r)
⊢ f (↑⋯.unit⁻¹ * y) = x

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
e : c * f r * x = c * f y
hc : IsUnit c
hr : IsUnit (f r)
⊢ f (↑⋯.unit⁻¹ * y) = x

Tactic:
apply hr.mul_right_injective

Result:
case intro.intro.intro.intro.intro.a
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
f : R →+* S
inst✝¹ : IsLocalRing S
inst✝ : IsLocalHom f
H : f.SurjectiveOnStalks
x : S
y r : R
c : S
e : c * f r * x = c * f y
hc : IsUnit c
hr : IsUnit (f r)
⊢ (fun x => f r * x) (f (↑⋯.unit⁻¹ * y)) = (fun x => f r * x) x