-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
theorem QuasiSeparated.of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [QuasiSeparated (f ≫ g)] :
    QuasiSeparated f

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
i : 𝒰.J
⊢ IsAffine ((pullback g (Z.affineCover.map i.fst)).affineCover.obj i.snd)

Tactic:
infer_instance

Result:
no goals

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
i : Z.affineCover.J
j : (pullback g (Z.affineCover.map i)).affineCover.J
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
simp

Result:
no goals

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
⊢ QuasiSeparated f

Tactic:
let 𝒰 := (Z.affineCover.pullbackCover g).bind fun x => Scheme.affineCover _

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
⊢ QuasiSeparated f

Proof state:
case mk
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
i : Z.affineCover.J
j : (pullback g (Z.affineCover.map i)).affineCover.J
⊢ QuasiSeparatedSpace
    ↑↑((((Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
                    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover).pullbackCover
                f).obj
            ⟨i, j⟩).toPresheafedSpace

Tactic:
refine @quasiSeparatedSpace_of_quasiSeparated _ _ ?_
  (HasAffineProperty.of_isPullback (.of_hasPullback _ (Z.affineCover.map i)) ‹_›) ?_

Result:
case mk.refine_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
i : Z.affineCover.J
j : (pullback g (Z.affineCover.map i)).affineCover.J
⊢ (((Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
              ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover).pullbackCover
          f).obj
      ⟨i, j⟩ ⟶
    pullback (f ≫ g) (Z.affineCover.map i)

case mk.refine_2
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
i : Z.affineCover.J
j : (pullback g (Z.affineCover.map i)).affineCover.J
⊢ QuasiSeparated ?mk.refine_1

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
i : 𝒰.J
⊢ IsAffine (𝒰.obj i)

Tactic:
dsimp [𝒰]

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
i : 𝒰.J
⊢ IsAffine ((pullback g (Z.affineCover.map i.fst)).affineCover.obj i.snd)

Proof state:
case mk.refine_2
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
i : Z.affineCover.J
j : (pullback g (Z.affineCover.map i)).affineCover.J
⊢ QuasiSeparated
    (pullback.map f
        (((Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
              ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover).map
          ⟨i, j⟩)
        f ((Scheme.Cover.pullbackCover Z.affineCover g).map ⟨i, j⟩.fst) (𝟙 X)
        (((fun x => ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover) ⟨i, j⟩.fst).map ⟨i, j⟩.snd) (𝟙 Y)
        ⋯ ⋯ ≫
      (pullbackRightPullbackFstIso g (Z.affineCover.map i) f).hom)

Tactic:
exact inferInstance

Result:
no goals

Proof state:
case mk
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
i : (Scheme.Cover.pullbackCover Z.affineCover g).J
j : ((fun x => ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover) i).J
⊢ QuasiSeparatedSpace
    ↑↑((((Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
                    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover).pullbackCover
                f).obj
            ⟨i, j⟩).toPresheafedSpace

Tactic:
dsimp at i j

Result:
case mk
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
i : Z.affineCover.J
j : (pullback g (Z.affineCover.map i)).affineCover.J
⊢ QuasiSeparatedSpace
    ↑↑((((Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
                    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover).pullbackCover
                f).obj
            ⟨i, j⟩).toPresheafedSpace

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
⊢ QuasiSeparated f

Tactic:
apply HasAffineProperty.of_openCover
  ((Z.affineCover.pullbackCover g).bind fun x => Scheme.affineCover _)

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : Scheme.Cover (@IsOpenImmersion) Y :=
  (Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
    ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover
this : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
⊢ ∀
    (i :
      ((Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
          ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover).1),
    QuasiSeparatedSpace
      ↑↑((((Scheme.Cover.pullbackCover Z.affineCover g).bind fun x =>
                      ((Scheme.Cover.pullbackCover Z.affineCover g).obj x).affineCover).pullbackCover
                  f).obj
              i).toPresheafedSpace