awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
x : ↥Y
⊢ Eq (α :=
    Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Scheme.forgetToTop.obj (X ⨿ Y))
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
            ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (BinaryCofan.inr ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat)) :
        Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
            { as := WalkingPair.right : Discrete WalkingPair } ⟶
          Functor.obj
            (Functor.obj (Functor.const (Discrete WalkingPair))
              (Cocone.pt (F := pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
                ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat))))
            { as := WalkingPair.right : Discrete WalkingPair })
      (CategoryStruct.comp (Y := colimit (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)))
          (Iso.inv
            (colimit.isoColimitCocone
              { cocone := (↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat),
                isColimit := (↑X.toPresheafedSpace : TopCat).binaryCofanIsColimit (↑Y.toPresheafedSpace : TopCat) }))
          (Iso.hom (PreservesColimitPair.iso Scheme.forgetToTop X Y)) :
        Functor.obj
            (Functor.obj (Functor.const (Discrete WalkingPair))
              (Cocone.pt (F := pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
                ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat))))
            { as := WalkingPair.right : Discrete WalkingPair } ⟶
          Scheme.forgetToTop.obj (X ⨿ Y)))
    (Scheme.forgetToTop.map coprod.inr)

Tactic:
(colimit.isoColimitCocone_ι_inv_assoc ⟨_, TopCat.binaryCofanIsColimit _ _⟩ _ _).trans ?_

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv_assoc, CategoryTheory.Limits.ColimitCocone.mk, Eq.trans, TopCat.binaryCofanIsColimit
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
x : ↥Y
e_a :
  Eq (α :=
    Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Scheme.forgetToTop.obj (X ⨿ Y))
    (CategoryStruct.comp (Y := colimit (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)))
      (colimit.ι (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)) { as := WalkingPair.right })
      (Iso.hom (PreservesColimitPair.iso Scheme.forgetToTop X Y)))
    (Scheme.forgetToTop.map coprod.inr)
⊢ Eq (α :=
    Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Scheme.forgetToTop.obj (X ⨿ Y))
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj (Functor.const (Discrete WalkingPair))
          (Cocone.pt (F := pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
            ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (BinaryCofan.inr ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat)) :
        Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
            { as := WalkingPair.right : Discrete WalkingPair } ⟶
          Functor.obj
            (Functor.obj (Functor.const (Discrete WalkingPair))
              (Cocone.pt (F := pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
                ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat))))
            { as := WalkingPair.right : Discrete WalkingPair })
      (CategoryStruct.comp (Y := colimit (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)))
          (Iso.inv
            (colimit.isoColimitCocone
              { cocone := (↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat),
                isColimit := (↑X.toPresheafedSpace : TopCat).binaryCofanIsColimit (↑Y.toPresheafedSpace : TopCat) }))
          (Iso.hom (PreservesColimitPair.iso Scheme.forgetToTop X Y)) :
        Functor.obj
            (Functor.obj (Functor.const (Discrete WalkingPair))
              (Cocone.pt (F := pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
                ((↑X.toPresheafedSpace : TopCat).binaryCofan (↑Y.toPresheafedSpace : TopCat))))
            { as := WalkingPair.right : Discrete WalkingPair } ⟶
          Scheme.forgetToTop.obj (X ⨿ Y)))
    (Scheme.forgetToTop.map coprod.inr)

Tactic:
refine (colimit.isoColimitCocone_ι_inv_assoc ⟨_, TopCat.binaryCofanIsColimit _ _⟩ _ _).trans ?_

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv_assoc, CategoryTheory.Limits.ColimitCocone.mk, Eq.trans, TopCat.binaryCofanIsColimit
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
x : ↥Y
⊢ Eq (α :=
    Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Scheme.forgetToTop.obj (X ⨿ Y))
    (CategoryStruct.comp (Y := colimit (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)))
      (colimit.ι (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)) { as := WalkingPair.right })
      (Iso.hom (PreservesColimitPair.iso Scheme.forgetToTop X Y)))
    (Scheme.forgetToTop.map coprod.inr)

Tactic:
coprodComparison_inr Scheme.forgetToTop

