awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
h : i ≠ j
U : (∐ g).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι g j)
x : ↥(g i)
hx : Membership.mem (α := ↥(∐ g)) U ((Sigma.ι g i) x : ↥(∐ g))
obtain :
  ∀ (y : ↥(g j)) (hy : Eq (α := ↥(∐ g)) ((Sigma.ι g j) y : ↥(∐ g)) ((Sigma.ι g i) x : ↥(∐ g))),
    Membership.mem (α := ↥(∐ g)) (γ := Opens ↥(∐ g)) ⊥ ((Sigma.ι g i) x : ↥(∐ g))
⊢ Membership.mem (α := ↥(∐ g)) (γ := Opens ↥(∐ g)) ⊥ ((Sigma.ι g i) x : ↥(∐ g))

Tactic:
obtain ⟨y, hy⟩ := hU' hx
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
h : i ≠ j
U : (∐ g).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι g j)
x : ↥(g i)
hx : Membership.mem (α := ↥(∐ g)) U ((Sigma.ι g i) x : ↥(∐ g))
y : ↥(g j)
hy : Eq (α := ↥(∐ g)) ((Sigma.ι g j) y : ↥(∐ g)) ((Sigma.ι g i) x : ↥(∐ g))
⊢ i ≠ i

Tactic:
obtain ⟨rfl⟩ := (sigmaι_eq_iff _ _ _ _ _).mp hy

Premises used: AlgebraicGeometry.sigmaι_eq_iff, Iff.mp, rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
h : i ≠ j
U : (∐ g).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι g j)
x : ↥(g i)
hx : Membership.mem (α := ↥(∐ g)) U ((Sigma.ι g i) x : ↥(∐ g))
y : ↥(g j)
hy : Eq (α := ↥(∐ g)) ((Sigma.ι g j) y : ↥(∐ g)) ((Sigma.ι g i) x : ↥(∐ g))
h₁ : i ≠ i
⊢ U ≤ Scheme.Hom.opensRange (Sigma.ι g i)

Tactic:
obtain ⟨rfl⟩ := (sigmaι_eq_iff _ _ _ _ _).mp hy

Premises used: AlgebraicGeometry.sigmaι_eq_iff, Iff.mp, rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
h : i ≠ j
U : (∐ g).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι g j)
x : ↥(g i)
hx : Membership.mem (α := ↥(∐ g)) U ((Sigma.ι g i) x : ↥(∐ g))
y : ↥(g j)
hy : Eq (α := ↥(∐ g)) ((Sigma.ι g j) y : ↥(∐ g)) ((Sigma.ι g i) x : ↥(∐ g))
h₁ : i ≠ i
hU'₁ : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
⊢ Eq (α := ↥(∐ g)) ((Sigma.ι g i) x : ↥(∐ g)) ((Sigma.ι g i) x : ↥(∐ g))

Tactic:
obtain ⟨rfl⟩ := (sigmaι_eq_iff _ _ _ _ _).mp hy

Premises used: AlgebraicGeometry.sigmaι_eq_iff, Iff.mp, rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i : σ
U : (∐ g).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
x : ↥(g i)
hx : Membership.mem (α := ↥(∐ g)) U ((Sigma.ι g i) x : ↥(∐ g))
h : i ≠ i
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
hy : Eq (α := ↥(∐ g)) ((Sigma.ι g i) x : ↥(∐ g)) ((Sigma.ι g i) x : ↥(∐ g))
⊢ Membership.mem (α := ↥(∐ g)) (γ := Opens ↥(∐ g)) ⊥ ((Sigma.ι g i) x : ↥(∐ g))

Tactic:
cases h rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq (Z := ∐ g) a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
⊢ IsEmpty.{u + 1} ↥Z

Tactic:
⟨fun z ↦ ?_⟩

Premises used: IsEmpty.mk
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq (Z := ∐ g) a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
refine : ∀ (z : ↥Z), False
⊢ IsEmpty.{u + 1} ↥Z

