-- 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
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
⊢ ∃ a' h' iDh',
    U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h' i) ∧
      (∀ i ∈ t, ∀ j ∈ t, a' i * h' j = h' i * a' j) ∧
        ∀ i ∈ t,
          (ConcreteCategory.hom ((structureSheaf R).val.map (iDh' i).op)) s =
            const R (a' i) (h' i) (PrimeSpectrum.basicOpen (h' i)) ⋯

Tactic:
have basic_opens_eq : ∀ i : ι, PrimeSpectrum.basicOpen (h i ^ (N + 1)) =
  PrimeSpectrum.basicOpen (h i) := fun i => PrimeSpectrum.basicOpen_pow _ _ (by omega)

Result:
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)
⊢ ∃ a' h' iDh',
    U ≤ ⨆ i ∈ t, PrimeSpectrum.basicOpen (h' i) ∧
      (∀ i ∈ t, ∀ j ∈ t, a' i * h' j = h' i * a' j) ∧
        ∀ i ∈ t,
          (ConcreteCategory.hom ((structureSheaf R).val.map (iDh' i).op)) s =
            const R (a' i) (h' i) (PrimeSpectrum.basicOpen (h' i)) ⋯

Proof state:
case refine_2
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 ∈ t,
    ∀ j ∈ t,
      (fun i => a i * h i ^ N) i * (fun i => h i ^ (N + 1)) j = (fun i => h i ^ (N + 1)) i * (fun i => a i * h i ^ N) j

Tactic:
intro i hi j hj

Result:
case refine_2
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
⊢ (fun i => a i * h i ^ N) i * (fun i => h i ^ (N + 1)) j = (fun i => h i ^ (N + 1)) i * (fun i => a i * h i ^ N) j

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 + 1) = a i * h i ^ N * h i

Tactic:
rw [pow_succ]

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