-- 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 i * h j) (h i * h j) (PrimeSpectrum.basicOpen (h i * h j)) ⋯ = ?m.186516

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 ⋯
⊢ ?m.186516 = const R (h i * a j) (h i * h j) (PrimeSpectrum.basicOpen (h i * h j)) ⋯

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 ⋯
⊢ ↑((structureSheaf R).val.obj (op (PrimeSpectrum.basicOpen (h i * h j))))

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

Result:
case h.e'_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
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)) ⋯ =
    (ConcreteCategory.hom ((structureSheaf R).val.map iDi.op)) (const R (a i) (h i) (PrimeSpectrum.basicOpen (h i)) ⋯)

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 ⋯
⊢ (ConcreteCategory.hom ((structureSheaf R).val.map iDj.op)) (const R (a j) (h j) (PrimeSpectrum.basicOpen (h j)) ⋯) =
    const R (h i * a j) (h i * h j) (PrimeSpectrum.basicOpen (h i * h 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 * (fun i => h i ^ (N + 1)) i = (fun i => a i * h i ^ N) i * h i

Tactic:
dsimp

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