awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
eq :
  Eq (α := pullback (D.f i i) (D.f i j) ⟶ pullback (D.f i j) (D.f i i)) (Iso.hom (pullbackSymmetry (D.f i i) (D.f i j)))
    (pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i)))
this : D.t' i j i ≫ D.t' j i i ≫ D.t' i i j = 𝟙 (pullback (D.f i j) (D.f i i))
⊢ CategoryStruct.comp (Y := pullback (D.f j i) (D.f j i))
      (pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ inv (pullback.snd (D.f j i) (D.f j i)))
      (CategoryStruct.comp (Y := pullback (D.f i i) (D.f i j))
        (pullback.snd (D.f j i) (D.f j i) ≫ D.t j i ≫ inv (pullback.snd (D.f i i) (D.f i j)))
        (pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i)))) =
    𝟙 (pullback (D.f i j) (D.f i i))

Tactic:
rw [D.t'_iij, D.t'_jii, D.t'_iji, fst_eq_snd_of_mono_eq, eq] at this

Premises used: CategoryTheory.GlueData.t'_iij, CategoryTheory.GlueData.t'_iji, CategoryTheory.GlueData.t'_jii, CategoryTheory.Limits.fst_eq_snd_of_mono_eq
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
eq :
  Eq (α := pullback (D.f i i) (D.f i j) ⟶ pullback (D.f i j) (D.f i i)) (Iso.hom (pullbackSymmetry (D.f i i) (D.f i j)))
    (pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i)))
this :
  CategoryStruct.comp (Y := pullback (D.f j i) (D.f j i))
      (pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ inv (pullback.snd (D.f j i) (D.f j i)))
      (CategoryStruct.comp (Y := pullback (D.f i i) (D.f i j))
        (pullback.snd (D.f j i) (D.f j i) ≫ D.t j i ≫ inv (pullback.snd (D.f i i) (D.f i j)))
        (pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i)))) =
    𝟙 (pullback (D.f i j) (D.f i i))
⊢ pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ D.t j i ≫ inv (pullback.fst (D.f i j) (D.f i i)) =
    𝟙 (pullback (D.f i j) (D.f i i))

Tactic:
simp only [Category.assoc, IsIso.inv_hom_id_assoc] at this

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
eq :
  Eq (α := pullback (D.f i i) (D.f i j) ⟶ pullback (D.f i j) (D.f i i)) (Iso.hom (pullbackSymmetry (D.f i i) (D.f i j)))
    (pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i)))
this :
  pullback.fst (D.f i j) (D.f i i) ≫ D.t i j ≫ D.t j i ≫ inv (pullback.fst (D.f i j) (D.f i i)) =
    𝟙 (pullback (D.f i j) (D.f i i))
⊢ D.t i j ≫ D.t j i =
    (inv (pullback.fst (D.f i j) (D.f i i)) ≫ 𝟙 (pullback (D.f i j) (D.f i i))) ≫ pullback.fst (D.f i j) (D.f i i)

Tactic:
rw [← IsIso.eq_inv_comp, ← Category.assoc, IsIso.comp_inv_eq] at this

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.eq_inv_comp, CategoryTheory.IsIso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
eq :
  Eq (α := pullback (D.f i i) (D.f i j) ⟶ pullback (D.f i j) (D.f i i)) (Iso.hom (pullbackSymmetry (D.f i i) (D.f i j)))
    (pullback.snd (D.f i i) (D.f i j) ≫ inv (pullback.fst (D.f i j) (D.f i i)))
this :
  D.t i j ≫ D.t j i =
    (inv (pullback.fst (D.f i j) (D.f i i)) ≫ 𝟙 (pullback (D.f i j) (D.f i i))) ≫ pullback.fst (D.f i j) (D.f i i)
⊢ D.t i j ≫ D.t j i = 𝟙 (D.V (i, j))

