awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
i : Discrete ι
rw :
  IsOpenEmbedding (X := (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)) (Y :=
    (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Y := (↑(colimit F).toPresheafedSpace : TopCat))
          (CategoryStruct.comp (Y := colimit (F ⋙ forget C))
            (colimit.ι (F ⋙ forget C) i : (F ⋙ forget C).obj i ⟶ colimit (F ⋙ forget C))
            (Iso.inv (preservesColimitIso (forget C) F) :
              colimit (F ⋙ forget C) ⟶ Functor.obj (forget C) (colimit F)))) :
      (a : (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)) → (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))
⊢ IsOpenEmbedding (X := (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)) (Y :=
    (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Y := (↑(colimit F).toPresheafedSpace : TopCat))
          (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι F i)))) :
      (a : (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)) → (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))

Tactic:
rw [← show _ = (colimit.ι F i).hom.base from
    ι_preservesColimitIso_inv (SheafedSpace.forget C) F i]

Premises used: AlgebraicGeometry.SheafedSpace.forget, CategoryTheory.ι_preservesColimitIso_inv
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
i : Discrete ι
⊢ Eq (α := (F ⋙ forget C).obj i ⟶ colimit (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)))
    (CategoryStruct.comp (Y := colimit (F ⋙ forget C)) (colimit.ι (F ⋙ forget C) i)
      (Iso.hom (HasColimit.isoOfNatIso Discrete.natIsoFunctor)))
    (NatTrans.app (Iso.hom Discrete.natIsoFunctor) i ≫
      colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i)

Tactic:
have : _ = _ ≫ colimit.ι (Discrete.functor ((F ⋙ SheafedSpace.forget C).obj ∘ Discrete.mk)) i :=
    HasColimit.isoOfNatIso_ι_hom Discrete.natIsoFunctor i
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
i : Discrete ι
this :
  Eq (α := (F ⋙ forget C).obj i ⟶ colimit (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)))
    (CategoryStruct.comp (Y := colimit (F ⋙ forget C)) (colimit.ι (F ⋙ forget C) i)
      (Iso.hom (HasColimit.isoOfNatIso Discrete.natIsoFunctor)))
    (NatTrans.app (Iso.hom Discrete.natIsoFunctor) i ≫
      colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i)
⊢ Eq (α := (F ⋙ forget C).obj i ⟶ colimit (F ⋙ forget C)) (colimit.ι (F ⋙ forget C) i)
    (CategoryStruct.comp (Y := colimit (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)))
      (NatTrans.app (Iso.hom Discrete.natIsoFunctor) i ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i)
      (Iso.inv (HasColimit.isoOfNatIso Discrete.natIsoFunctor)))

Tactic:
rw [← Iso.eq_comp_inv] at this

Premises used: CategoryTheory.Iso.eq_comp_inv
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
i : Discrete ι
this :
  Eq (α := (F ⋙ forget C).obj i ⟶ colimit (F ⋙ forget C)) (colimit.ι (F ⋙ forget C) i)
    (CategoryStruct.comp (Y := colimit (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)))
      (NatTrans.app (Iso.hom Discrete.natIsoFunctor) i ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i)
      (Iso.inv (HasColimit.isoOfNatIso Discrete.natIsoFunctor)))
rw :
  IsOpenEmbedding (X := (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)) (Y :=
    (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X := (↑(F.obj i).toPresheafedSpace : TopCat)) (Y := (↑(colimit F).toPresheafedSpace : TopCat))
            (CategoryStruct.comp (Y := colimit (F ⋙ forget C))
                (CategoryStruct.comp (Y := colimit (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)))
                    (NatTrans.app (Iso.hom Discrete.natIsoFunctor) i ≫
                      colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i)
                    (Iso.inv (HasColimit.isoOfNatIso Discrete.natIsoFunctor)) :
                  (F ⋙ forget C).obj i ⟶ colimit (F ⋙ forget C))
                (Iso.inv (preservesColimitIso (forget C) F) :
                  colimit (F ⋙ forget C) ⟶ Functor.obj (forget C) (colimit F)) :
              (F ⋙ forget C).obj i ⟶ Functor.obj (forget C) (colimit F)) :
          C((↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v),
            (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))) :
      (a : (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)) → (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))
