[GOAL]
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
⊢ Category.{?u.1823, u + 1} (Bundled c)
[PROOFSTEP]
refine'
  { Hom := fun X Y => @hom X Y X.str Y.str
    id := fun X => @BundledHom.id c hom 𝒞 X X.str
    comp := @fun X Y Z f g => @BundledHom.comp c hom 𝒞 X Y Z X.str Y.str Z.str g f
    comp_id := _
    id_comp := _
    assoc := _ }
[GOAL]
case refine'_1
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
⊢ ∀ {X Y : Bundled c} (f : X ⟶ Y), 𝟙 X ≫ f = f
[PROOFSTEP]
intros
[GOAL]
case refine'_2
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
⊢ ∀ {X Y : Bundled c} (f : X ⟶ Y), f ≫ 𝟙 Y = f
[PROOFSTEP]
intros
[GOAL]
case refine'_3
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
⊢ ∀ {W X Y Z : Bundled c} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
intros
[GOAL]
case refine'_1
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
X✝ Y✝ : Bundled c
f✝ : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f✝ = f✝
[PROOFSTEP]
apply 𝒞.hom_ext
[GOAL]
case refine'_2
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
X✝ Y✝ : Bundled c
f✝ : X✝ ⟶ Y✝
⊢ f✝ ≫ 𝟙 Y✝ = f✝
[PROOFSTEP]
apply 𝒞.hom_ext
[GOAL]
case refine'_3
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
W✝ X✝ Y✝ Z✝ : Bundled c
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝
[PROOFSTEP]
apply 𝒞.hom_ext
[GOAL]
case refine'_1.a
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
X✝ Y✝ : Bundled c
f✝ : X✝ ⟶ Y✝
⊢ toFun 𝒞 X✝.str Y✝.str (𝟙 X✝ ≫ f✝) = toFun 𝒞 X✝.str Y✝.str f✝
[PROOFSTEP]
aesop_cat
[GOAL]
case refine'_2.a
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
X✝ Y✝ : Bundled c
f✝ : X✝ ⟶ Y✝
⊢ toFun 𝒞 X✝.str Y✝.str (f✝ ≫ 𝟙 Y✝) = toFun 𝒞 X✝.str Y✝.str f✝
[PROOFSTEP]
aesop_cat
[GOAL]
case refine'_3.a
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
W✝ X✝ Y✝ Z✝ : Bundled c
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
⊢ toFun 𝒞 W✝.str Z✝.str ((f✝ ≫ g✝) ≫ h✝) = toFun 𝒞 W✝.str Z✝.str (f✝ ≫ g✝ ≫ h✝)
[PROOFSTEP]
aesop_cat
[GOAL]
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
X✝ Y✝ Z✝ : Bundled c
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => ↑X, map := fun X Y f => toFun 𝒞 X.str Y.str f }.map (f ≫ g) =
    { obj := fun X => ↑X, map := fun X Y f => toFun 𝒞 X.str Y.str f }.map f ≫
      { obj := fun X => ↑X, map := fun X Y f => toFun 𝒞 X.str Y.str f }.map g
[PROOFSTEP]
dsimp
[GOAL]
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
X✝ Y✝ Z✝ : Bundled c
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ toFun 𝒞 X✝.str Z✝.str (f ≫ g) = toFun 𝒞 X✝.str Y✝.str f ≫ toFun 𝒞 Y✝.str Z✝.str g
[PROOFSTEP]
erw [𝒞.comp_toFun]
[GOAL]
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
X✝ Y✝ Z✝ : Bundled c
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ toFun 𝒞 Y✝.str Z✝.str g ∘ toFun 𝒞 X✝.str Y✝.str f = toFun 𝒞 X✝.str Y✝.str f ≫ toFun 𝒞 Y✝.str Z✝.str g
[PROOFSTEP]
rfl
[GOAL]
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
⊢ ∀ {X Y : Bundled c},
    Function.Injective (Functor.mk { obj := fun X => ↑X, map := fun X Y f => toFun 𝒞 X.str Y.str f }).map
[PROOFSTEP]
intros
[GOAL]
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
X✝ Y✝ : Bundled c
⊢ Function.Injective (Functor.mk { obj := fun X => ↑X, map := fun X Y f => toFun 𝒞 X.str Y.str f }).map
[PROOFSTEP]
apply 𝒞.hom_ext
[GOAL]
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
d : Type u → Type u
hom_d : ⦃α β : Type u⦄ → d α → d β → Type u
inst✝ : BundledHom hom_d
obj : ⦃α : Type u⦄ → c α → d α
map : {X Y : Bundled c} → (X ⟶ Y) → (Bundled.map obj X ⟶ Bundled.map obj Y)
h_map : ∀ {X Y : Bundled c} (f : X ⟶ Y), ↑(map f) = ↑f
⊢ ∀ {X Y : Bundled c} {f : X ⟶ Y}, HEq ((forget (Bundled d)).map ((fun {X Y} => map) f)) ((forget (Bundled c)).map f)
[PROOFSTEP]
intros X Y f
[GOAL]
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
d : Type u → Type u
hom_d : ⦃α β : Type u⦄ → d α → d β → Type u
inst✝ : BundledHom hom_d
obj : ⦃α : Type u⦄ → c α → d α
map : {X Y : Bundled c} → (X ⟶ Y) → (Bundled.map obj X ⟶ Bundled.map obj Y)
h_map : ∀ {X Y : Bundled c} (f : X ⟶ Y), ↑(map f) = ↑f
X Y : Bundled c
f : X ⟶ Y
⊢ HEq ((forget (Bundled d)).map ((fun {X Y} => map) f)) ((forget (Bundled c)).map f)
[PROOFSTEP]
rw [heq_eq_eq, forget_map_eq_coe, forget_map_eq_coe, h_map f]
