-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem locally_const_basicOpen (U : Opens (PrimeSpectrum.Top R))
    (s : (structureSheaf R).1.obj (op U)) (x : U) :
    ∃ (f g : R) (i : PrimeSpectrum.basicOpen g ⟶ U), x.1 ∈ PrimeSpectrum.basicOpen g ∧
      (const R f g (PrimeSpectrum.basicOpen g) fun _ hy => hy) =
      (structureSheaf R).1.map i.op s

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
x : ↥U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = (ConcreteCategory.hom ((structureSheaf R).val.map iVU.op)) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheaf R).val.map i.op)) s

Tactic:
have basic_opens_eq := PrimeSpectrum.basicOpen_pow h (n + 1) (by omega)

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
x : ↥U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = (ConcreteCategory.hom ((structureSheaf R).val.map iVU.op)) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheaf R).val.map i.op)) s

Proof state:
case intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
x : ↥U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = (ConcreteCategory.hom ((structureSheaf R).val.map iVU.op)) s
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheaf R).val.map i.op)) s

Tactic:
obtain ⟨_, ⟨h, rfl⟩, hxDh, hDhV : PrimeSpectrum.basicOpen h ≤ V⟩ :=
  PrimeSpectrum.isTopologicalBasis_basic_opens.exists_subset_of_mem_open hxV V.2

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
x : ↥U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = (ConcreteCategory.hom ((structureSheaf R).val.map iVU.op)) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheaf R).val.map i.op)) s

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
x : ↥U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = (ConcreteCategory.hom ((structureSheaf R).val.map iVU.op)) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheaf R).val.map i.op)) s

Tactic:
have i_basic_open := eqToHom basic_opens_eq ≫ homOfLE hDhV

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
x : ↥U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = (ConcreteCategory.hom ((structureSheaf R).val.map iVU.op)) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheaf R).val.map i.op)) s

Proof state:
case right.h
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
x : ↥U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = (ConcreteCategory.hom ((structureSheaf R).val.map iVU.op)) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h
i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V
⊢ f * c * g = f * h ^ (n + 1)

Tactic:
rw [mul_assoc f c g, hc]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
x : ↥U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = (ConcreteCategory.hom ((structureSheaf R).val.map iVU.op)) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
hn : ∃ a, a * g = h ^ (n + 1)
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheaf R).val.map i.op)) s

Tactic:
obtain ⟨c, hc⟩ := hn

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
x : ↥U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑x ∈ V.carrier
iVU : V ⟶ U
f g : R
hVDg : V ≤ PrimeSpectrum.basicOpen g
s_eq : const R f g V hVDg = (ConcreteCategory.hom ((structureSheaf R).val.map iVU.op)) s
h : R
hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h
hDhV : PrimeSpectrum.basicOpen h ≤ V
n : ℕ
c : R
hc : c * g = h ^ (n + 1)
⊢ ∃ f g i,
    ↑x ∈ PrimeSpectrum.basicOpen g ∧
      const R f g (PrimeSpectrum.basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheaf R).val.map i.op)) s