[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
f : J → I
⊢ (j : J) → Category.{?u.5215, u₁} ((C ∘ f) j)
[PROOFSTEP]
dsimp
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
f : J → I
⊢ (j : J) → Category.{?u.5215, u₁} (C (f j))
[PROOFSTEP]
infer_instance
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
g : J → I
⊢ (j : J) → Category.{?u.19534, u₁} (C (g j))
[PROOFSTEP]
infer_instance
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ (comap C g ⋙ comap (C ∘ g) f).map f' ≫ (fun X b => 𝟙 (X (g (f b)))) Y =
    (fun X b => 𝟙 (X (g (f b)))) X ≫ (comap C (g ∘ f)).map f'
[PROOFSTEP]
simp only [comap, Function.comp]
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ ((Functor.mk { obj := fun f i => f (g i), map := fun {X Y} α i => α (g i) } ⋙
            Functor.mk { obj := fun f_1 i => f_1 (f i), map := fun {X Y} α i => α (f i) }).map
        f' ≫
      fun b => 𝟙 (Y (g (f b)))) =
    (fun b => 𝟙 (X (g (f b)))) ≫ fun i => f' (g (f i))
[PROOFSTEP]
funext
[GOAL]
case h
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
x✝ : K
⊢ ((Functor.mk { obj := fun f i => f (g i), map := fun {X Y} α i => α (g i) } ⋙
              Functor.mk { obj := fun f_1 i => f_1 (f i), map := fun {X Y} α i => α (f i) }).map
          f' ≫
        fun b => 𝟙 (Y (g (f b))))
      x✝ =
    ((fun b => 𝟙 (X (g (f b)))) ≫ fun i => f' (g (f i))) x✝
[PROOFSTEP]
simp
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ (comap C (g ∘ f)).map f' ≫ (fun X b => 𝟙 (X (g (f b)))) Y =
    (fun X b => 𝟙 (X (g (f b)))) X ≫ (comap C g ⋙ comap (C ∘ g) f).map f'
[PROOFSTEP]
simp only [comap, Function.comp]
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ ((fun i => f' (g (f i))) ≫ fun b => 𝟙 (Y (g (f b)))) =
    (fun b => 𝟙 (X (g (f b)))) ≫
      (Functor.mk { obj := fun f i => f (g i), map := fun {X Y} α i => α (g i) } ⋙
            Functor.mk { obj := fun f_1 i => f_1 (f i), map := fun {X Y} α i => α (f i) }).map
        f'
[PROOFSTEP]
funext
[GOAL]
case h
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
x✝ : K
⊢ ((fun i => f' (g (f i))) ≫ fun b => 𝟙 (Y (g (f b)))) x✝ =
    ((fun b => 𝟙 (X (g (f b)))) ≫
        (Functor.mk { obj := fun f i => f (g i), map := fun {X Y} α i => α (g i) } ⋙
              Functor.mk { obj := fun f_1 i => f_1 (f i), map := fun {X Y} α i => α (f i) }).map
          f')
      x✝
[PROOFSTEP]
simp
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
h : J → I
j : J
⊢ ∀ {X Y : (i : I) → C i} (f : X ⟶ Y),
    (comap C h ⋙ eval (C ∘ h) j).map f ≫ ((fun f => Iso.refl ((comap C h ⋙ eval (C ∘ h) j).obj f)) Y).hom =
      ((fun f => Iso.refl ((comap C h ⋙ eval (C ∘ h) j).obj f)) X).hom ≫ (eval C (h j)).map f
[PROOFSTEP]
simp only [Iso.refl]
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
h : J → I
j : J
⊢ ∀ {X Y : (i : I) → C i} (f : X ⟶ Y),
    (comap C h ⋙ eval (C ∘ h) j).map f ≫ 𝟙 ((comap C h ⋙ eval (C ∘ h) j).obj Y) =
      𝟙 ((comap C h ⋙ eval (C ∘ h) j).obj X) ≫ (eval C (h j)).map f
[PROOFSTEP]
aesop_cat
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₀
D : J → Type u₁
inst✝ : (j : J) → Category.{v₁, u₁} (D j)
i : I
⊢ Category.{v₁, u₁} (Sum.elim C D (Sum.inl i))
[PROOFSTEP]
dsimp
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₀
D : J → Type u₁
inst✝ : (j : J) → Category.{v₁, u₁} (D j)
i : I
⊢ Category.{v₁, u₁} (C i)
[PROOFSTEP]
infer_instance
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₀
D : J → Type u₁
inst✝ : (j : J) → Category.{v₁, u₁} (D j)
j : J
⊢ Category.{v₁, u₁} (Sum.elim C D (Sum.inr j))
[PROOFSTEP]
dsimp
[GOAL]
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₀
D : J → Type u₁
inst✝ : (j : J) → Category.{v₁, u₁} (D j)
j : J
⊢ Category.{v₁, u₁} (D j)
[PROOFSTEP]
infer_instance
[GOAL]
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ f.hom i ≫ f.inv i = 𝟙 (X i)
[PROOFSTEP]
rw [← comp_apply, Iso.hom_inv_id, id_apply]
[GOAL]
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ f.inv i ≫ f.hom i = 𝟙 (Y i)
[PROOFSTEP]
rw [← comp_apply, Iso.inv_hom_id, id_apply]
[GOAL]
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
x x' : (i : I) → C i
h : x = x'
i : I
⊢ eqToHom h i = eqToHom (_ : x i = x' i)
[PROOFSTEP]
subst h
[GOAL]
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
x : (i : I) → C i
i : I
⊢ eqToHom (_ : x = x) i = eqToHom (_ : x i = x i)
[PROOFSTEP]
rfl
[GOAL]
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f : (i : I) → A ⥤ C i
i : I
⊢ pi' f ⋙ Pi.eval C i = f i
[PROOFSTEP]
apply Functor.ext
[GOAL]
case h_map
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f : (i : I) → A ⥤ C i
i : I
⊢ autoParam
    (∀ (X Y : A) (f_1 : X ⟶ Y),
      (pi' f ⋙ Pi.eval C i).map f_1 =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫ (f i).map f_1 ≫ eqToHom (_ : (f i).obj Y = (pi' f ⋙ Pi.eval C i).obj Y))
    _auto✝
case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f : (i : I) → A ⥤ C i
i : I
⊢ ∀ (X : A), (pi' f ⋙ Pi.eval C i).obj X = (f i).obj X
[PROOFSTEP]
intro _ _ _
[GOAL]
case h_map
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f : (i : I) → A ⥤ C i
i : I
X✝ Y✝ : A
f✝ : X✝ ⟶ Y✝
⊢ (pi' f ⋙ Pi.eval C i).map f✝ =
    eqToHom (_ : ?F.obj X✝ = ?G.obj X✝) ≫ (f i).map f✝ ≫ eqToHom (_ : (f i).obj Y✝ = (pi' f ⋙ Pi.eval C i).obj Y✝)
[PROOFSTEP]
simp
[GOAL]
case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f : (i : I) → A ⥤ C i
i : I
⊢ ∀ (X : A), (pi' f ⋙ Pi.eval C i).obj X = (f i).obj X
[PROOFSTEP]
intro _
[GOAL]
case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f : (i : I) → A ⥤ C i
i : I
X✝ : A
⊢ (pi' f ⋙ Pi.eval C i).obj X✝ = (f i).obj X✝
[PROOFSTEP]
rfl
[GOAL]
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ f = f'
[PROOFSTEP]
apply Functor.ext
[GOAL]
case h_map
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ autoParam
    (∀ (X Y : A) (f_1 : X ⟶ Y),
      f.map f_1 = eqToHom (_ : ?F.obj X = ?G.obj X) ≫ f'.map f_1 ≫ eqToHom (_ : f'.obj Y = f.obj Y))
    _auto✝
case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ ∀ (X : A), f.obj X = f'.obj X
[PROOFSTEP]
rotate_left
[GOAL]
case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ ∀ (X : A), f.obj X = f'.obj X
[PROOFSTEP]
intro X
[GOAL]
case h_obj
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X : A
⊢ f.obj X = f'.obj X
[PROOFSTEP]
ext i
[GOAL]
case h_obj.h
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X : A
i : I
⊢ f.obj X i = f'.obj X i
[PROOFSTEP]
specialize h i
[GOAL]
case h_obj.h
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
X : A
i : I
h : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ f.obj X i = f'.obj X i
[PROOFSTEP]
have := congr_obj h X
[GOAL]
case h_obj.h
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
X : A
i : I
h : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
this : (f ⋙ Pi.eval C i).obj X = (f' ⋙ Pi.eval C i).obj X
⊢ f.obj X i = f'.obj X i
[PROOFSTEP]
simpa
[GOAL]
case h_map
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ autoParam
    (∀ (X Y : A) (f_1 : X ⟶ Y),
      f.map f_1 = eqToHom (_ : f.obj X = f'.obj X) ≫ f'.map f_1 ≫ eqToHom (_ : f'.obj Y = f.obj Y))
    _auto✝
[PROOFSTEP]
intro X Y g
[GOAL]
case h_map
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
⊢ f.map g = eqToHom (_ : f.obj X = f'.obj X) ≫ f'.map g ≫ eqToHom (_ : f'.obj Y = f.obj Y)
[PROOFSTEP]
dsimp
[GOAL]
case h_map
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
⊢ f.map g = eqToHom (_ : f.obj X = f'.obj X) ≫ f'.map g ≫ eqToHom (_ : f'.obj Y = f.obj Y)
[PROOFSTEP]
funext i
[GOAL]
case h_map.h
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
i : I
⊢ f.map g i = (eqToHom (_ : f.obj X = f'.obj X) ≫ f'.map g ≫ eqToHom (_ : f'.obj Y = f.obj Y)) i
[PROOFSTEP]
specialize h i
[GOAL]
case h_map.h
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h✝ : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
i : I
h : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
⊢ f.map g i = (eqToHom (_ : f.obj X = f'.obj X) ≫ f'.map g ≫ eqToHom (_ : f'.obj Y = f.obj Y)) i
[PROOFSTEP]
have := congr_hom h g
[GOAL]
case h_map.h
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
D : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (D i)
A : Type u₁
inst✝ : Category.{u₁, u₁} A
f f' : A ⥤ ((i : I) → C i)
h✝ : ∀ (i : I), f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
X Y : A
g : X ⟶ Y
i : I
h : f ⋙ Pi.eval C i = f' ⋙ Pi.eval C i
this :
  (f ⋙ Pi.eval C i).map g =
    eqToHom (_ : (f ⋙ Pi.eval C i).obj X = (f' ⋙ Pi.eval C i).obj X) ≫
      (f' ⋙ Pi.eval C i).map g ≫ eqToHom (_ : (f' ⋙ Pi.eval C i).obj Y = (f ⋙ Pi.eval C i).obj Y)
⊢ f.map g i = (eqToHom (_ : f.obj X = f'.obj X) ≫ f'.map g ≫ eqToHom (_ : f'.obj Y = f.obj Y)) i
[PROOFSTEP]
simpa
