-- 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:
case h.e'_2.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 i ∈ x.asIdeal.primeCompl

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:
exacts [PrimeSpectrum.basicOpen_mul_le_left _ _, PrimeSpectrum.basicOpen_mul_le_right _ _]

Result:
no goals

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)
⊢ 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, ⋯⟩

Tactic:
let iDi : D ⟶ PrimeSpectrum.basicOpen (h i) := homOfLE (PrimeSpectrum.basicOpen_mul_le_left _ _)

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
i j : ι
D : Opens (PrimeSpectrum R) := PrimeSpectrum.basicOpen (h i * h j)
iDi : D ⟶ PrimeSpectrum.basicOpen (h i) := homOfLE ⋯
⊢ 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, ⋯⟩

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 ^ n (i, j) * h i ^ k * h i * (a j * (h j ^ n (i, j) * h j ^ k)) =
    h (i, j).1 * a (i, j).2 * (h (i, j).1 * h (i, j).2) ^ ⋯.choose * (h i * h j) ^ k

Tactic:
simp only [n, mul_pow]

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

Proof state:
case refine_3.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
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
⊢ ∀ x ∈ PrimeSpectrum.basicOpen ((fun i => h i ^ (N + 1)) i), h i ∈ x.asIdeal.primeCompl

Tactic:
exact (basic_opens_eq i).le

Result:
no goals