awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : HasMulticoequalizer D.diagram
inst_3 : PreservesColimit D.diagram.multispan F
inst_4 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst_5 : ReflectsLimit (cospan (Z := D.glued) (D.ι i) (D.ι j)) F
hc :
  IsLimit (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
    ((D.mapGlueData F).vPullbackCone i j)
e : cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j)) ≅
  cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (fun (x : WalkingCospan) ↦
      Option.casesOn (motive := fun (t : Option WalkingPair) ↦
        (h : x = t) →
          (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
            (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
        x
        (fun (h : x = none) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (D.gluedIso F) ⋯)
        (fun (val : WalkingPair) (h : x = some val) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (Iso.refl ((cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯)
        ⋯)
    ⋯
refine :
  ∀ (j_1 : WalkingCospan),
    NatTrans.app (Cone.π ((D.mapGlueData F).vPullbackCone i j)) j_1 =
      Iso.hom
          (Iso.refl
            (Cone.pt (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
              ((D.mapGlueData F).vPullbackCone i j))) ≫
        ((Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)).π.app j_1
⊢ (D.mapGlueData F).vPullbackCone i j ≅
    (Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)

Tactic:
refine Cone.ext (Iso.refl _) ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- 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 : HasMulticoequalizer D.diagram
inst_3 : PreservesColimit D.diagram.multispan F
inst_4 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst_5 : ReflectsLimit (cospan (Z := D.glued) (D.ι i) (D.ι j)) F
hc :
  IsLimit (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
    ((D.mapGlueData F).vPullbackCone i j)
e : cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j)) ≅
  cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (fun (x : WalkingCospan) ↦
      Option.casesOn (motive := fun (t : Option WalkingPair) ↦
        (h : x = t) →
          (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
            (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
        x
        (fun (h : x = Option.none) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (D.gluedIso F) ⋯)
        (fun (val : WalkingPair) (h : x = some val) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (Iso.refl ((cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯)
        ⋯)
    ⋯
none :
  Eq (α :=
    Cone.pt (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
        ((D.mapGlueData F).vPullbackCone i j) ⟶
      (D.mapGlueData F).glued)
    (PullbackCone.fst ((D.mapGlueData F).vPullbackCone i j) ≫ (D.mapGlueData F).ι i)
    (F.map (D.f i j) ≫ (D.mapGlueData F).ι i)
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u₂}
        (Functor.obj (Functor.const WalkingCospan)
          (Cone.pt (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
            ((D.mapGlueData F).vPullbackCone i j)))
        Option.none ⟶
      (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj Option.none)
    (NatTrans.app (Cone.π ((D.mapGlueData F).vPullbackCone i j)) Option.none)
    (Iso.hom
        (Iso.refl
          (Cone.pt (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
            ((D.mapGlueData F).vPullbackCone i j))) ≫
      ((Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)).π.app
        Option.none)

Tactic:
simp [e]
-- 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 : HasMulticoequalizer D.diagram
inst_3 : PreservesColimit D.diagram.multispan F
inst_4 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst_5 : ReflectsLimit (cospan (Z := D.glued) (D.ι i) (D.ι j)) F
hc :
  IsLimit (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
    ((D.mapGlueData F).vPullbackCone i j)
e : cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j)) ≅
  cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (fun (x : WalkingCospan) ↦
      Option.casesOn (motive := fun (t : Option WalkingPair) ↦
        (h : x = t) →
          (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
            (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
        x
        (fun (h : x = none) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (D.gluedIso F) ⋯)
        (fun (val : WalkingPair) (h : x = some val) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (Iso.refl ((cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯)
        ⋯)
    ⋯
⊢ Eq (α :=
    Cone.pt (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
        ((D.mapGlueData F).vPullbackCone i j) ⟶
      (D.mapGlueData F).glued)
    (PullbackCone.fst ((D.mapGlueData F).vPullbackCone i j) ≫ (D.mapGlueData F).ι i)
    (F.map (D.f i j) ≫ (D.mapGlueData F).ι i)

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 : HasMulticoequalizer D.diagram
inst_3 : PreservesColimit D.diagram.multispan F
inst_4 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst_5 : ReflectsLimit (cospan (Z := D.glued) (D.ι i) (D.ι j)) F
hc :
  IsLimit (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
    ((D.mapGlueData F).vPullbackCone i j)
e : cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j)) ≅
  cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (fun (x : WalkingCospan) ↦
      Option.casesOn (motive := fun (t : Option WalkingPair) ↦
        (h : x = t) →
          (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
            (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
        x
        (fun (h : x = none) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (D.gluedIso F) ⋯)
        (fun (val : WalkingPair) (h : x = Option.some val) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (Iso.refl ((cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj (Option.some val))) ⋯)
        ⋯)
    ⋯
some : NatTrans.app (Cone.π ((D.mapGlueData F).vPullbackCone i j)) (Option.some WalkingPair.left) = F.map (D.f i j)
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u₂}
        (Functor.obj (Functor.const WalkingCospan)
          (Cone.pt (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
            ((D.mapGlueData F).vPullbackCone i j)))
        (Option.some WalkingPair.left) ⟶
      (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj
        (Option.some WalkingPair.left))
    (NatTrans.app (Cone.π ((D.mapGlueData F).vPullbackCone i j)) (Option.some WalkingPair.left))
    (Iso.hom
        (Iso.refl
          (Cone.pt (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
            ((D.mapGlueData F).vPullbackCone i j))) ≫
      ((Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)).π.app
        (Option.some WalkingPair.left))

Tactic:
simp [e]
-- 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 : HasMulticoequalizer D.diagram
inst_3 : PreservesColimit D.diagram.multispan F
inst_4 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst_5 : ReflectsLimit (cospan (Z := D.glued) (D.ι i) (D.ι j)) F
hc :
  IsLimit (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
    ((D.mapGlueData F).vPullbackCone i j)
e : cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j)) ≅
  cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (fun (x : WalkingCospan) ↦
      Option.casesOn (motive := fun (t : Option WalkingPair) ↦
        (h : x = t) →
          (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
            (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
        x
        (fun (h : x = none) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (D.gluedIso F) ⋯)
        (fun (val : WalkingPair) (h : x = some val) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (Iso.refl ((cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯)
        ⋯)
    ⋯
⊢ NatTrans.app (Cone.π ((D.mapGlueData F).vPullbackCone i j)) (some WalkingPair.left) = F.map (D.f i j)

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 : HasMulticoequalizer D.diagram
inst_3 : PreservesColimit D.diagram.multispan F
inst_4 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst_5 : ReflectsLimit (cospan (Z := D.glued) (D.ι i) (D.ι j)) F
hc :
  IsLimit (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
    ((D.mapGlueData F).vPullbackCone i j)
e : cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j)) ≅
  cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (fun (x : WalkingCospan) ↦
      Option.casesOn (motive := fun (t : Option WalkingPair) ↦
        (h : x = t) →
          (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
            (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
        x
        (fun (h : x = none) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (D.gluedIso F) ⋯)
        (fun (val : WalkingPair) (h : x = Option.some val) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (Iso.refl ((cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj (Option.some val))) ⋯)
        ⋯)
    ⋯
some :
  NatTrans.app (Cone.π ((D.mapGlueData F).vPullbackCone i j)) (Option.some WalkingPair.right) =
    F.map (D.t i j) ≫ F.map (D.f j i)
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u₂}
        (Functor.obj (Functor.const WalkingCospan)
          (Cone.pt (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
            ((D.mapGlueData F).vPullbackCone i j)))
        (Option.some WalkingPair.right) ⟶
      (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj
        (Option.some WalkingPair.right))
    (NatTrans.app (Cone.π ((D.mapGlueData F).vPullbackCone i j)) (Option.some WalkingPair.right))
    (Iso.hom
        (Iso.refl
          (Cone.pt (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
            ((D.mapGlueData F).vPullbackCone i j))) ≫
      ((Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)).π.app
        (Option.some WalkingPair.right))

Tactic:
simp [e]
-- 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 : HasMulticoequalizer D.diagram
inst_3 : PreservesColimit D.diagram.multispan F
inst_4 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst_5 : ReflectsLimit (cospan (Z := D.glued) (D.ι i) (D.ι j)) F
hc :
  IsLimit (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
    ((D.mapGlueData F).vPullbackCone i j)
e : cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j)) ≅
  cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (fun (x : WalkingCospan) ↦
      Option.casesOn (motive := fun (t : Option WalkingPair) ↦
        (h : x = t) →
          (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
            (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
        x
        (fun (h : x = none) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (D.gluedIso F) ⋯)
        (fun (val : WalkingPair) (h : x = some val) ↦
          Eq.ndrec (motive := fun (x : WalkingCospan) ↦
            (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
              (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
            (Iso.refl ((cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯)
        ⋯)
    ⋯
⊢ NatTrans.app (Cone.π ((D.mapGlueData F).vPullbackCone i j)) (some WalkingPair.right) =
    F.map (D.t i j) ≫ F.map (D.f j i)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
inst_1 : HasMulticoequalizer D.diagram
F : C ⥤ Type v
inst_2 : PreservesColimit D.diagram.multispan F
inst_3 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
x : F.obj D.glued
e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F
obtain :
  ∀ (i : (D.mapGlueData F).J) (y : (D.mapGlueData F).U i)
    (eq :
      Eq (α := (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((D.mapGlueData F).ι i) :
              (a : (fun (X : Type v) ↦ X) ((D.mapGlueData F).U i)) → (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
            y :
          (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) e.hom :
              (a : (fun (X : Type v) ↦ X) (F.obj D.glued)) → (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
            x :
          (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)),
    ∃ (i : D.J) (y : F.obj (D.U i)),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (D.ι i)) :
            (a : (fun (X : Type v) ↦ X) (F.obj (D.U i))) → (fun (X : Type v) ↦ X) (F.obj D.glued))
          y =
        x
⊢ ∃ (i : D.J) (y : F.obj (D.U i)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (D.ι i)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (D.U i))) → (fun (X : Type v) ↦ X) (F.obj D.glued))
        y =
      x

Tactic:
obtain ⟨i, y, eq⟩ := (D.mapGlueData F).types_ι_jointly_surjective (e.hom x)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.GlueData.mapGlueData, CategoryTheory.GlueData.types_ι_jointly_surjective, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
inst_1 : HasMulticoequalizer D.diagram
F : C ⥤ Type v
inst_2 : PreservesColimit D.diagram.multispan F
inst_3 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
x : F.obj D.glued
e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F
i : (D.mapGlueData F).J
y : (D.mapGlueData F).U i
eq :
  Eq (α := (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((D.mapGlueData F).ι i) :
          (a : (fun (X : Type v) ↦ X) ((D.mapGlueData F).U i)) → (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
        y :
      (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) e.hom :
          (a : (fun (X : Type v) ↦ X) (F.obj D.glued)) → (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
        x :
      (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
⊢ Eq (α := (fun (X : Type v) ↦ X) (F.obj D.glued))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) e.inv :
          (a : (fun (X : Type v) ↦ X) (D.mapGlueData F).glued) → (fun (X : Type v) ↦ X) (F.obj D.glued))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((D.mapGlueData F).ι i) :
              (a : (fun (X : Type v) ↦ X) ((D.mapGlueData F).U i)) → (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
            y :
          (fun (X : Type v) ↦ X) (D.mapGlueData F).glued) :
      (fun (X : Type v) ↦ X) (F.obj D.glued))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) e.inv :
          (a : (fun (X : Type v) ↦ X) (D.mapGlueData F).glued) → (fun (X : Type v) ↦ X) (F.obj D.glued))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) e.hom :
              (a : (fun (X : Type v) ↦ X) (F.obj D.glued)) → (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
            x :
          (fun (X : Type v) ↦ X) (D.mapGlueData F).glued) :
      (fun (X : Type v) ↦ X) (F.obj D.glued))

Tactic:
replace eq := congr_arg e.inv eq
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
D : GlueData.{v, u₁} C
inst_1 : HasMulticoequalizer D.diagram
F : C ⥤ Type v
inst_2 : PreservesColimit D.diagram.multispan F
inst_3 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
x : F.obj D.glued
e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F
i : (D.mapGlueData F).J
y : (D.mapGlueData F).U i
eq :
  Eq (α := (fun (X : Type v) ↦ X) (F.obj D.glued))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) e.inv :
          (a : (fun (X : Type v) ↦ X) (D.mapGlueData F).glued) → (fun (X : Type v) ↦ X) (F.obj D.glued))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((D.mapGlueData F).ι i) :
              (a : (fun (X : Type v) ↦ X) ((D.mapGlueData F).U i)) → (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
            y :
          (fun (X : Type v) ↦ X) (D.mapGlueData F).glued) :
      (fun (X : Type v) ↦ X) (F.obj D.glued))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) e.inv :
          (a : (fun (X : Type v) ↦ X) (D.mapGlueData F).glued) → (fun (X : Type v) ↦ X) (F.obj D.glued))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) e.hom :
              (a : (fun (X : Type v) ↦ X) (F.obj D.glued)) → (fun (X : Type v) ↦ X) (D.mapGlueData F).glued)
            x :
          (fun (X : Type v) ↦ X) (D.mapGlueData F).glued) :
      (fun (X : Type v) ↦ X) (F.obj D.glued))
⊢ Eq (α := (fun (X : Type v) ↦ X) (F.obj D.glued))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((D.mapGlueData F).ι i ≫ e.inv) :
          (a : (fun (X : Type v) ↦ X) ((D.mapGlueData F).U i)) → (fun (X : Type v) ↦ X) (F.obj D.glued))
        y :
      (fun (X : Type v) ↦ X) (F.obj D.glued))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom ≫ e.inv) :
          (a : (fun (X : Type v) ↦ X) (F.obj D.glued)) → (fun (X : Type v) ↦ X) (F.obj D.glued))
        x :
      (fun (X : Type v) ↦ X) (F.obj D.glued))

Tactic:
change ((D.mapGlueData F).ι i ≫ e.inv) y = (e.hom ≫ e.inv) x at eq

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.GlueData.mapGlueData, CategoryTheory.GlueData.ι, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Iso.inv