Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: case refine_3
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
H :
  ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
𝒰 : S.OpenCover := S.affineOpenCover.openCover
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover :=
  fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).affineOpenCover.openCover
𝒲 : (i : (Precoverage.ZeroHypercover.pullback₁ g 𝒰).I₀) → ((Precoverage.ZeroHypercover.pullback₁ g 𝒰).X i).OpenCover :=
  fun i ↦ ((Precoverage.ZeroHypercover.pullback₁ g 𝒰).X i).affineOpenCover.openCover
U : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) × (𝒱 i).I₀ × (𝒲 i).I₀ → TopologicalSpace.Opens (↥X × ↥Y) :=
  fun ijk ↦
    {
      carrier :=
        {P |
          P.1 ∈ Scheme.Hom.opensRange ((𝒱 ijk.fst).f ijk.snd.1 ≫ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f ijk.fst) ∧
            P.2 ∈
              Scheme.Hom.opensRange ((𝒲 ijk.fst).f ijk.snd.2 ≫ (Precoverage.ZeroHypercover.pullback₁ g 𝒰).f ijk.fst)},
      is_open' := ⋯ }
this✝ : Set.range L ⊆ ↑(iSup U)
𝓤 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f g) :=
  Precoverage.ZeroHypercover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f g) fun i ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒱 i) (𝒲 i) (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i))
i : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) × (𝒱 i).I₀ × (𝒲 i).I₀
this :
  IsEmbedding
    (L ∘
      ⇑(pullback.map ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst)
          ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst) f g
          ((𝒱 i.fst).f i.snd.1 ≫ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i.fst)
          ((𝒲 i.fst).f i.snd.2 ≫ (Precoverage.ZeroHypercover.pullback₁ g 𝒰).f i.fst) (𝒰.f i.fst) ⋯ ⋯))
⊢ IsEmbedding ((fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)) ∘ ⇑(𝓤.f i))

Tactic:
convert! this using 7

Goal state after:
case e'_5.e'_5.e'_5.e'_9.e'_5.e'_3.e'_3
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := ⋯
H :
  ∀ (R A B : CommRingCat) (f' : Spec A ⟶ Spec R) (g' : Spec B ⟶ Spec R) (iX : Spec A ⟶ X) (iY : Spec B ⟶ Y)
    (iS : Spec R ⟶ S) (e₁ : f' ≫ iS = iX ≫ f) (e₂ : g' ≫ iS = iY ≫ g),
    IsOpenImmersion iX →
      IsOpenImmersion iY → IsOpenImmersion iS → IsEmbedding (L ∘ ⇑(pullback.map f' g' f g iX iY iS e₁ e₂))
𝒰 : S.OpenCover := ⋯
𝒱 : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover := ⋯
𝒲 : (i : (Precoverage.ZeroHypercover.pullback₁ g 𝒰).I₀) →
  ((Precoverage.ZeroHypercover.pullback₁ g 𝒰).X i).OpenCover := ⋯
U : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) × (𝒱 i).I₀ × (𝒲 i).I₀ → TopologicalSpace.Opens (↥X × ↥Y) := ⋯
this✝ : Set.range L ⊆ ↑(iSup U)
𝓤 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f g) := ⋯
i : (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) × (𝒱 i).I₀ × (𝒲 i).I₀
this :
  IsEmbedding
    (L ∘
      ⇑(pullback.map ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst)
          ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst) f g
          ((𝒱 i.fst).f i.snd.1 ≫ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i.fst)
          ((𝒲 i.fst).f i.snd.2 ≫ (Precoverage.ZeroHypercover.pullback₁ g 𝒰).f i.fst) (𝒰.f i.fst) ⋯ ⋯))
e_1✝³ :
  ↥(𝓤.X i) =
    ↥(pullback ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst)
        ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst))
e_1✝² :
  (fun X Y ↦ C(↑X, ↑Y)) ↑(𝓤.X i).toPresheafedSpace ↑(pullback f g).toPresheafedSpace =
    (fun X Y ↦ C(↑X, ↑Y))
      ↑(pullback ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst)
            ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst)).toPresheafedSpace
      ↑(pullback f g).toPresheafedSpace
e_7✝ :
  ↑(𝓤.X i).toPresheafedSpace =
    ↑(pullback ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst)
          ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst)).toPresheafedSpace
e_3✝ :
  (𝓤.X i).toPresheafedSpace =
    (pullback ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst)
        ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst)).toPresheafedSpace
e_1✝¹ :
  (𝓤.X i).toLocallyRingedSpace =
    (pullback ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst)
        ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst)).toLocallyRingedSpace
e_1✝ :
  𝓤.X i =
    pullback ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst)
      ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst)
⊢ 𝓤.f i =
    pullback.map ((𝒱 i.fst).f i.snd.1 ≫ Scheme.Cover.pullbackHom 𝒰 f i.fst)
      ((𝒲 i.fst).f i.snd.2 ≫ Scheme.Cover.pullbackHom 𝒰 g i.fst) f g
      ((𝒱 i.fst).f i.snd.1 ≫ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i.fst)
      ((𝒲 i.fst).f i.snd.2 ≫ (Precoverage.ZeroHypercover.pullback₁ g 𝒰).f i.fst) (𝒰.f i.fst) ⋯ ⋯