-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
inst_4 : Algebra.FiniteType (↥(𝒜 0)) A
O : Type u_2
commRing : CommRing O
domain : IsDomain O
valuationRing : ValuationRing O
K : Type u_2
field : Field K
algebra : Algebra O K
isFractionRing : IsFractionRing O K
i₁ : Spec (CommRingCat.of K) ⟶ Proj 𝒜
i₂ : Spec (CommRingCat.of O) ⟶ Spec (CommRingCat.of ↥(𝒜 0))
w : CommSq i₁ (Spec.map (CommRingCat.ofHom (algebraMap O K))) (toSpecZero 𝒜) i₂
x : Finset A
hx : Eq (α := Subalgebra (↥(𝒜 0)) A) (Algebra.adjoin ↥(𝒜 0) (↑x : Set A)) ⊤
d : (i : A) → i ∈ x → ℕ
hd : ∀ (i : A) (a : i ∈ x), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x), i ∈ 𝒜 (d i a)
i : ↥x
hi :
  Membership.mem (α := ↥(Proj 𝒜)) (γ := TopologicalSpace.Opens ↥(Proj 𝒜)) (basicOpen 𝒜 (↑i : A))
    (i₁ (IsLocalRing.closedPoint K) : ↥(Proj 𝒜))
this : Set.range (ι := ↥(Spec (CommRingCat.of K))) ⇑i₁ ⊆ (↑(Hom.opensRange (awayι 𝒜 (↑i : A) ⋯ ⋯)) : Set ↥(Proj 𝒜))
φ : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of (Away 𝒜 (↑i : A))) :=
  IsOpenImmersion.lift (awayι 𝒜 (↑i : A) ⋯ ⋯) i₁ this
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑i : A))) ≫ Spec.preimage φ
i₀ : ↥x
φ' : Away 𝒜 ((↑i : A) * (↑i₀ : A)) →+* K
hφ : φ'.comp (awayMap 𝒜 ⋯ ⋯) = CommRingCat.Hom.hom (Spec.preimage φ)
hφ' :
  LE.le.{u_2} (α := Subring K) (RingHom.range (R := Away 𝒜 (↑i₀ : A)) (φ'.comp (awayMap 𝒜 ⋯ ⋯)))
    (RingHom.range (R := O) (algebraMap O K))
e : O ≃+* ↥(RingHom.range (R := O) (algebraMap O K)) := AlgEquiv.toRingEquiv (AlgEquiv.ofInjective (Algebra.ofId O K) ⋯)
φ'' : Away 𝒜 (↑i₀ : A) →+* O :=
  e.symm.toRingHom.comp ((Subring.inclusion hφ').comp (RingHom.rangeRestrict (φ'.comp (awayMap 𝒜 ⋯ ⋯))))
hφ'' : RingHom.comp (algebraMap O K) φ'' = φ'.comp (awayMap 𝒜 ⋯ ⋯)
h :
  Spec.map
        (CommRingCat.ofHom
          (RingHom.comp
            (algebraMap
              { R := O, commRing := commRing, domain := domain, valuationRing := valuationRing, K := K, field := field,
                  algebra := algebra, isFractionRing := isFractionRing, i₁ := i₁, i₂ := i₂, commSq := w :
                  ValuativeCommSq (X := Proj 𝒜) (toSpecZero 𝒜) }.R
              { R := O, commRing := commRing, domain := domain, valuationRing := valuationRing, K := K, field := field,
                  algebra := algebra, isFractionRing := isFractionRing, i₁ := i₁, i₂ := i₂, commSq := w :
                  ValuativeCommSq (X := Proj 𝒜) (toSpecZero 𝒜) }.K)
            φ'')) ≫
      awayι 𝒜 (↑i₀ : A) ⋯ ⋯ =
    Spec.map (CommRingCat.ofHom (φ'.comp (awayMap 𝒜 ⋯ ⋯))) ≫ awayι 𝒜 (↑i : A) ⋯ ⋯
⊢ Spec.map
        (CategoryStruct.comp (Y :=
          CommRingCat.of
            { R := O, commRing := commRing, domain := domain, valuationRing := valuationRing, K := K, field := field,
                algebra := algebra, isFractionRing := isFractionRing, i₁ := i₁, i₂ := i₂, commSq := w :
                ValuativeCommSq (X := Proj 𝒜) (toSpecZero 𝒜) }.R)
          (CommRingCat.ofHom φ'')
          (CommRingCat.ofHom
            (algebraMap
              { R := O, commRing := commRing, domain := domain, valuationRing := valuationRing, K := K, field := field,
                  algebra := algebra, isFractionRing := isFractionRing, i₁ := i₁, i₂ := i₂, commSq := w :
                  ValuativeCommSq (X := Proj 𝒜) (toSpecZero 𝒜) }.R
              { R := O, commRing := commRing, domain := domain, valuationRing := valuationRing, K := K, field := field,
                  algebra := algebra, isFractionRing := isFractionRing, i₁ := i₁, i₂ := i₂, commSq := w :
                  ValuativeCommSq (X := Proj 𝒜) (toSpecZero 𝒜) }.K))) ≫
      awayι 𝒜 (↑i₀ : A) ⋯ ⋯ =
    φ ≫ awayι 𝒜 (↑i : A) ⋯ ⋯

Tactic:
rw [← Spec.map_preimage φ, ← CommRingCat.ofHom_hom (Spec.preimage φ), ← hφ,
      ← CommRingCat.ofHom_comp]

Premises used: CommRingCat.ofHom_hom, AlgebraicGeometry.Spec.map_preimage, AlgebraicGeometry.Spec.preimage, CommRingCat.ofHom_comp