-- Mathlib/AlgebraicGeometry/Modules/Tilde.lean
lemma isUnit_toStalk (x : PrimeSpectrum.Top R) (r : x.asIdeal.primeCompl) :
    IsUnit ((algebraMap R (Module.End R ((tildeInModuleCat M).stalk x))) r)

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
r : ↥x.asIdeal.primeCompl
U : Opens ↑(PrimeSpectrum.Top R)
mem : x ∈ U
s : ToType (M.tildeInModuleCat.obj (op U))
O : Opens ↑(PrimeSpectrum.Top R) := U ⊓ PrimeSpectrum.basicOpen ↑r
q : ↥(unop (op O))
V : Opens ↑(PrimeSpectrum.Top R)
mem_V : ↑⟨↑q, ⋯⟩ ∈ V
iV : V ⟶ unop (op U)
num : ↑M
den : R
hV : ∀ (x : ↥V), den ∉ (↑x).asIdeal ∧ den • (fun x => ↑s (iV x)) x = (mkLinearMap (↑x).asIdeal.primeCompl ↑M) num
y : ↥(V ⊓ O)
h1 : den ∉ (↑⟨↑y, ⋯⟩).asIdeal
h2 : ↑s ⟨↑y, ⋯⟩ = LocalizedModule.mk num ⟨den, h1⟩
⊢ 1 • (↑r * den) • num = 1 • (⟨↑r, ⋯⟩ * ⟨den, h1⟩) • num

Tactic:
simp only [one_smul]

Result:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
r : ↥x.asIdeal.primeCompl
U : Opens ↑(PrimeSpectrum.Top R)
mem : x ∈ U
s : ToType (M.tildeInModuleCat.obj (op U))
O : Opens ↑(PrimeSpectrum.Top R) := U ⊓ PrimeSpectrum.basicOpen ↑r
q : ↥(unop (op O))
V : Opens ↑(PrimeSpectrum.Top R)
mem_V : ↑⟨↑q, ⋯⟩ ∈ V
iV : V ⟶ unop (op U)
num : ↑M
den : R
hV : ∀ (x : ↥V), den ∉ (↑x).asIdeal ∧ den • (fun x => ↑s (iV x)) x = (mkLinearMap (↑x).asIdeal.primeCompl ↑M) num
y : ↥(V ⊓ O)
h1 : den ∉ (↑⟨↑y, ⋯⟩).asIdeal
h2 : ↑s ⟨↑y, ⋯⟩ = LocalizedModule.mk num ⟨den, h1⟩
⊢ (↑r * den) • num = (⟨↑r, ⋯⟩ * ⟨den, h1⟩) • num

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
r : ↥x.asIdeal.primeCompl
U : Opens ↑(PrimeSpectrum.Top R)
mem : x ∈ U
s : ToType (M.tildeInModuleCat.obj (op U))
O : Opens ↑(PrimeSpectrum.Top R) := U ⊓ PrimeSpectrum.basicOpen ↑r
q : ↥(unop (op O))
V : Opens ↑(PrimeSpectrum.Top R)
mem_V : ↑⟨↑q, ⋯⟩ ∈ V
iV : V ⟶ unop (op U)
num : ↑M
den : R
hV : ∀ (x : ↥V), den ∉ (↑x).asIdeal ∧ den • (fun x => ↑s (iV x)) x = (mkLinearMap (↑x).asIdeal.primeCompl ↑M) num
y : ↥(V ⊓ O)
h1 : den ∉ (↑⟨↑y, ⋯⟩).asIdeal
h2 : den • (fun x => ↑s (iV x)) ⟨↑y, ⋯⟩ = (mkLinearMap (↑⟨↑y, ⋯⟩).asIdeal.primeCompl ↑M) num
⊢ ↑r * den ∉ (↑y).asIdeal ∧
    (↑r * den) • (fun x_1 => (fun q => Localization.mk 1 ⟨↑r, ⋯⟩ • ↑s ⟨↑q, ⋯⟩) ((homOfLE ⋯) x_1)) y =
      (mkLinearMap (↑y).asIdeal.primeCompl ↑M) num