Premises used: AlgebraicGeometry.Scheme.forgetToTop, CategoryTheory.Limits.coprodComparison_inr
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
X Y : Scheme
x : ↥Y
⊢ Eq (α :=
    Functor.obj (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat))
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Scheme.forgetToTop.obj (X ⨿ Y))
    (CategoryStruct.comp (Y := colimit (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)))
      (colimit.ι (pair (↑X.toPresheafedSpace : TopCat) (↑Y.toPresheafedSpace : TopCat)) { as := WalkingPair.right })
      (Iso.hom (PreservesColimitPair.iso Scheme.forgetToTop X Y)))
    (Scheme.forgetToTop.map coprod.inr)

Tactic:
exact coprodComparison_inr Scheme.forgetToTop

Premises used: AlgebraicGeometry.Scheme.forgetToTop, CategoryTheory.Limits.coprodComparison_inr
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥X ⊕ ↥Y
h :
  ∃ (y :
    ↥(Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y)
        (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit)
          (((coprodMk X Y).symm : (a : ↥(X ⨿ Y)) → ↥X ⊕ ↥Y)
            ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y)))))),
    Eq (α := ↥(X ⨿ Y))
      ((Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
            (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr)
            (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit)
              (((coprodMk X Y).symm : (a : ↥(X ⨿ Y)) → ↥X ⊕ ↥Y)
                ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y)))))
          y :
        ↥(X ⨿ Y))
      ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))
⊢ Membership.mem (α := ↥(X ⨿ Y)) (γ := Set ↥(X ⨿ Y))
    (Set.range (ι :=
      ↥(PreZeroHypercover.X.{w, u, u + 1} (S := X ⨿ Y)
          { I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1},
            X := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
              Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x,
            f := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
              Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
                Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
                (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr) x :
            PreZeroHypercover.{w, u, u + 1} (X ⨿ Y) }
          (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit)
            (((coprodMk X Y).symm : (a : ↥(X ⨿ Y)) → ↥X ⊕ ↥Y)
              ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))))))
      ⇑(PreZeroHypercover.f
          { I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1},
            X := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
              Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x,
            f := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
              Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
                Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
                (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr) x }
          (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit)
            (((coprodMk X Y).symm : (a : ↥(X ⨿ Y)) → ↥X ⊕ ↥Y)
              ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))))))
    ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))

Tactic:
simp only [Sum.elim_inl, Sum.elim_inr, Set.mem_range]

Premises used: Set.mem_range, Sum.elim_inr, Sum.elim_inl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥X ⊕ ↥Y
h :
  ∃ (y :
    ↥(Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y)
        (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) x))),
    Eq (α := ↥(X ⨿ Y))
      ((Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
            (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr)
            (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) x))
          y :
        ↥(X ⨿ Y))
      ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))
⊢ ∃ (y :
    ↥(Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y)
        (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit)
          (((coprodMk X Y).symm : (a : ↥(X ⨿ Y)) → ↥X ⊕ ↥Y)
            ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y)))))),
    Eq (α := ↥(X ⨿ Y))
      ((Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
            (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr)
            (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit)
              (((coprodMk X Y).symm : (a : ↥(X ⨿ Y)) → ↥X ⊕ ↥Y)
                ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y)))))
          y :
        ↥(X ⨿ Y))
      ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))

Tactic:
rw [Homeomorph.symm_apply_apply]

Premises used: Homeomorph.symm_apply_apply
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥X ⊕ ↥Y
h :
  ∀ (x : ↥X),
    ∃ (y :
      ↥(Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y)
          (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) (Sum.inl x)))),
      Eq (α := ↥(X ⨿ Y))
        ((Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
              Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
              (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr)
              (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) (Sum.inl x)))
            y :
          ↥(X ⨿ Y))
        ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inl x) : ↥(X ⨿ Y))
h₁ :
  ∀ (x : ↥Y),
    ∃ (y :
      ↥(Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y)
          (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) (Sum.inr x)))),
      Eq (α := ↥(X ⨿ Y))
        ((Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
              Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
              (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr)
              (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) (Sum.inr x)))
            y :
          ↥(X ⨿ Y))
        ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inr x) : ↥(X ⨿ Y))
⊢ ∃ (y :
    ↥(Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y)
        (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) x))),
    Eq (α := ↥(X ⨿ Y))
      ((Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
            (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr)
            (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) x))
          y :
        ↥(X ⨿ Y))
      ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) x : ↥(X ⨿ Y))