Tactic:
refine ⟨fun z ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq (Z := ∐ g) a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
z : ↥Z
x : ↥(∐ g)
a₁ :
  Membership.mem (α := ↥(∐ g)) (γ := Opens ↥(∐ g))
    (Scheme.Hom.opensRange (Sigma.ι g i) ⊓ Scheme.Hom.opensRange (Sigma.ι g j)) ((a ≫ Sigma.ι g i) z : ↥(∐ g))
⊢ False

Tactic:
fapply eq_bot_iff.mp <| disjoint_iff.mp <| disjoint_opensRange_sigmaι g i j hij

Premises used: disjoint_iff, AlgebraicGeometry.disjoint_opensRange_sigmaι, Iff.mp, eq_bot_iff
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq (Z := ∐ g) a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
z : ↥Z
⊢ ↥(∐ g)

Tactic:
exact (a ≫ Sigma.ι g i).base z

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Sigma.ι, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq (Z := ∐ g) a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
z : ↥Z
rw : Eq (α := ↥(∐ g)) ((b ≫ Sigma.ι g j) z : ↥(∐ g)) ((a ≫ Sigma.ι g i) z : ↥(∐ g))
rw₁ rw₂ : Eq (α := ↥(∐ g)) ((b ≫ Sigma.ι g j) z : ↥(∐ g)) ((b ≫ Sigma.ι g j) z : ↥(∐ g))
⊢ Eq (α := ↥(∐ g)) ((Sigma.ι g j) (b z : ↥(g j)) : ↥(∐ g)) ((a ≫ Sigma.ι g i) z : ↥(∐ g))

Tactic:
rw [← Scheme.Hom.comp_apply, h.w]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.CommSq.w
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
Z : Scheme
a : Z ⟶ g i
b : Z ⟶ g j
h : CommSq (Z := ∐ g) a b (Sigma.ι g i) (Sigma.ι g j)
hij : i ≠ j
z : ↥Z
⊢ Membership.mem (α := ↥(∐ g)) (γ := Opens ↥(∐ g))
    (Scheme.Hom.opensRange (Sigma.ι g i) ⊓ Scheme.Hom.opensRange (Sigma.ι g j)) ((a ≫ Sigma.ι g i) z : ↥(∐ g))

Tactic:
exact ⟨⟨a.base z, rfl⟩, ⟨b.base z, by rw [← Scheme.Hom.comp_apply, h.w]⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
σ : Type v
g : σ → Scheme
inst : Small.{u, v} σ
i j : σ
hij : i ≠ j
⊢ IsEmpty.{u + 1} ↥(pullback (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j))

Tactic:
isEmpty_of_commSq_sigmaι_of_ne ⟨pullback.condition⟩ hij

Premises used: AlgebraicGeometry.isEmpty_of_commSq_sigmaι_of_ne, CategoryTheory.CommSq.mk, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g_1 : σ → Scheme
inst : Small.{u, v} σ
g : σ → Scheme
⊢ CoproductDisjoint g

Tactic:
.of_hasCoproduct (fun _ ↦ pullback.cone _ _) (fun _ ↦ pullback.isLimit _ _) ?_

Premises used: CategoryTheory.Limits.CoproductDisjoint.of_hasCoproduct, CategoryTheory.Limits.Sigma.ι, CategoryTheory.Limits.pullback.isLimit, CategoryTheory.Limits.pullback.cone
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g_1 : σ → Scheme
inst : Small.{u, v} σ
g : σ → Scheme
refine :
  {i j : σ} →
    (hij : i ≠ j) →
      IsInitial (C := Scheme)
        (Cone.pt (J := WalkingCospan) (F := cospan (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j))
          ((fun {i j : σ} (x : i ≠ j) ↦
              (pullback.cone (Sigma.ι g i) (Sigma.ι g j) : PullbackCone (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j)))
            hij))
⊢ CoproductDisjoint g

