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
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) ((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))
⊢ Eq (α := (fun (X : Type v) ↦ X) (F.obj D.glued))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (D.ι i)) :
          (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) (𝟙 (F.obj D.glued)) :
          (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:
rw [e.hom_inv_id, D.ι_gluedIso_inv] at eq

Premises used: CategoryTheory.GlueData.ι_gluedIso_inv, CategoryTheory.Iso.hom_inv_id
-- 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) (F.map (D.ι i)) :
          (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) (𝟙 (F.obj D.glued)) :
          (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))
⊢ ∃ (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:
⟨i, y, eq⟩

Premises used: Exists.intro
-- 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) (F.map (D.ι i)) :
          (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) (𝟙 (F.obj D.glued)) :
          (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))
⊢ ∃ (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:
exact ⟨i, y, eq⟩
-- 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
pos : ∀ (h : i = j), Mono.{v, u₁} (eqToHom ⋯)
neg : ∀ (h : ¬i = j), Mono (eqToHom ⋯ ≫ D.f i j h)
⊢ Mono.{v, u₁} (C := C) (X := if h : i = j then D.U i else D.V i j h) (Y := D.U i)
    (if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i j h)

Tactic:
split_ifs
-- 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
h : i = j
⊢ Mono.{v, u₁} (eqToHom ⋯)

Tactic:
infer_instance
-- 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
h : ¬i = j
⊢ Mono (eqToHom ⋯ ≫ D.f i j h)

Tactic:
infer_instance
-- 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 : D.J
simp : IsIso.{v, u₁} (eqToHom ⋯)
⊢ IsIso (D.f' i i)

Tactic:
simp only [GlueData'.f', ↓reduceDIte]

Premises used: reduceDIte, CategoryTheory.GlueData'.f'
-- 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 : D.J
⊢ IsIso.{v, u₁} (eqToHom ⋯)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst_1 : Category.{v, u₁} C
C' : Type u₂
inst_2 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : i = j
inst : IsIso (D.f' i j)
⊢ HasPullback (D.f' i j) (D.f' i k)

Tactic:
apply +allowSynthFailures hasPullback_of_left_iso

Premises used: CategoryTheory.Limits.hasPullback_of_left_iso
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst_1 : Category.{v, u₁} C
C' : Type u₂
inst_2 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : i = j
inst : IsIso.{v, u₁} (eqToHom ⋯)
⊢ IsIso (D.f' i j)

Tactic:
simp only [GlueData'.f', dif_pos hij]

Premises used: dif_pos, CategoryTheory.GlueData'.f'
-- 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
hij : i = j
⊢ IsIso.{v, u₁} (eqToHom ⋯)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst_1 : Category.{v, u₁} C
C' : Type u₂
inst_2 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : ¬i = j
hik : i = k
inst : IsIso (D.f' i k)
⊢ HasPullback (D.f' i j) (D.f' i k)

Tactic:
apply +allowSynthFailures hasPullback_of_right_iso

Premises used: CategoryTheory.Limits.hasPullback_of_right_iso
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst_1 : Category.{v, u₁} C
C' : Type u₂
inst_2 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : ¬i = j
hik : i = k
inst : IsIso.{v, u₁} (eqToHom ⋯)
⊢ IsIso (D.f' i k)

Tactic:
simp only [GlueData'.f', dif_pos hik]

Premises used: dif_pos, CategoryTheory.GlueData'.f'
-- 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
hij : ¬i = j
hik : i = k
⊢ IsIso.{v, u₁} (eqToHom ⋯)

Tactic:
infer_instance
-- 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
hij : ¬i = j
hik : ¬i = k
X Y Z : C
f : X ⟶ Y
e : Z = X
subst : ∀ (f : Z ⟶ Y), eqToHom ⋯ ≫ f ≍ f
⊢ eqToHom e ≫ f ≍ f

Tactic:
subst 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
i j k : D.J
hij : ¬i = j
hik : ¬i = k
Y Z : C
f : Z ⟶ Y
⊢ eqToHom ⋯ ≫ f ≍ f

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
i j k : D.J
hij : ¬i = j
hik : ¬i = k
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) (e : Z = X), eqToHom e ≫ f ≍ f

Tactic:
have {X Y Z : C} (f : X ⟶ Y) (e : Z = X) : eqToHom e ≫ f ≍ f := by subst e; 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
i j k : D.J
hij : ¬i = j
hik : ¬i = k
this : ∀ {X Y Z : C} (f : X ⟶ Y) (e : Z = X), eqToHom e ≫ f ≍ f
⊢ HasPullback (D.f i j hij) (D.f i k hik)

Tactic:
D.f_hasPullback i j k hij hik

Premises used: CategoryTheory.GlueData'.f_hasPullback
-- 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
hij : ¬i = j
hik : ¬i = k
this : ∀ {X Y Z : C} (f : X ⟶ Y) (e : Z = X), eqToHom e ≫ f ≍ f
h : (if h : i = j then D.U i else D.V i j h) = D.V i j hij
h₁ : (if h : i = k then D.U i else D.V i k h) = D.V i k hik
h₂ : (if h : i = j then D.U i else D.V i j h) = D.V i j hij → D.f' i j ≍ D.f i j hij
h₃ : (if h : i = k then D.U i else D.V i k h) = D.V i k hik → D.f' i k ≍ D.f i k hik
⊢ HasPullback (D.f' i j) (D.f' i k)

Tactic:
convert! D.f_hasPullback i j k hij hik

Premises used: CategoryTheory.GlueData'.f_hasPullback
-- 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
hij : ¬i = j
hik : ¬i = k
this : ∀ {X Y Z : C} (f : X ⟶ Y) (e : Z = X), eqToHom e ≫ f ≍ f
⊢ (if h : i = j then D.U i else D.V i j h) = D.V i j hij

Tactic:
simp [GlueData'.f', hij, hik, this]

Premises used: CategoryTheory.GlueData'.f'
-- 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
hij : ¬i = j
hik : ¬i = k
this : ∀ {X Y Z : C} (f : X ⟶ Y) (e : Z = X), eqToHom e ≫ f ≍ f
⊢ (if h : i = k then D.U i else D.V i k h) = D.V i k hik

Tactic:
simp [GlueData'.f', hij, hik, this]

Premises used: CategoryTheory.GlueData'.f'
-- 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
hij : ¬i = j
hik : ¬i = k
this : ∀ {X Y Z : C} (f : X ⟶ Y) (e : Z = X), eqToHom e ≫ f ≍ f
e_3 : (if h : i = j then D.U i else D.V i j h) = D.V i j hij
⊢ D.f' i j ≍ D.f i j hij

Tactic:
simp [GlueData'.f', hij, hik, this]

Premises used: CategoryTheory.GlueData'.f'
-- 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
hij : ¬i = j
hik : ¬i = k
this : ∀ {X Y Z : C} (f : X ⟶ Y) (e : Z = X), eqToHom e ≫ f ≍ f
e_4 : (if h : i = k then D.U i else D.V i k h) = D.V i k hik
⊢ D.f' i k ≍ D.f i k hik

Tactic:
simp [GlueData'.f', hij, hik, this]

Premises used: CategoryTheory.GlueData'.f'
-- 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
hij : ¬i = j
if : ∀ (hik : i = k), HasPullback (D.f' i j) (D.f' i k)
if₁ : ∀ (hik : ¬i = k), HasPullback (D.f' i j) (D.f' i k)
if₂ : ∀ (hik : i = k), HasPullback (D.f' i j) (D.f' i k)
if₃ if₄ : ∀ (hik : ¬i = k), HasPullback (D.f' i j) (D.f' i k)
⊢ HasPullback (D.f' i j) (D.f' i k)

Tactic:
if hik : i = k then
    apply +allowSynthFailures hasPullback_of_right_iso
    simp only [GlueData'.f', dif_pos hik]
    infer_instance
  else
    have {X Y Z : C} (f : X ⟶ Y) (e : Z = X) : eqToHom e ≫ f ≍ f := by subst e; simp
    convert! D.f_hasPullback i j k hij hik <;> simp [GlueData'.f', hij, hik, this]

Premises used: CategoryTheory.GlueData'.f', CategoryTheory.Limits.hasPullback_of_right_iso
-- 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
if : ∀ (hij : i = j), HasPullback (D.f' i j) (D.f' i k)
if₁ : ∀ (hij : ¬i = j), HasPullback (D.f' i j) (D.f' i k)
if₂ : ∀ (hij : i = j), HasPullback (D.f' i j) (D.f' i k)
if₃ if₄ : ∀ (hij : ¬i = j), HasPullback (D.f' i j) (D.f' i k)
⊢ HasPullback (D.f' i j) (D.f' i k)

Tactic:
if hij : i = j then
    apply +allowSynthFailures hasPullback_of_left_iso
    simp only [GlueData'.f', dif_pos hij]
    infer_instance
  else if hik : i = k then
    apply +allowSynthFailures hasPullback_of_right_iso
    simp only [GlueData'.f', dif_pos hik]
    infer_instance
  else
    have {X Y Z : C} (f : X ⟶ Y) (e : Z = X) : eqToHom e ≫ f ≍ f := by subst e; simp
    convert! D.f_hasPullback i j k hij hik <;> simp [GlueData'.f', hij, hik, this]

Premises used: CategoryTheory.Limits.hasPullback_of_left_iso, CategoryTheory.GlueData'.f', CategoryTheory.Limits.hasPullback_of_right_iso
-- 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
hij : i = j
⊢ Eq.{u₁ + 1} (α := C) (if h : i = k then D.U i else D.V i k h) (if h : j = k then D.U j else D.V j k h)

Tactic:
aesop
-- 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
hij : i = j
⊢ Eq.{u₁ + 1} (α := C) (if h : i = j then D.U i else D.V i j h) (if h : j = i then D.U j else D.V j i h)

Tactic:
aesop
-- 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
hij : i = j
⊢ D.U i = D.U j

Tactic:
aesop
-- 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
hij : i = j
⊢ D.f' i k ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f' j k

Tactic:
aesop
-- 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
hij : i = j
⊢ D.f' i j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f' j i

Tactic:
aesop
-- 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
hij : ¬i = j
hik : i = k
subst : IsIso (X := pullback (D.f' j i) (D.f' j i)) (pullback.snd (D.f' j i) (D.f' j i))
⊢ IsIso (X := pullback (D.f' j k) (D.f' j i)) (pullback.snd (D.f' j k) (D.f' j i))

Tactic:
subst hik
-- 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
hij : ¬i = j
⊢ IsIso (X := pullback (D.f' j i) (D.f' j i)) (pullback.snd (D.f' j i) (D.f' j i))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst_1 : Category.{v, u₁} C
C' : Type u₂
inst_2 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : j = k
inst : IsIso (D.f' j k)
⊢ IsIso (X := pullback (D.f' j k) (D.f' j i)) (pullback.snd (D.f' j k) (D.f' j i))

Tactic:
apply +allowSynthFailures pullback_snd_iso_of_left_iso

Premises used: CategoryTheory.Limits.pullback_snd_iso_of_left_iso
-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst_1 : Category.{v, u₁} C
C' : Type u₂
inst_2 : Category.{v, u₂} C'
D : GlueData'.{v, u₁} C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : j = k
inst : IsIso.{v, u₁} (eqToHom ⋯)
⊢ IsIso (D.f' j k)

Tactic:
simp only [hjk, GlueData'.f', ↓reduceDIte]

Premises used: reduceDIte, CategoryTheory.GlueData'.f'
-- 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
hij : ¬i = j
hik : ¬i = k
hjk : j = k
⊢ IsIso.{v, u₁} (eqToHom ⋯)

Tactic:
infer_instance
-- 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
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ (if h : i = j then D.U i else D.V i j h) = D.V i j hij

Tactic:
aesop
-- 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
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
rw rw₁ : D.V i k hik = D.V i k hik
⊢ (if h : i = k then D.U i else D.V i k h) = D.V i k hik

Tactic:
rw [dif_neg hik]

Premises used: dif_neg
-- 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
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.U i = D.U 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
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
delta : (if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i j h) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i j hij
⊢ D.f' i j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i j hij

Tactic:
delta f'

Premises used: CategoryTheory.GlueData'.f'
-- 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
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ (if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i j h) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i j hij

Tactic:
aesop
-- 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
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
delta : (if h : i = k then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i k h) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i k hik
⊢ D.f' i k ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i k hik

Tactic:
delta f'

Premises used: CategoryTheory.GlueData'.f'
-- 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
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ (if h : i = k then eqToHom ⋯ else eqToHom ⋯ ≫ D.f i k h) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f i k hik

Tactic:
aesop
-- 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
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.V j k hjk = if h : j = k then D.U j else D.V j k h

Tactic:
aesop
-- 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
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.V j i ⋯ = if h : j = i then D.U j else D.V j i h

Tactic:
aesop
-- 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
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.U j = D.U 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
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
delta : D.f j k hjk ≫ eqToHom ⋯ = eqToHom ⋯ ≫ if h : j = k then eqToHom ⋯ else eqToHom ⋯ ≫ D.f j k h
⊢ D.f j k hjk ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f' j k

Tactic:
delta f'

Premises used: CategoryTheory.GlueData'.f'
-- 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
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f j k hjk ≫ eqToHom ⋯ = eqToHom ⋯ ≫ if h : j = k then eqToHom ⋯ else eqToHom ⋯ ≫ D.f j k h

Tactic:
aesop
-- 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
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
delta : D.f j i ⋯ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ D.f j i h
⊢ D.f j i ⋯ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ D.f' j i

Tactic:
delta f'

Premises used: CategoryTheory.GlueData'.f'
-- 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
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.f j i ⋯ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ D.f j i h

Tactic:
aesop
-- 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 : D.J
simp : IsIso.{v, u₁} (eqToHom ⋯)
⊢ IsIso (D.f' i i)

Tactic:
simp only [↓reduceDIte, GlueData'.f']

Premises used: reduceDIte, CategoryTheory.GlueData'.f'
-- 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
h : i = j
⊢ Eq.{u₁ + 1} (α := C) (if h : (i, j).1 = (i, j).2 then D.U (i, j).1 else D.V (i, j).1 (i, j).2 h)
    (if h : (j, i).1 = (j, i).2 then D.U (j, i).1 else D.V (j, i).1 (j, i).2 h)

Tactic:
simp [h]
-- 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 : D.J
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u₁} (V := C) (if h : (i, i).1 = (i, i).2 then D.U (i, i).1 else D.V (i, i).1 (i, i).2 h)
      (if h : (i, i).1 = (i, i).2 then D.U (i, i).1 else D.V (i, i).1 (i, i).2 h))
    (if h : i = i then eqToHom ⋯ else eqToHom ⋯ ≫ D.t i i h ≫ eqToHom ⋯)
    (𝟙 (if h : (i, i).1 = (i, i).2 then D.U (i, i).1 else D.V (i, i).1 (i, i).2 h))

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
i j k : D.J
delta :
  Eq (α := pullback (D.f' i j) (D.f' i k) ⟶ if h : (j, i).1 = (j, i).2 then D.U (j, i).1 else D.V (j, i).1 (j, i).2 h)
    (CategoryStruct.comp (Y := pullback (D.f' j k) (D.f' j i))
      (if hij : i = j then
        Iso.hom (pullbackSymmetry (D.f' i j) (D.f' i k)) ≫
          pullback.map (D.f' i k) (D.f' i j) (D.f' j k) (D.f' j i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯
      else
        if hik : i = k then
          have this := ⋯;
          pullback.fst (D.f' i j) (D.f' i k) ≫
            eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' j k) (D.f' j i))
        else
          if hjk : j = k then
            have this := ⋯;
            pullback.fst (D.f' i j) (D.f' i k) ≫
              eqToHom ⋯ ≫ D.t i j hij ≫ eqToHom ⋯ ≫ inv (pullback.snd (D.f' j k) (D.f' j i))
          else
            pullback.map (D.f' i j) (D.f' i k) (D.f i j hij) (D.f i k hik) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯ ≫
              D.t' i j k hij hik hjk ≫
                pullback.map (D.f j k hjk) (D.f j i ⋯) (D.f' j k) (D.f' j i) (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯) ⋯ ⋯)
      (pullback.snd (D.f' j k) (D.f' j i)))
    (pullback.fst (D.f' i j) (D.f' i k) ≫ if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.t i j h ≫ eqToHom ⋯)
⊢ D.t'' i j k ≫ pullback.snd (D.f' j k) (D.f' j i) =
    pullback.fst (D.f' i j) (D.f' i k) ≫ if h : i = j then eqToHom ⋯ else eqToHom ⋯ ≫ D.t i j h ≫ eqToHom ⋯

Tactic:
delta GlueData'.t''

Premises used: CategoryTheory.GlueData'.t''