Tactic:
simpa using this
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j k : D.J
rw :
  (D.t' i j k ≫
        Iso.hom (pullbackSymmetry (D.f j k) (D.f j i)) ≫ D.t' j i k ≫ Iso.hom (pullbackSymmetry (D.f i k) (D.f i j))) ≫
      pullback.fst (D.f i j) (D.f i k) =
    𝟙 (pullback (D.f i j) (D.f i k)) ≫ pullback.fst (D.f i j) (D.f i k)
⊢ D.t' i j k ≫
      Iso.hom (pullbackSymmetry (D.f j k) (D.f j i)) ≫ D.t' j i k ≫ Iso.hom (pullbackSymmetry (D.f i k) (D.f i j)) =
    𝟙 (pullback (D.f i j) (D.f i k))

Tactic:
rw [← cancel_mono (pullback.fst (D.f i j) (D.f i k))]

Premises used: CategoryTheory.GlueData.f, CategoryTheory.cancel_mono, CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j k : D.J
⊢ (D.t' i j k ≫
        Iso.hom (pullbackSymmetry (D.f j k) (D.f j i)) ≫ D.t' j i k ≫ Iso.hom (pullbackSymmetry (D.f i k) (D.f i j))) ≫
      pullback.fst (D.f i j) (D.f i k) =
    𝟙 (pullback (D.f i j) (D.f i k)) ≫ pullback.fst (D.f i j) (D.f i k)

Tactic:
simp [t_fac, t_fac_assoc]

Premises used: CategoryTheory.GlueData.t_fac, CategoryTheory.GlueData.t_fac_assoc
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData.{v, u₁} C
i j : D.J
⊢ IsIso (D.t i j)

Tactic:
⟨⟨D.t j i, D.t_inv _ _, D.t_inv _ _⟩⟩

Premises used: CategoryTheory.GlueData.t, CategoryTheory.GlueData.t_inv, And.intro, Exists.intro, CategoryTheory.IsIso.mk
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData.{v, u₁} C
i j k : D.J
⊢ (D.t' j k i ≫ D.t' k i j) ≫ D.t' i j k = 𝟙 (pullback (D.f j k) (D.f j i))

Tactic:
simpa using D.cocycle _ _ _

Premises used: CategoryTheory.GlueData.cocycle
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j k : D.J
trans : D.t' j k i ≫ D.t' k i j = inv (D.t' i j k)
trans₁ :
  inv (D.t' i j k) =
    Iso.hom (pullbackSymmetry (D.f j k) (D.f j i)) ≫ D.t' j i k ≫ Iso.hom (pullbackSymmetry (D.f i k) (D.f i j))
⊢ D.t' j k i ≫ D.t' k i j =
    Iso.hom (pullbackSymmetry (D.f j k) (D.f j i)) ≫ D.t' j i k ≫ Iso.hom (pullbackSymmetry (D.f i k) (D.f i j))

Tactic:
trans inv (D.t' i j k)

Premises used: CategoryTheory.GlueData.t', CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j k : D.J
⊢ D.t' j k i ≫ D.t' k i j = inv (D.t' i j k)

Tactic:
IsIso.eq_inv_of_hom_inv_id (D.cocycle _ _ _)

Premises used: CategoryTheory.IsIso.eq_inv_of_hom_inv_id, CategoryTheory.GlueData.cocycle
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j k : D.J
⊢ D.t' j k i ≫ D.t' k i j = inv (D.t' i j k)

Tactic:
exact IsIso.eq_inv_of_hom_inv_id (D.cocycle _ _ _)

Premises used: CategoryTheory.IsIso.eq_inv_of_hom_inv_id, CategoryTheory.GlueData.cocycle
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j k : D.J
rw :
  inv (D.t' i j k) ≫ pullback.fst (D.f i j) (D.f i k) =
    (Iso.hom (pullbackSymmetry (D.f j k) (D.f j i)) ≫ D.t' j i k ≫ Iso.hom (pullbackSymmetry (D.f i k) (D.f i j))) ≫
      pullback.fst (D.f i j) (D.f i k)
⊢ inv (D.t' i j k) =
    Iso.hom (pullbackSymmetry (D.f j k) (D.f j i)) ≫ D.t' j i k ≫ Iso.hom (pullbackSymmetry (D.f i k) (D.f i j))

Tactic:
rw [← cancel_mono (pullback.fst (D.f i j) (D.f i k))]

Premises used: CategoryTheory.GlueData.f, CategoryTheory.cancel_mono, CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j k : D.J
⊢ inv (D.t' i j k) ≫ pullback.fst (D.f i j) (D.f i k) =
    (Iso.hom (pullbackSymmetry (D.f j k) (D.f j i)) ≫ D.t' j i k ≫ Iso.hom (pullbackSymmetry (D.f i k) (D.f i j))) ≫
      pullback.fst (D.f i j) (D.f i k)

Tactic:
simp [t_fac, t_fac_assoc]

Premises used: CategoryTheory.GlueData.t_fac, CategoryTheory.GlueData.t_fac_assoc
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
⊢ D.diagram.fst (i, j) = D.f i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
i j : D.J
⊢ D.diagram.snd (i, j) = D.t i j ≫ D.f j i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
⊢ D.diagram.left = D.V

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
⊢ D.diagram.right = D.U

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
inst_1 : HasMulticoequalizer D.diagram
i j : D.J
⊢ Eq (α := D.V (i, j) ⟶ D.glued) (D.t i j ≫ D.f j i ≫ D.ι j) (D.f i j ≫ D.ι i)

Tactic:
(Category.assoc _ _ _).symm.trans (Multicoequalizer.condition D.diagram ⟨i, j⟩).symm

Premises used: CategoryTheory.GlueData.diagram, CategoryTheory.Category.assoc, CategoryTheory.Limits.Multicoequalizer.condition, Prod.mk, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData.{v, u₁} C
inst_2 : HasMulticoequalizer D.diagram
i j : D.J
⊢ Eq (α := D.V (i, j) ⟶ D.glued) (D.f i j ≫ D.ι i) ((D.t i j ≫ D.f j i) ≫ D.ι j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData.{v, u₁} C
inst_2 : HasMulticoequalizer D.diagram
inst_3 : HasColimits.{v, u₁} C
⊢ Epi (X := D.sigmaOpens) (Y := D.glued) (D.π : D.sigmaOpens ⟶ D.glued)

Tactic:
inferInstanceAs <| Epi (Multicoequalizer.sigmaπ D.diagram)

Premises used: _private.0.CategoryTheory.GlueData.π_epi._proof_1
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
D : GlueData (Type u_1)
⊢ Function.Surjective (α := (fun (X : Type u_1) ↦ X) D.sigmaOpens) (β := (fun (X : Type u_1) ↦ X) D.glued)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
      (a : (fun (X : Type u_1) ↦ X) D.sigmaOpens) → (fun (X : Type u_1) ↦ X) D.glued)

Tactic:
(epi_iff_surjective _).mp inferInstance

Premises used: CategoryTheory.epi_iff_surjective, inferInstance, Iff.mp
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
D : GlueData (Type v)
x : D.glued
delta :
  ∃ (i : D.J) (y : D.U i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Multicoequalizer.π D.diagram i) :
          (a : (fun (X : Type v) ↦ X) (D.U i)) → (fun (X : Type v) ↦ X) D.glued)
        y =
      x
⊢ ∃ (i : D.J) (y : D.U i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (D.ι i) :
          (a : (fun (X : Type v) ↦ X) (D.U i)) → (fun (X : Type v) ↦ X) D.glued)
        y =
      x

Tactic:
delta CategoryTheory.GlueData.ι

Premises used: CategoryTheory.GlueData.ι
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
D : GlueData (Type v)
x : D.glued
simp_rw :
  ∃ (i : D.J) (y : D.U i),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : D.U i) → D.glued)
        y =
      x
⊢ ∃ (i : D.J) (y : D.U i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Multicoequalizer.π D.diagram i) :
          (a : (fun (X : Type v) ↦ X) (D.U i)) → (fun (X : Type v) ↦ X) D.glued)
        y =
      x

Tactic:
simp_rw [← Multicoequalizer.ι_sigmaπ D.diagram]

Premises used: CategoryTheory.GlueData.diagram, CategoryTheory.Limits.Multicoequalizer.ι_sigmaπ
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
D : GlueData (Type v)
x : D.glued
rcases :
  ∀ (x' : D.sigmaOpens),
    ∃ (i : D.J) (y : D.U i),
      Eq (α := D.glued)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
                  (Multicoequalizer.sigmaπ D.diagram)) :
              (a : D.U i) → D.glued)
            y :
          D.glued)
        (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
              (a : (fun (X : Type v) ↦ X) D.sigmaOpens) → (fun (X : Type v) ↦ X) D.glued)
            x' :
          (fun (X : Type v) ↦ X) D.glued)
⊢ ∃ (i : D.J) (y : D.U i),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : D.U i) → D.glued)
        y =
      x

Tactic:
rcases D.types_π_surjective x with ⟨x', rfl⟩

Premises used: CategoryTheory.GlueData.types_π_surjective, rfl
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
D : GlueData (Type v)
x' : D.sigmaOpens
rw :
  ∃ (i : D.J) (y : D.U i),
    Eq (α := D.glued)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
                (Multicoequalizer.sigmaπ D.diagram)) :
            (a : D.U i) → D.glued)
          y :
        D.glued)
      (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
            (a : (fun (X : Type v) ↦ X) D.sigmaOpens) → (fun (X : Type v) ↦ X) D.glued)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Iso.inv (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
                (a : (Types.coproductColimitCocone D.U).cocone.pt) → colimit (Discrete.functor D.U))
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (Iso.hom (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
                    (a : colimit (Discrete.functor D.U)) → (Types.coproductColimitCocone D.U).cocone.pt)
                  x' :
                (Types.coproductColimitCocone D.U).cocone.pt) :
            colimit (Discrete.functor D.U)) :
        (fun (X : Type v) ↦ X) D.glued)
