awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this :
  Eq (α := (pullback g f).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan g f)) :
        Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
      (limit.π (cospan g f ⋙ forget) left : limit (cospan g f ⋙ forget) ⟶ (cospan g f ⋙ forget).obj left))
    (InducedCategory.Hom.hom (pullback.fst g f))
⊢ PresheafedSpace.IsOpenImmersion (X := (pullback g f).toPresheafedSpace) (InducedCategory.Hom.hom (pullback.fst g f))
have rw : PresheafedSpace.IsOpenImmersion (X := (pullback g f).toPresheafedSpace)
  (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
    (Iso.hom (preservesLimitIso forget (cospan g f)) :
      Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
    (limit.π (cospan g f ⋙ forget) left : limit (cospan g f ⋙ forget) ⟶ (cospan g f ⋙ forget).obj left))
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this :
  Eq (α := (pullback g f).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan g f)) :
        Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
      (limit.π (cospan g f ⋙ forget) left : limit (cospan g f ⋙ forget) ⟶ (cospan g f ⋙ forget).obj left))
    (InducedCategory.Hom.hom (pullback.fst g f))
⊢ PresheafedSpace.IsOpenImmersion (X := (pullback g f).toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan g f)) :
        Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
      (limit.π (cospan g f ⋙ forget) left : limit (cospan g f ⋙ forget) ⟶ (cospan g f ⋙ forget).obj left))
have this₁ : Eq (α :=
  limit (cospan g f ⋙ forget) ⟶
    (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr)).obj left)
  (CategoryStruct.comp (Y := limit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr)))
    (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget))))
    (limit.π (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr)) left))
  (limit.π (cospan g f ⋙ forget) left ≫ (diagramIsoCospan (cospan g f ⋙ forget)).hom.app left)
Tactic: have := HasLimit.isoOfNatIso_hom_π (diagramIsoCospan (cospan g f ⋙ forget)) left
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this_1 :
  Eq (α := (pullback g f).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan g f)) :
        Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
      (limit.π (cospan g f ⋙ forget) left : limit (cospan g f ⋙ forget) ⟶ (cospan g f ⋙ forget).obj left))
    (InducedCategory.Hom.hom (pullback.fst g f))
this :
  Eq (α := limit (cospan g f ⋙ forget) ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g.hom f.hom))
      (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget)))) (limit.π (cospan g.hom f.hom) left))
    (limit.π (cospan g f ⋙ forget) left ≫ 𝟙 Y.toPresheafedSpace)
⊢ PresheafedSpace.IsOpenImmersion (X := (pullback g f).toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan g f)) :
        Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
      (limit.π (cospan g f ⋙ forget) left : limit (cospan g f ⋙ forget) ⟶ (cospan g f ⋙ forget).obj left))
have this₁ : Eq (α := limit (cospan g f ⋙ forget) ⟶ Y.toPresheafedSpace)
  (CategoryStruct.comp (Y := limit (cospan g.hom f.hom))
    (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget)))) (limit.π (cospan g.hom f.hom) left))
  (limit.π (cospan g f ⋙ forget) left)
Tactic: rw [Category.comp_id] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
this_1 :
  Eq (α := (pullback g f).toPresheafedSpace ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan g f)) :
        Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
      (limit.π (cospan g f ⋙ forget) left : limit (cospan g f ⋙ forget) ⟶ (cospan g f ⋙ forget).obj left))
    (InducedCategory.Hom.hom (pullback.fst g f))
this :
  Eq (α := limit (cospan g f ⋙ forget) ⟶ Y.toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g.hom f.hom))
      (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget)))) (limit.π (cospan g.hom f.hom) left))
    (limit.π (cospan g f ⋙ forget) left)