Tactic:
refine ⟨y.1.asIdeal.primeCompl.mul_mem y.2.2.2 h1, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
r : ↥x.asIdeal.primeCompl
U : Opens ↑(PrimeSpectrum.Top R)
mem : x ∈ U
s : ToType (M.tildeInModuleCat.obj (op U))
O : Opens ↑(PrimeSpectrum.Top R) := U ⊓ PrimeSpectrum.basicOpen ↑r
q : ↥(unop (op O))
V : Opens ↑(PrimeSpectrum.Top R)
mem_V : ↑⟨↑q, ⋯⟩ ∈ V
iV : V ⟶ unop (op U)
num : ↑M
den : R
hV : ∀ (x : ↥V), den ∉ (↑x).asIdeal ∧ den • (fun x => ↑s (iV x)) x = (mkLinearMap (↑x).asIdeal.primeCompl ↑M) num
y : ↥(V ⊓ O)
h1 : den ∉ (↑⟨↑y, ⋯⟩).asIdeal
h2 : den • (fun x => ↑s (iV x)) ⟨↑y, ⋯⟩ = (mkLinearMap (↑⟨↑y, ⋯⟩).asIdeal.primeCompl ↑M) num
⊢ (↑r * den) • (fun x_1 => (fun q => Localization.mk 1 ⟨↑r, ⋯⟩ • ↑s ⟨↑q, ⋯⟩) ((homOfLE ⋯) x_1)) y =
    (mkLinearMap (↑y).asIdeal.primeCompl ↑M) num

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
r : ↥x.asIdeal.primeCompl
U : Opens ↑(PrimeSpectrum.Top R)
mem : x ∈ U
s : ToType (M.tildeInModuleCat.obj (op U))
O : Opens ↑(PrimeSpectrum.Top R) := U ⊓ PrimeSpectrum.basicOpen ↑r
q : ↥(unop (op O))
V : Opens ↑(PrimeSpectrum.Top R)
mem_V : ↑⟨↑q, ⋯⟩ ∈ V
iV : V ⟶ unop (op U)
num : ↑M
den : R
hV : ∀ (x : ↥V), den ∉ (↑x).asIdeal ∧ den • (fun x => ↑s (iV x)) x = (mkLinearMap (↑x).asIdeal.primeCompl ↑M) num
y : ↥(V ⊓ O)
⊢ ↑r * den ∉ (↑y).asIdeal ∧
    (↑r * den) • (fun x_1 => (fun q => Localization.mk 1 ⟨↑r, ⋯⟩ • ↑s ⟨↑q, ⋯⟩) ((homOfLE ⋯) x_1)) y =
      (mkLinearMap (↑y).asIdeal.primeCompl ↑M) num

Tactic:
obtain ⟨h1, h2⟩ := hV ⟨y, y.2.1⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
r : ↥x.asIdeal.primeCompl
U : Opens ↑(PrimeSpectrum.Top R)
mem : x ∈ U
s : ToType (M.tildeInModuleCat.obj (op U))
O : Opens ↑(PrimeSpectrum.Top R) := U ⊓ PrimeSpectrum.basicOpen ↑r
q : ↥(unop (op O))
V : Opens ↑(PrimeSpectrum.Top R)
mem_V : ↑⟨↑q, ⋯⟩ ∈ V
iV : V ⟶ unop (op U)
num : ↑M
den : R
hV : ∀ (x : ↥V), den ∉ (↑x).asIdeal ∧ den • (fun x => ↑s (iV x)) x = (mkLinearMap (↑x).asIdeal.primeCompl ↑M) num
y : ↥(V ⊓ O)
h1 : den ∉ (↑⟨↑y, ⋯⟩).asIdeal
h2 : den • (fun x => ↑s (iV x)) ⟨↑y, ⋯⟩ = (mkLinearMap (↑⟨↑y, ⋯⟩).asIdeal.primeCompl ↑M) num
⊢ ↑r * den ∉ (↑y).asIdeal ∧
    (↑r * den) • (fun x_1 => (fun q => Localization.mk 1 ⟨↑r, ⋯⟩ • ↑s ⟨↑q, ⋯⟩) ((homOfLE ⋯) x_1)) y =
      (mkLinearMap (↑y).asIdeal.primeCompl ↑M) num

Proof state:
case intro.intro.intro
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
r : ↥x.asIdeal.primeCompl
U : Opens ↑(PrimeSpectrum.Top R)
mem : x ∈ U
s : ToType (M.tildeInModuleCat.obj (op U))
O : Opens ↑(PrimeSpectrum.Top R) := U ⊓ PrimeSpectrum.basicOpen ↑r
q : ↥(unop (op O))
⊢ ∃ V,
    ∃ (_ : ↑q ∈ V),
      ∃ i, (isFractionPrelocal M).pred fun x_2 => (fun q => Localization.mk 1 ⟨↑r, ⋯⟩ • ↑s ⟨↑q, ⋯⟩) (i x_2)

