[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]