⊢ IsOpenEmbedding (X := (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)) (Y :=
    (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Y := (↑(colimit F).toPresheafedSpace : TopCat))
          (CategoryStruct.comp (Y := colimit (F ⋙ forget C))
            (colimit.ι (F ⋙ forget C) i : (F ⋙ forget C).obj i ⟶ colimit (F ⋙ forget C))
            (Iso.inv (preservesColimitIso (forget C) F) :
              colimit (F ⋙ forget C) ⟶ Functor.obj (forget C) (colimit F)))) :
      (a : (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)) → (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))

Tactic:
rw [this]
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
i : Discrete ι
this :
  Eq (α := (F ⋙ forget C).obj i ⟶ colimit (F ⋙ forget C)) (colimit.ι (F ⋙ forget C) i)
    (CategoryStruct.comp (Y := colimit (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)))
      (NatTrans.app (Iso.hom Discrete.natIsoFunctor) i ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i)
      (Iso.inv (HasColimit.isoOfNatIso Discrete.natIsoFunctor)))
⊢ Eq (α :=
    Functor.obj (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := i.as : Discrete ι } ⟶
      TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v)))
    (colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := i.as } ≫
      (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom)
    (TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) i.as)

Tactic:
have : colimit.ι _ _ ≫ _ = _ :=
    TopCat.sigmaIsoSigma_hom_ι.{v, v} ((F ⋙ SheafedSpace.forget C).obj ∘ Discrete.mk) i.as
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
i : Discrete ι
this_1 :
  Eq (α := (F ⋙ forget C).obj i ⟶ colimit (F ⋙ forget C)) (colimit.ι (F ⋙ forget C) i)
    (CategoryStruct.comp (Y := colimit (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)))
      (NatTrans.app (Iso.hom Discrete.natIsoFunctor) i ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) i)
      (Iso.inv (HasColimit.isoOfNatIso Discrete.natIsoFunctor)))
this :
  Eq (α :=
    Functor.obj (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := i.as : Discrete ι } ⟶
      TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v)))
    (colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := i.as } ≫
      (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom)
    (TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) i.as)
⊢ Eq (α :=
    Functor.obj (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := i.as : Discrete ι } ⟶
      colimit (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)))
    (colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := i.as })
    (TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) i.as ≫
      (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv)

Tactic:
rw [← Iso.eq_comp_inv] at this

Premises used: CategoryTheory.Iso.eq_comp_inv
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
as : ι
this_1 :
  Eq (α := (F ⋙ forget C).obj { as := as : Discrete ι } ⟶ colimit (F ⋙ forget C))
    (colimit.ι (F ⋙ forget C) { as := as })
    (CategoryStruct.comp (Y := colimit (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)))
      (NatTrans.app (Iso.hom Discrete.natIsoFunctor) { as := as : Discrete ι } ≫
        colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as })
      (Iso.inv (HasColimit.isoOfNatIso Discrete.natIsoFunctor)))
this :
  Eq (α :=
    Functor.obj (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk))
        { as := { as := as : Discrete ι }.as : Discrete ι } ⟶
      colimit (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)))
    (colimit.ι (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := { as := as }.as })
    (TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) { as := as }.as ≫
      (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).inv)
⊢ IsOpenEmbedding (X :=
    (↑(Functor.obj (Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)) { as := as : Discrete ι }) : Type v)) (Y :=
    (i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) as)) :
      (a : (↑((Discrete.functor ((F ⋙ forget C).obj ∘ Discrete.mk)).obj { as := as }) : Type v)) →
        (i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))

Tactic:
exact .sigmaMk
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
i j : Discrete ι
h : i ≠ j
U : Opens (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)
h₁ :
  ∀ (x : (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v)),
    x ∈
        (↑(Functor.obj (C := Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
              (Opens.map (PresheafedSpace.Hom.base (colimit.ι (F ⋙ forgetToPresheafedSpace) j)) :
                Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v) ⥤
                  Opens (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v))
              (Functor.obj (C := Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v))
                  (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
                    Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                      Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
                  (Functor.obj (IsOpenEmbedding.functor ⋯) U) :
                Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))) :
          Set (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v)) ↔
      x ∈ (↑⊥ : Set (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v))
