awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan (C := Scheme) fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y :=
  Cofan.mk S fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y ⟶ S :=
  fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
convert_1 : IsOpenImmersion g
⊢ IsOpenImmersion (fi WalkingPair.right)

Tactic:
simp [fi]
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan (C := Scheme) fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y :=
  Cofan.mk S fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y ⟶ S :=
  fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
⊢ IsOpenImmersion g

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan (C := Scheme) fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y :=
  Cofan.mk S fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y ⟶ S :=
  fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
⊢ Eq.{u + 1} (α := S.Opens) (⨆ (i : WalkingPair), Scheme.Hom.opensRange (fi i)) ⊤

Tactic:
simpa [← WalkingPair.equivBool.symm.iSup_comp, iSup_bool_eq, ← codisjoint_iff] using hf.2

Premises used: iSup_bool_eq, codisjoint_iff, Equiv.iSup_comp, CategoryTheory.Limits.WalkingPair.equivBool, Equiv.symm, IsCompl.codisjoint
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan (C := Scheme) fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y :=
  Cofan.mk S fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
i_1 : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y ⟶ S :=
  fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
i j : WalkingPair
hij : WalkingPair.left ≠ WalkingPair.right
⊢ Function.onFun.{1, u + 1, 1} (β := S.Opens) Disjoint (fun (x : WalkingPair) ↦ Scheme.Hom.opensRange (fi x))
    WalkingPair.left WalkingPair.right

Tactic:
simpa [fi] using hf.1

Premises used: IsCompl.disjoint
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan (C := Scheme) fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y :=
  Cofan.mk S fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
i_1 : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y ⟶ S :=
  fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
i j : WalkingPair
hij : WalkingPair.right ≠ WalkingPair.left
⊢ Function.onFun.{1, u + 1, 1} (β := S.Opens) Disjoint (fun (x : WalkingPair) ↦ Scheme.Hom.opensRange (fi x))
    WalkingPair.right WalkingPair.left

Tactic:
simpa [fi] using hf.1.symm

Premises used: Disjoint.symm, IsCompl.disjoint
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan (C := Scheme) fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y :=
  Cofan.mk S fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
i_1 : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) j X Y ⟶ S :=
  fun (j : WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
      WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Scheme) x X Y ⟶ S) j f g
i j : WalkingPair
hij : i ≠ j
⊢ Function.onFun.{1, u + 1, 1} (β := S.Opens) Disjoint (fun (x : WalkingPair) ↦ Scheme.Hom.opensRange (fi x)) i j

Tactic:
match i, j with
    | .left, .right => simpa [fi] using hf.1
    | .right, .left => simpa [fi] using hf.1.symm
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ Eq (α := X ⟶ X' ⨿ Y') (CategoryStruct.comp (Y := X ⨿ Y) coprod.inl (coprod.map f g)) (f ≫ coprod.inl)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
refine :
  Eq (α := (X ⨿ Y).Opens) (coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange coprod.inl)
⊢ IsPullback (Y := X ⨿ Y) (Z := X' ⨿ Y') f coprod.inl coprod.inl (coprod.map f g)

Tactic:
refine IsOpenImmersion.isPullback _ _ _ _ (by simp) ?_

Premises used: AlgebraicGeometry.IsOpenImmersion.isPullback
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
a : LE.le (α := (X ⨿ Y).Opens) (coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange coprod.inl)
a₁ : LE.le (α := (X ⨿ Y).Opens) (Scheme.Hom.opensRange coprod.inl) (coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl)
⊢ Eq (α := (X ⨿ Y).Opens) (coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) (Scheme.Hom.opensRange coprod.inl)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
x : ↥(X ⨿ Y)
y : ↥X'
hxy : Eq (α := ↥(X' ⨿ Y')) (coprod.inl y : ↥(X' ⨿ Y')) ((coprod.map f g) x : ↥(X' ⨿ Y'))
a :
  ∀ (x : ↥X)
    (hxy :
      Eq (α := ↥(X' ⨿ Y')) (coprod.inl y : ↥(X' ⨿ Y'))
        ((coprod.map f g) ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inl x) : ↥(X ⨿ Y)) : ↥(X' ⨿ Y'))),
    Membership.mem (α := ↥(X ⨿ Y)) (γ := Opens ↥(X ⨿ Y)) (Scheme.Hom.opensRange coprod.inl)
      ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inl x) : ↥(X ⨿ Y))
