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)
j : (MultispanShape.prod D.J).R
w :
  Eq (α := limit (D.diagramOverOpen U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right j)))
    (D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)))
    (𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)))
⊢ Eq (α := limit (D.diagramOverOpen U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right j)))
    ((D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
      limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)))
    (𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)))

Tactic:
simp_rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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)
j : (MultispanShape.prod D.J).R
w :
  Eq (α := limit (D.diagramOverOpen U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right j)))
    (D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)))
    (limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)))
⊢ Eq (α := limit (D.diagramOverOpen U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right j)))
    (D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)))
    (𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)))

Tactic:
rw [Category.id_comp]

Premises used: CategoryTheory.Category.id_comp
-- 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)
j : (MultispanShape.prod D.J).R
⊢ Eq (α := limit (D.diagramOverOpen U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right j)))
    (D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)))
    (limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)))

Tactic:
apply π_ι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 :
  D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 (limit (D.diagramOverOpen U)) ∧
    Eq (α :=
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
      ((D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ D.diagramOverOpenπ U i :
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
          (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
      (𝟙 ((D.diagramOverOpen U).obj (op (WalkingMultispan.right i))) :
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
          (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
⊢ IsIso (X := limit (D.diagramOverOpen U)) (D.diagramOverOpenπ U i)

Tactic:
use D.ιInvAppπEqMap U ≫ D.ιInvApp U

Premises used: AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp, AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπEqMap
-- 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 : D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 (limit (D.diagramOverOpen U))
h₁ :
  Eq (α :=
    (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    ((D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ D.diagramOverOpenπ U i :
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    (𝟙 ((D.diagramOverOpen U).obj (op (WalkingMultispan.right i))) :
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
⊢ D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 (limit (D.diagramOverOpen U)) ∧
    Eq (α :=
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
      ((D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ D.diagramOverOpenπ U i :
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
          (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
      (𝟙 ((D.diagramOverOpen U).obj (op (WalkingMultispan.right i))) :
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
          (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))

Tactic:
constructor
-- 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)
⊢ D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 (limit (D.diagramOverOpen U))

Tactic:
apply π_ιInvApp_eq_id

Premises used: AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_eq_id
-- 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.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    (D.ιInvAppπEqMap U ≫ (D.U i).presheaf.map (eqToHom ⋯) :
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    (𝟙 ((D.diagramOverOpen U).obj (op (WalkingMultispan.right i))) :
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
⊢ Eq (α :=
    (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    ((D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ D.diagramOverOpenπ U i :
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    (𝟙 ((D.diagramOverOpen U).obj (op (WalkingMultispan.right i))) :
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))

Tactic:
rw [Category.assoc, (D.ιInvApp_π _).choose_spec]

Premises used: CategoryTheory.Category.assoc, Exists.choose_spec, 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)
⊢ Eq (α :=
    (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    (D.ιInvAppπEqMap U ≫ (D.U i).presheaf.map (eqToHom ⋯) :
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    (𝟙 ((D.diagramOverOpen U).obj (op (WalkingMultispan.right i))) :
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))

Tactic:
Iso.inv_hom_id ((D.U i).presheaf.mapIso (eqToIso _))

Premises used: Eq.mpr, CategoryTheory.Iso.inv_hom_id, Set.Mem, CategoryTheory.eqToHom, setOf, CategoryTheory.eqToIso, Set.preimage, AlgebraicGeometry.PresheafedSpace.presheaf, Set.image, CategoryTheory.GlueData.U, CategoryTheory.Functor.mapIso, 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)
⊢ Eq (α :=
    (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    (D.ιInvAppπEqMap U ≫ (D.U i).presheaf.map (eqToHom ⋯) :
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))
    (𝟙 ((D.diagramOverOpen U).obj (op (WalkingMultispan.right i))) :
      (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)) ⟶
        (D.diagramOverOpen U).obj (op (WalkingMultispan.right i)))

Tactic:
exact Iso.inv_hom_id ((D.U i).presheaf.mapIso (eqToIso _))

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.eqToIso, AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.GlueData.U, CategoryTheory.Functor.mapIso, 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 j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
refine_1 : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)
refine_2 : lift (D.f i j) s.fst ⋯ ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst
refine_3 : lift (D.f i j) s.fst ⋯ ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd
refine_4 :
  ∀ {m : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)},
    m ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst →
      m ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd → m = lift (D.f i j) s.fst ⋯
⊢ { l : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j) //
    l ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst ∧
      l ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd ∧
        ∀ {m : s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)},
          m ≫ PullbackCone.fst (D.vPullbackCone i j) = s.fst →
            m ≫ PullbackCone.snd (D.vPullbackCone i j) = s.snd → m = l }

Tactic:
refine ⟨?_, ?_, ?_, ?_⟩
-- 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 j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
refine_1 :
  Subset (α := Set (↑(↑(D.U i) : TopCat) : Type v))
    (Set.range (ι := (↑(↑s.pt : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            s.fst.base) :
        (a : (↑(↑s.pt : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)))
    (Set.range (ι :=
      (↑(↑(Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.f i j).base) :
        (a : (↑(↑(D.vPullbackCone i j).pt : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)))
⊢ s.pt ⟶ Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)

Tactic:
refine PresheafedSpace.IsOpenImmersion.lift (D.f i j) s.fst ?_

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift, CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.GlueData.f, 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 j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
refine_1 :
  Subset (α := Set (↑(↑(D.U i) : TopCat) : Type v))
    (Set.range (ι := (↑(↑s.pt : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            s.fst.base) :
        (a : (↑(↑s.pt : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)))
    (Set.preimage (β := (↑D.toTopGlueData.glued : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := D.toTopGlueData.glued) (D.toTopGlueData.ι i)) :
        (a : (↑(D.toTopGlueData.U i) : Type v)) → (↑D.toTopGlueData.glued : Type v))
      (Set.range (ι := (↑(D.toTopGlueData.U j) : Type v))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (Y := D.toTopGlueData.glued) (D.toTopGlueData.ι j)) :
          (a : (↑(D.toTopGlueData.U j) : Type v)) → (↑D.toTopGlueData.glued : Type v))))
⊢ Subset (α := Set (↑(↑(D.U i) : TopCat) : Type v))
    (Set.range (ι := (↑(↑s.pt : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            s.fst.base) :
        (a : (↑(↑s.pt : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)))
    (Set.range (ι :=
      (↑(↑(Cone.pt (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.f i j).base) :
        (a : (↑(↑(D.vPullbackCone i j).pt : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)))

Tactic:
erw [← D.toTopGlueData.preimage_range j i]

Premises used: AlgebraicGeometry.PresheafedSpace.GlueData.toTopGlueData, TopCat.GlueData.preimage_range
-- 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 j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
rw :
  Eq (α := (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
    (s.fst.base ≫
        CategoryStruct.comp (Y := Functor.obj (forget C) D.glued) (CategoryTheory.Functor.map (forget C) (D.ι i))
          (Iso.hom (D.gluedIso (forget C))) :
      (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
    (s.snd.base ≫
        CategoryStruct.comp (Y := Functor.obj (forget C) D.glued) (CategoryTheory.Functor.map (forget C) (D.ι j))
          (Iso.hom (D.gluedIso (forget C))) :
      (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
⊢ Eq (α := (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued) (s.fst.base ≫ D.toTopGlueData.ι i)
    (s.snd.base ≫ D.toTopGlueData.ι j)

Tactic:
rw [← 𝖣.ι_gluedIso_hom (PresheafedSpace.forget _) _, ←
          𝖣.ι_gluedIso_hom (PresheafedSpace.forget _) _]
-- 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 j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
⊢ Eq (α := (↑s.pt : TopCat) ⟶ (↑D.glued : TopCat)) (Hom.base (s.fst ≫ D.ι i)) (Hom.base (s.snd ≫ D.ι j))

Tactic:
have := congr_arg PresheafedSpace.Hom.base s.condition
-- 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 j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
this : Eq (α := (↑s.pt : TopCat) ⟶ (↑D.glued : TopCat)) (Hom.base (s.fst ≫ D.ι i)) (Hom.base (s.snd ≫ D.ι j))
⊢ Eq (α := (↑s.pt : TopCat) ⟶ (↑D.glued : TopCat)) (s.fst.base ≫ Hom.base (D.ι i)) (s.snd.base ≫ Hom.base (D.ι j))

Tactic:
rw [comp_base, comp_base] at this

Premises used: AlgebraicGeometry.PresheafedSpace.comp_base
-- 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 j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
this : Eq (α := (↑s.pt : TopCat) ⟶ (↑D.glued : TopCat)) (s.fst.base ≫ Hom.base (D.ι i)) (s.snd.base ≫ Hom.base (D.ι j))
⊢ ∀ {Z : TopCat.{v}} (h : (↑D.glued : TopCat) ⟶ Z),
    s.fst.base ≫ Hom.base (D.ι i) ≫ h = s.snd.base ≫ Hom.base (D.ι j) ≫ h

Tactic:
replace this := reassoc_of% this
-- 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 j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
this :
  ∀ {Z : TopCat.{v}} (h : (↑D.glued : TopCat) ⟶ Z),
    s.fst.base ≫ Hom.base (D.ι i) ≫ h = s.snd.base ≫ Hom.base (D.ι j) ≫ h
⊢ Eq (α := (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
    (s.fst.base ≫
        CategoryStruct.comp (Y := Functor.obj (forget C) D.glued) (CategoryTheory.Functor.map (forget C) (D.ι i))
          (Iso.hom (D.gluedIso (forget C))) :
      (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
    (s.snd.base ≫
        CategoryStruct.comp (Y := Functor.obj (forget C) D.glued) (CategoryTheory.Functor.map (forget C) (D.ι j))
          (Iso.hom (D.gluedIso (forget C))) :
      (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)

Tactic:
this _

Premises used: CategoryTheory.GlueData.mapGlueData
-- 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 j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
this :
  ∀ {Z : TopCat.{v}} (h : (↑D.glued : TopCat) ⟶ Z),
    s.fst.base ≫ Hom.base (D.ι i) ≫ h = s.snd.base ≫ Hom.base (D.ι j) ≫ h
⊢ Eq (α := (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
    (s.fst.base ≫
        CategoryStruct.comp (Y := Functor.obj (forget C) D.glued) (CategoryTheory.Functor.map (forget C) (D.ι i))
          (Iso.hom (D.gluedIso (forget C))) :
      (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)
    (s.snd.base ≫
        CategoryStruct.comp (Y := Functor.obj (forget C) D.glued) (CategoryTheory.Functor.map (forget C) (D.ι j))
          (Iso.hom (D.gluedIso (forget C))) :
      (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued)

Tactic:
exact this _
-- 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 j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
⊢ Eq (α := (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued) (s.fst.base ≫ D.toTopGlueData.ι i)
    (s.snd.base ≫ D.toTopGlueData.ι j)

Tactic:
have :
        s.fst.base ≫ D.toTopGlueData.ι i =
          s.snd.base ≫ D.toTopGlueData.ι j := by
        rw [← 𝖣.ι_gluedIso_hom (PresheafedSpace.forget _) _, ←
          𝖣.ι_gluedIso_hom (PresheafedSpace.forget _) _]
        have := congr_arg PresheafedSpace.Hom.base s.condition
        rw [comp_base, comp_base] at this
        replace this := reassoc_of% this
        exact this _
-- 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 j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
this :
  Eq (α := (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued) (s.fst.base ≫ D.toTopGlueData.ι i)
    (s.snd.base ≫ D.toTopGlueData.ι j)
refine_1 :
  Subset (α := Set (↑(↑(D.U i) : TopCat) : Type v))
    (Set.range (ι := (↑(↑s.pt : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            s.fst.base) :
        (a : (↑(↑s.pt : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)))
    (Set.preimage (β := (↑(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)
            (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))
      (Set.range (ι := (↑(↑(D.U j) : 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)).ι j)) :
          (a : (↑(↑(D.U j) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v))))
⊢ Subset (α := Set (↑(↑(D.U i) : TopCat) : Type v))
    (Set.range (ι := (↑(↑s.pt : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            s.fst.base) :
        (a : (↑(↑s.pt : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)))
    (Set.preimage (β := (↑D.toTopGlueData.glued : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (Y := D.toTopGlueData.glued) (D.toTopGlueData.ι i)) :
        (a : (↑(D.toTopGlueData.U i) : Type v)) → (↑D.toTopGlueData.glued : Type v))
      (Set.range (ι := (↑(D.toTopGlueData.U j) : Type v))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (Y := D.toTopGlueData.glued) (D.toTopGlueData.ι j)) :
          (a : (↑(D.toTopGlueData.U j) : Type v)) → (↑D.toTopGlueData.glued : Type v))))

Tactic:
simp only [mapGlueData_U, forget_obj]

Premises used: AlgebraicGeometry.PresheafedSpace.forget_obj, CategoryTheory.GlueData.mapGlueData_U
-- 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 j : D.J
s : PullbackCone (Z := D.glued) (D.ι i) (D.ι j)
this :
  Eq (α := (↑s.pt : TopCat) ⟶ D.toTopGlueData.glued) (s.fst.base ≫ D.toTopGlueData.ι i)
    (s.snd.base ≫ D.toTopGlueData.ι j)
refine_1 :
  Subset (α := Set (↑(D.mapGlueData (forget C)).glued : Type v))
    (Set.image (α := (↑(↑(D.U j) : 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.toTopGlueData.ι j)) :
        (a : (↑(↑(D.U j) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v))
      (Set.image (α := (↑(↑s.pt : TopCat) : Type v))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              s.snd.base) :
          (a : (↑(↑s.pt : TopCat) : Type v)) → (↑(↑(D.U j) : TopCat) : Type v))
        Set.univ))
    (Set.range (ι := (↑(↑(D.U j) : 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)).ι j)) :
        (a : (↑(↑(D.U j) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v)))
⊢ Subset (α := Set (↑(↑(D.U i) : TopCat) : Type v))
    (Set.range (ι := (↑(↑s.pt : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            s.fst.base) :
        (a : (↑(↑s.pt : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)))
    (Set.preimage (β := (↑(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)
            (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))
      (Set.range (ι := (↑(↑(D.U j) : 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)).ι j)) :
          (a : (↑(↑(D.U j) : TopCat) : Type v)) → (↑(D.mapGlueData (forget C)).glued : Type v))))

Tactic:
rw [← Set.image_subset_iff, ← Set.image_univ, ← Set.image_comp, Set.image_univ,
        ← TopCat.coe_comp, this, TopCat.coe_comp, ← Set.image_univ, Set.image_comp]

Premises used: Set.image_univ, Set.image_comp, Set.image_subset_iff, TopCat.coe_comp