⊢ Functor.obj (C := Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
      (Opens.map (PresheafedSpace.Hom.base (colimit.ι (F ⋙ forgetToPresheafedSpace) j)) :
        Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v) ⥤
          Opens (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v))
      (Functor.obj (C := Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v))
          (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
            Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
              Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
          (Functor.obj (IsOpenEmbedding.functor ⋯) U) :
        Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v)) =
    ⊥

Tactic:
ext x
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
i j : Discrete ι
h : i ≠ j
U : Opens (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)
x : (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v)
h₁ :
  x ∉
    (↑(Functor.obj (C := Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
          (Opens.map (PresheafedSpace.Hom.base (colimit.ι (F ⋙ forgetToPresheafedSpace) j)) :
            Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v) ⥤
              Opens (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v))
          (Functor.obj (C := Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v))
              (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
                Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                  Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
              (Functor.obj (IsOpenEmbedding.functor ⋯) U) :
            Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))) :
      Set (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v))
⊢ x ∈
      (↑(Functor.obj (C := Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
            (Opens.map (PresheafedSpace.Hom.base (colimit.ι (F ⋙ forgetToPresheafedSpace) j)) :
              Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v) ⥤
                Opens (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v))
            (Functor.obj (C := Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v))
                (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
                  Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                    Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
                (Functor.obj (IsOpenEmbedding.functor ⋯) U) :
              Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))) :
        Set (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v)) ↔
    x ∈ (↑⊥ : Set (↑(↑((F ⋙ forgetToPresheafedSpace).obj j) : TopCat) : Type v))

Tactic:
apply iff_false_intro

Premises used: iff_false_intro
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
as : ι
U : Opens (↑(↑(F.obj { as := as : Discrete ι }).toPresheafedSpace : TopCat) : Type v)
y : (↑(↑(F.obj { as := as : Discrete ι }).toPresheafedSpace : TopCat) : Type v)
hy : y ∈ (↑U : Set (↑(↑(F.obj { as := as }).toPresheafedSpace : TopCat) : Type v))
as_1 : ι
x : (↑(↑((F ⋙ forgetToPresheafedSpace).obj { as := as_1 : Discrete ι }) : TopCat) : Type v)
h : { as := as : Discrete ι } ≠ { as := as_1 }
eq :
  Eq (α := (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : Type v))
    (((@ConcreteCategory.hom _ TopCat.instCategory (fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v)))
              TopCat.carrier _ _ (Functor.obj (forget C) (F.obj { as := as : Discrete ι }))
              (TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v)))
              (NatTrans.app (Iso.hom Discrete.natIsoFunctor) { as := as } ≫
                  TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) as :
                (F ⋙ forget C).obj { as := as : Discrete ι } ⟶
                  TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) :
            C((↑(Functor.obj (forget C) (F.obj { as := as : Discrete ι })) : Type v),
              (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : Type v))) :
          (a : (↑((forget C).obj (F.obj { as := as })) : Type v)) →
            (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : Type v))
        y :
      (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : Type v))
    (((@ConcreteCategory.hom _ TopCat.instCategory (fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v)))
              TopCat.carrier _ _ (Functor.obj (forget C) (F.obj { as := as_1 : Discrete ι }))
              (TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v)))
              (NatTrans.app (Iso.hom Discrete.natIsoFunctor) { as := as_1 } ≫
                  TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) as_1 :
                (F ⋙ forget C).obj { as := as_1 : Discrete ι } ⟶
                  TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) :
            C((↑(Functor.obj (forget C) (F.obj { as := as_1 : Discrete ι })) : Type v),
              (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : Type v))) :
          (a : (↑((forget C).obj (F.obj { as := as_1 })) : Type v)) →
            (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : Type v))
        x :
      (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : Type v))
⊢ False

