awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
inst_1 : AddCommGroup β
s : β
m n : ℤ
h : ∀ (x : β), x + (m + n) • s = ((fun (b : β) ↦ b + m • s) ∘ fun (b : β) ↦ b + n • s) x
⊢ Eq.{u_1 + 1} (α := β → β) (fun (b : β) ↦ b + (m + n) • s) ((fun (b : β) ↦ b + m • s) ∘ fun (b : β) ↦ b + n • s)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
inst_1 : AddCommGroup β
s : β
m n : ℤ
x : β
h : x + (m + n) • s = x + n • s + m • s
⊢ x + (m + n) • s = ((fun (b : β) ↦ b + m • s) ∘ fun (b : β) ↦ b + n • s) x

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
inst_1 : AddCommGroup β
s : β
m n : ℤ
x : β
h : x + (n + m) • s = x + n • s + m • s
h₁ : x + (n • s + m • s) = x + n • s + m • s
h₂ h₃ : x + (n • s + m • s) = x + (n • s + m • s)
⊢ x + (m + n) • s = x + n • s + m • s

Tactic:
rw [add_comm m n, add_zsmul, add_assoc]

Premises used: add_assoc, add_zsmul, add_comm
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
inst_1 : AddCommGroup β
s : β
X : β → C
t : β
n : ℤ
⊢ Functor.obj (shiftFunctor (GradedObjectWithShift s C) n) X t = X (t + n • s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
β : Type u_1
inst_1 : AddCommGroup β
s : β
X Y : GradedObjectWithShift s C
f : X ⟶ Y
t : β
n : ℤ
⊢ Eq.{v + 1} (α :=
    Functor.obj (shiftFunctor (GradedObjectWithShift s C) n) X t ⟶
      Functor.obj (shiftFunctor (GradedObjectWithShift s C) n) Y t)
    (Functor.map (shiftFunctor (GradedObjectWithShift s C) n) f t :
      Functor.obj (shiftFunctor (GradedObjectWithShift s C) n) X t ⟶
        Functor.obj (shiftFunctor (GradedObjectWithShift s C) n) Y t)
    (f (t + n • s) : X (t + n • s) ⟶ Y (t + n • s))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
β : Type w
X Y : GradedObject β C
b : β
⊢ Eq.{v + 1} (α := X b ⟶ Y b) (0 b) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
β : Type w
⊢ HasZeroObject (GradedObject β C)

Tactic:
⟨⟨fun _ => 0, fun X => ⟨⟨⟨fun b => 0⟩, fun f => ?_⟩⟩, fun X =>
    ⟨⟨⟨fun b => 0⟩, fun f => ?_⟩⟩⟩⟩

Premises used: Unique.mk, CategoryTheory.Limits.HasZeroObject.mk, Nonempty.intro, Exists.intro, OfNat.ofNat, CategoryTheory.Limits.IsZero.mk, Inhabited.mk
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
β : Type w
refine_1 : ∀ (X : GradedObject β C) (f : (fun (x : β) ↦ 0) ⟶ X), f = default
refine_2 : ∀ (X : GradedObject β C) (f : X ⟶ fun (x : β) ↦ 0), f = default
⊢ HasZeroObject (GradedObject β C)

Tactic:
refine ⟨⟨fun _ => 0, fun X => ⟨⟨⟨fun b => 0⟩, fun f => ?_⟩⟩, fun X =>
    ⟨⟨⟨fun b => 0⟩, fun f => ?_⟩⟩⟩⟩
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
β : Type
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{0, v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : GradedObject β C
f g : X ⟶ Y
w :
  Eq (α := Functor.obj.{v, v, u, u} (total β C) X ⟶ Functor.obj.{v, v, u, u} (total β C) Y) (Functor.map (total β C) f)
    (Functor.map (total β C) g)
h : ∀ (i : β), f i = g i
⊢ f = g

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
β : Type
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{0, v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : GradedObject β C
f g : X ⟶ Y
w :
  Eq (α := Functor.obj.{v, v, u, u} (total β C) X ⟶ Functor.obj.{v, v, u, u} (total β C) Y) (Functor.map (total β C) f)
    (Functor.map (total β C) g)
i : β
⊢ Eq.{v + 1} (α := X i ⟶ Functor.obj.{v, v, u, u} (total β C) Y)
    (CategoryStruct.comp (Y := sigmaObj.{0, v, u} fun (i : β) ↦ X i) (Sigma.ι (fun (i : β) ↦ X i) i)
      (Functor.map (total β C) f))
    (CategoryStruct.comp (Y := sigmaObj.{0, v, u} fun (i : β) ↦ X i) (Sigma.ι (fun (i : β) ↦ X i) i)
      (Functor.map (total β C) g))

Tactic:
replace w := Sigma.ι (fun i : β => X i) i ≫= w
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
β : Type
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{0, v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : GradedObject β C
f g : X ⟶ Y
i : β
w :
  Eq.{v + 1} (α := X i ⟶ Functor.obj.{v, v, u, u} (total β C) Y)
    (CategoryStruct.comp (Y := sigmaObj.{0, v, u} fun (i : β) ↦ X i) (Sigma.ι (fun (i : β) ↦ X i) i)
      (Functor.map (total β C) f))
    (CategoryStruct.comp (Y := sigmaObj.{0, v, u} fun (i : β) ↦ X i) (Sigma.ι (fun (i : β) ↦ X i) i)
      (Functor.map (total β C) g))
⊢ Eq.{v + 1} (α := X i ⟶ Functor.obj.{v, v, u, u} (total β C) Y)
    (NatTrans.app (Discrete.natTrans fun (X : Discrete β) ↦ (fun (i : β) ↦ f i) X.as) { as := i } ≫
        colimit.ι (Discrete.functor fun (i : β) ↦ Y i) { as := i : Discrete β } :
      Quiver.Hom.{v, u} (V := C)
        (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : β) ↦ X i) { as := i : Discrete β })
        (colimit.{0, 0, v, u} (J := Discrete β) (Discrete.functor fun (i : β) ↦ Y i)))
    (NatTrans.app (Discrete.natTrans fun (X : Discrete β) ↦ (fun (i : β) ↦ g i) X.as) { as := i } ≫
      colimit.ι (Discrete.functor fun (i : β) ↦ Y i) { as := i : Discrete β })

Tactic:
erw [colimit.ι_map, colimit.ι_map] at w

Premises used: CategoryTheory.Limits.colimit.ι_map
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
β : Type
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{0, v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : GradedObject β C
f g : X ⟶ Y
i : β
w :
  Eq.{v + 1} (α := X i ⟶ Functor.obj.{v, v, u, u} (total β C) Y)
    (NatTrans.app (Discrete.natTrans fun (X : Discrete β) ↦ (fun (i : β) ↦ f i) X.as) { as := i } ≫
        colimit.ι (Discrete.functor fun (i : β) ↦ Y i) { as := i : Discrete β } :
      Quiver.Hom.{v, u} (V := C)
        (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : β) ↦ X i) { as := i : Discrete β })
        (colimit.{0, 0, v, u} (J := Discrete β) (Discrete.functor fun (i : β) ↦ Y i)))
    (NatTrans.app (Discrete.natTrans fun (X : Discrete β) ↦ (fun (i : β) ↦ g i) X.as) { as := i } ≫
      colimit.ι (Discrete.functor fun (i : β) ↦ Y i) { as := i : Discrete β })
⊢ Eq.{v + 1} (α := X i ⟶ colimit.{0, 0, v, u} (Discrete.functor Y)) (f i ≫ colimit.ι (Discrete.functor Y) { as := i })
    (g i ≫ colimit.ι (Discrete.functor Y) { as := i })

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
β : Type
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{0, v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : GradedObject β C
f g : X ⟶ Y
i : β
w :
  Eq.{v + 1} (α := X i ⟶ Functor.obj.{v, v, u, u} (total β C) Y)
    (NatTrans.app (Discrete.natTrans fun (X : Discrete β) ↦ (fun (i : β) ↦ f i) X.as) { as := i } ≫
        colimit.ι (Discrete.functor fun (i : β) ↦ Y i) { as := i : Discrete β } :
      Quiver.Hom.{v, u} (V := C)
        (Functor.obj.{0, v, 0, u} (Discrete.functor fun (i : β) ↦ X i) { as := i : Discrete β })
        (colimit.{0, 0, v, u} (J := Discrete β) (Discrete.functor fun (i : β) ↦ Y i)))
    (NatTrans.app (Discrete.natTrans fun (X : Discrete β) ↦ (fun (i : β) ↦ g i) X.as) { as := i } ≫
      colimit.ι (Discrete.functor fun (i : β) ↦ Y i) { as := i : Discrete β })
⊢ Eq.{v + 1} (α := X i ⟶ colimit.{0, 0, v, u} (Discrete.functor Y)) (f i ≫ colimit.ι (Discrete.functor Y) { as := i })
    (g i ≫ colimit.ι (Discrete.functor Y) { as := i })

Tactic:
replace w : f i ≫ colimit.ι (Discrete.functor Y) ⟨i⟩ =
      g i ≫ colimit.ι (Discrete.functor Y) ⟨i⟩ := by simpa
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
β : Type
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{0, v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : GradedObject β C
f g : X ⟶ Y
i : β
w :
  Eq.{v + 1} (α := X i ⟶ colimit.{0, 0, v, u} (Discrete.functor Y)) (f i ≫ colimit.ι (Discrete.functor Y) { as := i })
    (g i ≫ colimit.ι (Discrete.functor Y) { as := i })
⊢ f i = g i

Tactic:
Mono.right_cancellation _ _ w

Premises used: CategoryTheory.Mono.right_cancellation
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
β : Type
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{0, v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
X Y : GradedObject β C
f g : X ⟶ Y
i : β
w :
  Eq.{v + 1} (α := X i ⟶ colimit.{0, 0, v, u} (Discrete.functor Y)) (f i ≫ colimit.ι (Discrete.functor Y) { as := i })
    (g i ≫ colimit.ι (Discrete.functor Y) { as := i })
⊢ f i = g i

Tactic:
exact Mono.right_cancellation _ _ w

Premises used: CategoryTheory.Mono.right_cancellation
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
I : Type u_1
J : Type u_2
C : Type u_4
inst : Category.{v_1, u_4} C
X Y : GradedObject I C
e : X ≅ Y
p : I → J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
j : J
have :
  ∀
    (α :
      Iso (C := Functor.{u_1, v_1, u_1, u_4} (Discrete (↑(p ⁻¹' {j}) : Type u_1)) C)
        (Discrete.functor (X.mapObjFun p j)) (Discrete.functor (Y.mapObjFun p j))),
    HasCoproduct.{u_1, v_1, u_4} (Y.mapObjFun p j)
⊢ HasCoproduct.{u_1, v_1, u_4} (Y.mapObjFun p j)

Tactic:
have α : Discrete.functor (X.mapObjFun p j) ≅ Discrete.functor (Y.mapObjFun p j) :=
    Discrete.natIso (fun ⟨i, _⟩ => (GradedObject.eval i).mapIso e)
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
I : Type u_1
J : Type u_2
C : Type u_4
inst : Category.{v_1, u_4} C
X Y : GradedObject I C
e : X ≅ Y
p : I → J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
j : J
α :
  Iso (C := Functor.{u_1, v_1, u_1, u_4} (Discrete (↑(p ⁻¹' {j}) : Type u_1)) C) (Discrete.functor (X.mapObjFun p j))
    (Discrete.functor (Y.mapObjFun p j))
⊢ HasCoproduct.{u_1, v_1, u_4} (Y.mapObjFun p j)

Tactic:
hasColimit_of_iso α.symm

Premises used: CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
I : Type u_1
J : Type u_2
C : Type u_4
inst : Category.{v_1, u_4} C
X Y : GradedObject I C
e : X ≅ Y
p : I → J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
j : J
α :
  Iso (C := Functor.{u_1, v_1, u_1, u_4} (Discrete (↑(p ⁻¹' {j}) : Type u_1)) C) (Discrete.functor (X.mapObjFun p j))
    (Discrete.functor (Y.mapObjFun p j))
⊢ HasCoproduct.{u_1, v_1, u_4} (Y.mapObjFun p j)

Tactic:
exact hasColimit_of_iso α.symm

Premises used: CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
I : Type u_1
J : Type u_2
C : Type u_4
inst : Category.{v_1, u_4} C
X : GradedObject I C
p : I → J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
A : C
j : J
f g : mapObj.{u_1, u_2, v_1, u_4} X p j ⟶ A
hfg : ∀ (i : I) (hij : p i = j), X.ιMapObj p i j hij ≫ f = X.ιMapObj p i j hij ≫ g
⊢ f = g

Tactic:
Cofan.IsColimit.hom_ext (X.isColimitCofanMapObj p j) _ _ (fun ⟨i, hij⟩ => hfg i hij)

Premises used: CategoryTheory.GradedObject.ιMapObj, CategoryTheory.GradedObject.cofanMapObj, CategoryTheory.Limits.Cofan.IsColimit.hom_ext, CategoryTheory.Limits.colimit, CategoryTheory.Discrete.natTrans, _private.0.CategoryTheory.GradedObject.mapObj_ext.match_1, CategoryTheory.Limits.Cofan.inj, CategoryTheory.GradedObject.isColimitCofanMapObj, CategoryTheory.CategoryStruct.comp, CategoryTheory.GradedObject.mapObj, Eq, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
I : Type u_1
J : Type u_2
C : Type u_4
inst : Category.{v_1, u_4} C
X : GradedObject I C
p : I → J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
A : C
j : J
φ : (i : I) → p i = j → (X i ⟶ A)
i : I
hi : p i = j
⊢ CategoryStruct.comp (Y := mapObj.{u_1, u_2, v_1, u_4} X p j) (X.ιMapObj p i j hi) (X.descMapObj p φ) = φ i hi

Tactic:
apply Cofan.IsColimit.fac

Premises used: CategoryTheory.Limits.Cofan.IsColimit.fac
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
I : Type u_1
J : Type u_2
C : Type u_4
inst : Category.{v_1, u_4} C
X : GradedObject I C
p : I → J
c : (j : J) → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → IsColimit (c j)
⊢ HasMap.{u_1, u_2, v_1, u_4} X p

Tactic:
fun j => ⟨_, hc j⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
I : Type u_1
J : Type u_2
C : Type u_4
inst : Category.{v_1, u_4} C
X : GradedObject I C
p : I → J
j : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
c : CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : IsColimit c
i : I
hi : p i = j
⊢ Eq (α := X.mapObjFun p j (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {j}) i hi) ⟶ mapObj.{u_1, u_2, v_1, u_4} X p j)
    (Cofan.inj c (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {j}) i hi) ≫ Iso.hom (iso hc)) (X.ιMapObj p i j hi)

Tactic:
apply IsColimit.comp_coconePointUniqueUpToIso_hom

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
I : Type u_1
J : Type u_2
C : Type u_4
inst : Category.{v_1, u_4} C
X : GradedObject I C
p : I → J
j : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
c : CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : IsColimit c
i : I
hi : p i = j
⊢ CategoryStruct.comp (Y := mapObj.{u_1, u_2, v_1, u_4} X p j) (X.ιMapObj p i j hi) (Iso.inv (iso hc)) =
    Cofan.inj c (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {j}) i hi)

Tactic:
apply IsColimit.comp_coconePointUniqueUpToIso_inv

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
I : Type u_1
J : Type u_2
C : Type u_4
inst : Category.{v_1, u_4} C
X Y : GradedObject I C
φ : X ⟶ Y
p : I → J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
i : I
j : J
hij : p i = j
⊢ Eq (α := X i ⟶ mapObj.{u_1, u_2, v_1, u_4} Y p j)
    (CategoryStruct.comp (Y := mapObj.{u_1, u_2, v_1, u_4} X p j) (X.ιMapObj p i j hij) (mapMap φ p j))
    (φ i ≫ Y.ιMapObj p i j hij)

Tactic:
simp only [mapMap, ι_descMapObj]

Premises used: CategoryTheory.GradedObject.mapMap, CategoryTheory.GradedObject.ι_descMapObj
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
I : Type u_1
J : Type u_2
C : Type u_4
inst : Category.{v_1, u_4} C
X Y : GradedObject I C
p : I → J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
φ₁ φ₂ : X ⟶ Y
h : φ₁ = φ₂
subst : Eq (α := mapObj.{u_1, u_2, v_1, u_4} X p ⟶ mapObj.{u_1, u_2, v_1, u_4} Y p) (mapMap φ₁ p) (mapMap φ₁ p)
⊢ Eq (α := mapObj.{u_1, u_2, v_1, u_4} X p ⟶ mapObj.{u_1, u_2, v_1, u_4} Y p) (mapMap φ₁ p) (mapMap φ₂ p)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
I : Type u_1
J : Type u_2
C : Type u_4
inst : Category.{v_1, u_4} C
X Y : GradedObject I C
p : I → J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
φ₁ : X ⟶ Y
⊢ Eq (α := mapObj.{u_1, u_2, v_1, u_4} X p ⟶ mapObj.{u_1, u_2, v_1, u_4} Y p) (mapMap φ₁ p) (mapMap φ₁ p)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
k : K
c : (j : J) → q j = k → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = k) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {k}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
i : I
hi rw : r i = k
rw₁ rw₂ : k = k
⊢ q (p i) = k

Tactic:
rw [hpqr, hi]
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
k : K
c : (j : J) → q j = k → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = k) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {k}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
i : I
hi : r i = k
rw : Membership.mem (γ := Set K) {k} (q (p i))
rw₁ : q (p i) = k
rw₂ : r i = k
rw₃ rw₄ : k = k
⊢ p i ∈ q ⁻¹' {k}

Tactic:
rw [Set.mem_preimage, Set.mem_singleton_iff, hpqr, hi]

Premises used: Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j_1 : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
k : K
c : (j : J) → q j = k → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = k) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {k}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
s : Cofan.{u_1, v_1, u_4} (X.mapObjFun r k)
x : (↑(q ⁻¹' {k}) : Type u_2)
j : J
hj : q j = k
x_1 : (↑(p ⁻¹' {j}) : Type u_1)
i : I
hi : p i = j
⊢ i ∈ r ⁻¹' {k}

Tactic:
simp only [Set.mem_preimage, Set.mem_singleton_iff, ← hpqr, hi, hj]

Premises used: Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
k : K
c : (j : J) → q j = k → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = k) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {k}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
s : Cofan.{u_1, v_1, u_4} (X.mapObjFun r k)
x : (↑(r ⁻¹' {k}) : Type u_1)
i : I
hi : r i = k
⊢ Eq (α := X.mapObjFun r k (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {k}) i hi) ⟶ s.pt)
    (Cofan.inj (X.cofanMapObjComp p q r hpqr k c c') (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {k}) i hi) ≫
      (fun (s : Cofan.{u_1, v_1, u_4} (X.mapObjFun r k)) ↦
          (Cofan.IsColimit.desc hc' fun (x : (↑(q ⁻¹' {k}) : Type u_2)) ↦
              match (motive := (x : (↑(q ⁻¹' {k}) : Type u_2)) → (c (↑x : J) ⋯).pt ⟶ s.pt) x with
              | ⟨j, hj⟩ =>
                Cofan.IsColimit.desc (hc j hj) fun (x : (↑(p ⁻¹' {j}) : Type u_1)) ↦
                  match (motive := (x : (↑(p ⁻¹' {j}) : Type u_1)) → X.mapObjFun p j x ⟶ s.pt) x with
                  | ⟨i, hi⟩ => s.inj (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {k}) i ⋯) :
            c'.pt ⟶ s.pt))
        s)
    (s.inj (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {k}) i hi))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
k : K
c : (j : J) → q j = k → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = k) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {k}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
s : Cofan.{u_1, v_1, u_4} (X.mapObjFun r k)
m : (X.cofanMapObjComp p q r hpqr k c c').pt ⟶ s.pt
hm : ∀ (j : (↑(r ⁻¹' {k}) : Type u_1)), Cofan.inj (X.cofanMapObjComp p q r hpqr k c c') j ≫ m = s.inj j
h :
  ∀ (i : (↑(q ⁻¹' {k}) : Type u_2)),
    c'.inj i ≫ m =
      c'.inj i ≫
        (fun (s : Cofan.{u_1, v_1, u_4} (X.mapObjFun r k)) ↦
            (Cofan.IsColimit.desc hc' fun (x : (↑(q ⁻¹' {k}) : Type u_2)) ↦
                match (motive := (x : (↑(q ⁻¹' {k}) : Type u_2)) → (c (↑x : J) ⋯).pt ⟶ s.pt) x with
                | ⟨j, hj⟩ =>
                  Cofan.IsColimit.desc (hc j hj) fun (x : (↑(p ⁻¹' {j}) : Type u_1)) ↦
                    match (motive := (x : (↑(p ⁻¹' {j}) : Type u_1)) → X.mapObjFun p j x ⟶ s.pt) x with
                    | ⟨i, hi⟩ => s.inj (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {k}) i ⋯) :
              c'.pt ⟶ s.pt))
          s
⊢ m =
    (fun (s : Cofan.{u_1, v_1, u_4} (X.mapObjFun r k)) ↦
        (Cofan.IsColimit.desc hc' fun (x : (↑(q ⁻¹' {k}) : Type u_2)) ↦
            match (motive := (x : (↑(q ⁻¹' {k}) : Type u_2)) → (c (↑x : J) ⋯).pt ⟶ s.pt) x with
            | ⟨j, hj⟩ =>
              Cofan.IsColimit.desc (hc j hj) fun (x : (↑(p ⁻¹' {j}) : Type u_1)) ↦
                match (motive := (x : (↑(p ⁻¹' {j}) : Type u_1)) → X.mapObjFun p j x ⟶ s.pt) x with
                | ⟨i, hi⟩ => s.inj (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {k}) i ⋯) :
          c'.pt ⟶ s.pt))
      s

Tactic:
apply Cofan.IsColimit.hom_ext hc'

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.GradedObject
Goal:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j_1 : J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
inst_2 : HasMap.{u_1, u_2, v_1, u_4} Y p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
j : J
c : (j_2 : J) → q j_2 = q j → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j_2
hc : (j_2 : J) → (hj : q j_2 = q j) → IsColimit (c j_2 hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j_2 : (↑(q ⁻¹' {q j}) : Type u_2)) ↦ (c (↑j_2 : J) ⋯).pt
hc' : IsColimit c'
s : Cofan.{u_1, v_1, u_4} (β := (↑(r ⁻¹' {q j}) : Type u_1)) (X.mapObjFun r (q j))
m : (X.cofanMapObjComp p q r hpqr (q j) c c').pt ⟶ s.pt
hm : ∀ (j_2 : (↑(r ⁻¹' {q j}) : Type u_1)), Cofan.inj (X.cofanMapObjComp p q r hpqr (q j) c c') j_2 ≫ m = s.inj j_2
h :
  ∀ (i : (↑(p ⁻¹' {j}) : Type u_1)),
    Eq (α := X.mapObjFun p j i ⟶ s.pt)
      (Cofan.inj (c j ⋯) i ≫ c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q j}) j ⋯) ≫ m)
      (Cofan.inj (c j ⋯) i ≫
        c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q j}) j ⋯) ≫
          (fun (s : Cofan.{u_1, v_1, u_4} (β := (↑(r ⁻¹' {q j}) : Type u_1)) (X.mapObjFun r (q j))) ↦
              (Cofan.IsColimit.desc hc' fun (x : (↑(q ⁻¹' {q j}) : Type u_2)) ↦
                  match (motive := (x : (↑(q ⁻¹' {q j}) : Type u_2)) → (c (↑x : J) ⋯).pt ⟶ s.pt) x with
                  | ⟨j_2, hj⟩ =>
                    Cofan.IsColimit.desc (hc j_2 hj) fun (x : (↑(p ⁻¹' {j_2}) : Type u_1)) ↦
                      match (motive := (x : (↑(p ⁻¹' {j_2}) : Type u_1)) → X.mapObjFun p j_2 x ⟶ s.pt) x with
                      | ⟨i, hi⟩ => s.inj (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {q j}) i ⋯) :
                c'.pt ⟶ s.pt))
            s)
⊢ Eq (α :=
    Cocone.pt.{u_1, v_1, u_1, u_4} (J :=
        Discrete (↑(p ⁻¹' {(↑(Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q j}) j ⋯) : J)}) : Type u_1))
        (c (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q j}) j ⋯) : J) ⋯) ⟶
      s.pt)
    (c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q j}) j ⋯) ≫ m)
    (c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q j}) j ⋯) ≫
      (fun (s : Cofan.{u_1, v_1, u_4} (β := (↑(r ⁻¹' {q j}) : Type u_1)) (X.mapObjFun r (q j))) ↦
          (Cofan.IsColimit.desc hc' fun (x : (↑(q ⁻¹' {q j}) : Type u_2)) ↦
              match (motive := (x : (↑(q ⁻¹' {q j}) : Type u_2)) → (c (↑x : J) ⋯).pt ⟶ s.pt) x with
              | ⟨j_2, hj⟩ =>
                Cofan.IsColimit.desc (hc j_2 hj) fun (x : (↑(p ⁻¹' {j_2}) : Type u_1)) ↦
                  match (motive := (x : (↑(p ⁻¹' {j_2}) : Type u_1)) → X.mapObjFun p j_2 x ⟶ s.pt) x with
                  | ⟨i, hi⟩ => s.inj (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {q j}) i ⋯) :
            c'.pt ⟶ s.pt))
        s)

Tactic:
apply Cofan.IsColimit.hom_ext (hc j rfl)

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext, rfl