⊢ PresheafedSpace.IsOpenImmersion (X := (pullback g f).toPresheafedSpace)
    (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
      (Iso.hom (preservesLimitIso forget (cospan g f)) :
        Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
      (limit.π (cospan g f ⋙ forget) left : limit (cospan g f ⋙ forget) ⟶ (cospan g f ⋙ forget).obj left))
have rw : PresheafedSpace.IsOpenImmersion (X := (pullback g f).toPresheafedSpace)
  (CategoryStruct.comp (Y := limit (cospan g f ⋙ forget))
    (Iso.hom (preservesLimitIso forget (cospan g f)) :
      Functor.obj forget (limit (cospan g f)) ⟶ limit (cospan g f ⋙ forget))
    (CategoryStruct.comp (Y := limit (cospan g.hom f.hom))
        (Iso.hom (HasLimit.isoOfNatIso (diagramIsoCospan (cospan g f ⋙ forget)))) (limit.π (cospan g.hom f.hom) left) :
      limit (cospan g f ⋙ forget) ⟶ Y.toPresheafedSpace))
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : SheafedSpace.{u, v, u_1} C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) one)
have rw : IsOpenImmersion (X := limit (cospan f g)) (limit.π (cospan f g) left ≫ f)
Tactic: rw [← limit.w (cospan f g) Hom.inl, cospan_map_inl]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
inst_2 : HasColimits.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst_3 : (X Y : C) → FunLike.{u_1 + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC (CC := CC)
inst_4 : Functor.ReflectsIsomorphisms (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimits (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_6 : PreservesFilteredColimits (CategoryTheory.forget C (FC := FC) (CC := CC))
X Y : SheafedSpace.{u, v, v} C
f : X ⟶ Y
hf :
  IsOpenEmbedding (X := (↑(↑X.toPresheafedSpace : TopCat) : Type v)) (Y := (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          f.hom.base) :
      (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
H :
  ∀ (x : (↑(↑X.toPresheafedSpace : TopCat) : Type v)),
    IsIso (X :=
      Y.presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              f.hom.base :
            (a : (↑(↑X.toPresheafedSpace : TopCat) : Type v)) → (↑(↑Y.toPresheafedSpace : TopCat) : Type v))
          x))
      (PresheafedSpace.Hom.stalkMap f.hom x)
U : Opens (↑(↑X.toPresheafedSpace : TopCat) : Type v)
⊢ IsIso (X := Y.presheaf.obj (op (hf.functor.obj U))) (f.hom.c.app (op (hf.functor.obj U)))
have inst : ∀ (x : ↥(hf.functor.obj U)),
  IsIso (X :=
    Functor.obj (TopCat.Presheaf.stalkFunctor C (↑x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
      (Y.sheaf.obj (P := Presheaf.IsSheaf (Opens.grothendieckTopology (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))))
    (Y :=
    Functor.obj (TopCat.Presheaf.stalkFunctor C (↑x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
      ((Functor.obj (TopCat.Sheaf.pushforward C f.hom.base) X.sheaf).obj (P :=
        Presheaf.IsSheaf (Opens.grothendieckTopology (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))))
    (CategoryTheory.Functor.map (TopCat.Presheaf.stalkFunctor C (↑x : (↑(↑Y.toPresheafedSpace : TopCat) : Type v)))
      (InducedCategory.Hom.hom
        (have this : Y.sheaf ⟶ Functor.obj (TopCat.Sheaf.pushforward C f.hom.base) X.sheaf := { hom := f.hom.c };
        this)))
Tactic: apply +allowSynthFailures TopCat.Presheaf.app_isIso_of_stalkFunctor_map_iso
          (show Y.sheaf ⟶ (TopCat.Sheaf.pushforward _ f.hom.base).obj X.sheaf from ⟨f.hom.c⟩)
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : SheafedSpace.{u, v, u_1} C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.hom.base
⊢ IsIso f
have this : IsIso (X := Functor.obj forgetToPresheafedSpace X) (CategoryTheory.Functor.map forgetToPresheafedSpace f)
Tactic: haveI : IsIso (forgetToPresheafedSpace.map f) := PresheafedSpace.IsOpenImmersion.to_iso f.hom
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
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 ι
⊢ 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))
have 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))
Tactic: rw [← show _ = (colimit.ι F i).hom.base from
    ι_preservesColimitIso_inv (SheafedSpace.forget C) F i]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
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 ι
⊢ 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))
have 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)
Tactic: have : _ = _ ≫ colimit.ι (Discrete.functor ((F ⋙ SheafedSpace.forget C).obj ∘ Discrete.mk)) i :=
    HasColimit.isoOfNatIso_ι_hom Discrete.natIsoFunctor i
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
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)
⊢ 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))
have 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)))
Tactic: rw [← Iso.eq_comp_inv] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (goal)
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)))
⊢ 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))
have 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))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
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)))
⊢ 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))
have 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)
Tactic: have : colimit.ι _ _ ≫ _ = _ :=
    TopCat.sigmaIsoSigma_hom_ι.{v, v} ((F ⋙ SheafedSpace.forget C).obj ∘ Discrete.mk) i.as
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.OpenImmersion (hypothesis)
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)
⊢ 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))
have this₁ : 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
Cleared hypotheses: this