[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
p : X = Y
⊢ X ⟶ Y
[PROOFSTEP]
rw [p]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
p : X = Y
⊢ Y ⟶ Y
[PROOFSTEP]
exact 𝟙 _
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ eqToHom p ≫ eqToHom q = eqToHom (_ : X = Z)
[PROOFSTEP]
cases p
[GOAL]
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
q : X = Z
⊢ eqToHom (_ : X = X) ≫ eqToHom q = eqToHom (_ : X = Z)
[PROOFSTEP]
cases q
[GOAL]
case refl.refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ eqToHom (_ : X = X) ≫ eqToHom (_ : X = X) = eqToHom (_ : X = X)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Y' : C
p : Y = Y'
f : X ⟶ Y
g : X ⟶ Y'
h : f ≫ eqToHom p = g
⊢ f = (f ≫ eqToHom p) ≫ eqToHom (_ : Y' = Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Y' : C
p : Y = Y'
f : X ⟶ Y
g : X ⟶ Y'
h : f = g ≫ eqToHom (_ : Y' = Y)
⊢ f ≫ eqToHom p = g
[PROOFSTEP]
simp [eq_whisker h (eqToHom p)]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X X' Y : C
p : X = X'
f : X ⟶ Y
g : X' ⟶ Y
h : eqToHom p ≫ g = f
⊢ g = eqToHom (_ : X' = X) ≫ eqToHom p ≫ g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X X' Y : C
p : X = X'
f : X ⟶ Y
g : X' ⟶ Y
h : g = eqToHom (_ : X' = X) ≫ f
⊢ eqToHom p ≫ eqToHom (_ : X' = X) ≫ f = f
[PROOFSTEP]
simp [whisker_eq _ h]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort ?u.2415
f g : β → C
z : (b : β) → f b ⟶ g b
j j' : β
w : j = j'
⊢ g j = g j'
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort ?u.2415
f g : β → C
z : (b : β) → f b ⟶ g b
j j' : β
w : j = j'
⊢ f j = f j'
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j j' : β
w : j = j'
⊢ z j ≫ eqToHom (_ : g j = g j') = eqToHom (_ : f j = f j') ≫ z j'
[PROOFSTEP]
cases w
[GOAL]
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ⟶ g b
j : β
⊢ z j ≫ eqToHom (_ : g j = g j) = eqToHom (_ : f j = f j) ≫ z j
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort ?u.3466
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ g j = g j'
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort ?u.3466
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ f j = f j'
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ (z j).hom ≫ eqToHom (_ : g j = g j') = eqToHom (_ : f j = f j') ≫ (z j').hom
[PROOFSTEP]
cases w
[GOAL]
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j : β
⊢ (z j).hom ≫ eqToHom (_ : g j = g j) = eqToHom (_ : f j = f j) ≫ (z j).hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort ?u.4552
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ f j = f j'
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort ?u.4552
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ g j = g j'
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ (z j).inv ≫ eqToHom (_ : f j = f j') = eqToHom (_ : g j = g j') ≫ (z j').inv
[PROOFSTEP]
cases w
[GOAL]
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j : β
⊢ (z j).inv ≫ eqToHom (_ : f j = f j) = eqToHom (_ : g j = g j) ≫ (z j).inv
[PROOFSTEP]
simp
  /- Porting note: simpNF complains about this not reducing but it is clearly used
  in `congrArg_mpr_hom_left`. It has been no-linted. -/
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y ⟶ Z
⊢ cast (_ : (Y ⟶ Z) = (X ⟶ Z)) q = eqToHom p ≫ q
[PROOFSTEP]
cases p
[GOAL]
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
q : X ⟶ Z
⊢ cast (_ : (X ⟶ Z) = (X ⟶ Z)) q = eqToHom (_ : X = X) ≫ q
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y ⟶ Z
⊢ Eq.mpr (_ : (X ⟶ Z) = (Y ⟶ Z)) q = eqToHom p ≫ q
[PROOFSTEP]
cases p
[GOAL]
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
q : X ⟶ Z
⊢ Eq.mpr (_ : (X ⟶ Z) = (X ⟶ Z)) q = eqToHom (_ : X = X) ≫ q
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X ⟶ Y
q : Z = Y
⊢ cast (_ : (X ⟶ Y) = (X ⟶ Z)) p = p ≫ eqToHom (_ : Y = Z)
[PROOFSTEP]
cases q
[GOAL]
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
p : X ⟶ Y
⊢ cast (_ : (X ⟶ Y) = (X ⟶ Y)) p = p ≫ eqToHom (_ : Y = Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X ⟶ Y
q : Z = Y
⊢ Eq.mpr (_ : (X ⟶ Z) = (X ⟶ Y)) p = p ≫ eqToHom (_ : Y = Z)
[PROOFSTEP]
cases q
[GOAL]
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
p : X ⟶ Y
⊢ Eq.mpr (_ : (X ⟶ Y) = (X ⟶ Y)) p = p ≫ eqToHom (_ : Y = Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
p : X = Y
⊢ eqToHom p ≫ eqToHom (_ : Y = X) = 𝟙 X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
p : X = Y
⊢ eqToHom (_ : Y = X) ≫ eqToHom p = 𝟙 Y
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ eqToIso p ≪≫ eqToIso q = eqToIso (_ : X = Z)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ (eqToIso p ≪≫ eqToIso q).hom = (eqToIso (_ : X = Z)).hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : X = Y
⊢ (eqToHom h).op = eqToHom (_ : op Y = op X)
[PROOFSTEP]
cases h
[GOAL]
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ (eqToHom (_ : X = X)).op = eqToHom (_ : op X = op X)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
h : X = Y
⊢ (eqToHom h).unop = eqToHom (_ : Y.unop = X.unop)
[PROOFSTEP]
cases h
[GOAL]
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
⊢ (eqToHom (_ : X = X)).unop = eqToHom (_ : X.unop = X.unop)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : X = Y
⊢ inv (eqToHom h) = eqToHom (_ : Y = X)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
h_obj : ∀ (X : C), F.obj X = G.obj X
h_map :
  autoParam
    (∀ (X Y : C) (f : X ⟶ Y), F.map f = eqToHom (_ : F.obj X = G.obj X) ≫ G.map f ≫ eqToHom (_ : G.obj Y = F.obj Y))
    _auto✝
⊢ F = G
[PROOFSTEP]
match F, G with
| mk F_pre _ _, mk G_pre _ _ =>
  match F_pre, G_pre with
    -- Porting note: did not unfold the Prefunctor unlike Lean3
  | Prefunctor.mk F_obj _,
    Prefunctor.mk G_obj
      _ =>
    obtain rfl : F_obj = G_obj := by
      ext X
      apply h_obj
    congr
    funext X Y f
    simpa using h_map X Y f
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_pre : C ⥤q D
map_id✝¹ : ∀ (X : C), F_pre.map (𝟙 X) = 𝟙 (F_pre.obj X)
map_comp✝¹ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), F_pre.map (f ≫ g) = F_pre.map f ≫ F_pre.map g
G_pre : C ⥤q D
map_id✝ : ∀ (X : C), G_pre.map (𝟙 X) = 𝟙 (G_pre.obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), G_pre.map (f ≫ g) = G_pre.map f ≫ G_pre.map g
h_obj : ∀ (X : C), (mk F_pre).obj X = (mk G_pre).obj X
h_map :
  autoParam
    (∀ (X Y : C) (f : X ⟶ Y),
      (mk F_pre).map f =
        eqToHom (_ : (mk F_pre).obj X = (mk G_pre).obj X) ≫
          (mk G_pre).map f ≫ eqToHom (_ : (mk G_pre).obj Y = (mk F_pre).obj Y))
    _auto✝
⊢ mk F_pre = mk G_pre
[PROOFSTEP]
match F_pre, G_pre with
  -- Porting note: did not unfold the Prefunctor unlike Lean3
| Prefunctor.mk F_obj _,
  Prefunctor.mk G_obj
    _ =>
  obtain rfl : F_obj = G_obj := by
    ext X
    apply h_obj
  congr
  funext X Y f
  simpa using h_map X Y f
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_pre G_pre : C ⥤q D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
G_obj : C → D
map✝ : {X Y : C} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝¹ : ∀ (X : C), { obj := F_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := F_obj, map := map✝¹ }.map f ≫ { obj := F_obj, map := map✝¹ }.map g
map_id✝ : ∀ (X : C), { obj := G_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj, map := map✝ }.map (f ≫ g) =
      { obj := G_obj, map := map✝ }.map f ≫ { obj := G_obj, map := map✝ }.map g
h_obj : ∀ (X : C), (mk { obj := F_obj, map := map✝¹ }).obj X = (mk { obj := G_obj, map := map✝ }).obj X
h_map :
  autoParam
    (∀ (X Y : C) (f : X ⟶ Y),
      (mk { obj := F_obj, map := map✝¹ }).map f =
        eqToHom (_ : (mk { obj := F_obj, map := map✝¹ }).obj X = (mk { obj := G_obj, map := map✝ }).obj X) ≫
          (mk { obj := G_obj, map := map✝ }).map f ≫
            eqToHom (_ : (mk { obj := G_obj, map := map✝ }).obj Y = (mk { obj := F_obj, map := map✝¹ }).obj Y))
    _auto✝
⊢ mk { obj := F_obj, map := map✝¹ } = mk { obj := G_obj, map := map✝ }
[PROOFSTEP]
obtain rfl : F_obj = G_obj := by
  ext X
  apply h_obj
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_pre G_pre : C ⥤q D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
G_obj : C → D
map✝ : {X Y : C} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝¹ : ∀ (X : C), { obj := F_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := F_obj, map := map✝¹ }.map f ≫ { obj := F_obj, map := map✝¹ }.map g
map_id✝ : ∀ (X : C), { obj := G_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj, map := map✝ }.map (f ≫ g) =
      { obj := G_obj, map := map✝ }.map f ≫ { obj := G_obj, map := map✝ }.map g
h_obj : ∀ (X : C), (mk { obj := F_obj, map := map✝¹ }).obj X = (mk { obj := G_obj, map := map✝ }).obj X
h_map :
  autoParam
    (∀ (X Y : C) (f : X ⟶ Y),
      (mk { obj := F_obj, map := map✝¹ }).map f =
        eqToHom (_ : (mk { obj := F_obj, map := map✝¹ }).obj X = (mk { obj := G_obj, map := map✝ }).obj X) ≫
          (mk { obj := G_obj, map := map✝ }).map f ≫
            eqToHom (_ : (mk { obj := G_obj, map := map✝ }).obj Y = (mk { obj := F_obj, map := map✝¹ }).obj Y))
    _auto✝
⊢ F_obj = G_obj
[PROOFSTEP]
ext X
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_pre G_pre : C ⥤q D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
G_obj : C → D
map✝ : {X Y : C} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id✝¹ : ∀ (X : C), { obj := F_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := F_obj, map := map✝¹ }.map f ≫ { obj := F_obj, map := map✝¹ }.map g
map_id✝ : ∀ (X : C), { obj := G_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := G_obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := G_obj, map := map✝ }.map (f ≫ g) =
      { obj := G_obj, map := map✝ }.map f ≫ { obj := G_obj, map := map✝ }.map g
h_obj : ∀ (X : C), (mk { obj := F_obj, map := map✝¹ }).obj X = (mk { obj := G_obj, map := map✝ }).obj X
h_map :
  autoParam
    (∀ (X Y : C) (f : X ⟶ Y),
      (mk { obj := F_obj, map := map✝¹ }).map f =
        eqToHom (_ : (mk { obj := F_obj, map := map✝¹ }).obj X = (mk { obj := G_obj, map := map✝ }).obj X) ≫
          (mk { obj := G_obj, map := map✝ }).map f ≫
            eqToHom (_ : (mk { obj := G_obj, map := map✝ }).obj Y = (mk { obj := F_obj, map := map✝¹ }).obj Y))
    _auto✝
X : C
⊢ F_obj X = G_obj X
[PROOFSTEP]
apply h_obj
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_pre G_pre : C ⥤q D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), { obj := F_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := F_obj, map := map✝¹ }.map f ≫ { obj := F_obj, map := map✝¹ }.map g
map✝ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : C), { obj := F_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝ }.map (f ≫ g) =
      { obj := F_obj, map := map✝ }.map f ≫ { obj := F_obj, map := map✝ }.map g
h_obj : ∀ (X : C), (mk { obj := F_obj, map := map✝¹ }).obj X = (mk { obj := F_obj, map := map✝ }).obj X
h_map :
  autoParam
    (∀ (X Y : C) (f : X ⟶ Y),
      (mk { obj := F_obj, map := map✝¹ }).map f =
        eqToHom (_ : (mk { obj := F_obj, map := map✝¹ }).obj X = (mk { obj := F_obj, map := map✝ }).obj X) ≫
          (mk { obj := F_obj, map := map✝ }).map f ≫
            eqToHom (_ : (mk { obj := F_obj, map := map✝ }).obj Y = (mk { obj := F_obj, map := map✝¹ }).obj Y))
    _auto✝
⊢ mk { obj := F_obj, map := map✝¹ } = mk { obj := F_obj, map := map✝ }
[PROOFSTEP]
congr
[GOAL]
case e_toPrefunctor.e_map
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_pre G_pre : C ⥤q D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), { obj := F_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := F_obj, map := map✝¹ }.map f ≫ { obj := F_obj, map := map✝¹ }.map g
map✝ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : C), { obj := F_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝ }.map (f ≫ g) =
      { obj := F_obj, map := map✝ }.map f ≫ { obj := F_obj, map := map✝ }.map g
h_obj : ∀ (X : C), (mk { obj := F_obj, map := map✝¹ }).obj X = (mk { obj := F_obj, map := map✝ }).obj X
h_map :
  autoParam
    (∀ (X Y : C) (f : X ⟶ Y),
      (mk { obj := F_obj, map := map✝¹ }).map f =
        eqToHom (_ : (mk { obj := F_obj, map := map✝¹ }).obj X = (mk { obj := F_obj, map := map✝ }).obj X) ≫
          (mk { obj := F_obj, map := map✝ }).map f ≫
            eqToHom (_ : (mk { obj := F_obj, map := map✝ }).obj Y = (mk { obj := F_obj, map := map✝¹ }).obj Y))
    _auto✝
⊢ map✝¹ = map✝
[PROOFSTEP]
funext X Y f
[GOAL]
case e_toPrefunctor.e_map.h.h.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
F_pre G_pre : C ⥤q D
F_obj : C → D
map✝¹ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝¹ : ∀ (X : C), { obj := F_obj, map := map✝¹ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝¹ }.obj X)
map_comp✝¹ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝¹ }.map (f ≫ g) =
      { obj := F_obj, map := map✝¹ }.map f ≫ { obj := F_obj, map := map✝¹ }.map g
map✝ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : C), { obj := F_obj, map := map✝ }.map (𝟙 X) = 𝟙 ({ obj := F_obj, map := map✝ }.obj X)
map_comp✝ :
  ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := F_obj, map := map✝ }.map (f ≫ g) =
      { obj := F_obj, map := map✝ }.map f ≫ { obj := F_obj, map := map✝ }.map g
h_obj : ∀ (X : C), (mk { obj := F_obj, map := map✝¹ }).obj X = (mk { obj := F_obj, map := map✝ }).obj X
h_map :
  autoParam
    (∀ (X Y : C) (f : X ⟶ Y),
      (mk { obj := F_obj, map := map✝¹ }).map f =
        eqToHom (_ : (mk { obj := F_obj, map := map✝¹ }).obj X = (mk { obj := F_obj, map := map✝ }).obj X) ≫
          (mk { obj := F_obj, map := map✝ }).map f ≫
            eqToHom (_ : (mk { obj := F_obj, map := map✝ }).obj Y = (mk { obj := F_obj, map := map✝¹ }).obj Y))
    _auto✝
X Y : C
f : X ⟶ Y
⊢ map✝¹ f = map✝ f
[PROOFSTEP]
simpa using h_map X Y f
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
h : W = Y
h' : X = Z
⊢ f = eqToHom h ≫ g ≫ eqToHom (_ : Z = X) ↔ HEq f g
[PROOFSTEP]
cases h
[GOAL]
case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
W X Z : C
f : W ⟶ X
h' : X = Z
g : W ⟶ Z
⊢ f = eqToHom (_ : W = W) ≫ g ≫ eqToHom (_ : Z = X) ↔ HEq f g
[PROOFSTEP]
cases h'
[GOAL]
case refl.refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
W X : C
f g : W ⟶ X
⊢ f = eqToHom (_ : W = W) ≫ g ≫ eqToHom (_ : X = X) ↔ HEq f g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
h : F = G
X : C
⊢ F.obj X = G.obj X
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
h : F = G
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom (_ : F.obj X = G.obj X) ≫ G.map f ≫ eqToHom (_ : G.obj Y = F.obj Y)
[PROOFSTEP]
subst h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ F.map f = eqToHom (_ : F.obj X = F.obj X) ≫ F.map f ≫ eqToHom (_ : F.obj Y = F.obj Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
⊢ F.obj X = G.obj X
[PROOFSTEP]
rw [hX]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
⊢ G.obj Y = F.obj Y
[PROOFSTEP]
rw [hY]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom (_ : F.obj X = G.obj X) ≫ G.map e.hom ≫ eqToHom (_ : G.obj Y = F.obj Y)
⊢ F.obj Y = G.obj Y
[PROOFSTEP]
rw [hY]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom (_ : F.obj X = G.obj X) ≫ G.map e.hom ≫ eqToHom (_ : G.obj Y = F.obj Y)
⊢ G.obj X = F.obj X
[PROOFSTEP]
rw [hX]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom (_ : F.obj X = G.obj X) ≫ G.map e.hom ≫ eqToHom (_ : G.obj Y = F.obj Y)
⊢ F.map e.inv = eqToHom (_ : F.obj Y = G.obj Y) ≫ G.map e.inv ≫ eqToHom (_ : G.obj X = F.obj X)
[PROOFSTEP]
simp only [← IsIso.Iso.inv_hom e, Functor.map_inv, h₂, IsIso.inv_comp, inv_eqToHom, Category.assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f g : X ⟶ Y
h : f = g
⊢ F.map f = F.map g
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hz : F.obj Z = G.obj Z
hf : HEq (F.map f) (G.map f)
hg : HEq (F.map g) (G.map g)
⊢ HEq (F.map (f ≫ g)) (G.map (f ≫ g))
[PROOFSTEP]
rw [F.map_comp, G.map_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hz : F.obj Z = G.obj Z
hf : HEq (F.map f) (G.map f)
hg : HEq (F.map g) (G.map g)
⊢ HEq (F.map f ≫ F.map g) (G.map f ≫ G.map g)
[PROOFSTEP]
congr
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hobj : ∀ (X : C), F.obj X = G.obj X
hmap : ∀ {X Y : C} (f : X ⟶ Y), HEq (F.map f) (G.map f)
⊢ HEq (F.map (f ≫ g)) (G.map (f ≫ g))
[PROOFSTEP]
rw [Functor.hext hobj fun _ _ => hmap]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
H : D ⥤ E
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hmap : HEq (F.map f) (G.map f)
⊢ HEq ((F ⋙ H).map f) ((G ⋙ H).map f)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
H : D ⥤ E
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hmap : HEq (F.map f) (G.map f)
⊢ HEq (H.map (F.map f)) (H.map (G.map f))
[PROOFSTEP]
congr
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
H : D ⥤ E
hobj : ∀ (X : C), F.obj X = G.obj X
hmap : ∀ {X Y : C} (f : X ⟶ Y), HEq (F.map f) (G.map f)
⊢ HEq ((F ⋙ H).map f) ((G ⋙ H).map f)
[PROOFSTEP]
rw [Functor.hext hobj fun _ _ => hmap]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F✝ G✝ : C ⥤ D
X✝ Y✝ Z : C
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
F G : C ⥤ D
h : F = G
X Y : C
f : X ⟶ Y
⊢ HEq (F.map f) (G.map f)
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
p : X = Y
⊢ F.map (eqToHom p) = eqToHom (_ : F.obj X = F.obj Y)
[PROOFSTEP]
cases p
[GOAL]
case refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ F.map (eqToHom (_ : X = X)) = eqToHom (_ : F.obj X = F.obj X)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
p : X = Y
⊢ F.mapIso (eqToIso p) = eqToIso (_ : F.obj X = F.obj Y)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
p : X = Y
⊢ (F.mapIso (eqToIso p)).hom = (eqToIso (_ : F.obj X = F.obj Y)).hom
[PROOFSTEP]
cases p
[GOAL]
case w.refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ (F.mapIso (eqToIso (_ : X = X))).hom = (eqToIso (_ : F.obj X = F.obj X)).hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
h : F = G
X : C
⊢ NatTrans.app (eqToHom h) X = eqToHom (_ : F.obj X = G.obj X)
[PROOFSTEP]
subst h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
⊢ NatTrans.app (eqToHom (_ : F = F)) X = eqToHom (_ : F.obj X = F.obj X)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
h : X = Y
⊢ app α X = F.map (eqToHom h) ≫ app α Y ≫ G.map (eqToHom (_ : Y = X))
[PROOFSTEP]
rw [α.naturality_assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
h : X = Y
⊢ app α X = app α X ≫ G.map (eqToHom h) ≫ G.map (eqToHom (_ : Y = X))
[PROOFSTEP]
simp [eqToHom_map]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
⊢ f = eqToHom (_ : X = X) ≫ f ≫ eqToHom (_ : Y = Y)
[PROOFSTEP]
simp only [Category.id_comp, eqToHom_refl, Category.comp_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
ι : Type u_1
F G : ι → C
α : (i : ι) → F i ⟶ G i
i j : ι
h : i = j
⊢ α i = eqToHom (_ : F i = F j) ≫ α j ≫ eqToHom (_ : G j = G i)
[PROOFSTEP]
subst h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
ι : Type u_1
F G : ι → C
α : (i : ι) → F i ⟶ G i
i : ι
⊢ α i = eqToHom (_ : F i = F i) ≫ α i ≫ eqToHom (_ : G i = G i)
[PROOFSTEP]
simp