Tactic:
obtain (x | x) := x
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥X
⊢ ∃ (y :
    ↥(Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y)
        (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) (Sum.inl x)))),
    Eq (α := ↥(X ⨿ Y))
      ((Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
            (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr)
            (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) (Sum.inl x)))
          y :
        ↥(X ⨿ Y))
      ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inl x) : ↥(X ⨿ Y))

Tactic:
simp only [Sum.elim_inl, coprodMk_inl, exists_apply_eq_apply]

Premises used: AlgebraicGeometry.coprodMk_inl, Sum.elim_inl, exists_apply_eq_apply
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥Y
⊢ ∃ (y :
    ↥(Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y)
        (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) (Sum.inr x)))),
    Eq (α := ↥(X ⨿ Y))
      ((Sum.rec (motive := fun (x : PUnit.{w + 1} ⊕ PUnit.{w + 1}) ↦
            Sum.elim (fun (x : PUnit.{w + 1}) ↦ X) (fun (x : PUnit.{w + 1}) ↦ Y) x ⟶ X ⨿ Y)
            (fun (x : PUnit.{w + 1}) ↦ coprod.inl) (fun (x : PUnit.{w + 1}) ↦ coprod.inr)
            (Sum.elim (fun (x : ↥X) ↦ Sum.inl PUnit.unit) (fun (x : ↥Y) ↦ Sum.inr PUnit.unit) (Sum.inr x)))
          y :
        ↥(X ⨿ Y))
      ((coprodMk X Y : (a : ↥X ⊕ ↥Y) → ↥(X ⨿ Y)) (Sum.inr x) : ↥(X ⨿ Y))

Tactic:
simp only [Sum.elim_inr, coprodMk_inr, exists_apply_eq_apply]

Premises used: Sum.elim_inr, AlgebraicGeometry.coprodMk_inr, exists_apply_eq_apply
-- 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
⊢ Cofan.inj (BinaryCofan.mk f g) WalkingPair.left ≫ Iso.hom (Iso.refl (BinaryCofan.mk f g).pt) = c'.inj WalkingPair.left

Tactic:
rfl
-- 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
⊢ Cofan.inj (BinaryCofan.mk f g) WalkingPair.right ≫ Iso.hom (Iso.refl (BinaryCofan.mk f g).pt) =
    c'.inj WalkingPair.right

Tactic:
rfl
-- 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) ⋯
⊢ Nonempty (IsColimit (BinaryCofan.mk f g))

Tactic:
⟨IsColimit.ofIsoColimit (Nonempty.some ?_) i.symm⟩

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, Nonempty.some, Nonempty.intro, CategoryTheory.Iso.symm
-- 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) ⋯
refine : Nonempty.{u + 2} (IsColimit c')
⊢ Nonempty (IsColimit (BinaryCofan.mk f g))

Tactic:
refine ⟨IsColimit.ofIsoColimit (Nonempty.some ?_) i.symm⟩
-- 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
⊢ Nonempty (IsColimit (Cofan.mk S fi))

Tactic:
nonempty_isColimit_cofanMk_of fi _ _

Premises used: AlgebraicGeometry.nonempty_isColimit_cofanMk_of
-- 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 : ∀ (i : WalkingPair), IsOpenImmersion (fi i)
convert_2 : Eq.{u + 1} (α := S.Opens) (⨆ (i : WalkingPair), Scheme.Hom.opensRange (fi i)) ⊤
convert_3 :
  _root_.Pairwise (α := WalkingPair)
    (Function.onFun.{1, u + 1, 1} (β := S.Opens) Disjoint fun (x : WalkingPair) ↦ Scheme.Hom.opensRange (fi x))
⊢ Nonempty.{u + 2} (IsColimit c')

Tactic:
convert! nonempty_isColimit_cofanMk_of fi _ _

Premises used: AlgebraicGeometry.nonempty_isColimit_cofanMk_of
-- 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 : WalkingPair
convert_1 : IsOpenImmersion (fi WalkingPair.left)
convert_1₁ : IsOpenImmersion (fi WalkingPair.right)
⊢ IsOpenImmersion (fi i)

Tactic:
cases i
-- 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 f
⊢ IsOpenImmersion (fi WalkingPair.left)

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 f

Tactic:
infer_instance