⊢ ∃ (i : D.J) (y : D.U i),
    Eq (α := D.glued)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
                (Multicoequalizer.sigmaπ D.diagram)) :
            (a : D.U i) → D.glued)
          y :
        D.glued)
      (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
            (a : (fun (X : Type v) ↦ X) D.sigmaOpens) → (fun (X : Type v) ↦ X) D.glued)
          x' :
        (fun (X : Type v) ↦ X) D.glued)

Tactic:
rw [← dsimp% ConcreteCategory.congr_hom
    (colimit.isoColimitCocone (Types.coproductColimitCocone _)).hom_inv_id x']

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Limits.Types.coproductColimitCocone, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
D : GlueData (Type v)
x' : D.sigmaOpens
rcases :
  ∀ (i : D.J) (y : D.U i),
    ∃ (i_1 : D.J) (y_1 : D.U i_1),
      Eq (α := D.glued)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i_1)
                  (Multicoequalizer.sigmaπ D.diagram)) :
              (a : D.U i_1) → D.glued)
            y_1 :
          D.glued)
        (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
              (a : (fun (X : Type v) ↦ X) D.sigmaOpens) → (fun (X : Type v) ↦ X) D.glued)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (Iso.inv (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
                  (a : (Types.coproductColimitCocone D.U).cocone.pt) → colimit (Discrete.functor D.U))
                (Sigma.mk (β := fun (j : D.J) ↦ D.U j) i y) :
              colimit (Discrete.functor D.U)) :
          (fun (X : Type v) ↦ X) D.glued)