a₁ :
  ∀ (x : ↥Y)
    (hxy :
      Eq (α := ↥(X' ⨿ Y')) (coprod.inl y : ↥(X' ⨿ Y'))
        ((coprod.map f g) ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inr x) : ↥(X ⨿ Y)) : ↥(X' ⨿ Y'))),
    Membership.mem (α := ↥(X ⨿ Y)) (γ := Opens ↥(X ⨿ Y)) (Scheme.Hom.opensRange coprod.inl)
      ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inr x) : ↥(X ⨿ Y))
⊢ Membership.mem (γ := Opens ↥(X ⨿ Y)) (Scheme.Hom.opensRange coprod.inl) x

Tactic:
obtain ⟨(x | x), rfl⟩ := (coprodMk _ _).surjective x

Premises used: AlgebraicGeometry.coprodMk, Homeomorph.surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
y : ↥X'
x : ↥X
hxy :
  Eq (α := ↥(X' ⨿ Y')) (coprod.inl y : ↥(X' ⨿ Y'))
    ((coprod.map f g) ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inl x) : ↥(X ⨿ Y)) : ↥(X' ⨿ Y'))
⊢ Membership.mem (α := ↥(X ⨿ Y)) (↑(Scheme.Hom.opensRange coprod.inl) : Set ↥(X ⨿ Y))
    ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inl x) : ↥(X ⨿ Y))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
y : ↥X'
x : ↥Y
hxy :
  Eq (α := ↥(X' ⨿ Y')) (coprod.inl y : ↥(X' ⨿ Y'))
    ((coprod.map f g) ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inr x) : ↥(X ⨿ Y)) : ↥(X' ⨿ Y'))
⊢ Eq (α := ↥(X' ⨿ Y')) (coprod.inl y : ↥(X' ⨿ Y')) ((g ≫ coprod.inr) x : ↥(X' ⨿ Y'))

Tactic:
simp only [coprodMk_inr, ← Scheme.Hom.comp_apply, coprod.inr_map] at hxy

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.Limits.coprod.inr_map, AlgebraicGeometry.coprodMk_inr
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
y : ↥X'
x : ↥Y
hxy : Eq (α := ↥(X' ⨿ Y')) (coprod.inl y : ↥(X' ⨿ Y')) ((g ≫ coprod.inr) x : ↥(X' ⨿ Y'))
⊢ Membership.mem (α := ↥(X ⨿ Y)) (γ := Opens ↥(X ⨿ Y)) (Scheme.Hom.opensRange coprod.inl)
    ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inr x) : ↥(X ⨿ Y))

Tactic:
cases Set.disjoint_iff_forall_ne.mp (isCompl_range_inl_inr _ _).1 ⟨y, rfl⟩ ⟨_, rfl⟩ hxy

