awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
i : I
c : (j : J) → q j = q (p i) → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = q (p i)) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {q (p i)}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
s : Cofan.{u_1, v_1, u_4} (β := (↑(r ⁻¹' {q (p i)}) : Type u_1)) (X.mapObjFun r (q (p i)))
m : (X.cofanMapObjComp p q r hpqr (q (p i)) c c').pt ⟶ s.pt
hm : ∀ (j : (↑(r ⁻¹' {q (p i)}) : Type u_1)), Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') j ≫ m = s.inj j
h :
  Eq (α := X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ⟶ s.pt)
    (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫ m)
    (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫
        Cofan.IsColimit.desc hc' fun (x : (↑(q ⁻¹' {q (p i)}) : Type u_2)) ↦
          Cofan.IsColimit.desc (hc (↑x : J) ⋯) fun (x_1 : (↑(p ⁻¹' {(↑x : J)}) : Type u_1)) ↦
            s.inj (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {q (p i)}) (↑x_1 : I) ⋯))
⊢ Eq (α := X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ⟶ s.pt)
    (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫ m)
    (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫
        (fun (s : Cofan.{u_1, v_1, u_4} (β := (↑(r ⁻¹' {q (p i)}) : Type u_1)) (X.mapObjFun r (q (p i)))) ↦
            (Cofan.IsColimit.desc hc' fun (x : (↑(q ⁻¹' {q (p i)}) : Type u_2)) ↦
                match (motive := (x : (↑(q ⁻¹' {q (p i)}) : 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_1, hi⟩ => s.inj (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {q (p i)}) i_1 ⋯) :
              c'.pt ⟶ s.pt))
          s)

Tactic:
dsimp
-- 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
i : I
c : (j : J) → q j = q (p i) → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = q (p i)) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {q (p i)}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
s : Cofan.{u_1, v_1, u_4} (β := (↑(r ⁻¹' {q (p i)}) : Type u_1)) (X.mapObjFun r (q (p i)))
m : (X.cofanMapObjComp p q r hpqr (q (p i)) c c').pt ⟶ s.pt
hm : ∀ (j : (↑(r ⁻¹' {q (p i)}) : Type u_1)), Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') j ≫ m = s.inj j
h :
  Eq (α := X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ⟶ s.pt)
    (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫ m)
    (Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c')
        (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {q (p i)})
          (↑(Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) : I) ⋯) ≫
      m)
⊢ Eq (α := X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ⟶ s.pt)
    (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫ m)
    (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫
        Cofan.IsColimit.desc hc' fun (x : (↑(q ⁻¹' {q (p i)}) : Type u_2)) ↦
          Cofan.IsColimit.desc (hc (↑x : J) ⋯) fun (x_1 : (↑(p ⁻¹' {(↑x : J)}) : Type u_1)) ↦
            s.inj (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {q (p i)}) (↑x_1 : I) ⋯))

Tactic:
rw [Cofan.IsColimit.fac, Cofan.IsColimit.fac, ← hm]

Premises used: CategoryTheory.Limits.Cofan.IsColimit.fac
-- 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
i : I
c : (j : J) → q j = q (p i) → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = q (p i)) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {q (p i)}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
s : Cofan.{u_1, v_1, u_4} (β := (↑(r ⁻¹' {q (p i)}) : Type u_1)) (X.mapObjFun r (q (p i)))
m : (X.cofanMapObjComp p q r hpqr (q (p i)) c c').pt ⟶ s.pt
hm : ∀ (j : (↑(r ⁻¹' {q (p i)}) : Type u_1)), Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') j ≫ m = s.inj j
h :
  Eq (α := X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ⟶ s.pt)
    (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫ m)
    (CategoryStruct.comp (Y := Cocone.pt.{u_1, v_1, u_1, u_4} (J := Discrete (↑(p ⁻¹' {p i}) : Type u_1)) (c (p i) ⋯))
        (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) :
          X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ⟶
            Cocone.pt.{u_1, v_1, u_1, u_4} (J := Discrete (↑(p ⁻¹' {p i}) : Type u_1)) (F :=
              (Discrete.functor (X.mapObjFun p (p i)) :
                Functor.{u_1, v_1, u_1, u_4} (Discrete (↑(p ⁻¹' {p i}) : Type u_1)) C))
              (c (p i) ⋯ : CofanMapObjFun.{u_1, u_2, v_1, u_4} X p (p i)))
        (c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) :
          Cocone.pt.{u_1, v_1, u_1, u_4} (J :=
              Discrete (↑(p ⁻¹' {(↑(Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) : J)}) : Type u_1))
              (c (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) : J) ⋯) ⟶
            c'.pt) ≫
      m)
⊢ Eq (α := X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ⟶ s.pt)
    (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫ m)
    (Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c')
        (Subtype.mk (p := fun (x : I) ↦ x ∈ r ⁻¹' {q (p i)})
          (↑(Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) : I) ⋯) ≫
      m)

Tactic:
dsimp
-- 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
i : I
c : (j : J) → q j = q (p i) → CofanMapObjFun.{u_1, u_2, v_1, u_4} X p j
hc : (j : J) → (hj : q j = q (p i)) → IsColimit (c j hj)
c' : Cofan.{u_2, v_1, u_4} (C := C) fun (j : (↑(q ⁻¹' {q (p i)}) : Type u_2)) ↦ (c (↑j : J) ⋯).pt
hc' : IsColimit c'
s : Cofan.{u_1, v_1, u_4} (β := (↑(r ⁻¹' {q (p i)}) : Type u_1)) (X.mapObjFun r (q (p i)))
m : (X.cofanMapObjComp p q r hpqr (q (p i)) c c').pt ⟶ s.pt
hm : ∀ (j : (↑(r ⁻¹' {q (p i)}) : Type u_1)), Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') j ≫ m = s.inj j
h h₁ :
  Eq (α := X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ⟶ s.pt)
    (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫ m)
    (CategoryStruct.comp (Y := Cocone.pt.{u_1, v_1, u_1, u_4} (J := Discrete (↑(p ⁻¹' {p i}) : Type u_1)) (c (p i) ⋯))
      (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) :
        X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ⟶
          Cocone.pt.{u_1, v_1, u_1, u_4} (J := Discrete (↑(p ⁻¹' {p i}) : Type u_1)) (F :=
            (Discrete.functor (X.mapObjFun p (p i)) :
              Functor.{u_1, v_1, u_1, u_4} (Discrete (↑(p ⁻¹' {p i}) : Type u_1)) C))
            (c (p i) ⋯ : CofanMapObjFun.{u_1, u_2, v_1, u_4} X p (p i)))
      (c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫ m :
        Cocone.pt.{u_1, v_1, u_1, u_4} (J := Discrete (↑(p ⁻¹' {p i}) : Type u_1)) (c (p i) ⋯) ⟶ s.pt))
⊢ Eq (α := X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ⟶ s.pt)
    (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ≫
      c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) ≫ m)
    (CategoryStruct.comp (Y := Cocone.pt.{u_1, v_1, u_1, u_4} (J := Discrete (↑(p ⁻¹' {p i}) : Type u_1)) (c (p i) ⋯))
        (Cofan.inj (c (p i) ⋯) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) :
          X.mapObjFun p (p i) (Subtype.mk (p := fun (x : I) ↦ x ∈ p ⁻¹' {p i}) i ⋯) ⟶
            Cocone.pt.{u_1, v_1, u_1, u_4} (J := Discrete (↑(p ⁻¹' {p i}) : Type u_1)) (F :=
              (Discrete.functor (X.mapObjFun p (p i)) :
                Functor.{u_1, v_1, u_1, u_4} (Discrete (↑(p ⁻¹' {p i}) : Type u_1)) C))
              (c (p i) ⋯ : CofanMapObjFun.{u_1, u_2, v_1, u_4} X p (p i)))
        (c'.inj (Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) :
          Cocone.pt.{u_1, v_1, u_1, u_4} (J :=
              Discrete (↑(p ⁻¹' {(↑(Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) : J)}) : Type u_1))
              (c (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ q ⁻¹' {q (p i)}) (p i) ⋯) : J) ⋯) ⟶
            c'.pt) ≫
      m)

Tactic:
rw [assoc]

Premises used: CategoryTheory.Category.assoc
-- 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 : GradedObject I C
p : I → J
inst_1 : HasMap.{u_1, u_2, v_1, u_4} X p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
inst_2 : HasMap.{u_2, u_3, v_1, u_4} (mapObj.{u_1, u_2, v_1, u_4} X p) q
⊢ HasMap.{u_1, u_3, v_1, u_4} X r

Tactic:
fun k => ⟨_, isColimitCofanMapObjComp X p q r hpqr k _
    (fun j _ => X.isColimitCofanMapObj p j) _ ((X.mapObj p).isColimitCofanMapObj q k)⟩

Premises used: CategoryTheory.GradedObject.isColimitCofanMapObjComp, CategoryTheory.GradedObject.cofanMapObj, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.GradedObject.isColimitCofanMapObj, CategoryTheory.GradedObject.mapObj, CategoryTheory.GradedObject.cofanMapObjComp
-- 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
inst_2 : HasZeroMorphisms.{v_1, u_4} C
inst_3 : DecidableEq J
i : I
j : J
h : p i = j
⊢ Eq.{v_1 + 1} (α := X i ⟶ mapObj.{u_1, u_2, v_1, u_4} X p j) (X.ιMapObjOrZero p i j) (X.ιMapObj p i j h)

Tactic:
dif_pos h

Premises used: dif_pos, CategoryTheory.GradedObject.ιMapObjOrZero
-- 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
inst_2 : HasZeroMorphisms.{v_1, u_4} C
inst_3 : DecidableEq J
i : I
j : J
h : p i ≠ j
⊢ Eq.{v_1 + 1} (α := X i ⟶ mapObj.{u_1, u_2, v_1, u_4} X p j) (X.ιMapObjOrZero p i j) 0

Tactic:
dif_neg h

Premises used: dif_neg, CategoryTheory.GradedObject.ιMapObjOrZero
-- 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
inst_3 : HasZeroMorphisms.{v_1, u_4} C
inst_4 : DecidableEq J
i : I
j : J
pos :
  ∀ (h : 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.ιMapObjOrZero p i j) (mapMap φ p j))
      (φ i ≫ Y.ιMapObjOrZero p i j)
neg :
  ∀ (h : ¬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.ιMapObjOrZero p i j) (mapMap φ p j))
      (φ i ≫ Y.ιMapObjOrZero 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.ιMapObjOrZero p i j) (mapMap φ p j))
    (φ i ≫ Y.ιMapObjOrZero p i j)

Tactic:
by_cases h : p i = j
-- 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
inst_3 : HasZeroMorphisms.{v_1, u_4} C
inst_4 : DecidableEq J
i : I
j : J
h : 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.ιMapObjOrZero p i j) (mapMap φ p j))
    (φ i ≫ Y.ιMapObjOrZero p i j)

Tactic:
simp only [ιMapObjOrZero_eq _ _ _ _ h, ι_mapMap]

Premises used: CategoryTheory.GradedObject.ιMapObjOrZero_eq, CategoryTheory.GradedObject.ι_mapMap
-- 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
inst_3 : HasZeroMorphisms.{v_1, u_4} C
inst_4 : DecidableEq J
i : I
j : J
h : ¬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.ιMapObjOrZero p i j) (mapMap φ p j))
    (φ i ≫ Y.ιMapObjOrZero p i j)

Tactic:
simp only [ιMapObjOrZero_eq_zero _ _ _ _ h, zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp, CategoryTheory.GradedObject.ιMapObjOrZero_eq_zero
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f g : X.Hom Y
w_base : f.base = g.base
rw rw₁ : (F.map g.base).toFunctor.obj X.fiber = (F.map g.base).toFunctor.obj X.fiber
⊢ (F.map g.base).toFunctor.obj X.fiber = (F.map f.base).toFunctor.obj X.fiber

Tactic:
rw [w_base]
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f g : X.Hom Y
w_base : f.base = g.base
w_fiber : eqToHom ⋯ ≫ f.fiber = g.fiber
mk :
  ∀ (base : X.base ⟶ Y.base) (fiber : (F.map base).toFunctor.obj X.fiber ⟶ Y.fiber)
    (w_base : { base := base, fiber := fiber : X.Hom Y }.base = g.base)
    (w_fiber : eqToHom ⋯ ≫ { base := base, fiber := fiber : X.Hom Y }.fiber = g.fiber),
    { base := base, fiber := fiber : X.Hom Y } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
g : X.Hom Y
base : X.base ⟶ Y.base
fiber : (F.map base).toFunctor.obj X.fiber ⟶ Y.fiber
w_base : { base := base, fiber := fiber : X.Hom Y }.base = g.base
w_fiber : eqToHom ⋯ ≫ { base := base, fiber := fiber : X.Hom Y }.fiber = g.fiber
mk :
  ∀ (base_1 : X.base ⟶ Y.base) (fiber_1 : (F.map base_1).toFunctor.obj X.fiber ⟶ Y.fiber)
    (w_base : { base := base, fiber := fiber : X.Hom Y }.base = { base := base_1, fiber := fiber_1 }.base)
    (w_fiber :
      eqToHom ⋯ ≫ { base := base, fiber := fiber : X.Hom Y }.fiber = { base := base_1, fiber := fiber_1 }.fiber),
    { base := base, fiber := fiber : X.Hom Y } = { base := base_1, fiber := fiber_1 }
⊢ { base := base, fiber := fiber : X.Hom Y } = g

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
base : X.base ⟶ Y.base
fiber : (F.map base).toFunctor.obj X.fiber ⟶ Y.fiber
base_1 : X.base ⟶ Y.base
fiber_1 : (F.map base_1).toFunctor.obj X.fiber ⟶ Y.fiber
w_base : { base := base, fiber := fiber : X.Hom Y }.base = { base := base_1, fiber := fiber_1 }.base
w_fiber : eqToHom ⋯ ≫ { base := base, fiber := fiber : X.Hom Y }.fiber = { base := base_1, fiber := fiber_1 }.fiber
mk : fiber ≍ fiber_1
⊢ { base := base, fiber := fiber : X.Hom Y } = { base := base_1, fiber := fiber_1 }

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ (F.map (𝟙 X.base)).toFunctor.obj X.fiber = X.fiber

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y Z : Grothendieck F
f : X.Hom Y
g : Y.Hom Z
⊢ (F.map (f.base ≫ g.base)).toFunctor.obj X.fiber = (F.map g.base).toFunctor.obj ((F.map f.base).toFunctor.obj X.fiber)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
w_base : (comp X.id f).base = f.base
w_fiber : eqToHom ⋯ ≫ (comp X.id f).fiber = f.fiber
⊢ comp X.id f = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ (comp X.id f).base = f.base

Tactic:
simp [comp, id]

Premises used: CategoryTheory.Grothendieck.id, CategoryTheory.Grothendieck.comp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ eqToHom ⋯ ≫ (comp X.id f).fiber = f.fiber

Tactic:
simp [comp, id]

Premises used: CategoryTheory.Grothendieck.id, CategoryTheory.Grothendieck.comp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
w_base : (comp f Y.id).base = f.base
w_fiber : eqToHom ⋯ ≫ (comp f Y.id).fiber = f.fiber
⊢ comp f Y.id = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ (comp f Y.id).base = f.base

Tactic:
simp [comp, id]

Premises used: CategoryTheory.Grothendieck.id, CategoryTheory.Grothendieck.comp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
w_fiber : eqToHom ⋯ ≫ eqToHom ⋯ ≫ (F.map (𝟙 Y.base)).toFunctor.map f.fiber ≫ eqToHom ⋯ = f.fiber
⊢ eqToHom ⋯ ≫ (comp f Y.id).fiber = f.fiber

Tactic:
dsimp [comp, id]

Premises used: CategoryTheory.Grothendieck.id, CategoryTheory.Grothendieck.comp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
w_fiber :
  eqToHom ⋯ ≫
      eqToHom ⋯ ≫
        (NatTrans.app (Iso.hom (Cat.Hom.toNatIso (eqToIso ⋯) ≪≫ eqToIso ⋯)) ((F.map f.base).toFunctor.obj X.fiber) ≫
            map (𝟭 (↑(F.obj Y.base) : Type u₂)) f.fiber ≫
              NatTrans.app (Iso.inv (Cat.Hom.toNatIso (eqToIso ⋯) ≪≫ eqToIso ⋯)) Y.fiber) ≫
          eqToHom ⋯ =
    f.fiber
⊢ eqToHom ⋯ ≫ eqToHom ⋯ ≫ (F.map (𝟙 Y.base)).toFunctor.map f.fiber ≫ eqToHom ⋯ = f.fiber

Tactic:
rw [← NatIso.naturality_2 ((Cat.Hom.toNatIso <| eqToIso (F.map_id Y.base)) ≪≫
        (eqToIso Cat.Hom.id_toFunctor)) f.fiber]

Premises used: CategoryTheory.Grothendieck.base, CategoryTheory.eqToIso, CategoryTheory.Cat.Hom.toNatIso, CategoryTheory.Grothendieck.Hom.fiber, CategoryTheory.Functor.map_id, CategoryTheory.Iso.trans, CategoryTheory.NatIso.naturality_2, CategoryTheory.Cat.Hom.id_toFunctor
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f : X.Hom Y
⊢ eqToHom ⋯ ≫
      eqToHom ⋯ ≫
        (NatTrans.app (Iso.hom (Cat.Hom.toNatIso (eqToIso ⋯) ≪≫ eqToIso ⋯)) ((F.map f.base).toFunctor.obj X.fiber) ≫
            map (𝟭 (↑(F.obj Y.base) : Type u₂)) f.fiber ≫
              NatTrans.app (Iso.inv (Cat.Hom.toNatIso (eqToIso ⋯) ≪≫ eqToIso ⋯)) Y.fiber) ≫
          eqToHom ⋯ =
    f.fiber

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
W X Y Z : Grothendieck F
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
w_base : (comp (comp f g) h).base = (comp f (comp g h)).base
w_fiber : eqToHom ⋯ ≫ (comp (comp f g) h).fiber = (comp f (comp g h)).fiber
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
W X Y Z : Grothendieck F
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
⊢ (comp (comp f g) h).base = (comp f (comp g h)).base

Tactic:
simp [comp]

Premises used: CategoryTheory.Grothendieck.comp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
W X Y Z : Grothendieck F
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
⊢ eqToHom ⋯ ≫ (comp (comp f g) h).fiber = (comp f (comp g h)).fiber

Tactic:
simp [comp, ← NatIso.naturality_2 (Cat.Hom.toNatIso (eqToIso (F.map_comp g.base h.base)) ≪≫
        (eqToIso (Cat.Hom.comp_toFunctor _ _))) f.fiber]

Premises used: CategoryTheory.eqToIso, CategoryTheory.Cat.Hom.comp_toFunctor, CategoryTheory.Cat.Hom.toNatIso, CategoryTheory.Grothendieck.Hom.fiber, CategoryTheory.Iso.trans, CategoryTheory.NatIso.naturality_2, CategoryTheory.Functor.map_comp, CategoryTheory.Grothendieck.Hom.base, CategoryTheory.Grothendieck.comp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ Hom.base (𝟙 X) = 𝟙 X.base

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X : Grothendieck F
⊢ (F.map (Hom.base (𝟙 X))).toFunctor.obj X.fiber = X.fiber

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X : Grothendieck F
⊢ Hom.fiber (𝟙 X) = eqToHom ⋯

Tactic:
rfl

Premises used: Eq.mpr, CategoryTheory.eqToHom, rfl
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y Z : Grothendieck F
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).base = f.base ≫ g.base

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y Z : Grothendieck F
f : X ⟶ Y
g : Y ⟶ Z
⊢ (F.map (f ≫ g).base).toFunctor.obj X.fiber = (F.map g.base).toFunctor.obj ((F.map f.base).toFunctor.obj X.fiber)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
F : C ⥤ Cat
X Y Z : Grothendieck F
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).fiber = eqToHom ⋯ ≫ (F.map g.base).toFunctor.map f.fiber ≫ g.fiber

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Grothendieck
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y : Grothendieck F
f g : X ⟶ Y
h : f = g
subst : (F.map f.base).toFunctor.obj X.fiber = (F.map f.base).toFunctor.obj X.fiber
⊢ (F.map f.base).toFunctor.obj X.fiber = (F.map g.base).toFunctor.obj X.fiber

Tactic:
subst h