Tactic:
h (congr_arg Discrete.mk (congr_arg Sigma.fst eq))

Premises used: Sigma.fst, CategoryTheory.Discrete.mk, congr_arg
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
as : ι
U : Opens (↑(↑(F.obj { as := as : Discrete ι }).toPresheafedSpace : TopCat) : Type v)
y : (↑(↑(F.obj { as := as : Discrete ι }).toPresheafedSpace : TopCat) : Type v)
hy : y ∈ (↑U : Set (↑(↑(F.obj { as := as }).toPresheafedSpace : TopCat) : Type v))
as_1 : ι
x : (↑(↑((F ⋙ forgetToPresheafedSpace).obj { as := as_1 : Discrete ι }) : TopCat) : Type v)
h : { as := as : Discrete ι } ≠ { as := as_1 }
eq :
  Eq (α := (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : Type v))
    (((@ConcreteCategory.hom _ TopCat.instCategory (fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v)))
              TopCat.carrier _ _ (Functor.obj (forget C) (F.obj { as := as : Discrete ι }))
              (TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v)))
              (NatTrans.app (Iso.hom Discrete.natIsoFunctor) { as := as } ≫
                  TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) as :
                (F ⋙ forget C).obj { as := as : Discrete ι } ⟶
                  TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) :
            C((↑(Functor.obj (forget C) (F.obj { as := as : Discrete ι })) : Type v),
              (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : Type v))) :
          (a : (↑((forget C).obj (F.obj { as := as })) : Type v)) →
            (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : Type v))
        y :
      (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : Type v))
    (((@ConcreteCategory.hom _ TopCat.instCategory (fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v)))
              TopCat.carrier _ _ (Functor.obj (forget C) (F.obj { as := as_1 : Discrete ι }))
              (TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v)))
              (NatTrans.app (Iso.hom Discrete.natIsoFunctor) { as := as_1 } ≫
                  TopCat.sigmaι ((F ⋙ forget C).obj ∘ Discrete.mk) as_1 :
                (F ⋙ forget C).obj { as := as_1 : Discrete ι } ⟶
                  TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) :
            C((↑(Functor.obj (forget C) (F.obj { as := as_1 : Discrete ι })) : Type v),
              (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : Type v))) :
          (a : (↑((forget C).obj (F.obj { as := as_1 })) : Type v)) →
            (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : Type v))
        x :
      (↑(TopCat.of ((i : ι) × (↑(((F ⋙ forget C).obj ∘ Discrete.mk) i) : Type v))) : Type v))
⊢ False

Tactic:
convert! h (congr_arg Discrete.mk (congr_arg Sigma.fst eq))

Premises used: Sigma.fst, CategoryTheory.Discrete.mk, congr_arg
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
i : Discrete ι
inst_3 : HasStrictTerminalObjects.{v, u} C
U : Opens (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)
⊢ Eq (α := (F ⋙ forgetToPresheafedSpace).obj i ⟶ Functor.obj forgetToPresheafedSpace (colimit F))
    (CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
      (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
        (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
      (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
        colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)))
    (CategoryTheory.Functor.map forgetToPresheafedSpace (colimit.ι F i))

Tactic:
have h₁ := ι_preservesColimitIso_inv SheafedSpace.forgetToPresheafedSpace F i
-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
i : Discrete ι
inst_3 : HasStrictTerminalObjects.{v, u} C
U : Opens (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)
h₁ :
  Eq (α := (F ⋙ forgetToPresheafedSpace).obj i ⟶ Functor.obj forgetToPresheafedSpace (colimit F))
    (CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
      (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
        (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
      (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
        colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)))
    (CategoryTheory.Functor.map forgetToPresheafedSpace (colimit.ι F i))
⊢ Eq (α := F.obj i ⟶ colimit F) (colimit.ι F i)
    {
      hom :=
        CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
          (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
            (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
          (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
            colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)) }

Tactic:
have h₂ : colimit.ι F i =
      { hom := (colimit.ι (F ⋙ forgetToPresheafedSpace) i ≫
        (preservesColimitIso _ F).inv) } :=
      InducedCategory.hom_ext h₁.symm