-- Mathlib/AlgebraicGeometry/Modules/Tilde.lean
theorem localizationToStalk_mk (x : PrimeSpectrum.Top R) (f : M) (s : x.asIdeal.primeCompl) :
    (localizationToStalk M x).hom (LocalizedModule.mk f s) =
      (tildeInModuleCat M).germ (PrimeSpectrum.basicOpen (s : R)) x s.2
        (const M f s (PrimeSpectrum.basicOpen s) fun _ => id) :=
  (Module.End_isUnit_iff _ |>.1 (isUnit_toStalk M x s)).injective <| by
  erw [← LinearMap.mul_apply]
  simp only [IsUnit.mul_val_inv, LinearMap.one_apply, Module.algebraMap_end_apply]
  show (M.tildeInModuleCat.germ ⊤ x ⟨⟩) ((toOpen M ⊤) f) = _
  rw [← map_smul]
  fapply TopCat.Presheaf.germ_ext (W := PrimeSpectrum.basicOpen s.1) (hxW := s.2)
    (F := M.tildeInModuleCat)
  · exact homOfLE le_top
  · exact 𝟙 _
  refine Subtype.eq <| funext fun y => show LocalizedModule.mk f 1 = _ from ?_
  #adaptation_note /-- https://github.com/leanprover/lean4/pull/6024
    added this refine hack to be able to add type hint in `change` -/
  refine (?_ : @Eq ?ty _ _)
  change LocalizedModule.mk f 1 = (s.1 • LocalizedModule.mk f _ : ?ty)
  rw [LocalizedModule.smul'_mk, LocalizedModule.mk_eq]
  exact ⟨1, by simp⟩

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
⊢ ((algebraMap R (Module.End R ↑(M.tildeInModuleCat.stalk x))) ↑s)
      ((Hom.hom (localizationToStalk M x)) (LocalizedModule.mk f s)) =
    ((algebraMap R (Module.End R ↑(M.tildeInModuleCat.stalk x))) ↑s)
      ((ConcreteCategory.hom (M.tildeInModuleCat.germ (PrimeSpectrum.basicOpen ↑s) x ⋯))
        (const M f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯))

Tactic:
erw [← LinearMap.mul_apply]

Result:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
⊢ ((algebraMap R (Module.End R ↑(M.tildeInModuleCat.stalk x))) ↑s * ↑⋯.unit⁻¹) ((Hom.hom (toStalk M x)) (f, s).1) =
    ((algebraMap R (Module.End R ↑(M.tildeInModuleCat.stalk x))) ↑s)
      ((ConcreteCategory.hom (M.tildeInModuleCat.germ (PrimeSpectrum.basicOpen ↑s) x ⋯))
        (const M f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯))

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
⊢ ((algebraMap R (Module.End R ↑(M.tildeInModuleCat.stalk x))) ↑s * ↑⋯.unit⁻¹) ((Hom.hom (toStalk M x)) (f, s).1) =
    ((algebraMap R (Module.End R ↑(M.tildeInModuleCat.stalk x))) ↑s)
      ((ConcreteCategory.hom (M.tildeInModuleCat.germ (PrimeSpectrum.basicOpen ↑s) x ⋯))
        (const M f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯))

Tactic:
simp only [IsUnit.mul_val_inv, LinearMap.one_apply, Module.algebraMap_end_apply]

Result:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
⊢ (Hom.hom (toStalk M x)) f =
    ↑s •
      (ConcreteCategory.hom (M.tildeInModuleCat.germ (PrimeSpectrum.basicOpen ↑s) x ⋯))
        (const M f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯)

Proof state:
case ih
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
y : ↥(unop (op (PrimeSpectrum.basicOpen ↑s)))
⊢ ∃ u, u • ⟨↑s, ⋯⟩ • f = u • 1 • ↑s • f

Tactic:
exact ⟨1, by simp⟩

Result:
no goals

Proof state:
case ih
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
y : ↥(unop (op (PrimeSpectrum.basicOpen ↑s)))
⊢ LocalizedModule.mk f 1 = ↑s • LocalizedModule.mk f ⟨↑s, ⋯⟩

Tactic:
rw [LocalizedModule.smul'_mk, LocalizedModule.mk_eq]

Result:
case ih
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
y : ↥(unop (op (PrimeSpectrum.basicOpen ↑s)))
⊢ ∃ u, u • ⟨↑s, ⋯⟩ • f = u • 1 • ↑s • f

Proof state:
case ih
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
⊢ (ConcreteCategory.hom (M.tildeInModuleCat.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (toOpen M ⊤)) f) =
    (ConcreteCategory.hom (M.tildeInModuleCat.map (𝟙 (PrimeSpectrum.basicOpen ↑s)).op))
      (↑s • const M f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯)

Tactic:
refine Subtype.eq <| funext fun y => show LocalizedModule.mk f 1 = _ from ?_

Result:
case ih
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
y : ↥(unop (op (PrimeSpectrum.basicOpen ↑s)))
⊢ LocalizedModule.mk f 1 =
    ↑((ConcreteCategory.hom (M.tildeInModuleCat.map (𝟙 (PrimeSpectrum.basicOpen ↑s)).op))
          (↑s • const M f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯))
      y

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
⊢ (ConcreteCategory.hom (M.tildeInModuleCat.germ ⊤ x True.intro)) ((ConcreteCategory.hom (toOpen M ⊤)) f) =
    ↑s •
      (ConcreteCategory.hom (M.tildeInModuleCat.germ (PrimeSpectrum.basicOpen ↑s) x ⋯))
        (const M f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯)

Tactic:
rw [← map_smul]

Result:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
⊢ (ConcreteCategory.hom (M.tildeInModuleCat.germ ⊤ x True.intro)) ((ConcreteCategory.hom (toOpen M ⊤)) f) =
    (ConcreteCategory.hom (M.tildeInModuleCat.germ (PrimeSpectrum.basicOpen ↑s) x ⋯))
      (↑s • const M f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯)

Proof state:
case ih
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
y : ↥(unop (op (PrimeSpectrum.basicOpen ↑s)))
⊢ LocalizedModule.mk f 1 =
    ↑((ConcreteCategory.hom (M.tildeInModuleCat.map (𝟙 (PrimeSpectrum.basicOpen ↑s)).op))
          (↑s • const M f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯))
      y

Tactic:
change LocalizedModule.mk f 1 = (s.1 • LocalizedModule.mk f _ : ?ty)

Result:
case ih
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
y : ↥(unop (op (PrimeSpectrum.basicOpen ↑s)))
⊢ LocalizedModule.mk f 1 = ↑s • LocalizedModule.mk f ⟨↑s, ⋯⟩

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
⊢ (ConcreteCategory.hom (M.tildeInModuleCat.germ ⊤ x True.intro)) ((ConcreteCategory.hom (toOpen M ⊤)) f) =
    (ConcreteCategory.hom (M.tildeInModuleCat.germ (PrimeSpectrum.basicOpen ↑s) x ⋯))
      (↑s • const M f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯)

Tactic:
fapply TopCat.Presheaf.germ_ext (W := PrimeSpectrum.basicOpen s.1) (hxW := s.2)
  (F := M.tildeInModuleCat)

Result:
case iWU
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
⊢ PrimeSpectrum.basicOpen ↑s ⟶ ⊤

case iWV
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
⊢ PrimeSpectrum.basicOpen ↑s ⟶ PrimeSpectrum.basicOpen ↑s

case ih
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
⊢ (ConcreteCategory.hom (M.tildeInModuleCat.map (Quiver.Hom.op ?iWU))) ((ConcreteCategory.hom (toOpen M ⊤)) f) =
    (ConcreteCategory.hom (M.tildeInModuleCat.map (Quiver.Hom.op ?iWV)))
      (↑s • const M f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯)

Proof state:
case iWV
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
⊢ PrimeSpectrum.basicOpen ↑s ⟶ PrimeSpectrum.basicOpen ↑s

Tactic:
exact 𝟙 _

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
x : ↑(PrimeSpectrum.Top R)
f : ↑M
s : ↥x.asIdeal.primeCompl
y : ↥(unop (op (PrimeSpectrum.basicOpen ↑s)))
⊢ 1 • ⟨↑s, ⋯⟩ • f = 1 • 1 • ↑s • f

Tactic:
simp

Result:
no goals