Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks

Goal state before:
pp: 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) ⋯ ⋯

Tactic:
apply pullback.hom_ext

Goal state after:
case e'_5.e'_5.e'_5.e'_9.e'_5.e'_3.e'_3.h₀
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.fst f g =
    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) ⋯ ⋯ ≫
      pullback.fst f g

case h₁
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.snd f g =
    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) ⋯ ⋯ ≫
      pullback.snd f g