-- Mathlib/AlgebraicGeometry/Modules/Tilde.lean
theorem exists_const (U) (s : (tildeInModuleCat M).obj (op U)) (x : PrimeSpectrum.Top R)
    (hx : x ∈ U) :
    ∃ (V : Opens (PrimeSpectrum.Top R)) (_ : x ∈ V) (i : V ⟶ U) (f : M) (g : R) (hg : _),
      const M f g V hg = (tildeInModuleCat M).map i.op s :=
  let ⟨V, hxV, iVU, f, g, hfg⟩ := s.2 ⟨x, hx⟩
  ⟨V, hxV, iVU, f, g, fun y hyV => (hfg ⟨y, hyV⟩).1, Subtype.eq <| funext fun y => by
    obtain ⟨h1, (h2 : g • s.1 ⟨y, _⟩ = LocalizedModule.mk f 1)⟩ := hfg y
    exact show LocalizedModule.mk f ⟨g, by exact h1⟩ = s.1 (iVU y) by
      set x := s.1 (iVU y); change g • x = _ at h2; clear_value x
      induction x using LocalizedModule.induction_on with
      | h a b =>
        rw [LocalizedModule.smul'_mk, LocalizedModule.mk_eq] at h2
        obtain ⟨c, hc⟩ := h2
        exact LocalizedModule.mk_eq.mpr ⟨c, by simpa using hc.symm⟩⟩

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑(M.tildeInModuleCat.obj (op U))
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : ↑M
g : R
hfg :
  ∀ (x : ↥V),
    g ∉ (↑x).asIdeal ∧ g • (fun x => ↑s (iVU x)) x = (LocalizedModule.mkLinearMap (↑x).asIdeal.primeCompl ↑M) f
y : ↥(unop (op V))
h1 : g ∉ (↑y).asIdeal
a : ↑M
b c : ↥(↑(iVU y)).asIdeal.primeCompl
hc : c • 1 • g • a = c • b • f
⊢ c • b • f = c • ⟨g, h1⟩ • a

Tactic:
simpa using hc.symm

Result:
no goals

Proof state:
case h
R : Type u
inst✝ : CommRing R
M : ModuleCat R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑(M.tildeInModuleCat.obj (op U))
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : ↑M
g : R
hfg :
  ∀ (x : ↥V),
    g ∉ (↑x).asIdeal ∧ g • (fun x => ↑s (iVU x)) x = (LocalizedModule.mkLinearMap (↑x).asIdeal.primeCompl ↑M) f
y : ↥(unop (op V))
h1 : g ∉ (↑y).asIdeal
a : ↑M
b : ↥(↑(iVU y)).asIdeal.primeCompl
h2 : g • LocalizedModule.mk a b = LocalizedModule.mk f 1
⊢ LocalizedModule.mk f ⟨g, h1⟩ = LocalizedModule.mk a b

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

Result:
case h
R : Type u
inst✝ : CommRing R
M : ModuleCat R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑(M.tildeInModuleCat.obj (op U))
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : ↑M
g : R
hfg :
  ∀ (x : ↥V),
    g ∉ (↑x).asIdeal ∧ g • (fun x => ↑s (iVU x)) x = (LocalizedModule.mkLinearMap (↑x).asIdeal.primeCompl ↑M) f
y : ↥(unop (op V))
h1 : g ∉ (↑y).asIdeal
a : ↑M
b : ↥(↑(iVU y)).asIdeal.primeCompl
h2 : ∃ u, u • 1 • g • a = u • b • f
⊢ LocalizedModule.mk f ⟨g, h1⟩ = LocalizedModule.mk a b

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑(M.tildeInModuleCat.obj (op U))
x✝ : ↑(PrimeSpectrum.Top R)
hx : x✝ ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x✝, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : ↑M
g : R
hfg :
  ∀ (x : ↥V),
    g ∉ (↑x).asIdeal ∧ g • (fun x => ↑s (iVU x)) x = (LocalizedModule.mkLinearMap (↑x).asIdeal.primeCompl ↑M) f
y : ↥(unop (op V))
h1 : g ∉ (↑y).asIdeal
x : Localizations M ↑(iVU y) := ↑s (iVU y)
h2 : g • x = LocalizedModule.mk f 1
⊢ LocalizedModule.mk f ⟨g, h1⟩ = x

Tactic:
clear_value x

Result:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑(M.tildeInModuleCat.obj (op U))
x✝ : ↑(PrimeSpectrum.Top R)
hx : x✝ ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x✝, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : ↑M
g : R
hfg :
  ∀ (x : ↥V),
    g ∉ (↑x).asIdeal ∧ g • (fun x => ↑s (iVU x)) x = (LocalizedModule.mkLinearMap (↑x).asIdeal.primeCompl ↑M) f
y : ↥(unop (op V))
h1 : g ∉ (↑y).asIdeal
x : Localizations M ↑(iVU y)
h2 : g • x = LocalizedModule.mk f 1
⊢ LocalizedModule.mk f ⟨g, h1⟩ = x

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑(M.tildeInModuleCat.obj (op U))
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : ↑M
g : R
hfg :
  ∀ (x : ↥V),
    g ∉ (↑x).asIdeal ∧ g • (fun x => ↑s (iVU x)) x = (LocalizedModule.mkLinearMap (↑x).asIdeal.primeCompl ↑M) f
y : ↥(unop (op V))
⊢ ↑(const M f g V ⋯) y = ↑((ConcreteCategory.hom (M.tildeInModuleCat.map iVU.op)) s) y

Tactic:
obtain ⟨h1, (h2 : g • s.1 ⟨y, _⟩ = LocalizedModule.mk f 1)⟩ := hfg y

Result:
case intro
R : Type u
inst✝ : CommRing R
M : ModuleCat R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑(M.tildeInModuleCat.obj (op U))
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : ↑M
g : R
hfg :
  ∀ (x : ↥V),
    g ∉ (↑x).asIdeal ∧ g • (fun x => ↑s (iVU x)) x = (LocalizedModule.mkLinearMap (↑x).asIdeal.primeCompl ↑M) f
y : ↥(unop (op V))
h1 : g ∉ (↑y).asIdeal
h2 : g • ↑s ⟨↑y, ⋯⟩ = LocalizedModule.mk f 1
⊢ ↑(const M f g V ⋯) y = ↑((ConcreteCategory.hom (M.tildeInModuleCat.map iVU.op)) s) y

Proof state:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑(M.tildeInModuleCat.obj (op U))
x✝ : ↑(PrimeSpectrum.Top R)
hx : x✝ ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x✝, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : ↑M
g : R
hfg :
  ∀ (x : ↥V),
    g ∉ (↑x).asIdeal ∧ g • (fun x => ↑s (iVU x)) x = (LocalizedModule.mkLinearMap (↑x).asIdeal.primeCompl ↑M) f
y : ↥(unop (op V))
h1 : g ∉ (↑y).asIdeal
h2 : g • ↑s ⟨↑y, ⋯⟩ = LocalizedModule.mk f 1
x : Localizations M ↑(iVU y) := ↑s (iVU y)
⊢ LocalizedModule.mk f ⟨g, h1⟩ = x

Tactic:
change g • x = _ at h2

Result:
R : Type u
inst✝ : CommRing R
M : ModuleCat R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑(M.tildeInModuleCat.obj (op U))
x✝ : ↑(PrimeSpectrum.Top R)
hx : x✝ ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x✝, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : ↑M
g : R
hfg :
  ∀ (x : ↥V),
    g ∉ (↑x).asIdeal ∧ g • (fun x => ↑s (iVU x)) x = (LocalizedModule.mkLinearMap (↑x).asIdeal.primeCompl ↑M) f
y : ↥(unop (op V))
h1 : g ∉ (↑y).asIdeal
x : Localizations M ↑(iVU y) := ↑s (iVU y)
h2 : g • x = LocalizedModule.mk f 1
⊢ LocalizedModule.mk f ⟨g, h1⟩ = x

Proof state:
case h.intro
R : Type u
inst✝ : CommRing R
M : ModuleCat R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑(M.tildeInModuleCat.obj (op U))
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : ↑M
g : R
hfg :
  ∀ (x : ↥V),
    g ∉ (↑x).asIdeal ∧ g • (fun x => ↑s (iVU x)) x = (LocalizedModule.mkLinearMap (↑x).asIdeal.primeCompl ↑M) f
y : ↥(unop (op V))
h1 : g ∉ (↑y).asIdeal
a : ↑M
b c : ↥(↑(iVU y)).asIdeal.primeCompl
hc : c • 1 • g • a = c • b • f
⊢ LocalizedModule.mk f ⟨g, h1⟩ = LocalizedModule.mk a b

Tactic:
exact LocalizedModule.mk_eq.mpr ⟨c, by simpa using hc.symm⟩

Result:
no goals

Proof state:
case intro
R : Type u
inst✝ : CommRing R
M : ModuleCat R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑(M.tildeInModuleCat.obj (op U))
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : ↑M
g : R
hfg :
  ∀ (x : ↥V),
    g ∉ (↑x).asIdeal ∧ g • (fun x => ↑s (iVU x)) x = (LocalizedModule.mkLinearMap (↑x).asIdeal.primeCompl ↑M) f
y : ↥(unop (op V))
h1 : g ∉ (↑y).asIdeal
h2 : g • ↑s ⟨↑y, ⋯⟩ = LocalizedModule.mk f 1
⊢ ↑(const M f g V ⋯) y = ↑((ConcreteCategory.hom (M.tildeInModuleCat.map iVU.op)) s) y

Tactic:
exact show LocalizedModule.mk f ⟨g, by exact h1⟩ = s.1 (iVU y) by
  set x := s.1 (iVU y); change g • x = _ at h2; clear_value x
  induction x using LocalizedModule.induction_on with
  | h a b =>
    rw [LocalizedModule.smul'_mk, LocalizedModule.mk_eq] at h2
    obtain ⟨c, hc⟩ := h2
    exact LocalizedModule.mk_eq.mpr ⟨c, by simpa using hc.symm⟩

Result:
no goals