Premises used: AlgebraicGeometry.isCompl_range_inl_inr, Set.disjoint_iff_forall_ne, Exists.intro, Iff.mp, IsCompl.disjoint, rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
x : ↥X
⊢ Eq (α := ↥(X' ⨿ Y')) (coprod.inl (f x : ↥X') : ↥(X' ⨿ Y')) ((coprod.map f g) (coprod.inl x : ↥(X ⨿ Y)) : ↥(X' ⨿ Y'))

Tactic:
simp [← Scheme.Hom.comp_apply, - Scheme.Hom.comp_base]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Scheme.Hom.comp_base
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
x : ↥X
⊢ Membership.mem (α := ↥(X ⨿ Y)) (γ := Opens ↥(X ⨿ Y)) (coprod.map f g ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl)
    (coprod.inl x : ↥(X ⨿ Y))

Tactic:
exact ⟨f x, by simp [← Scheme.Hom.comp_apply, - Scheme.Hom.comp_base]⟩
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ g ≫ Iso.hom (Iso.refl Y') = Iso.hom (Iso.refl Y) ≫ g

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ Eq (α := Y ⟶ X ⨿ Y)
    (CategoryStruct.comp (Y := Y ⨿ X) (coprod.inl : Y ⟶ Y ⨿ X) (Iso.hom (coprod.braiding Y X) : Y ⨿ X ⟶ X ⨿ Y) :
      Y ⟶ X ⨿ Y)
    (Iso.hom (Iso.refl Y) ≫ coprod.inr : Y ⟶ X ⨿ Y)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ Eq (α := Y' ⟶ X' ⨿ Y')
    (CategoryStruct.comp (Y := Y' ⨿ X') (coprod.inl : Y' ⟶ Y' ⨿ X')
        (Iso.hom (coprod.braiding Y' X') : Y' ⨿ X' ⟶ X' ⨿ Y') :
      Y' ⟶ X' ⨿ Y')
    (Iso.hom (Iso.refl Y') ≫ coprod.inr : Y' ⟶ X' ⨿ Y')

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y X' Y' : Scheme
f : X ⟶ X'
g : Y ⟶ Y'
⊢ Eq (α := Y ⨿ X ⟶ X' ⨿ Y')
    (CategoryStruct.comp (Y := Y' ⨿ X') (coprod.map g f : Y ⨿ X ⟶ Y' ⨿ X')
        (Iso.hom (coprod.braiding Y' X') : Y' ⨿ X' ⟶ X' ⨿ Y') :
      Y ⨿ X ⟶ X' ⨿ Y')
    (CategoryStruct.comp (Y := X ⨿ Y) (Iso.hom (coprod.braiding Y X) : Y ⨿ X ⟶ X ⨿ Y)
        (coprod.map f g : X ⨿ Y ⟶ X' ⨿ Y') :
      Y ⨿ X ⟶ X' ⨿ Y')

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
suffices :
  IsVanKampenColimit.{0, 0, u_1, u_1 + 1} (C := Scheme) (F := pair X Y)
    (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)
⊢ IsVanKampenColimit c

Tactic:
suffices IsVanKampenColimit (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr) from
      this.of_iso (hc.uniqueUpToIso (coprodIsCoprod _ _)).symm
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
⊢ IsVanKampenColimit.{0, 0, u_1, u_1 + 1} (C := Scheme) (F := pair X Y)
    (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)

Tactic:
BinaryCofan.isVanKampen_mk _ _ (fun _ _ ↦ coprodIsCoprod _ _) _
      (fun _ _ ↦ pullbackIsPullback _ _) ?_ ?_

Premises used: CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.Limits.pullbackIsPullback, CategoryTheory.BinaryCofan.isVanKampen_mk
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
refine_1 :
  ∀ {X' Y' : Scheme.{u_1}} (αX : X' ⟶ X) (αY : Y' ⟶ Y)
    (f :
      Quiver.Hom (V := Scheme) (Cocone.pt (F := pair X' Y') (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr))
        (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))),
    αX ≫ BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr) =
        BinaryCofan.inl (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr) ≫ f →
      αY ≫ BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr) =
          BinaryCofan.inr (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr) ≫ f →
        IsPullback (BinaryCofan.inl (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr)) αX f
            (BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)) ∧
          IsPullback (BinaryCofan.inr (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr)) αY f
            (BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))
refine_2 :
  {Z : Scheme.{u_1}} →
    (f : Z ⟶ Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)) →
      IsColimit
        (BinaryCofan.mk
          (PullbackCone.mk (W := pullback f (BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
              (pullback.fst f (BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
              (pullback.snd f (BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))) ⋯).fst
          (PullbackCone.mk (W := pullback f (BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
              (pullback.fst f (BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
              (pullback.snd f (BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))) ⋯).fst)
⊢ IsVanKampenColimit.{0, 0, u_1, u_1 + 1} (C := Scheme) (F := pair X Y)
    (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)

Tactic:
refine BinaryCofan.isVanKampen_mk _ _ (fun _ _ ↦ coprodIsCoprod _ _) _
      (fun _ _ ↦ pullbackIsPullback _ _) ?_ ?_

Premises used: CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.Limits.pullbackIsPullback, CategoryTheory.BinaryCofan.isVanKampen_mk
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f_1 : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f :
  Quiver.Hom (V := Scheme) (Cocone.pt (F := pair X' Y') (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr))
    (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))
h₁ :
  αX ≫ BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr) =
    BinaryCofan.inl (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr) ≫ f
h₂ :
  αY ≫ BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr) =
    BinaryCofan.inr (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr) ≫ f
⊢ ∀ (x : ↥X'),
    Eq (α :=
      ↥(Functor.obj
          (Functor.obj (Functor.const (Discrete WalkingPair))
            (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
          { as := WalkingPair.left : Discrete WalkingPair }))
      ((BinaryCofan.inl (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr) ≫ f) x :
        ↥(Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
      ((αX ≫ BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)) x :
        ↥(Functor.obj
            (Functor.obj (Functor.const (Discrete WalkingPair))
              (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
            { as := WalkingPair.left : Discrete WalkingPair }))

Tactic:
have h₁' (x : _) := congr($h₁ x).symm
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f_1 : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f :
  Quiver.Hom (V := Scheme) (Cocone.pt (F := pair X' Y') (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr))
    (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))
h₁ :
  αX ≫ BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr) =
    BinaryCofan.inl (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr) ≫ f
h₂ :
  αY ≫ BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr) =
    BinaryCofan.inr (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr) ≫ f
h₁' :
  ∀ (x : ↥X'),
    Eq (α :=
      ↥(Functor.obj
          (Functor.obj (Functor.const (Discrete WalkingPair))
            (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
          { as := WalkingPair.left : Discrete WalkingPair }))
      ((BinaryCofan.inl (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr) ≫ f) x :
        ↥(Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
      ((αX ≫ BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)) x :
        ↥(Functor.obj
            (Functor.obj (Functor.const (Discrete WalkingPair))
              (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
            { as := WalkingPair.left : Discrete WalkingPair }))
⊢ ∀ (x : ↥Y'),
    Eq (α :=
      ↥(Functor.obj
          (Functor.obj (Functor.const (Discrete WalkingPair))
            (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
          { as := WalkingPair.right : Discrete WalkingPair }))
      ((BinaryCofan.inr (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr) ≫ f) x :
        ↥(Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
      ((αY ≫ BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)) x :
        ↥(Functor.obj
            (Functor.obj (Functor.const (Discrete WalkingPair))
              (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)))
            { as := WalkingPair.right : Discrete WalkingPair }))

Tactic:
have h₂' (x : _) := congr($h₂ x).symm
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f_1 : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f :
  Quiver.Hom (V := Scheme) (Cocone.pt (F := pair X' Y') (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr))
    (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
                (a : ↥X') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
            (a : ↥X) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αX.base : (a : ↥X') → ↥X) x : ↥X) :
        ↥(X ⨿ Y))
h₂' :
  ∀ (x : ↥Y'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
                (a : ↥Y') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
            (a : ↥Y) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αY.base : (a : ↥Y') → ↥Y) x : ↥Y) :
        ↥(X ⨿ Y))
⊢ IsPullback (BinaryCofan.inl (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr)) αX f
      (BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)) ∧
    IsPullback (BinaryCofan.inr (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr)) αY f
      (BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))

Tactic:
⟨(IsOpenImmersion.isPullback _ _ _ _ h₁.symm ?_).flip,
        (IsOpenImmersion.isPullback _ _ _ _ h₂.symm ?_).flip⟩

Premises used: AlgebraicGeometry.IsOpenImmersion.isPullback, CategoryTheory.IsPullback.flip, And.intro, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f_1 : ι → Scheme
σ : Type v
g : σ → Scheme
X_1 Y_1 : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f :
  Quiver.Hom (V := Scheme) (Cocone.pt (F := pair X' Y') (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr))
    (Cocone.pt (F := pair X Y) (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
                (a : ↥X') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inl))) :
            (a : ↥X) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αX.base : (a : ↥X') → ↥X) x : ↥X) :
        ↥(X ⨿ Y))
h₂' :
  ∀ (x : ↥Y'),
    Eq (α := ↥(X ⨿ Y))
      ((TopCat.Hom.hom f.base : (a : ↥(X' ⨿ Y')) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
                (a : ↥Y') → ↥(X' ⨿ Y'))
              x :
            ↥(X' ⨿ Y')) :
        ↥(X ⨿ Y))
      ((TopCat.Hom.hom (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Scheme.Hom.toLRSHom' coprod.inr))) :
            (a : ↥Y) → ↥(X ⨿ Y))
          ((TopCat.Hom.hom αY.base : (a : ↥Y') → ↥Y) x : ↥Y) :
        ↥(X ⨿ Y))
refine_1 : f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl = Scheme.Hom.opensRange coprod.inl
refine_1₁ : f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr = Scheme.Hom.opensRange coprod.inr
⊢ IsPullback (BinaryCofan.inl (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr)) αX f
      (BinaryCofan.inl (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr)) ∧
    IsPullback (BinaryCofan.inr (BinaryCofan.mk (P := X' ⨿ Y') coprod.inl coprod.inr)) αY f
      (BinaryCofan.inr (BinaryCofan.mk (P := X ⨿ Y) coprod.inl coprod.inr))

Tactic:
refine ⟨(IsOpenImmersion.isPullback _ _ _ _ h₁.symm ?_).flip,
        (IsOpenImmersion.isPullback _ _ _ _ h₂.symm ?_).flip⟩