Tactic:
obtain ⟨V, mem_V, iV, num, den, hV⟩ := s.2 ⟨q.1, q.2.1⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
r : ↥x.asIdeal.primeCompl
U : Opens ↑(PrimeSpectrum.Top R)
mem : x ∈ U
s : ToType (M.tildeInModuleCat.obj (op U))
O : Opens ↑(PrimeSpectrum.Top R) := U ⊓ PrimeSpectrum.basicOpen ↑r
q : ↥(unop (op O))
V : Opens ↑(PrimeSpectrum.Top R)
mem_V : ↑⟨↑q, ⋯⟩ ∈ V
iV : V ⟶ unop (op U)
num : ↑M
den : R
hV : ∀ (x : ↥V), den ∉ (↑x).asIdeal ∧ den • (fun x => ↑s (iV x)) x = (mkLinearMap (↑x).asIdeal.primeCompl ↑M) num
⊢ ∃ V,
    ∃ (_ : ↑q ∈ V),
      ∃ i, (isFractionPrelocal M).pred fun x_2 => (fun q => Localization.mk 1 ⟨↑r, ⋯⟩ • ↑s ⟨↑q, ⋯⟩) (i x_2)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
r : ↥x.asIdeal.primeCompl
U : Opens ↑(PrimeSpectrum.Top R)
mem : x ∈ U
s : ToType (M.tildeInModuleCat.obj (op U))
O : Opens ↑(PrimeSpectrum.Top R) := U ⊓ PrimeSpectrum.basicOpen ↑r
q : ↥(unop (op O))
V : Opens ↑(PrimeSpectrum.Top R)
mem_V : ↑⟨↑q, ⋯⟩ ∈ V
iV : V ⟶ unop (op U)
num : ↑M
den : R
hV : ∀ (x : ↥V), den ∉ (↑x).asIdeal ∧ den • (fun x => ↑s (iV x)) x = (mkLinearMap (↑x).asIdeal.primeCompl ↑M) num
y : ↥(V ⊓ O)
h1 : den ∉ (↑⟨↑y, ⋯⟩).asIdeal
h2 : den • (fun x => ↑s (iV x)) ⟨↑y, ⋯⟩ = (mkLinearMap (↑⟨↑y, ⋯⟩).asIdeal.primeCompl ↑M) num
⊢ (↑r * den) • (fun x_1 => (fun q => Localization.mk 1 ⟨↑r, ⋯⟩ • ↑s ⟨↑q, ⋯⟩) ((homOfLE ⋯) x_1)) y =
    (mkLinearMap (↑y).asIdeal.primeCompl ↑M) num

Tactic:
simp only [Opens.coe_inf, Opens.apply_def, isLocallyFraction_pred, mkLinearMap_apply,
  smul_eq_iff_of_mem (S := y.1.1.primeCompl) (hr := h1), mk_smul_mk, one_smul, mul_one] at h2 ⊢

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
r : ↥x.asIdeal.primeCompl
U : Opens ↑(PrimeSpectrum.Top R)
mem : x ∈ U
s : ToType (M.tildeInModuleCat.obj (op U))
O : Opens ↑(PrimeSpectrum.Top R) := U ⊓ PrimeSpectrum.basicOpen ↑r
q : ↥(unop (op O))
V : Opens ↑(PrimeSpectrum.Top R)
mem_V : ↑⟨↑q, ⋯⟩ ∈ V
iV : V ⟶ unop (op U)
num : ↑M
den : R
hV : ∀ (x : ↥V), den ∉ (↑x).asIdeal ∧ den • (fun x => ↑s (iV x)) x = (mkLinearMap (↑x).asIdeal.primeCompl ↑M) num
y : ↥(V ⊓ O)
h1 : den ∉ (↑⟨↑y, ⋯⟩).asIdeal
h2 : ↑s ⟨↑y, ⋯⟩ = LocalizedModule.mk num ⟨den, h1⟩
⊢ (↑r * den) • Localization.mk 1 ⟨↑r, ⋯⟩ • ↑s ⟨↑y, ⋯⟩ = LocalizedModule.mk num 1