-- 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 𝒜 ⋯ ⋯)
refine_1 :
  CategoryStruct.comp (Y :=
      Spec
        (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))
      (Spec.map
        (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)))
      (Spec.map (CommRingCat.ofHom φ'') ≫ awayι 𝒜 (↑i₀ : A) ⋯ ⋯) =
    { 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 𝒜) }.i₁
refine_2 :
  CategoryStruct.comp (Y := Proj 𝒜) (Spec.map (CommRingCat.ofHom φ'') ≫ awayι 𝒜 (↑i₀ : A) ⋯ ⋯) (toSpecZero 𝒜) =
    { 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 𝒜) }.i₂
⊢ ⋯.HasLift

Tactic:
refine ⟨⟨Spec.map (CommRingCat.ofHom φ'') ≫ Proj.awayι 𝒜 _ (hxd _ i₀.2) (hd _ _).bot_lt, ?_, ?_⟩⟩