-- 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
st : ↑(M.tildeInModuleCat.stalk x)
⊢ ∃ a, ((algebraMap R (Module.End R ↑(M.tildeInModuleCat.stalk x))) ↑r) a = st

Tactic:
obtain ⟨U, mem, s, rfl⟩ := germ_exist (F := M.tildeInModuleCat) x st

Result:
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))
⊢ ∃ a,
    ((algebraMap R (Module.End R ↑(M.tildeInModuleCat.stalk x))) ↑r) a =
      (ConcreteCategory.hom (M.tildeInModuleCat.germ U x mem)) s

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
⊢ ((algebraMap R (Module.End R ↑(M.tildeInModuleCat.stalk x))) ↑r)
      ((ConcreteCategory.hom (M.tildeInModuleCat.germ O x ⋯)) ⟨fun q => Localization.mk 1 ⟨↑r, ⋯⟩ • ↑s ⟨↑q, ⋯⟩, ⋯⟩) =
    (ConcreteCategory.hom (M.tildeInModuleCat.germ U x mem)) s

Tactic:
simpa only [Module.algebraMap_end_apply, ← map_smul] using
  germ_ext (C := ModuleCat R) (W := O) (hxW := ⟨mem, r.2⟩) (iWU := 𝟙 _)
    (iWV := homOfLE inf_le_left) _ <|
  Subtype.eq <| funext fun y ↦ smul_eq_iff_of_mem (S := y.1.1.primeCompl) r _ _ _ |>.2 rfl

Result:
no goals

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
⊢ ∃ V,
    ∃ (_ : ↑q ∈ V),
      ∃ i, (isFractionPrelocal M).pred fun x_2 => (fun q => Localization.mk 1 ⟨↑r, ⋯⟩ • ↑s ⟨↑q, ⋯⟩) (i x_2)

Tactic:
refine ⟨V ⊓ O, ⟨mem_V, q.2⟩, homOfLE inf_le_right, num, r * den, fun y ↦ ?_⟩

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

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))
⊢ ∃ a,
    ((algebraMap R (Module.End R ↑(M.tildeInModuleCat.stalk x))) ↑r) a =
      (ConcreteCategory.hom (M.tildeInModuleCat.germ U x mem)) s

Tactic:
let O := U ⊓ (PrimeSpectrum.basicOpen r)

Result:
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
⊢ ∃ a,
    ((algebraMap R (Module.End R ↑(M.tildeInModuleCat.stalk x))) ↑r) a =
      (ConcreteCategory.hom (M.tildeInModuleCat.germ U x mem)) s

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
⊢ ∃ a,
    ((algebraMap R (Module.End R ↑(M.tildeInModuleCat.stalk x))) ↑r) a =
      (ConcreteCategory.hom (M.tildeInModuleCat.germ U x mem)) s

Tactic:
refine ⟨germ M.tildeInModuleCat O x ⟨mem, r.2⟩
  ⟨fun q ↦ (Localization.mk 1 ⟨r, q.2.2⟩ : Localization.AtPrime q.1.asIdeal) • s.1
    ⟨q.1, q.2.1⟩, fun q ↦ ?_⟩, by
      simpa only [Module.algebraMap_end_apply, ← map_smul] using
        germ_ext (C := ModuleCat R) (W := O) (hxW := ⟨mem, r.2⟩) (iWU := 𝟙 _)
          (iWV := homOfLE inf_le_left) _ <|
        Subtype.eq <| funext fun y ↦ smul_eq_iff_of_mem (S := y.1.1.primeCompl) r _ _ _ |>.2 rfl⟩

Result:
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)

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 : ↑s ⟨↑y, ⋯⟩ = LocalizedModule.mk num ⟨den, h1⟩
⊢ (↑r * den) • Localization.mk 1 ⟨↑r, ⋯⟩ • ↑s ⟨↑y, ⋯⟩ = LocalizedModule.mk num 1

Tactic:
simpa only [h2, mk_smul_mk, one_smul, smul'_mk, mk_eq] using ⟨1, by simp only [one_smul]; rfl⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
r : ↥x.asIdeal.primeCompl
⊢ IsUnit ((algebraMap R (Module.End R ↑(M.tildeInModuleCat.stalk x))) ↑r)

Tactic:
rw [Module.End_isUnit_iff]

Result:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
r : ↥x.asIdeal.primeCompl
⊢ Function.Bijective ⇑((algebraMap R (Module.End R ↑(M.tildeInModuleCat.stalk x))) ↑r)

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
r : ↥x.asIdeal.primeCompl
⊢ Function.Bijective ⇑((algebraMap R (Module.End R ↑(M.tildeInModuleCat.stalk x))) ↑r)

Tactic:
refine ⟨LinearMap.ker_eq_bot.1 <| eq_bot_iff.2 fun st (h : r.1 • st = 0) ↦
  smul_stalk_no_nonzero_divisor M r st h, fun st ↦ ?_⟩

Result:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
r : ↥x.asIdeal.primeCompl
st : ↑(M.tildeInModuleCat.stalk x)
⊢ ∃ a, ((algebraMap R (Module.End R ↑(M.tildeInModuleCat.stalk x))) ↑r) a = st

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⟩
⊢ (↑r * den) • num = (⟨↑r, ⋯⟩ * ⟨den, h1⟩) • num

Tactic:
rfl

Result:
no goals