Tactic:
refine .of_hasCoproduct (fun _ ↦ pullback.cone _ _) (fun _ ↦ pullback.isLimit _ _) ?_
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g_1 : σ → Scheme
inst : Small.{u, v} σ
g : σ → Scheme
i j : σ
hij : i ≠ j
h :
  Nonempty.{u + 2}
    (IsInitial (C := Scheme)
      (Cone.pt (J := WalkingCospan) (F := cospan (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j))
        ((fun {i j : σ} (x : i ≠ j) ↦
            (pullback.cone (Sigma.ι g i) (Sigma.ι g j) : PullbackCone (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j)))
          hij)))
⊢ IsInitial (C := Scheme)
    (Cone.pt (J := WalkingCospan) (F := cospan (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j))
      ((fun {i j : σ} (x : i ≠ j) ↦
          (pullback.cone (Sigma.ι g i) (Sigma.ι g j) : PullbackCone (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j)))
        hij))

Tactic:
apply Nonempty.some

Premises used: Nonempty.some
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g_1 : σ → Scheme
inst : Small.{u, v} σ
g : σ → Scheme
i j : σ
hij : i ≠ j
h :
  IsEmpty.{u + 1}
    ↥(Cone.pt (J := WalkingCospan) (F := cospan (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j))
        ((fun {i j : σ} (x : i ≠ j) ↦
            (pullback.cone (Sigma.ι g i) (Sigma.ι g j) : PullbackCone (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j)))
          hij))
⊢ Nonempty.{u + 2}
    (IsInitial (C := Scheme)
      (Cone.pt (J := WalkingCospan) (F := cospan (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j))
        ((fun {i j : σ} (x : i ≠ j) ↦
            (pullback.cone (Sigma.ι g i) (Sigma.ι g j) : PullbackCone (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j)))
          hij)))

Tactic:
rw [isInitial_iff_isEmpty]

Premises used: AlgebraicGeometry.isInitial_iff_isEmpty
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g_1 : σ → Scheme
inst : Small.{u, v} σ
g : σ → Scheme
i j : σ
hij : i ≠ j
⊢ IsEmpty.{u + 1}
    ↥(Cone.pt (J := WalkingCospan) (F := cospan (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j))
        ((fun {i j : σ} (x : i ≠ j) ↦
            (pullback.cone (Sigma.ι g i) (Sigma.ι g j) : PullbackCone (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j)))
          hij))

Tactic:
isEmpty_pullback_sigmaι_of_ne _ hij

Premises used: AlgebraicGeometry.isEmpty_pullback_sigmaι_of_ne
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g_1 : σ → Scheme
inst : Small.{u, v} σ
g : σ → Scheme
i j : σ
hij : i ≠ j
⊢ IsEmpty.{u + 1}
    ↥(Cone.pt (J := WalkingCospan) (F := cospan (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j))
        ((fun {i j : σ} (x : i ≠ j) ↦
            (pullback.cone (Sigma.ι g i) (Sigma.ι g j) : PullbackCone (Z := ∐ g) (Sigma.ι g i) (Sigma.ι g j)))
          hij))

Tactic:
exact isEmpty_pullback_sigmaι_of_ne _ hij

Premises used: AlgebraicGeometry.isEmpty_pullback_sigmaι_of_ne
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
⊢ MonoCoprod Scheme

Tactic:
.mk' fun X Y ↦ ⟨.mk coprod.inl coprod.inr, coprodIsCoprod X Y, inferInstanceAs <| Mono coprod.inl⟩

