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₀
⊢ IsEmbedding ((fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)) ∘ ⇑(𝓤.f i))

Tactic:
have := H (S.affineOpenCover.X i.1) (((𝒰.pullback₁ f).X i.1).affineOpenCover.X i.2.1)
        (((𝒰.pullback₁ g).X i.1).affineOpenCover.X i.2.2)
        ((𝒱 i.1).f i.2.1 ≫ 𝒰.pullbackHom f i.1)
        ((𝒲 i.1).f i.2.2 ≫ 𝒰.pullbackHom g i.1)
        ((𝒱 i.1).f i.2.1 ≫ (𝒰.pullback₁ f).f i.1)
        ((𝒲 i.1).f i.2.2 ≫ (𝒰.pullback₁ g).f i.1)
        (𝒰.f i.1) (by simp [pullback.condition]) (by simp [pullback.condition])
        inferInstance inferInstance inferInstance

Goal state after:
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))