Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : 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 : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
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 : i₁ (IsLocalRing.closedPoint K) ∈ basicOpen 𝒜 ↑i
this : Set.range ⇑i₁ ⊆ ↑(Hom.opensRange (awayι 𝒜 ↑i ⋯ ⋯))
φ : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of (Away 𝒜 ↑i)) := IsOpenImmersion.lift (awayι 𝒜 ↑i ⋯ ⋯) i₁ this
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers ↑i)) ≫ Spec.preimage φ
i₀ : ↥x
φ' : Away 𝒜 (↑i * ↑i₀) →+* K
hφ : φ'.comp (awayMap 𝒜 ⋯ ⋯) = CommRingCat.Hom.hom (Spec.preimage φ)
hφ' : (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range
e : O ≃+* ↥(algebraMap O K).range := (AlgEquiv.ofInjective (Algebra.ofId O K) ⋯).toRingEquiv
φ'' : Away 𝒜 ↑i₀ →+* O := e.symm.toRingHom.comp ((Subring.inclusion hφ').comp (φ'.comp (awayMap 𝒜 ⋯ ⋯)).rangeRestrict)
⊢ ⋯.HasLift

Tactic:
have hφ'' : (algebraMap O K).comp φ'' = φ'.comp (awayMap 𝒜 (hxd _ i.2) (mul_comm _ _)) := by
    ext x
    exact congr_arg Subtype.val (e.apply_symm_apply _)

Goal state after:
σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : 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 : Algebra.adjoin ↥(𝒜 0) ↑x = ⊤
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 : i₁ (IsLocalRing.closedPoint K) ∈ basicOpen 𝒜 ↑i
this : Set.range ⇑i₁ ⊆ ↑(Hom.opensRange (awayι 𝒜 ↑i ⋯ ⋯))
φ : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of (Away 𝒜 ↑i)) := IsOpenImmersion.lift (awayι 𝒜 ↑i ⋯ ⋯) i₁ this
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers ↑i)) ≫ Spec.preimage φ
i₀ : ↥x
φ' : Away 𝒜 (↑i * ↑i₀) →+* K
hφ : φ'.comp (awayMap 𝒜 ⋯ ⋯) = CommRingCat.Hom.hom (Spec.preimage φ)
hφ' : (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range
e : O ≃+* ↥(algebraMap O K).range := (AlgEquiv.ofInjective (Algebra.ofId O K) ⋯).toRingEquiv
φ'' : Away 𝒜 ↑i₀ →+* O := e.symm.toRingHom.comp ((Subring.inclusion hφ').comp (φ'.comp (awayMap 𝒜 ⋯ ⋯)).rangeRestrict)
hφ'' : (algebraMap O K).comp φ'' = φ'.comp (awayMap 𝒜 ⋯ ⋯)
⊢ ⋯.HasLift