[GOAL]
I : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
i : I
x✝³ x✝² : C i
x✝¹ x✝ : x✝³ ⟶ x✝²
h : (incl i).map x✝¹ = (incl i).map x✝
⊢ x✝¹ = x✝
[PROOFSTEP]
injection h
[GOAL]
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ : (i : I) → C i ⥤ D
F G : (i : I) × C i ⥤ D
h : (i : I) → incl i ⋙ F ⟶ incl i ⋙ G
⊢ ∀ ⦃X Y : (i : I) × C i⦄ (f : X ⟶ Y),
    F.map f ≫
        (fun x =>
            match x with
            | { fst := j, snd := X } => NatTrans.app (h j) X)
          Y =
      (fun x =>
            match x with
            | { fst := j, snd := X } => NatTrans.app (h j) X)
          X ≫
        G.map f
[PROOFSTEP]
rintro ⟨j, X⟩ ⟨_, _⟩ ⟨f⟩
[GOAL]
case mk.mk.mk
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F✝ : (i : I) → C i ⥤ D
F G : (i : I) × C i ⥤ D
h : (i : I) → incl i ⋙ F ⟶ incl i ⋙ G
j : I
X Y✝ : C j
f : X ⟶ Y✝
⊢ F.map (SigmaHom.mk f) ≫
      (fun x =>
          match x with
          | { fst := j, snd := X } => NatTrans.app (h j) X)
        { fst := j, snd := Y✝ } =
    (fun x =>
          match x with
          | { fst := j, snd := X } => NatTrans.app (h j) X)
        { fst := j, snd := X } ≫
      G.map (SigmaHom.mk f)
[PROOFSTEP]
apply (h j).naturality
[GOAL]
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
⊢ ∀ (X : (i : I) × C i),
    { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map (𝟙 X) =
      𝟙 ({ obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.obj X)
[PROOFSTEP]
rintro ⟨i, X⟩
[GOAL]
case mk
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
i : I
X : C i
⊢ { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map (𝟙 { fst := i, snd := X }) =
    𝟙 ({ obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.obj { fst := i, snd := X })
[PROOFSTEP]
apply (F i).map_id
[GOAL]
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
⊢ ∀ {X Y Z : (i : I) × C i} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map (f ≫ g) =
      { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map f ≫
        { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map g
[PROOFSTEP]
rintro ⟨i, X⟩ ⟨_, Y⟩ ⟨_, Z⟩ ⟨f⟩ ⟨g⟩
[GOAL]
case mk.mk.mk.mk.mk
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
i : I
X Y✝¹ : C i
f : X ⟶ Y✝¹
Y✝ : C i
g : Y✝¹ ⟶ Y✝
⊢ { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map (SigmaHom.mk f ≫ SigmaHom.mk g) =
    { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map (SigmaHom.mk f) ≫
      { obj := fun X => (F X.fst).obj X.snd, map := fun {X Y} g => descMap F X Y g }.map (SigmaHom.mk g)
[PROOFSTEP]
apply (F i).map_comp
[GOAL]
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
q : (i : I) × C i ⥤ D
h : (i : I) → incl i ⋙ q ≅ F i
⊢ ∀ {X Y : (i : I) × C i} (f : X ⟶ Y),
    q.map f ≫
        ((fun x =>
              match x with
              | { fst := i, snd := X } => (h i).app X)
            Y).hom =
      ((fun x =>
              match x with
              | { fst := i, snd := X } => (h i).app X)
            X).hom ≫
        (desc F).map f
[PROOFSTEP]
rintro ⟨i, X⟩ ⟨_, _⟩ ⟨f⟩
[GOAL]
case mk.mk.mk
I : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : (i : I) → C i ⥤ D
q : (i : I) × C i ⥤ D
h : (i : I) → incl i ⋙ q ≅ F i
i : I
X Y✝ : C i
f : X ⟶ Y✝
⊢ q.map (SigmaHom.mk f) ≫
      ((fun x =>
            match x with
            | { fst := i, snd := X } => (h i).app X)
          { fst := i, snd := Y✝ }).hom =
    ((fun x =>
            match x with
            | { fst := i, snd := X } => (h i).app X)
          { fst := i, snd := X }).hom ≫
      (desc F).map (SigmaHom.mk f)
[PROOFSTEP]
apply (h i).hom.naturality f
[GOAL]
I : 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)
F G : (i : I) → C i ⥤ D i
α : (i : I) → F i ⟶ G i
⊢ ∀ ⦃X Y : (i : I) × C i⦄ (f : X ⟶ Y),
    (Functor.sigma F).map f ≫ (fun f => SigmaHom.mk (NatTrans.app (α f.fst) f.snd)) Y =
      (fun f => SigmaHom.mk (NatTrans.app (α f.fst) f.snd)) X ≫ (Functor.sigma G).map f
[PROOFSTEP]
rintro ⟨i, X⟩ ⟨_, _⟩ ⟨f⟩
[GOAL]
case mk.mk.mk
I : 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)
F G : (i : I) → C i ⥤ D i
α : (i : I) → F i ⟶ G i
i : I
X Y✝ : C i
f : X ⟶ Y✝
⊢ (Functor.sigma F).map (SigmaHom.mk f) ≫
      (fun f => SigmaHom.mk (NatTrans.app (α f.fst) f.snd)) { fst := i, snd := Y✝ } =
    (fun f => SigmaHom.mk (NatTrans.app (α f.fst) f.snd)) { fst := i, snd := X } ≫ (Functor.sigma G).map (SigmaHom.mk f)
[PROOFSTEP]
change SigmaHom.mk _ = SigmaHom.mk _
[GOAL]
case mk.mk.mk
I : 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)
F G : (i : I) → C i ⥤ D i
α : (i : I) → F i ⟶ G i
i : I
X Y✝ : C i
f : X ⟶ Y✝
⊢ SigmaHom.mk
      ((F { fst := i, snd := X }.fst).map f ≫
        NatTrans.app (α { fst := i, snd := Y✝ }.fst) { fst := i, snd := Y✝ }.snd) =
    SigmaHom.mk
      (NatTrans.app (α { fst := i, snd := X }.fst) { fst := i, snd := X }.snd ≫ (G { fst := i, snd := X }.fst).map f)
[PROOFSTEP]
rw [(α i).naturality]