⊢ ∃ (i : D.J) (y : D.U i),
    Eq (α := D.glued)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
                (Multicoequalizer.sigmaπ D.diagram)) :
            (a : D.U i) → D.glued)
          y :
        D.glued)
      (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
            (a : (fun (X : Type v) ↦ X) D.sigmaOpens) → (fun (X : Type v) ↦ X) D.glued)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Iso.inv (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
                (a : (Types.coproductColimitCocone D.U).cocone.pt) → colimit (Discrete.functor D.U))
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (Iso.hom (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
                    (a : colimit (Discrete.functor D.U)) → (Types.coproductColimitCocone D.U).cocone.pt)
                  x' :
                (Types.coproductColimitCocone D.U).cocone.pt) :
            colimit (Discrete.functor D.U)) :
        (fun (X : Type v) ↦ X) D.glued)

Tactic:
rcases (colimit.isoColimitCocone (Types.coproductColimitCocone _)).hom x' with ⟨i, y⟩

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Types.coproductColimitCocone, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
D : GlueData (Type v)
x' : D.sigmaOpens
i : D.J
y : D.U i
⊢ ∃ (i_1 : D.J) (y_1 : D.U i_1),
    Eq (α := D.glued)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i_1)
                (Multicoequalizer.sigmaπ D.diagram)) :
            (a : D.U i_1) → D.glued)
          y_1 :
        D.glued)
      (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
            (a : (fun (X : Type v) ↦ X) D.sigmaOpens) → (fun (X : Type v) ↦ X) D.glued)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Iso.inv (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
                (a : (Types.coproductColimitCocone D.U).cocone.pt) → colimit (Discrete.functor D.U))
              (Sigma.mk (β := fun (j : D.J) ↦ D.U j) i y) :
            colimit (Discrete.functor D.U)) :
        (fun (X : Type v) ↦ X) D.glued)

Tactic:
⟨i, y, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
D : GlueData (Type v)
x' : D.sigmaOpens
i : D.J
y : D.U i
refine :
  Eq (α := D.glued)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : D.U i) → D.glued)
        y :
      D.glued)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
          (a : (fun (X : Type v) ↦ X) D.sigmaOpens) → (fun (X : Type v) ↦ X) D.glued)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (Iso.inv (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
              (a : (Types.coproductColimitCocone D.U).cocone.pt) → colimit (Discrete.functor D.U))
            (Sigma.mk (β := fun (j : D.J) ↦ D.U j) i y) :
          colimit (Discrete.functor D.U)) :
      (fun (X : Type v) ↦ X) D.glued)