Premises used: CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.Limits.coprod.inl, CategoryTheory.Limits.BinaryCofan.mk, CategoryTheory.Limits.MonoCoprod.mk', Exists.intro, CategoryTheory.Limits.coprod.inr, _private.0.AlgebraicGeometry.instMonoCoprodScheme._proof_1
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
i : ι
x : ↥(f i)
change :
  Eq (α := (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (Y :=
            Scheme.forgetToTop.obj (∐ f))
            (CategoryStruct.comp (Y :=
              Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
                (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
              (Cofan.inj (f := fun (x : ι) ↦ (f x).toTopCat) (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) i :
                (f i).toTopCat ⟶
                  Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
                    (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
              (CategoryStruct.comp (Y := colimit (J := Discrete ι) (Discrete.functor fun (x : ι) ↦ (f x).toTopCat))
                  (Iso.inv
                    (colimit.isoColimitCocone
                      { cocone := TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat,
                        isColimit := TopCat.sigmaCofanIsColimit fun (x : ι) ↦ (f x).toTopCat }))
                  (Iso.hom (Iso.symm (PreservesCoproduct.iso Scheme.forgetToTop f))) :
                Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
                    (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) ⟶
                  Scheme.forgetToTop.obj (∐ f))) :
          (a : (↑(f i).toTopCat : Type u)) → (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
        x :
      (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (Y :=
            Scheme.forgetToTop.obj (∐ f)) (Scheme.forgetToTop.map (Sigma.ι f i)) :
          (a : (↑(Scheme.forgetToTop.obj (f i)) : Type u)) → (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
        x :
      (↑(Scheme.forgetToTop.obj (∐ f)) : Type u))
⊢ Eq (α := ↥(∐ f)) ((sigmaMk f : (a : (i : ι) × ↥(f i)) → ↥(∐ f)) (Sigma.mk (β := fun (i : ι) ↦ ↥(f i)) i x) : ↥(∐ f))
    ((Sigma.ι f i) x : ↥(∐ f))

Tactic:
change ((TopCat.sigmaCofan (fun x ↦ (f x).toTopCat)).inj i ≫
    (colimit.isoColimitCocone ⟨_, TopCat.sigmaCofanIsColimit _⟩).inv ≫ _) x =
      Scheme.forgetToTop.map (Sigma.ι f i) x

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone, TopCat.sigmaCofan, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Sigma.ι, AlgebraicGeometry.LocallyRingedSpace.toTopCat, AlgebraicGeometry.Scheme.forgetToTop, CategoryTheory.Functor.map, TopCat.sigmaCofanIsColimit, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.Cofan.inj, CategoryTheory.CategoryStruct.comp, DFunLike.coe, CategoryTheory.Iso.inv, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
i : ι
x : ↥(f i)
⊢ Eq (α := (f i).toTopCat ⟶ Scheme.forgetToTop.obj (∐ f))
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
        (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
      (Cofan.inj (f := fun (x : ι) ↦ (f x).toTopCat) (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) i :
        (f i).toTopCat ⟶
          Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
            (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
      (CategoryStruct.comp (Y := colimit (J := Discrete ι) (Discrete.functor fun (x : ι) ↦ (f x).toTopCat))
          (Iso.inv
            (colimit.isoColimitCocone
              { cocone := TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat,
                isColimit := TopCat.sigmaCofanIsColimit fun (x : ι) ↦ (f x).toTopCat }))
          (Iso.hom (Iso.symm (PreservesCoproduct.iso Scheme.forgetToTop f))) :
        Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
            (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) ⟶
          Scheme.forgetToTop.obj (∐ f)))
    (Scheme.forgetToTop.map (Sigma.ι f i))

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

Premises used: AlgebraicGeometry.LocallyRingedSpace.toTopCat, CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv_assoc, TopCat.sigmaCofanIsColimit, CategoryTheory.Limits.ColimitCocone.mk, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
i : ι
x : ↥(f i)
e_a :
  Eq (α :=
    Functor.obj (Discrete.functor fun (x : ι) ↦ (f x).toTopCat) { as := i : Discrete ι } ⟶ Scheme.forgetToTop.obj (∐ f))
    (CategoryStruct.comp (Y := colimit (J := Discrete ι) (Discrete.functor fun (x : ι) ↦ (f x).toTopCat))
      (colimit.ι (Discrete.functor fun (x : ι) ↦ (f x).toTopCat) { as := i })
      (Iso.hom (Iso.symm (PreservesCoproduct.iso Scheme.forgetToTop f))))
    (Scheme.forgetToTop.map (Sigma.ι f i))
⊢ Eq (α := (f i).toTopCat ⟶ Scheme.forgetToTop.obj (∐ f))
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
        (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
      (Cofan.inj (f := fun (x : ι) ↦ (f x).toTopCat) (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) i :
        (f i).toTopCat ⟶
          Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
            (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat))
      (CategoryStruct.comp (Y := colimit (J := Discrete ι) (Discrete.functor fun (x : ι) ↦ (f x).toTopCat))
          (Iso.inv
            (colimit.isoColimitCocone
              { cocone := TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat,
                isColimit := TopCat.sigmaCofanIsColimit fun (x : ι) ↦ (f x).toTopCat }))
          (Iso.hom (Iso.symm (PreservesCoproduct.iso Scheme.forgetToTop f))) :
        Cocone.pt (J := Discrete ι) (F := Discrete.functor fun (x : ι) ↦ (f x).toTopCat)
            (TopCat.sigmaCofan fun (x : ι) ↦ (f x).toTopCat) ⟶
          Scheme.forgetToTop.obj (∐ f)))
    (Scheme.forgetToTop.map (Sigma.ι f i))

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

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv_assoc, TopCat.sigmaCofanIsColimit, CategoryTheory.Limits.ColimitCocone.mk, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
i : ι
x : ↥(f i)
⊢ Eq (α :=
    Functor.obj (Discrete.functor fun (x : ι) ↦ (f x).toTopCat) { as := i : Discrete ι } ⟶ Scheme.forgetToTop.obj (∐ f))
    (CategoryStruct.comp (Y := colimit (J := Discrete ι) (Discrete.functor fun (x : ι) ↦ (f x).toTopCat))
      (colimit.ι (Discrete.functor fun (x : ι) ↦ (f x).toTopCat) { as := i })
      (Iso.hom (Iso.symm (PreservesCoproduct.iso Scheme.forgetToTop f))))
    (Scheme.forgetToTop.map (Sigma.ι f i))

Tactic:
ι_comp_sigmaComparison Scheme.forgetToTop _ _

Premises used: CategoryTheory.Limits.ι_comp_sigmaComparison, AlgebraicGeometry.LocallyRingedSpace.toTopCat, AlgebraicGeometry.Scheme.forgetToTop
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
i : ι
x : ↥(f i)
⊢ Eq (α :=
    Functor.obj (Discrete.functor fun (x : ι) ↦ (f x).toTopCat) { as := i : Discrete ι } ⟶ Scheme.forgetToTop.obj (∐ f))
    (CategoryStruct.comp (Y := colimit (J := Discrete ι) (Discrete.functor fun (x : ι) ↦ (f x).toTopCat))
      (colimit.ι (Discrete.functor fun (x : ι) ↦ (f x).toTopCat) { as := i })
      (Iso.hom (Iso.symm (PreservesCoproduct.iso Scheme.forgetToTop f))))
    (Scheme.forgetToTop.map (Sigma.ι f i))

Tactic:
exact ι_comp_sigmaComparison Scheme.forgetToTop _ _

Premises used: CategoryTheory.Limits.ι_comp_sigmaComparison, AlgebraicGeometry.Scheme.forgetToTop
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
rw :
  Topology.IsOpenEmbedding (X := ↥(∐ f)) (Y := ↥X) ⇑(Sigma.desc α) ∧
    ∀ (x : ↥(∐ f)), IsIso (X := X.presheaf.stalk ((Sigma.desc α) x)) (Scheme.Hom.stalkMap (Sigma.desc α) x)
⊢ IsOpenImmersion (X := ∐ f) (Sigma.desc α)

Tactic:
rw [IsOpenImmersion.iff_isIso_stalkMap]

Premises used: AlgebraicGeometry.IsOpenImmersion.iff_isIso_stalkMap
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
left : Topology.IsOpenEmbedding (X := ↥(∐ f)) (Y := ↥X) ⇑(Sigma.desc α)
right : ∀ (x : ↥(∐ f)), IsIso (X := X.presheaf.stalk ((Sigma.desc α) x)) (Scheme.Hom.stalkMap (Sigma.desc α) x)
⊢ Topology.IsOpenEmbedding (X := ↥(∐ f)) (Y := ↥X) ⇑(Sigma.desc α) ∧
    ∀ (x : ↥(∐ f)), IsIso (X := X.presheaf.stalk ((Sigma.desc α) x)) (Scheme.Hom.stalkMap (Sigma.desc α) x)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
this :
  Topology.IsOpenEmbedding (X := (i : ι) × ↥(f i)) (Y := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
⊢ Topology.IsOpenEmbedding (X := ↥(∐ f)) (Y := ↥X)
    (Function.comp (β := (i : ι) × ↥(f i))
      (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
      (⇑(sigmaMk f).symm : (a : ↥(∐ f)) → (i : ι) × ↥(f i)))

Tactic:
this.comp (sigmaMk f).symm.isOpenEmbedding

Premises used: AlgebraicGeometry.sigmaMk, Homeomorph.symm, Homeomorph.isOpenEmbedding, Topology.IsOpenEmbedding.comp
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
this :
  Topology.IsOpenEmbedding (X := (i : ι) × ↥(f i)) (Y := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
h :
  Eq (α := ↥(∐ f) → ↥X) (⇑(Sigma.desc α))
    (Function.comp (β := (i : ι) × ↥(f i))
      (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
      (⇑(sigmaMk f).symm : (a : ↥(∐ f)) → (i : ι) × ↥(f i)))
⊢ Topology.IsOpenEmbedding (X := ↥(∐ f)) (Y := ↥X) ⇑(Sigma.desc α)

Tactic:
convert! this.comp (sigmaMk f).symm.isOpenEmbedding

Premises used: AlgebraicGeometry.sigmaMk, Homeomorph.symm, Homeomorph.isOpenEmbedding, Topology.IsOpenEmbedding.comp
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
this :
  Topology.IsOpenEmbedding (X := (i : ι) × ↥(f i)) (Y := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
h :
  ∀ (x : ↥(∐ f)),
    Eq (α := ↥X) ((Sigma.desc α) x : ↥X)
      (Function.comp (β := (i : ι) × ↥(f i))
          (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
          (⇑(sigmaMk f).symm : (a : ↥(∐ f)) → (i : ι) × ↥(f i)) x :
        ↥X)
⊢ Eq (α := ↥(∐ f) → ↥X) (⇑(Sigma.desc α))
    (Function.comp (β := (i : ι) × ↥(f i))
      (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
      (⇑(sigmaMk f).symm : (a : ↥(∐ f)) → (i : ι) × ↥(f i)))

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
this :
  Topology.IsOpenEmbedding (X := (i : ι) × ↥(f i)) (Y := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
x : ↥(∐ f)
⊢ Eq (α := ↥X) ((Sigma.desc α) x : ↥X)
    (Function.comp (β := (i : ι) × ↥(f i))
        (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
        (⇑(sigmaMk f).symm : (a : ↥(∐ f)) → (i : ι) × ↥(f i)) x :
      ↥X)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
left :
  Topology.IsOpenEmbedding (X := (i : ι) × ↥(f i)) (Y := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))
⊢ Topology.IsOpenEmbedding (X := ↥(∐ f)) (Y := ↥X) ⇑(Sigma.desc α)

Tactic:
suffices Topology.IsOpenEmbedding (Sigma.desc α ∘ sigmaMk f) by
      convert! this.comp (sigmaMk f).symm.isOpenEmbedding; ext; simp
-- Module: Mathlib.AlgebraicGeometry.Limits
Goal:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise.{u} (α := ι) (Function.onFun (β := Set ↥X) Disjoint fun (x : ι) ↦ Set.range (ι := ↥(f x)) ⇑(α x))
⊢ Topology.IsOpenEmbedding (X := (i : ι) × ↥(f i)) (Y := ↥X)
    (Function.comp (β := ↥(∐ f)) ⇑(Sigma.desc α) (⇑(sigmaMk f) : (a : (i : ι) × ↥(f i)) → ↥(∐ f)))

Tactic:
.of_continuous_injective_isOpenMap ?_ ?_ ?_

Premises used: Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap