awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
x y : (↑(↑(D.U i) : TopCat) : Type v)
h1 : y ∈ U
h2 :
  Eq (α := (↑(↑D.glued : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (Y :=
            (↑D.glued : TopCat)) (Hom.base (D.ι i)) :
          (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v))
        y :
      (↑(↑D.glued : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            (↑(D.diagram.multispan.obj (WalkingMultispan.right i)) : TopCat)) (Y :=
            (↑(Limits.colimit D.diagram.multispan) : TopCat))
            (Hom.base (colimit.ι D.diagram.multispan (WalkingMultispan.right i))) :
          (a : (↑(↑(D.diagram.multispan.obj (WalkingMultispan.right i)) : TopCat) : Type v)) →
            (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
        x :
      (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
h : x = y
⊢ x ∈ U

Tactic:
convert! h1 using 1
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
x y : (↑(↑(D.U i) : TopCat) : Type v)
h1 : y ∈ U
h2 :
  Eq (α := (↑(↑D.glued : TopCat) : Type v))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (↑(D.U i) : TopCat)) (Y := (↑D.glued : TopCat))
              (Hom.base (colimit.ι D.diagram.multispan (WalkingMultispan.right i)) :
                (↑(D.U i) : TopCat) ⟶ (↑D.glued : TopCat)) :
            C((↑(↑(D.U i) : TopCat) : Type v), (↑(↑D.glued : TopCat) : Type v))) :
          (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v))
        y :
      (↑(↑D.glued : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            (↑(D.diagram.multispan.obj (WalkingMultispan.right i)) : TopCat)) (Y :=
            (↑(Limits.colimit D.diagram.multispan) : TopCat))
            (Hom.base (colimit.ι D.diagram.multispan (WalkingMultispan.right i))) :
          (a : (↑(↑(D.diagram.multispan.obj (WalkingMultispan.right i)) : TopCat) : Type v)) →
            (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
        x :
      (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
h :
  Eq (α := (↑(↑D.glued : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (Y :=
            (↑D.glued : TopCat)) (Hom.base (D.ι i)) :
          (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v))
        x :
      (↑(↑D.glued : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (Y :=
            (↑D.glued : TopCat)) (Hom.base (D.ι i)) :
          (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v))
        y :
      (↑(↑D.glued : TopCat) : Type v))
h₁ :
  Function.Injective (α := (↑(↑(D.U i) : TopCat) : Type v)) (β := (↑(↑D.glued : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Y := (↑D.glued : TopCat)) (Hom.base (D.ι i))) :
      (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v))
⊢ x = y

Tactic:
apply_fun (D.ι _).base

Premises used: CategoryTheory.GlueData.ι, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
x y : (↑(↑(D.U i) : TopCat) : Type v)
h1 : y ∈ U
h2 :
  Eq (α := (↑(↑D.glued : TopCat) : Type v))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (↑(D.U i) : TopCat)) (Y := (↑D.glued : TopCat))
              (Hom.base (colimit.ι D.diagram.multispan (WalkingMultispan.right i)) :
                (↑(D.U i) : TopCat) ⟶ (↑D.glued : TopCat)) :
            C((↑(↑(D.U i) : TopCat) : Type v), (↑(↑D.glued : TopCat) : Type v))) :
          (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v))
        y :
      (↑(↑D.glued : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            (↑(D.diagram.multispan.obj (WalkingMultispan.right i)) : TopCat)) (Y :=
            (↑(Limits.colimit D.diagram.multispan) : TopCat))
            (Hom.base (colimit.ι D.diagram.multispan (WalkingMultispan.right i))) :
          (a : (↑(↑(D.diagram.multispan.obj (WalkingMultispan.right i)) : TopCat) : Type v)) →
            (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
        x :
      (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
⊢ Eq (α := (↑(↑D.glued : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (Y :=
            (↑D.glued : TopCat)) (Hom.base (D.ι i)) :
          (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v))
        x :
      (↑(↑D.glued : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (Y :=
            (↑D.glued : TopCat)) (Hom.base (D.ι i)) :
          (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v))
        y :
      (↑(↑D.glued : TopCat) : Type v))

Tactic:
exact h2.symm

Premises used: Eq.symm
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
x y : (↑(↑(D.U i) : TopCat) : Type v)
h1 : y ∈ U
h2 :
  Eq (α := (↑(↑D.glued : TopCat) : Type v))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (↑(D.U i) : TopCat)) (Y := (↑D.glued : TopCat))
              (Hom.base (colimit.ι D.diagram.multispan (WalkingMultispan.right i)) :
                (↑(D.U i) : TopCat) ⟶ (↑D.glued : TopCat)) :
            C((↑(↑(D.U i) : TopCat) : Type v), (↑(↑D.glued : TopCat) : Type v))) :
          (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v))
        y :
      (↑(↑D.glued : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            (↑(D.diagram.multispan.obj (WalkingMultispan.right i)) : TopCat)) (Y :=
            (↑(Limits.colimit D.diagram.multispan) : TopCat))
            (Hom.base (colimit.ι D.diagram.multispan (WalkingMultispan.right i))) :
          (a : (↑(↑(D.diagram.multispan.obj (WalkingMultispan.right i)) : TopCat) : Type v)) →
            (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
        x :
      (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
⊢ Eq (α := (D.mapGlueData (forget C)).U i ⟶ Functor.obj (forget C) D.glued)
    (CategoryStruct.comp (Y := (D.mapGlueData (forget C)).glued)
      ((D.mapGlueData (forget C)).ι i : (D.mapGlueData (forget C)).U i ⟶ (D.mapGlueData (forget C)).glued)
      (Iso.inv (D.gluedIso (forget C)) : (D.mapGlueData (forget C)).glued ⟶ Functor.obj (forget C) D.glued))
    (CategoryTheory.Functor.map (forget C) (D.ι i))

Tactic:
have := D.ι_gluedIso_inv (PresheafedSpace.forget _) i
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
x y : (↑(↑(D.U i) : TopCat) : Type v)
h1 : y ∈ U
h2 :
  Eq (α := (↑(↑D.glued : TopCat) : Type v))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (↑(D.U i) : TopCat)) (Y := (↑D.glued : TopCat))
              (Hom.base (colimit.ι D.diagram.multispan (WalkingMultispan.right i)) :
                (↑(D.U i) : TopCat) ⟶ (↑D.glued : TopCat)) :
            C((↑(↑(D.U i) : TopCat) : Type v), (↑(↑D.glued : TopCat) : Type v))) :
          (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v))
        y :
      (↑(↑D.glued : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            (↑(D.diagram.multispan.obj (WalkingMultispan.right i)) : TopCat)) (Y :=
            (↑(Limits.colimit D.diagram.multispan) : TopCat))
            (Hom.base (colimit.ι D.diagram.multispan (WalkingMultispan.right i))) :
          (a : (↑(↑(D.diagram.multispan.obj (WalkingMultispan.right i)) : TopCat) : Type v)) →
            (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
        x :
      (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
this :
  Eq (α := (↑(D.U i) : TopCat) ⟶ (↑D.glued : TopCat))
    (CategoryStruct.comp (Y := (D.mapGlueData (forget C)).glued)
      ((D.mapGlueData (forget C)).ι i : (D.mapGlueData (forget C)).U i ⟶ (D.mapGlueData (forget C)).glued)
      (Iso.inv (D.gluedIso (forget C)) : (D.mapGlueData (forget C)).glued ⟶ (↑D.glued : TopCat)))
    (Hom.base (D.ι i))
⊢ Function.Injective (α := (↑(↑(D.U i) : TopCat) : Type v)) (β := (↑(↑D.glued : TopCat) : Type v))
    (Function.comp (β := (↑(D.mapGlueData (forget C)).glued : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (D.mapGlueData (forget C)).glued) (Y := (↑D.glued : TopCat))
              (Iso.inv (D.gluedIso (forget C)) : (D.mapGlueData (forget C)).glued ⟶ (↑D.glued : TopCat)) :
            C((↑(D.mapGlueData (forget C)).glued : Type v), (↑(↑D.glued : TopCat) : Type v))) :
        (a : (↑(D.mapGlueData (forget C)).glued : Type v)) → (↑(↑D.glued : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := (D.mapGlueData (forget C)).glued) ((D.mapGlueData (forget C)).ι i)) :
        (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v)))

Tactic:
Function.Injective.comp ?_ (TopCat.GlueData.ι_injective D.toTopGlueData i)

Premises used: AlgebraicGeometry.PresheafedSpace.GlueData.toTopGlueData, Function.Injective.comp, TopCat.GlueData.ι_injective
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
x y : (↑(↑(D.U i) : TopCat) : Type v)
h1 : y ∈ U
h2 :
  Eq (α := (↑(↑D.glued : TopCat) : Type v))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (↑(D.U i) : TopCat)) (Y := (↑D.glued : TopCat))
              (Hom.base (colimit.ι D.diagram.multispan (WalkingMultispan.right i)) :
                (↑(D.U i) : TopCat) ⟶ (↑D.glued : TopCat)) :
            C((↑(↑(D.U i) : TopCat) : Type v), (↑(↑D.glued : TopCat) : Type v))) :
          (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v))
        y :
      (↑(↑D.glued : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            (↑(D.diagram.multispan.obj (WalkingMultispan.right i)) : TopCat)) (Y :=
            (↑(Limits.colimit D.diagram.multispan) : TopCat))
            (Hom.base (colimit.ι D.diagram.multispan (WalkingMultispan.right i))) :
          (a : (↑(↑(D.diagram.multispan.obj (WalkingMultispan.right i)) : TopCat) : Type v)) →
            (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
        x :
      (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
this :
  Eq (α := (↑(D.U i) : TopCat) ⟶ (↑D.glued : TopCat))
    (CategoryStruct.comp (Y := (D.mapGlueData (forget C)).glued)
      ((D.mapGlueData (forget C)).ι i : (D.mapGlueData (forget C)).U i ⟶ (D.mapGlueData (forget C)).glued)
      (Iso.inv (D.gluedIso (forget C)) : (D.mapGlueData (forget C)).glued ⟶ (↑D.glued : TopCat)))
    (Hom.base (D.ι i))
h :
  Mono (X := (D.mapGlueData (forget C)).glued) (Y := (↑D.glued : TopCat))
    (Iso.inv (D.gluedIso (forget C)) : (D.mapGlueData (forget C)).glued ⟶ (↑D.glued : TopCat))
⊢ Function.Injective (α := (↑(D.mapGlueData (forget C)).glued : Type v)) (β := (↑(↑D.glued : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X := (D.mapGlueData (forget C)).glued) (Y := (↑D.glued : TopCat))
            (Iso.inv (D.gluedIso (forget C)) : (D.mapGlueData (forget C)).glued ⟶ (↑D.glued : TopCat)) :
          C((↑(D.mapGlueData (forget C)).glued : Type v), (↑(↑D.glued : TopCat) : Type v))) :
      (a : (↑(D.mapGlueData (forget C)).glued : Type v)) → (↑(↑D.glued : TopCat) : Type v))

Tactic:
rw [← TopCat.mono_iff_injective]

Premises used: TopCat.mono_iff_injective
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
x y : (↑(↑(D.U i) : TopCat) : Type v)
h1 : y ∈ U
h2 :
  Eq (α := (↑(↑D.glued : TopCat) : Type v))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (↑(D.U i) : TopCat)) (Y := (↑D.glued : TopCat))
              (Hom.base (colimit.ι D.diagram.multispan (WalkingMultispan.right i)) :
                (↑(D.U i) : TopCat) ⟶ (↑D.glued : TopCat)) :
            C((↑(↑(D.U i) : TopCat) : Type v), (↑(↑D.glued : TopCat) : Type v))) :
          (a : (↑(↑(D.U i) : TopCat) : Type v)) → (↑(↑D.glued : TopCat) : Type v))
        y :
      (↑(↑D.glued : TopCat) : Type v))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier) (X :=
            (↑(D.diagram.multispan.obj (WalkingMultispan.right i)) : TopCat)) (Y :=
            (↑(Limits.colimit D.diagram.multispan) : TopCat))
            (Hom.base (colimit.ι D.diagram.multispan (WalkingMultispan.right i))) :
          (a : (↑(↑(D.diagram.multispan.obj (WalkingMultispan.right i)) : TopCat) : Type v)) →
            (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
        x :
      (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
this :
  Eq (α := (↑(D.U i) : TopCat) ⟶ (↑D.glued : TopCat))
    (CategoryStruct.comp (Y := (D.mapGlueData (forget C)).glued)
      ((D.mapGlueData (forget C)).ι i : (D.mapGlueData (forget C)).U i ⟶ (D.mapGlueData (forget C)).glued)
      (Iso.inv (D.gluedIso (forget C)) : (D.mapGlueData (forget C)).glued ⟶ (↑D.glued : TopCat)))
    (Hom.base (D.ι i))
⊢ Mono (X := (D.mapGlueData (forget C)).glued) (Y := (↑D.glued : TopCat))
    (Iso.inv (D.gluedIso (forget C)) : (D.mapGlueData (forget C)).glued ⟶ (↑D.glued : TopCat))

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
h :
  Eq (α := (D.U i).presheaf.obj (op U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    (limit.lift (D.diagramOverOpen U)
          { pt := (D.U i).presheaf.obj (op U),
            π :=
              { app := fun (j : (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ) ↦ D.ιInvAppπApp U (unop j),
                naturality := ⋯ } } ≫
        D.diagramOverOpenπ U i :
      (D.U i).presheaf.obj (op U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    ((D.U i).presheaf.map (eqToHom ⋯) :
      (D.U i).presheaf.obj (op U) ⟶
        (D.U i).presheaf.obj
          (op
            (Functor.obj (C := Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
              (Opens.map (Hom.base (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i))))) :
                Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v) ⥤
                  Opens (↑(↑(D.diagram.multispan.obj (unop (op (WalkingMultispan.right i)))) : TopCat) : Type v))
              (Functor.obj
                  (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                    Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                  U :
                Opens (↑(↑D.glued : TopCat) : Type v)))))
⊢ Eq (α := (D.U i).presheaf.obj (op U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    (D.ιInvApp U ≫ D.diagramOverOpenπ U i) ((D.U i).presheaf.map (eqToHom ⋯))

Tactic:
delta ιInvApp

Premises used: AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
h :
  Eq.{v + 1} (α := (D.U i).presheaf.obj (op U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    (NatTrans.app
        (Cone.π
          { pt := (D.U i).presheaf.obj (op U),
            π :=
              { app := fun (j : (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ) ↦ D.ιInvAppπApp U (unop j),
                naturality := ⋯ } })
        (op (WalkingMultispan.right i)) :
      Functor.obj.{v, v, v, u} (C := (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ)
          (Functor.obj (Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ)
            (Cone.pt.{v, v, v, u} (J := (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ) (F := D.diagramOverOpen U)
              { pt := (D.U i).presheaf.obj (op U),
                π :=
                  { app := fun (j : (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ) ↦ D.ιInvAppπApp U (unop j),
                    naturality := ⋯ :
                    NatTrans
                      (Functor.obj (Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ)
                        ((D.U i).presheaf.obj (op U)))
                      (D.diagramOverOpen U) } :
                Cone (D.diagramOverOpen U) }))
          (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    ((D.U i).presheaf.map (eqToHom ⋯))
⊢ Eq (α := (D.U i).presheaf.obj (op U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    (limit.lift (D.diagramOverOpen U)
          { pt := (D.U i).presheaf.obj (op U),
            π :=
              { app := fun (j : (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ) ↦ D.ιInvAppπApp U (unop j),
                naturality := ⋯ } } ≫
        D.diagramOverOpenπ U i :
      (D.U i).presheaf.obj (op U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    ((D.U i).presheaf.map (eqToHom ⋯) :
      (D.U i).presheaf.obj (op U) ⟶
        (D.U i).presheaf.obj
          (op
            (Functor.obj (C := Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
              (Opens.map (Hom.base (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i))))) :
                Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v) ⥤
                  Opens (↑(↑(D.diagram.multispan.obj (unop (op (WalkingMultispan.right i)))) : TopCat) : Type v))
              (Functor.obj
                  (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                    Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                  U :
                Opens (↑(↑D.glued : TopCat) : Type v)))))

Tactic:
rw [limit.lift_π]

Premises used: CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ Eq (α :=
    (D.U i).presheaf.obj (op U) ⟶
      (D.U i).presheaf.obj
        (op
          (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
            (Opens.map (Hom.base (D.ι i)) :
              Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U i) : TopCat) : Type v))
            (Functor.obj
                (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                  Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                U :
              Opens (↑(↑D.glued : TopCat) : Type v)))))
    ((D.U i).presheaf.map
        (eqToHom ⋯ ≫
          (opensFunctor (D.f i i)).op.map (𝟙 (op ((Opens.map (D.f i i).base).obj U)) ≫ eqToHom ⋯) ≫ eqToHom ⋯) :
      (D.U i).presheaf.obj (op U) ⟶
        (D.U i).presheaf.obj
          (op
            (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
              (Opens.map (Hom.base (D.ι i)) :
                Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U i) : TopCat) : Type v))
              (Functor.obj
                  (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                    Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                  U :
                Opens (↑(↑D.glued : TopCat) : Type v)))))
    ((D.U i).presheaf.map (eqToHom ⋯) :
      (D.U i).presheaf.obj (op U) ⟶
        (D.U i).presheaf.obj
          (op
            (Functor.obj (C := Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
              (Opens.map (Hom.base (Multicoequalizer.π D.diagram i)) :
                Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v) ⥤
                  Opens (↑(↑(D.U i) : TopCat) : Type v))
              (Functor.obj
                  (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                    Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                  U :
                Opens (↑(↑D.glued : TopCat) : Type v)))))

Tactic:
rfl
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
h : (↑U : Set (↑(↑(D.U i) : TopCat) : Type v)) ⊆ Set.univ
rw :
  Function.Surjective (α := (↑(↑(D.V (i, i)) : TopCat) : Type v)) (β := (↑(↑(D.U i) : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.f i i).base) :
      (a : (↑(↑(D.V (i, i)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v))
⊢ (↑U : Set (↑(↑(D.U i) : TopCat) : Type v)) ⊆
    Set.range (ι := (↑(↑(D.V (i, i)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.f i i).base) :
        (a : (↑(↑(D.V (i, i)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v))

Tactic:
rw [Set.range_eq_univ.mpr _]

Premises used: Iff.mpr, Set.range_eq_univ
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ (↑U : Set (↑(↑(D.U i) : TopCat) : Type v)) ⊆ Set.univ

Tactic:
simp
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
rw : Epi (D.f i i).base
⊢ Function.Surjective (α := (↑(↑(D.V (i, i)) : TopCat) : Type v)) (β := (↑(↑(D.U i) : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (D.f i i).base) :
      (a : (↑(↑(D.V (i, i)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v))

Tactic:
rw [← TopCat.epi_iff_surjective]

Premises used: TopCat.epi_iff_surjective