-- 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, ⋯⟩
i j : ι
⊢ ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n

Tactic:
obtain ⟨⟨c, n, rfl⟩, hc⟩ := IsLocalization.eq.mp (fractions_eq i j)

Result:
case intro.mk.intro
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, ⋯⟩
i j : ι
n : ℕ
hc :
  ↑⟨(fun x => (h i * h j) ^ x) n, ⋯⟩ * (↑⟨h i * h j, ⋯⟩ * (a i * h j)) =
    ↑⟨(fun x => (h i * h j) ^ x) n, ⋯⟩ * (↑⟨h i * h j, ⋯⟩ * (h i * a j))
⊢ ∃ n, a i * h j * (h i * h j) ^ n = h i * a j * (h i * h j) ^ n

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
⊢ ∃ 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 fractions_eq :
  ∀ i j : ι,
    IsLocalization.mk' (Localization.Away (h i * h j))
      (a i * h j) ⟨h i * h j, Submonoid.mem_powers _⟩ =
    IsLocalization.mk' _ (h i * a j) ⟨h i * h j, Submonoid.mem_powers _⟩ := by
  intro i j
  let D := PrimeSpectrum.basicOpen (h i * h j)
  let iDi : D ⟶ PrimeSpectrum.basicOpen (h i) := homOfLE (PrimeSpectrum.basicOpen_mul_le_left _ _)
  let iDj : D ⟶ PrimeSpectrum.basicOpen (h j) :=
    homOfLE (PrimeSpectrum.basicOpen_mul_le_right _ _)
  apply toBasicOpen_injective R (h i * h j)
  rw [toBasicOpen_mk', toBasicOpen_mk']
  simp only []
  trans
  on_goal 1 =>
    convert congr_arg ((structureSheaf R).1.map iDj.op) (hs j).symm using 1
    convert congr_arg ((structureSheaf R).1.map iDi.op) (hs i) using 1
  all_goals rw [res_const]; apply const_ext; ring
  exacts [PrimeSpectrum.basicOpen_mul_le_left _ _, PrimeSpectrum.basicOpen_mul_le_right _ _]

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, ⋯⟩
⊢ ∃ 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 a
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 ⋯
⊢ (toBasicOpen R (h i * h j)) (IsLocalization.mk' (Localization.Away (h i * h j)) (a i * h j) ⟨h i * h j, ⋯⟩) =
    (toBasicOpen R (h i * h j)) (IsLocalization.mk' (Localization.Away (h i * h j)) (h i * a j) ⟨h i * h j, ⋯⟩)

Tactic:
rw [toBasicOpen_mk', toBasicOpen_mk']

Result:
case a
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 i * h j) (↑⟨h i * h j, ⋯⟩) (PrimeSpectrum.basicOpen (h i * h j)) ⋯ =
    const R (h i * a j) (↑⟨h i * h j, ⋯⟩) (PrimeSpectrum.basicOpen (h i * h j)) ⋯