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)
hφ'' : (algebraMap O K).comp φ'' = φ'.comp (awayMap 𝒜 ⋯ ⋯)
⊢ Spec.map
        (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 }.R
              { R := O, commRing := commRing✝, domain := domain✝, valuationRing := valuationRing✝, K := K,
                  field := field✝, algebra := algebra✝, isFractionRing := isFractionRing✝, i₁ := i₁, i₂ := i₂,
                  commSq := w }.K)) ≫
      awayι 𝒜 ↑i₀ ⋯ ⋯ =
    φ ≫ awayι 𝒜 ↑i ⋯ ⋯

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

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 𝒜 ⋯ ⋯)
⊢ 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 }.R
                { R := O, commRing := commRing✝, domain := domain✝, valuationRing := valuationRing✝, K := K,
                    field := field✝, algebra := algebra✝, isFractionRing := isFractionRing✝, i₁ := i₁, i₂ := i₂,
                    commSq := w }.K).comp
            φ'')) ≫
      awayι 𝒜 ↑i₀ ⋯ ⋯ =
    Spec.map (CommRingCat.ofHom (φ'.comp (awayMap 𝒜 ⋯ ⋯))) ≫ awayι 𝒜 ↑i ⋯ ⋯