[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


[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
⊢ ∃ Y, Simple (underlying.obj Y)
[PROOFSTEP]
haveI : Nontrivial (Subobject X) := nontrivial_of_not_isZero h
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
this : Nontrivial (Subobject X)
⊢ ∃ Y, Simple (underlying.obj Y)
[PROOFSTEP]
haveI := isAtomic_of_orderBot_wellFounded_lt (ArtinianObject.subobject_lt_wellFounded X)
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
this✝ : Nontrivial (Subobject X)
this : IsAtomic (Subobject X)
⊢ ∃ Y, Simple (underlying.obj Y)
[PROOFSTEP]
obtain ⟨Y, s⟩ := (IsAtomic.eq_bot_or_exists_atom_le (⊤ : Subobject X)).resolve_left top_ne_bot
[GOAL]
case intro
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
this✝ : Nontrivial (Subobject X)
this : IsAtomic (Subobject X)
Y : Subobject X
s : IsAtom Y ∧ Y ≤ ⊤
⊢ ∃ Y, Simple (underlying.obj Y)
[PROOFSTEP]
exact ⟨Y, (subobject_simple_iff_isAtom _).mpr s.1⟩
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.7023, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
⊢ Mono (simpleSubobjectArrow h)
[PROOFSTEP]
dsimp only [simpleSubobjectArrow]
[GOAL]
C : Type u_1
inst✝³ : Category.{?u.7023, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : ArtinianObject X
h : ¬IsZero X
⊢ Mono (arrow (Exists.choose (_ : ∃ Y, Simple (underlying.obj Y))))
[PROOFSTEP]
infer_instance


[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : C
f : End X
h : IsIso f
⊢ f * inv f = 1
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : C
f : End X
h : IsIso f
⊢ inv f * f = 1
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : C
f g : (End X)ˣ
⊢ Equiv.toFun
      { toFun := fun f => Iso.mk (↑f) f.inv,
        invFun := fun f =>
          { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
        left_inv :=
          (_ :
            ∀ (x : (End X)ˣ),
              (fun f =>
                    { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                      inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                  ((fun f => Iso.mk (↑f) f.inv) x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : Aut X),
              (fun f => Iso.mk (↑f) f.inv)
                  ((fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    x) =
                x) }
      (f * g) =
    Equiv.toFun
        { toFun := fun f => Iso.mk (↑f) f.inv,
          invFun := fun f =>
            { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
          left_inv :=
            (_ :
              ∀ (x : (End X)ˣ),
                (fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    ((fun f => Iso.mk (↑f) f.inv) x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : Aut X),
                (fun f => Iso.mk (↑f) f.inv)
                    ((fun f =>
                        { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                          inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                      x) =
                  x) }
        f *
      Equiv.toFun
        { toFun := fun f => Iso.mk (↑f) f.inv,
          invFun := fun f =>
            { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
          left_inv :=
            (_ :
              ∀ (x : (End X)ˣ),
                (fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    ((fun f => Iso.mk (↑f) f.inv) x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : Aut X),
                (fun f => Iso.mk (↑f) f.inv)
                    ((fun f =>
                        { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                          inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                      x) =
                  x) }
        g
[PROOFSTEP]
cases f
[GOAL]
case mk
C : Type u
inst✝ : Category.{v, u} C
X : C
g : (End X)ˣ
val✝ inv✝ : End X
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ Equiv.toFun
      { toFun := fun f => Iso.mk (↑f) f.inv,
        invFun := fun f =>
          { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
        left_inv :=
          (_ :
            ∀ (x : (End X)ˣ),
              (fun f =>
                    { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                      inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                  ((fun f => Iso.mk (↑f) f.inv) x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : Aut X),
              (fun f => Iso.mk (↑f) f.inv)
                  ((fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    x) =
                x) }
      ({ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } * g) =
    Equiv.toFun
        { toFun := fun f => Iso.mk (↑f) f.inv,
          invFun := fun f =>
            { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
          left_inv :=
            (_ :
              ∀ (x : (End X)ˣ),
                (fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    ((fun f => Iso.mk (↑f) f.inv) x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : Aut X),
                (fun f => Iso.mk (↑f) f.inv)
                    ((fun f =>
                        { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                          inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                      x) =
                  x) }
        { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } *
      Equiv.toFun
        { toFun := fun f => Iso.mk (↑f) f.inv,
          invFun := fun f =>
            { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
          left_inv :=
            (_ :
              ∀ (x : (End X)ˣ),
                (fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    ((fun f => Iso.mk (↑f) f.inv) x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : Aut X),
                (fun f => Iso.mk (↑f) f.inv)
                    ((fun f =>
                        { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                          inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                      x) =
                  x) }
        g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X : C
val✝¹ inv✝¹ : End X
val_inv✝¹ : val✝¹ * inv✝¹ = 1
inv_val✝¹ : inv✝¹ * val✝¹ = 1
val✝ inv✝ : End X
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ Equiv.toFun
      { toFun := fun f => Iso.mk (↑f) f.inv,
        invFun := fun f =>
          { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
        left_inv :=
          (_ :
            ∀ (x : (End X)ˣ),
              (fun f =>
                    { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                      inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                  ((fun f => Iso.mk (↑f) f.inv) x) =
                x),
        right_inv :=
          (_ :
            ∀ (x : Aut X),
              (fun f => Iso.mk (↑f) f.inv)
                  ((fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    x) =
                x) }
      ({ val := val✝¹, inv := inv✝¹, val_inv := val_inv✝¹, inv_val := inv_val✝¹ } *
        { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }) =
    Equiv.toFun
        { toFun := fun f => Iso.mk (↑f) f.inv,
          invFun := fun f =>
            { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
          left_inv :=
            (_ :
              ∀ (x : (End X)ˣ),
                (fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    ((fun f => Iso.mk (↑f) f.inv) x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : Aut X),
                (fun f => Iso.mk (↑f) f.inv)
                    ((fun f =>
                        { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                          inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                      x) =
                  x) }
        { val := val✝¹, inv := inv✝¹, val_inv := val_inv✝¹, inv_val := inv_val✝¹ } *
      Equiv.toFun
        { toFun := fun f => Iso.mk (↑f) f.inv,
          invFun := fun f =>
            { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X), inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) },
          left_inv :=
            (_ :
              ∀ (x : (End X)ˣ),
                (fun f =>
                      { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                        inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                    ((fun f => Iso.mk (↑f) f.inv) x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : Aut X),
                (fun f => Iso.mk (↑f) f.inv)
                    ((fun f =>
                        { val := f.hom, inv := f.inv, val_inv := (_ : f.inv ≫ f.hom = 𝟙 X),
                          inv_val := (_ : f.hom ≫ f.inv = 𝟙 X) })
                      x) =
                  x) }
        { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X Y : C
h : X ≅ Y
x✝ : Aut X
⊢ (fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv))
      ((fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom)) x✝) =
    x✝
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X Y : C
h : X ≅ Y
x✝ : Aut Y
⊢ (fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom))
      ((fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv)) x✝) =
    x✝
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X Y : C
h : X ≅ Y
⊢ ∀ (x y : Aut X),
    Equiv.toFun
        { toFun := fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom),
          invFun := fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv),
          left_inv :=
            (_ :
              ∀ (x : Aut X),
                (fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv))
                    ((fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom)) x) =
                  x),
          right_inv :=
            (_ :
              ∀ (x : Aut Y),
                (fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom))
                    ((fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv)) x) =
                  x) }
        (x * y) =
      Equiv.toFun
          { toFun := fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom),
            invFun := fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv),
            left_inv :=
              (_ :
                ∀ (x : Aut X),
                  (fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv))
                      ((fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom)) x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : Aut Y),
                  (fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom))
                      ((fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv)) x) =
                    x) }
          x *
        Equiv.toFun
          { toFun := fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom),
            invFun := fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv),
            left_inv :=
              (_ :
                ∀ (x : Aut X),
                  (fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv))
                      ((fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom)) x) =
                    x),
            right_inv :=
              (_ :
                ∀ (x : Aut Y),
                  (fun x => Iso.mk (h.inv ≫ x.hom ≫ h.hom) (h.inv ≫ x.inv ≫ h.hom))
                      ((fun y => Iso.mk (h.hom ≫ y.hom ≫ h.inv) (h.hom ≫ y.inv ≫ h.inv)) x) =
                    x) }
          y
[PROOFSTEP]
simp [Aut_mul_def]


[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
⊢ Category.{?u.2036, u₁} (Skeleton C)
[PROOFSTEP]
apply InducedCategory.category
[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
⊢ Full (fromSkeleton C)
[PROOFSTEP]
apply InducedCategory.full
[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
⊢ Faithful (fromSkeleton C)
[PROOFSTEP]
apply InducedCategory.faithful
[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
⊢ Skeletal (Skeleton C)
[PROOFSTEP]
rintro X Y ⟨h⟩
[GOAL]
case intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X Y : Skeleton C
h : X ≅ Y
⊢ X = Y
[PROOFSTEP]
have : X.out ≈ Y.out := ⟨(fromSkeleton C).mapIso h⟩
[GOAL]
case intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X Y : Skeleton C
h : X ≅ Y
this : Quotient.out X ≈ Quotient.out Y
⊢ X = Y
[PROOFSTEP]
simpa using Quotient.sound this
[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
⊢ ∀ (a₁ b₁ a₂ b₂ : C), a₁ ≈ a₂ → b₁ ≈ b₂ → (fun X Y => Nonempty (X ⟶ Y)) a₁ b₁ = (fun X Y => Nonempty (X ⟶ Y)) a₂ b₂
[PROOFSTEP]
rintro _ _ _ _ ⟨i₁⟩ ⟨i₂⟩
[GOAL]
case intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
a₁✝ b₁✝ a₂✝ b₂✝ : C
i₁ : a₁✝ ≅ a₂✝
i₂ : b₁✝ ≅ b₂✝
⊢ (fun X Y => Nonempty (X ⟶ Y)) a₁✝ b₁✝ = (fun X Y => Nonempty (X ⟶ Y)) a₂✝ b₂✝
[PROOFSTEP]
exact propext ⟨Nonempty.map fun f => i₁.inv ≫ f ≫ i₂.hom, Nonempty.map fun f => i₁.hom ≫ f ≫ i₂.inv⟩
[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
⊢ ∀ (a : ThinSkeleton C), a ≤ a
[PROOFSTEP]
refine' Quotient.ind fun a => _
[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
a : C
⊢ Quotient.mk (isIsomorphicSetoid C) a ≤ Quotient.mk (isIsomorphicSetoid C) a
[PROOFSTEP]
exact ⟨𝟙 _⟩
[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
x✝¹ x✝ : ThinSkeleton C
⊢ ∀ (a b : x✝¹ ⟶ x✝), a = b
[PROOFSTEP]
rintro ⟨⟨f₁⟩⟩ ⟨⟨_⟩⟩
[GOAL]
case up.up.up.up
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
x✝¹ x✝ : ThinSkeleton C
f₁ down✝ : x✝¹ ≤ x✝
⊢ { down := { down := f₁ } } = { down := { down := down✝ } }
[PROOFSTEP]
rfl
[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
inst✝ : Quiver.IsThin C
src✝ : Preorder (ThinSkeleton C) := preorder C
⊢ ∀ (a b : C),
    Quotient.mk (isIsomorphicSetoid C) a ≤ Quotient.mk (isIsomorphicSetoid C) b →
      Quotient.mk (isIsomorphicSetoid C) b ≤ Quotient.mk (isIsomorphicSetoid C) a →
        Quotient.mk (isIsomorphicSetoid C) a = Quotient.mk (isIsomorphicSetoid C) b
[PROOFSTEP]
rintro _ _ ⟨f⟩ ⟨g⟩
[GOAL]
case intro.intro
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Quiver.IsThin C
src✝ : Preorder (ThinSkeleton C) := preorder C
a✝ b✝ : C
f : a✝ ⟶ b✝
g : b✝ ⟶ a✝
⊢ Quotient.mk (isIsomorphicSetoid C) a✝ = Quotient.mk (isIsomorphicSetoid C) b✝
[PROOFSTEP]
apply Quotient.sound (equiv_of_both_ways f g)
[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
R : D ⥤ C
L : C ⥤ D
h : L ⊣ R
X : ThinSkeleton C
⊢ (𝟭 (ThinSkeleton C)).obj X ⟶ (map L ⋙ map R).obj X
[PROOFSTEP]
letI := isIsomorphicSetoid C
[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
R : D ⥤ C
L : C ⥤ D
h : L ⊣ R
X : ThinSkeleton C
this : Setoid C := isIsomorphicSetoid C
⊢ (𝟭 (ThinSkeleton C)).obj X ⟶ (map L ⋙ map R).obj X
[PROOFSTEP]
refine' Quotient.recOnSubsingleton X fun x => homOfLE ⟨h.unit.app x⟩
[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
R : D ⥤ C
L : C ⥤ D
h : L ⊣ R
X : ThinSkeleton D
⊢ (map R ⋙ map L).obj X ⟶ (𝟭 (ThinSkeleton D)).obj X
[PROOFSTEP]
letI := isIsomorphicSetoid D
[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
R : D ⥤ C
L : C ⥤ D
h : L ⊣ R
X : ThinSkeleton D
this : Setoid D := isIsomorphicSetoid D
⊢ (map R ⋙ map L).obj X ⟶ (𝟭 (ThinSkeleton D)).obj X
[PROOFSTEP]
refine' Quotient.recOnSubsingleton X fun x => homOfLE ⟨h.counit.app x⟩


[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ (𝟙 X).hom = 𝟙 X
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : Core C}, Function.Injective (inclusion C).map
[PROOFSTEP]
intro _ _
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : Core C
⊢ Function.Injective (inclusion C).map
[PROOFSTEP]
apply Iso.ext
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
α : Core (Type u₁)
⊢ { obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.map (𝟙 α) =
    𝟙 ({ obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.obj α)
[PROOFSTEP]
apply Iso.ext
[GOAL]
case w
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
α : Core (Type u₁)
⊢ ({ obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.map (𝟙 α)).hom =
    (𝟙 ({ obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.obj α)).hom
[PROOFSTEP]
funext x
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
α : Core (Type u₁)
x : { obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.obj α
⊢ ({ obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.map (𝟙 α)).hom x =
    (𝟙 ({ obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.obj α)).hom x
[PROOFSTEP]
exact congr_fun (EquivFunctor.map_refl' _) x
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
X✝ Y✝ Z✝ : Core (Type u₁)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.map (f ≫ g) =
    { obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.map f ≫
      { obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.map g
[PROOFSTEP]
apply Iso.ext
[GOAL]
case w
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
X✝ Y✝ Z✝ : Core (Type u₁)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ({ obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.map (f ≫ g)).hom =
    ({ obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.map f ≫
        { obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.map g).hom
[PROOFSTEP]
funext x
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
X✝ Y✝ Z✝ : Core (Type u₁)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x : { obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.obj X✝
⊢ ({ obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.map (f ≫ g)).hom x =
    ({ obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.map f ≫
          { obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.map g).hom
      x
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
X✝ Y✝ Z✝ : Core (Type u₁)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x : { obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.obj X✝
⊢ EquivFunctor.map (f ≫ g).toEquiv x = EquivFunctor.map g.toEquiv (EquivFunctor.map f.toEquiv x)
[PROOFSTEP]
erw [Iso.toEquiv_comp, EquivFunctor.map_trans']
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
m : Type u₁ → Type u₂
inst✝ : EquivFunctor m
X✝ Y✝ Z✝ : Core (Type u₁)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x : { obj := m, map := fun {X Y} f => Equiv.toIso (EquivFunctor.mapEquiv m f.toEquiv) }.obj X✝
⊢ (EquivFunctor.map g.toEquiv ∘ EquivFunctor.map f.toEquiv) x =
    EquivFunctor.map g.toEquiv (EquivFunctor.map f.toEquiv x)
[PROOFSTEP]
rw [Function.comp]


[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (f.op ≫ (inv f).op).unop = (𝟙 (op Y)).unop
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ ((inv f).op ≫ f.op).unop = (𝟙 (op X)).unop
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f.op
⊢ (f ≫ (inv f.op).unop).op = (𝟙 X).op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f.op
⊢ ((inv f.op).unop ≫ f).op = (𝟙 Y).op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ IsIso f.unop ↔ IsIso f
[PROOFSTEP]
rw [← isIso_op_iff f.unop, Quiver.Hom.op_unop]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ (inv f).op = inv f.op
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case hom_inv_id
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : IsIso f
⊢ f.op ≫ (inv f).op = 𝟙 (op Y)
[PROOFSTEP]
rw [← op_comp, IsIso.inv_hom_id, op_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : IsIso f
⊢ (inv f).unop = inv f.unop
[PROOFSTEP]
aesop_cat_nonterminal
[GOAL]
case hom_inv_id
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
inst_1 : IsIso f
⊢ f.unop ≫ (inv f).unop = 𝟙 Y.unop
[PROOFSTEP]
rw [← unop_comp, IsIso.inv_hom_id, unop_id]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : Faithful F
X✝ Y✝ : Cᵒᵖ
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : F.op.map a₁✝ = F.op.map a₂✝
⊢ a₁✝.unop = a₂✝.unop
[PROOFSTEP]
simpa using map_injective F (Quiver.Hom.op_inj h)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
⊢ F.rightOp.leftOp = F
[PROOFSTEP]
cases F
[GOAL]
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
toPrefunctor✝ : Cᵒᵖ ⥤q D
map_id✝ : ∀ (X : Cᵒᵖ), toPrefunctor✝.map (𝟙 X) = 𝟙 (toPrefunctor✝.obj X)
map_comp✝ :
  ∀ {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z), toPrefunctor✝.map (f ≫ g) = toPrefunctor✝.map f ≫ toPrefunctor✝.map g
⊢ (mk toPrefunctor✝).rightOp.leftOp = mk toPrefunctor✝
[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ᵒᵖ
f : X ⟶ Y
⊢ (G.op.map f ≫ (fun X => (app α X.unop).op) Y).unop = ((fun X => (app α X.unop).op) X ≫ F.op.map f).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ⟶ G
X Y : C
f : X ⟶ Y
⊢ ((Functor.unop G).map f ≫ (fun X => (app α (op X)).unop) Y).op =
    ((fun X => (app α (op X)).unop) X ≫ (Functor.unop F).map f).op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ⟶ G.op
X Y : C
f : X ⟶ Y
⊢ (G.map f ≫ (fun X => (app α (op X)).unop) Y).op = ((fun X => (app α (op X)).unop) X ≫ F.map f).op
[PROOFSTEP]
simpa only [Functor.op_map] using (α.naturality f.op).symm
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : Functor.unop F ⟶ Functor.unop G
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (G.map f ≫ (fun X => (app α X.unop).op) Y).unop = ((fun X => (app α X.unop).op) X ≫ F.map f).unop
[PROOFSTEP]
simpa only [Functor.unop_map] using (α.naturality f.unop).symm
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : C ⥤ Dᵒᵖ
α : F ⟶ G
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (G.leftOp.map f ≫ (fun X => (app α X.unop).unop) Y).op = ((fun X => (app α X.unop).unop) X ≫ F.leftOp.map f).op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : C ⥤ Dᵒᵖ
α : F.leftOp ⟶ G.leftOp
X Y : C
f : X ⟶ Y
⊢ (G.map f ≫ (fun X => (app α (op X)).op) Y).unop = ((fun X => (app α (op X)).op) X ≫ F.map f).unop
[PROOFSTEP]
simpa only [Functor.leftOp_map] using (α.naturality f.op).symm
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : Cᵒᵖ ⥤ D
α : F ⟶ G
X Y : C
f : X ⟶ Y
⊢ (G.rightOp.map f ≫ (fun X => (app α (op X)).op) Y).unop = ((fun X => (app α (op X)).op) X ≫ F.rightOp.map f).unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : Cᵒᵖ ⥤ D
α : F.rightOp ⟶ G.rightOp
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (G.map f ≫ (fun X => (app α X.unop).unop) Y).op = ((fun X => (app α X.unop).unop) X ≫ F.map f).op
[PROOFSTEP]
simpa only [Functor.rightOp_map] using (α.naturality f.unop).symm
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.hom.unop ≫ f.inv.unop = 𝟙 Y.unop
[PROOFSTEP]
simp only [← unop_comp, f.inv_hom_id, unop_id]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.inv.unop ≫ f.hom.unop = 𝟙 X.unop
[PROOFSTEP]
simp only [← unop_comp, f.hom_inv_id, unop_id]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ Iso.op (unop f) = f
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ (Iso.op (unop f)).hom = f.hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ X Y : C
f : X ≅ Y
⊢ unop (Iso.op f) = f
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ X Y : C
f : X ≅ Y
⊢ (unop (Iso.op f)).hom = f.hom
[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
⊢ NatTrans.op α.hom ≫ NatTrans.op α.inv = 𝟙 G.op
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ NatTrans.app (NatTrans.op α.hom ≫ NatTrans.op α.inv) x✝ = NatTrans.app (𝟙 G.op) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (NatTrans.app α.hom x✝.unop).op ≫ (NatTrans.app α.inv x✝.unop).op = 𝟙 (op (G.obj x✝.unop))
[PROOFSTEP]
rw [← op_comp]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (NatTrans.app α.inv x✝.unop ≫ NatTrans.app α.hom x✝.unop).op = 𝟙 (op (G.obj x✝.unop))
[PROOFSTEP]
rw [α.inv_hom_id_app]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (𝟙 (G.obj x✝.unop)).op = 𝟙 (op (G.obj x✝.unop))
[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
⊢ NatTrans.op α.inv ≫ NatTrans.op α.hom = 𝟙 F.op
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ NatTrans.app (NatTrans.op α.inv ≫ NatTrans.op α.hom) x✝ = NatTrans.app (𝟙 F.op) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (NatTrans.app α.inv x✝.unop).op ≫ (NatTrans.app α.hom x✝.unop).op = 𝟙 (op (F.obj x✝.unop))
[PROOFSTEP]
rw [← op_comp]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (NatTrans.app α.hom x✝.unop ≫ NatTrans.app α.inv x✝.unop).op = 𝟙 (op (F.obj x✝.unop))
[PROOFSTEP]
rw [α.hom_inv_id_app]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
x✝ : Cᵒᵖ
⊢ (𝟙 (F.obj x✝.unop)).op = 𝟙 (op (F.obj x✝.unop))
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
⊢ NatTrans.removeOp α.hom ≫ NatTrans.removeOp α.inv = 𝟙 G
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
x✝ : C
⊢ NatTrans.app (NatTrans.removeOp α.hom ≫ NatTrans.removeOp α.inv) x✝ = NatTrans.app (𝟙 G) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
x✝ : C
⊢ (NatTrans.app α.hom (op x✝)).unop ≫ (NatTrans.app α.inv (op x✝)).unop = 𝟙 (G.obj x✝)
[PROOFSTEP]
rw [← unop_comp]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
x✝ : C
⊢ (NatTrans.app α.inv (op x✝) ≫ NatTrans.app α.hom (op x✝)).unop = 𝟙 (G.obj x✝)
[PROOFSTEP]
rw [α.inv_hom_id_app]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
x✝ : C
⊢ (𝟙 (G.op.obj (op x✝))).unop = 𝟙 (G.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.op ≅ G.op
⊢ NatTrans.removeOp α.inv ≫ NatTrans.removeOp α.hom = 𝟙 F
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
x✝ : C
⊢ NatTrans.app (NatTrans.removeOp α.inv ≫ NatTrans.removeOp α.hom) x✝ = NatTrans.app (𝟙 F) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
x✝ : C
⊢ (NatTrans.app α.inv (op x✝)).unop ≫ (NatTrans.app α.hom (op x✝)).unop = 𝟙 (F.obj x✝)
[PROOFSTEP]
rw [← unop_comp]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
x✝ : C
⊢ (NatTrans.app α.hom (op x✝) ≫ NatTrans.app α.inv (op x✝)).unop = 𝟙 (F.obj x✝)
[PROOFSTEP]
rw [α.hom_inv_id_app]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.op ≅ G.op
x✝ : C
⊢ (𝟙 (F.op.obj (op x✝))).unop = 𝟙 (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 : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
⊢ NatTrans.unop α.hom ≫ NatTrans.unop α.inv = 𝟙 (Functor.unop G)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
x✝ : C
⊢ NatTrans.app (NatTrans.unop α.hom ≫ NatTrans.unop α.inv) x✝ = NatTrans.app (𝟙 (Functor.unop G)) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
x✝ : C
⊢ (NatTrans.app α.hom (op x✝)).unop ≫ (NatTrans.app α.inv (op x✝)).unop = 𝟙 (G.obj (op x✝)).unop
[PROOFSTEP]
rw [← unop_comp]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
x✝ : C
⊢ (NatTrans.app α.inv (op x✝) ≫ NatTrans.app α.hom (op x✝)).unop = 𝟙 (G.obj (op x✝)).unop
[PROOFSTEP]
rw [α.inv_hom_id_app]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
x✝ : C
⊢ (𝟙 (G.obj (op x✝))).unop = 𝟙 (G.obj (op x✝)).unop
[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 : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
⊢ NatTrans.unop α.inv ≫ NatTrans.unop α.hom = 𝟙 (Functor.unop F)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
x✝ : C
⊢ NatTrans.app (NatTrans.unop α.inv ≫ NatTrans.unop α.hom) x✝ = NatTrans.app (𝟙 (Functor.unop F)) x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
x✝ : C
⊢ (NatTrans.app α.inv (op x✝)).unop ≫ (NatTrans.app α.hom (op x✝)).unop = 𝟙 (F.obj (op x✝)).unop
[PROOFSTEP]
rw [← unop_comp]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
x✝ : C
⊢ (NatTrans.app α.hom (op x✝) ≫ NatTrans.app α.inv (op x✝)).unop = 𝟙 (F.obj (op x✝)).unop
[PROOFSTEP]
rw [α.hom_inv_id_app]
[GOAL]
case w.h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ G✝ : C ⥤ D
F G : Cᵒᵖ ⥤ Dᵒᵖ
α : F ≅ G
x✝ : C
⊢ (𝟙 (F.obj (op x✝))).unop = 𝟙 (F.obj (op x✝)).unop
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : Cᵒᵖ
⊢ e.functor.op.map (NatTrans.app (NatIso.op e.unitIso).symm.hom X) ≫
      NatTrans.app (NatIso.op e.counitIso).symm.hom (e.functor.op.obj X) =
    𝟙 (e.functor.op.obj X)
[PROOFSTEP]
apply Quiver.Hom.unop_inj
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : Cᵒᵖ
⊢ (e.functor.op.map (NatTrans.app (NatIso.op e.unitIso).symm.hom X) ≫
        NatTrans.app (NatIso.op e.counitIso).symm.hom (e.functor.op.obj X)).unop =
    (𝟙 (e.functor.op.obj X)).unop
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : Cᵒᵖ
⊢ NatTrans.app e.counitIso.inv (e.functor.obj X.unop) ≫ e.functor.map (NatTrans.app e.unitIso.inv X.unop) =
    𝟙 (e.functor.obj X.unop)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : Cᵒᵖ ≌ Dᵒᵖ
X : C
⊢ (Functor.unop e.functor).map (NatTrans.app (NatIso.unop e.unitIso).symm.hom X) ≫
      NatTrans.app (NatIso.unop e.counitIso).symm.hom ((Functor.unop e.functor).obj X) =
    𝟙 ((Functor.unop e.functor).obj X)
[PROOFSTEP]
apply Quiver.Hom.op_inj
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : Cᵒᵖ ≌ Dᵒᵖ
X : C
⊢ ((Functor.unop e.functor).map (NatTrans.app (NatIso.unop e.unitIso).symm.hom X) ≫
        NatTrans.app (NatIso.unop e.counitIso).symm.hom ((Functor.unop e.functor).obj X)).op =
    (𝟙 ((Functor.unop e.functor).obj X)).op
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : Cᵒᵖ ≌ Dᵒᵖ
X : C
⊢ NatTrans.app e.counitIso.inv (e.functor.obj (Opposite.op X)) ≫
      e.functor.map (NatTrans.app e.unitIso.inv (Opposite.op X)) =
    𝟙 (e.functor.obj (Opposite.op X))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ
x✝ : A ≅ B
⊢ (fun g => Iso.op g) ((fun f => Iso.unop f) x✝) = x✝
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ
x✝ : A ≅ B
⊢ ((fun g => Iso.op g) ((fun f => Iso.unop f) x✝)).hom = x✝.hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ
x✝ : B.unop ≅ A.unop
⊢ (fun f => Iso.unop f) ((fun g => Iso.op g) x✝) = x✝
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ
x✝ : B.unop ≅ A.unop
⊢ ((fun f => Iso.unop f) ((fun g => Iso.op g) x✝)).hom = x✝.hom
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {X Y : (C ⥤ D)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (C ⥤ D)ᵒᵖ).map f ≫ ((fun F => Iso.op (opUnopIso F.unop)) Y).hom =
      ((fun F => Iso.op (opUnopIso F.unop)) X).hom ≫ (opHom C D ⋙ opInv C D).map f
[PROOFSTEP]
intro F G f
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (C ⥤ D)ᵒᵖ
f : F ⟶ G
⊢ (𝟭 (C ⥤ D)ᵒᵖ).map f ≫ ((fun F => Iso.op (opUnopIso F.unop)) G).hom =
    ((fun F => Iso.op (opUnopIso F.unop)) F).hom ≫ (opHom C D ⋙ opInv C D).map f
[PROOFSTEP]
dsimp [opUnopIso]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (C ⥤ D)ᵒᵖ
f : F ⟶ G
⊢ f ≫ (NatIso.ofComponents fun X => Iso.refl (G.unop.obj X)).hom.op =
    (NatIso.ofComponents fun X => Iso.refl (F.unop.obj X)).hom.op ≫ (NatTrans.mk fun X => NatTrans.app f.unop X).op
[PROOFSTEP]
rw [show f = f.unop.op by simp, ← op_comp, ← op_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (C ⥤ D)ᵒᵖ
f : F ⟶ G
⊢ f = f.unop.op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (C ⥤ D)ᵒᵖ
f : F ⟶ G
⊢ ((NatIso.ofComponents fun X => Iso.refl (G.unop.obj X)).hom ≫ f.unop).op =
    ((NatTrans.mk fun X => NatTrans.app f.unop.op.unop X) ≫
        (NatIso.ofComponents fun X => Iso.refl (F.unop.obj X)).hom).op
[PROOFSTEP]
congr 1
[GOAL]
case e_f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (C ⥤ D)ᵒᵖ
f : F ⟶ G
⊢ (NatIso.ofComponents fun X => Iso.refl (G.unop.obj X)).hom ≫ f.unop =
    (NatTrans.mk fun X => NatTrans.app f.unop.op.unop X) ≫ (NatIso.ofComponents fun X => Iso.refl (F.unop.obj X)).hom
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ ∀ {X Y : (Cᵒᵖ ⥤ D)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (Cᵒᵖ ⥤ D)ᵒᵖ).map f ≫ ((fun F => Iso.op (rightOpLeftOpIso F.unop)) Y).hom =
      ((fun F => Iso.op (rightOpLeftOpIso F.unop)) X).hom ≫
        (mk { obj := fun F => F.unop.rightOp, map := fun {X Y} η => NatTrans.rightOp η.unop } ⋙
              mk { obj := fun F => op F.leftOp, map := fun {X Y} η => (NatTrans.leftOp η).op }).map
          f
[PROOFSTEP]
intro F G η
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ (𝟭 (Cᵒᵖ ⥤ D)ᵒᵖ).map η ≫ ((fun F => Iso.op (rightOpLeftOpIso F.unop)) G).hom =
    ((fun F => Iso.op (rightOpLeftOpIso F.unop)) F).hom ≫
      (mk { obj := fun F => F.unop.rightOp, map := fun {X Y} η => NatTrans.rightOp η.unop } ⋙
            mk { obj := fun F => op F.leftOp, map := fun {X Y} η => (NatTrans.leftOp η).op }).map
        η
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ η ≫ (rightOpLeftOpIso G.unop).hom.op =
    (rightOpLeftOpIso F.unop).hom.op ≫ (NatTrans.leftOp (NatTrans.rightOp η.unop)).op
[PROOFSTEP]
rw [show η = η.unop.op by simp, ← op_comp, ← op_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ η = η.unop.op
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ ((rightOpLeftOpIso G.unop).hom ≫ η.unop).op =
    (NatTrans.leftOp (NatTrans.rightOp η.unop.op.unop) ≫ (rightOpLeftOpIso F.unop).hom).op
[PROOFSTEP]
congr 1
[GOAL]
case e_f
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ (rightOpLeftOpIso G.unop).hom ≫ η.unop =
    NatTrans.leftOp (NatTrans.rightOp η.unop.op.unop) ≫ (rightOpLeftOpIso F.unop).hom
[PROOFSTEP]
aesop_cat


[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 : C ⥤ D
G H : D ⥤ E
α : G ⟶ H
X Y : C
f : X ⟶ Y
⊢ (F ⋙ G).map f ≫ (fun X => NatTrans.app α (F.obj X)) Y = (fun X => NatTrans.app α (F.obj X)) X ≫ (F ⋙ H).map f
[PROOFSTEP]
rw [Functor.comp_map, Functor.comp_map, α.naturality]
[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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ (G ⋙ F).map f ≫ (fun X => F.map (NatTrans.app α X)) Y = (fun X => F.map (NatTrans.app α X)) X ≫ (H ⋙ F).map f
[PROOFSTEP]
rw [Functor.comp_map, Functor.comp_map, ← F.map_comp, ← F.map_comp, α.naturality]
[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
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
H : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ (((fun F => Functor.mk { obj := fun G => F ⋙ G, map := fun {X Y} α => whiskerLeft F α }) X✝).obj H).map f ≫
      (fun c => H.map (NatTrans.app τ c)) Y =
    (fun c => H.map (NatTrans.app τ c)) X ≫
      (((fun F => Functor.mk { obj := fun G => F ⋙ G, map := fun {X Y} α => whiskerLeft F α }) Y✝).obj 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
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
H : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ H.map (X✝.map f) ≫ H.map (NatTrans.app τ Y) = H.map (NatTrans.app τ X) ≫ H.map (Y✝.map f)
[PROOFSTEP]
rw [← H.map_comp, ← H.map_comp, ← τ.naturality]
[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
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
X Y : D ⥤ E
f : X ⟶ Y
⊢ ((fun F => Functor.mk { obj := fun G => F ⋙ G, map := fun {X Y} α => whiskerLeft F α }) X✝).map f ≫
      (fun H => NatTrans.mk fun c => H.map (NatTrans.app τ c)) Y =
    (fun H => NatTrans.mk fun c => H.map (NatTrans.app τ c)) X ≫
      ((fun F => Functor.mk { obj := fun G => F ⋙ G, map := fun {X Y} α => whiskerLeft F α }) Y✝).map f
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
X Y : D ⥤ E
f : X ⟶ Y
x✝ : C
⊢ NatTrans.app
      (((fun F => Functor.mk { obj := fun G => F ⋙ G, map := fun {X Y} α => whiskerLeft F α }) X✝).map f ≫
        (fun H => NatTrans.mk fun c => H.map (NatTrans.app τ c)) Y)
      x✝ =
    NatTrans.app
      ((fun H => NatTrans.mk fun c => H.map (NatTrans.app τ c)) X ≫
        ((fun F => Functor.mk { obj := fun G => F ⋙ G, map := fun {X Y} α => whiskerLeft F α }) Y✝).map f)
      x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
X Y : D ⥤ E
f : X ⟶ Y
x✝ : C
⊢ NatTrans.app f (X✝.obj x✝) ≫ Y.map (NatTrans.app τ x✝) = X.map (NatTrans.app τ x✝) ≫ NatTrans.app f (Y✝.obj x✝)
[PROOFSTEP]
rw [f.naturality]
[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
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (((fun H => Functor.mk { obj := fun F => F ⋙ H, map := fun {X Y} α => whiskerRight α H }) X✝).obj F).map f ≫
      (fun c => NatTrans.app τ (F.obj c)) Y =
    (fun c => NatTrans.app τ (F.obj c)) X ≫
      (((fun H => Functor.mk { obj := fun F => F ⋙ H, map := fun {X Y} α => whiskerRight α H }) Y✝).obj F).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
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ X✝.map (F.map f) ≫ NatTrans.app τ (F.obj Y) = NatTrans.app τ (F.obj X) ≫ Y✝.map (F.map f)
[PROOFSTEP]
rw [τ.naturality]
[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
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
X Y : C ⥤ D
f : X ⟶ Y
⊢ ((fun H => Functor.mk { obj := fun F => F ⋙ H, map := fun {X Y} α => whiskerRight α H }) X✝).map f ≫
      (fun F => NatTrans.mk fun c => NatTrans.app τ (F.obj c)) Y =
    (fun F => NatTrans.mk fun c => NatTrans.app τ (F.obj c)) X ≫
      ((fun H => Functor.mk { obj := fun F => F ⋙ H, map := fun {X Y} α => whiskerRight α H }) Y✝).map f
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
X Y : C ⥤ D
f : X ⟶ Y
x✝ : C
⊢ NatTrans.app
      (((fun H => Functor.mk { obj := fun F => F ⋙ H, map := fun {X Y} α => whiskerRight α H }) X✝).map f ≫
        (fun F => NatTrans.mk fun c => NatTrans.app τ (F.obj c)) Y)
      x✝ =
    NatTrans.app
      ((fun F => NatTrans.mk fun c => NatTrans.app τ (F.obj c)) X ≫
        ((fun H => Functor.mk { obj := fun F => F ⋙ H, map := fun {X Y} α => whiskerRight α H }) Y✝).map f)
      x✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
X Y : C ⥤ D
f : X ⟶ Y
x✝ : C
⊢ X✝.map (NatTrans.app f x✝) ≫ NatTrans.app τ (Y.obj x✝) = NatTrans.app τ (X.obj x✝) ≫ Y✝.map (NatTrans.app f x✝)
[PROOFSTEP]
rw [← NatTrans.naturality]
[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 : D ⥤ E
inst✝ : Faithful F
X✝ Y✝ : C ⥤ D
a₁✝ a₂✝ : X✝ ⟶ Y✝
hαβ : ((whiskeringRight C D E).obj F).map a₁✝ = ((whiskeringRight C D E).obj F).map a₂✝
⊢ a₁✝ = a₂✝
[PROOFSTEP]
ext X
[GOAL]
case w.h
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 : D ⥤ E
inst✝ : Faithful F
X✝ Y✝ : C ⥤ D
a₁✝ a₂✝ : X✝ ⟶ Y✝
hαβ : ((whiskeringRight C D E).obj F).map a₁✝ = ((whiskeringRight C D E).obj F).map a₂✝
X : C
⊢ NatTrans.app a₁✝ X = NatTrans.app a₂✝ X
[PROOFSTEP]
exact (F.map_injective <| congr_fun (congr_arg NatTrans.app hαβ) X)
[GOAL]
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : A ⥤ B
G : B ⥤ C
⊢ (associator F (𝟭 B) G).hom ≫ whiskerLeft F (leftUnitor G).hom = whiskerRight (rightUnitor F).hom G
[PROOFSTEP]
aesop_cat
[GOAL]
A : Type u₁
inst✝⁴ : Category.{v₁, u₁} A
B : Type u₂
inst✝³ : Category.{v₂, u₂} B
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 : A ⥤ B
G : B ⥤ C
H : C ⥤ D
K : D ⥤ E
⊢ whiskerRight (associator F G H).hom K ≫ (associator F (G ⋙ H) K).hom ≫ whiskerLeft F (associator G H K).hom =
    (associator (F ⋙ G) H K).hom ≫ (associator F G (H ⋙ K)).hom
[PROOFSTEP]
aesop_cat