⊢ ∃ (i_1 : D.J) (y_1 : D.U i_1),
    Eq (α := D.glued)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i_1)
                (Multicoequalizer.sigmaπ D.diagram)) :
            (a : D.U i_1) → D.glued)
          y_1 :
        D.glued)
      (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
            (a : (fun (X : Type v) ↦ X) D.sigmaOpens) → (fun (X : Type v) ↦ X) D.glued)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Iso.inv (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
                (a : (Types.coproductColimitCocone D.U).cocone.pt) → colimit (Discrete.functor D.U))
              (Sigma.mk (β := fun (j : D.J) ↦ D.U j) i y) :
            colimit (Discrete.functor D.U)) :
        (fun (X : Type v) ↦ X) D.glued)

Tactic:
refine ⟨i, y, ?_⟩
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
D : GlueData (Type v)
x' : D.sigmaOpens
i : D.J
y : D.U i
simp :
  Eq (α := D.glued)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ D.U) (Sigma.ι D.U i) (Multicoequalizer.sigmaπ D.diagram)) :
          (a : D.U i) → D.glued)
        y :
      D.glued)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) : (a : D.sigmaOpens) → D.glued)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (Iso.inv (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
              (a : (Types.coproductColimitCocone D.U).cocone.pt) → colimit (Discrete.functor D.U))
            (Sigma.mk (β := fun (j : D.J) ↦ D.U j) i y) :
          colimit (Discrete.functor D.U)) :
      D.glued)
⊢ Eq (α := D.glued)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : D.U i) → D.glued)
        y :
      D.glued)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
          (a : (fun (X : Type v) ↦ X) D.sigmaOpens) → (fun (X : Type v) ↦ X) D.glued)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (Iso.inv (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
              (a : (Types.coproductColimitCocone D.U).cocone.pt) → colimit (Discrete.functor D.U))
            (Sigma.mk (β := fun (j : D.J) ↦ D.U j) i y) :
          colimit (Discrete.functor D.U)) :
      (fun (X : Type v) ↦ X) D.glued)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
D : GlueData (Type v)
x' : D.sigmaOpens
i : D.J
y : D.U i
⊢ Eq (α := D.glued)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ D.U) (Sigma.ι D.U i) (Multicoequalizer.sigmaπ D.diagram)) :
          (a : D.U i) → D.glued)
        y :
      D.glued)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) : (a : D.sigmaOpens) → D.glued)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (Iso.inv (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
              (a : (Types.coproductColimitCocone D.U).cocone.pt) → colimit (Discrete.functor D.U))
            (Sigma.mk (β := fun (j : D.J) ↦ D.U j) i y) :
          colimit (Discrete.functor D.U)) :
      D.glued)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData.{v, u₁} C
F : Functor.{v, v, u₁, u₂} C C'
inst_2 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j k : D.J
⊢ HasPullback (F.map (D.f i j)) (F.map (D.f i k))

Tactic:
⟨⟨⟨_, isLimitOfHasPullbackOfPreservesLimit F (D.f i j) (D.f i k)⟩⟩⟩

Premises used: CategoryTheory.Limits.isLimitOfHasPullbackOfPreservesLimit, CategoryTheory.GlueData.f, Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData.{v, u₁} C
F : Functor.{v, v, u₁, u₂} C C'
inst_2 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i : D.J
⊢ F.map (D.t i i) = 𝟙 (F.obj (D.V (i, i)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData.{v, u₁} C
F : Functor.{v, v, u₁, u₂} C C'
inst_2 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j k : D.J
⊢ Eq (α := pullback (F.map (D.f i j)) (F.map (D.f i k)) ⟶ F.obj (D.V (j, i)))
    (CategoryStruct.comp (Y := pullback (F.map (D.f j k)) (F.map (D.f j i)))
      (Iso.inv (PreservesPullback.iso F (D.f i j) (D.f i k)) ≫
        F.map (D.t' i j k) ≫ Iso.hom (PreservesPullback.iso F (D.f j k) (D.f j i)))
      (pullback.snd (F.map (D.f j k)) (F.map (D.f j i))))
    (pullback.fst (F.map (D.f i j)) (F.map (D.f i k)) ≫ F.map (D.t i j))

Tactic:
simpa [Iso.inv_comp_eq] using congr_arg (fun f => F.map f) (D.t_fac i j k)

Premises used: CategoryTheory.Iso.inv_comp_eq, CategoryTheory.GlueData.t_fac, CategoryTheory.Functor.map, congr_arg