-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem normalize_finite_fraction_representation (U : Opens (PrimeSpectrum.Top R))
    (s : (structureSheaf R).1.obj (op U)) {ι : Type*} (t : Finset ι) (a h : ι → R)
    (iDh : ∀ i : ι, PrimeSpectrum.basicOpen (h i) ⟶ U)
    (h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i))
    (hs :
      ∀ i : ι,
        (const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) fun _ hy => hy) =
          (structureSheaf R).1.map (iDh i).op s) :
    ∃ (a' h' : ι → R) (iDh' : ∀ i : ι, PrimeSpectrum.basicOpen (h' i) ⟶ U),
      (U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h' i)) ∧
        (∀ (i) (_ : i ∈ t) (j) (_ : j ∈ t), a' i * h' j = h' i * a' j) ∧
          ∀ i ∈ t,
            (structureSheaf R).1.map (iDh' i).op s =
              const R (a' i) (h' i) (PrimeSpectrum.basicOpen (h' i)) fun _ hy => hy

Proof state:
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
ι : Type u_1
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U
h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)
hs :
  ∀ (i : ι),
    const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ =
      (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s
i j : ι
D : Opens (PrimeSpectrum R) := PrimeSpectrum.basicOpen (h i * h j)
iDi : D ⟶ PrimeSpectrum.basicOpen (h i) := homOfLE ⋯
iDj : D ⟶ PrimeSpectrum.basicOpen (h j) := homOfLE ⋯
⊢ const R (a j) (h j) D ?hv = const R (h i * a j) (h i * h j) (PrimeSpectrum.basicOpen (h i * h j)) ⋯

case hv
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
ι : Type u_1
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U
h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)
hs :
  ∀ (i : ι),
    const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ =
      (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s
i j : ι
D : Opens (PrimeSpectrum R) := PrimeSpectrum.basicOpen (h i * h j)
iDi : D ⟶ PrimeSpectrum.basicOpen (h i) := homOfLE ⋯
iDj : D ⟶ PrimeSpectrum.basicOpen (h j) := homOfLE ⋯
⊢ ∀ x ∈ D, h j ∈ x.asIdeal.primeCompl

Tactic:
apply const_ext

Result:
case h
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
ι : Type u_1
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U
h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)
hs :
  ∀ (i : ι),
    const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ =
      (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s
i j : ι
D : Opens (PrimeSpectrum R) := PrimeSpectrum.basicOpen (h i * h j)
iDi : D ⟶ PrimeSpectrum.basicOpen (h i) := homOfLE ⋯
iDj : D ⟶ PrimeSpectrum.basicOpen (h j) := homOfLE ⋯
⊢ a j * (h i * h j) = h i * a j * h j

case hv
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
ι : Type u_1
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U
h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)
hs :
  ∀ (i : ι),
    const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ =
      (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s
i j : ι
D : Opens (PrimeSpectrum R) := PrimeSpectrum.basicOpen (h i * h j)
iDi : D ⟶ PrimeSpectrum.basicOpen (h i) := homOfLE ⋯
iDj : D ⟶ PrimeSpectrum.basicOpen (h j) := homOfLE ⋯
⊢ ∀ x ∈ D, h j ∈ x.asIdeal.primeCompl

Proof state:
case h.e'_3
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
ι : Type u_1
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U
h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)
hs :
  ∀ (i : ι),
    const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ =
      (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s
fractions_eq :
  ∀ (i j : ι),
    IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩ =
      IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩
exists_power : ∀ (i j : ι), ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n
n : ι × ι → ℕ := fun p => ⋯.choose
n_spec : ∀ (p : ι × ι), a p.1 * h p.2 * (h p.1 * h p.2) ^ ⋯.choose = h p.1 * a p.2 * (h p.1 * h p.2) ^ ⋯.choose
N : ℕ := (t ×ˢ t).sup n
basic_opens_eq : ∀ (i : ι), PrimeSpectrum.basicOpen (h i ^ (N + 1)) = PrimeSpectrum.basicOpen (h i)
i : ι
hi : i ∈ t
j : ι
hj : j ∈ t
n_le_N : n (i, j) ≤ N
k : ℕ
hk : n (i, j) + k = N
⊢ h i ^ ⋯.choose * h i ^ k * h i * (a j * (h j ^ ⋯.choose * h j ^ k)) =
    h i * a j * (h i ^ ⋯.choose * h j ^ ⋯.choose) * (h i ^ k * h j ^ k)

Tactic:
ring

Result:
no goals

Proof state:
case refine_3.h
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
ι : Type u_1
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U
h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)
hs :
  ∀ (i : ι),
    const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ =
      (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s
fractions_eq :
  ∀ (i j : ι),
    IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩ =
      IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩
exists_power : ∀ (i j : ι), ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n
n : ι × ι → ℕ := fun p => ⋯.choose
n_spec : ∀ (p : ι × ι), a p.1 * h p.2 * (h p.1 * h p.2) ^ ⋯.choose = h p.1 * a p.2 * (h p.1 * h p.2) ^ ⋯.choose
N : ℕ := (t ×ˢ t).sup n
basic_opens_eq : ∀ (i : ι), PrimeSpectrum.basicOpen (h i ^ (N + 1)) = PrimeSpectrum.basicOpen (h i)
i : ι
a✝ : i ∈ t
⊢ a i * (h i ^ N * h i) = a i * h i ^ N * h i

Tactic:
ring

Result:
no goals

Proof state:
case h
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
ι : Type u_1
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U
h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)
hs :
  ∀ (i : ι),
    const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ =
      (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s
i j : ι
D : Opens (PrimeSpectrum R) := PrimeSpectrum.basicOpen (h i * h j)
iDi : D ⟶ PrimeSpectrum.basicOpen (h i) := homOfLE ⋯
iDj : D ⟶ PrimeSpectrum.basicOpen (h j) := homOfLE ⋯
⊢ a j * (h i * h j) = h i * a j * h j

case hv
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
ι : Type u_1
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U
h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)
hs :
  ∀ (i : ι),
    const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ =
      (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s
i j : ι
D : Opens (PrimeSpectrum R) := PrimeSpectrum.basicOpen (h i * h j)
iDi : D ⟶ PrimeSpectrum.basicOpen (h i) := homOfLE ⋯
iDj : D ⟶ PrimeSpectrum.basicOpen (h j) := homOfLE ⋯
⊢ ∀ x ∈ D, h j ∈ x.asIdeal.primeCompl

Tactic:
ring

Result:
case hv
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
s : ↑((structureSheaf R).val.obj (op U))
ι : Type u_1
t : Finset ι
a h : ι → R
iDh : (i : ι) → PrimeSpectrum.basicOpen (h i) ⟶ U
h_cover : U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h i)
hs :
  ∀ (i : ι),
    const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯ =
      (ConcreteCategory.hom ((structureSheaf R).val.map (iDh i).op)) s
i j : ι
D : Opens (PrimeSpectrum R) := PrimeSpectrum.basicOpen (h i * h j)
iDi : D ⟶ PrimeSpectrum.basicOpen (h i) := homOfLE ⋯
iDj : D ⟶ PrimeSpectrum.basicOpen (h j) := homOfLE ⋯
⊢ ∀ x ∈ D, h j ∈ x.asIdeal.primeCompl