[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f ↔ IsIso f.fst ∧ IsIso f.snd
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f → IsIso f.fst ∧ IsIso f.snd
[PROOFSTEP]
rintro ⟨g, hfg, hgf⟩
[GOAL]
case mp.mk.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f ≫ g = 𝟙 (P, S)
hgf : g ≫ f = 𝟙 (Q, T)
⊢ IsIso f.fst ∧ IsIso f.snd
[PROOFSTEP]
simp at hfg hgf 
[GOAL]
case mp.mk.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f.fst ≫ g.fst = 𝟙 P ∧ f.snd ≫ g.snd = 𝟙 S
hgf : g.fst ≫ f.fst = 𝟙 Q ∧ g.snd ≫ f.snd = 𝟙 T
⊢ IsIso f.fst ∧ IsIso f.snd
[PROOFSTEP]
rcases hfg with ⟨hfg₁, hfg₂⟩
[GOAL]
case mp.mk.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hgf : g.fst ≫ f.fst = 𝟙 Q ∧ g.snd ≫ f.snd = 𝟙 T
hfg₁ : f.fst ≫ g.fst = 𝟙 P
hfg₂ : f.snd ≫ g.snd = 𝟙 S
⊢ IsIso f.fst ∧ IsIso f.snd
[PROOFSTEP]
rcases hgf with ⟨hgf₁, hgf₂⟩
[GOAL]
case mp.mk.intro.intro.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg₁ : f.fst ≫ g.fst = 𝟙 P
hfg₂ : f.snd ≫ g.snd = 𝟙 S
hgf₁ : g.fst ≫ f.fst = 𝟙 Q
hgf₂ : g.snd ≫ f.snd = 𝟙 T
⊢ IsIso f.fst ∧ IsIso f.snd
[PROOFSTEP]
exact ⟨⟨⟨g.1, hfg₁, hgf₁⟩⟩, ⟨⟨g.2, hfg₂, hgf₂⟩⟩⟩
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f.fst ∧ IsIso f.snd → IsIso f
[PROOFSTEP]
rintro ⟨⟨g₁, hfg₁, hgf₁⟩, ⟨g₂, hfg₂, hgf₂⟩⟩
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 (P, S).fst
hgf₁ : g₁ ≫ f.fst = 𝟙 (Q, T).fst
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 (P, S).snd
hgf₂ : g₂ ≫ f.snd = 𝟙 (Q, T).snd
⊢ IsIso f
[PROOFSTEP]
dsimp at hfg₁ hgf₁ hfg₂ hgf₂ 
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ IsIso f
[PROOFSTEP]
refine' ⟨⟨(g₁, g₂), _, _⟩⟩
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ f ≫ (g₁, g₂) = 𝟙 (P, S)
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ (g₁, g₂) ≫ f = 𝟙 (Q, T)
[PROOFSTEP]
repeat {simp; constructor; assumption; assumption
}
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ f ≫ (g₁, g₂) = 𝟙 (P, S)
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ (g₁, g₂) ≫ f = 𝟙 (Q, T)
[PROOFSTEP]
{simp; constructor; assumption; assumption
}
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ f ≫ (g₁, g₂) = 𝟙 (P, S)
[PROOFSTEP]
simp
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ f.fst ≫ g₁ = 𝟙 P ∧ f.snd ≫ g₂ = 𝟙 S
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_1.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ f.fst ≫ g₁ = 𝟙 P
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_1.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ f.snd ≫ g₂ = 𝟙 S
[PROOFSTEP]
assumption
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_1.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ f.snd ≫ g₂ = 𝟙 S
[PROOFSTEP]
assumption
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ (g₁, g₂) ≫ f = 𝟙 (Q, T)
[PROOFSTEP]
{simp; constructor; assumption; assumption
}
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ (g₁, g₂) ≫ f = 𝟙 (Q, T)
[PROOFSTEP]
simp
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ g₁ ≫ f.fst = 𝟙 Q ∧ g₂ ≫ f.snd = 𝟙 T
[PROOFSTEP]
constructor
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ g₁ ≫ f.fst = 𝟙 Q
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ g₂ ≫ f.snd = 𝟙 T
[PROOFSTEP]
assumption
[GOAL]
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ g₂ ≫ f.snd = 𝟙 T
[PROOFSTEP]
assumption
[GOAL]

[PROOFSTEP]
{simp; constructor; assumption; assumption
}
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C × D
⊢ (𝟭 (C × D)).obj X = (swap C D ⋙ swap D C).obj X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : D × C
⊢ (swap D C ⋙ swap C D).obj X = (𝟭 (D × C)).obj X
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ IsEquivalence (braiding C D).functor
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C × (C ⥤ D)
f : X ⟶ Y
g : Y ⟶ Z
⊢ { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map (f ≫ g) =
    { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map f ≫
      { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map g
[PROOFSTEP]
cases g
[GOAL]
case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C × (C ⥤ D)
f : X ⟶ Y
fst✝ : Y.fst ⟶ Z.fst
snd✝ : Y.snd ⟶ Z.snd
⊢ { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
      (f ≫ (fst✝, snd✝)) =
    { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map f ≫
      { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝, snd✝)
[PROOFSTEP]
cases f
[GOAL]
case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C × (C ⥤ D)
fst✝¹ : Y.fst ⟶ Z.fst
snd✝¹ : Y.snd ⟶ Z.snd
fst✝ : X.fst ⟶ Y.fst
snd✝ : X.snd ⟶ Y.snd
⊢ { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
      ((fst✝, snd✝) ≫ (fst✝¹, snd✝¹)) =
    { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝, snd✝) ≫
      { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝¹, snd✝¹)
[PROOFSTEP]
cases Z
[GOAL]
case mk.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C × (C ⥤ D)
fst✝² : X.fst ⟶ Y.fst
snd✝² : X.snd ⟶ Y.snd
fst✝¹ : C
snd✝¹ : C ⥤ D
fst✝ : Y.fst ⟶ (fst✝¹, snd✝¹).fst
snd✝ : Y.snd ⟶ (fst✝¹, snd✝¹).snd
⊢ { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
      ((fst✝², snd✝²) ≫ (fst✝, snd✝)) =
    { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝², snd✝²) ≫
      { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝, snd✝)
[PROOFSTEP]
cases Y
[GOAL]
case mk.mk.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C × (C ⥤ D)
fst✝³ : C
snd✝³ : C ⥤ D
fst✝² : C
snd✝² : C ⥤ D
fst✝¹ : X.fst ⟶ (fst✝², snd✝²).fst
snd✝¹ : X.snd ⟶ (fst✝², snd✝²).snd
fst✝ : (fst✝², snd✝²).fst ⟶ (fst✝³, snd✝³).fst
snd✝ : (fst✝², snd✝²).snd ⟶ (fst✝³, snd✝³).snd
⊢ { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
      ((fst✝¹, snd✝¹) ≫ (fst✝, snd✝)) =
    { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝¹, snd✝¹) ≫
      { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝, snd✝)
[PROOFSTEP]
cases X
[GOAL]
case mk.mk.mk.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
fst✝⁴ : C
snd✝⁴ : C ⥤ D
fst✝³ : C
snd✝³ : C ⥤ D
fst✝² : (fst✝³, snd✝³).fst ⟶ (fst✝⁴, snd✝⁴).fst
snd✝² : (fst✝³, snd✝³).snd ⟶ (fst✝⁴, snd✝⁴).snd
fst✝¹ : C
snd✝¹ : C ⥤ D
fst✝ : (fst✝¹, snd✝¹).fst ⟶ (fst✝³, snd✝³).fst
snd✝ : (fst✝¹, snd✝¹).snd ⟶ (fst✝³, snd✝³).snd
⊢ { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
      ((fst✝, snd✝) ≫ (fst✝², snd✝²)) =
    { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝, snd✝) ≫
      { obj := fun p => p.snd.obj p.fst, map := fun {x y} f => x.snd.map f.fst ≫ NatTrans.app f.snd y.fst }.map
        (fst✝², snd✝²)
[PROOFSTEP]
simp only [prod_comp, NatTrans.comp_app, Functor.map_comp, Category.assoc]
[GOAL]
case mk.mk.mk.mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
fst✝⁴ : C
snd✝⁴ : C ⥤ D
fst✝³ : C
snd✝³ : C ⥤ D
fst✝² : (fst✝³, snd✝³).fst ⟶ (fst✝⁴, snd✝⁴).fst
snd✝² : (fst✝³, snd✝³).snd ⟶ (fst✝⁴, snd✝⁴).snd
fst✝¹ : C
snd✝¹ : C ⥤ D
fst✝ : (fst✝¹, snd✝¹).fst ⟶ (fst✝³, snd✝³).fst
snd✝ : (fst✝¹, snd✝¹).snd ⟶ (fst✝³, snd✝³).snd
⊢ snd✝¹.map fst✝ ≫ snd✝¹.map fst✝² ≫ NatTrans.app snd✝ fst✝⁴ ≫ NatTrans.app snd✝² fst✝⁴ =
    snd✝¹.map fst✝ ≫ NatTrans.app snd✝ fst✝³ ≫ snd✝³.map fst✝² ≫ NatTrans.app snd✝² fst✝⁴
[PROOFSTEP]
rw [← NatTrans.comp_app, NatTrans.naturality, NatTrans.comp_app, Category.assoc, NatTrans.naturality]
[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 G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
X Y : A × C
f : X ⟶ Y
⊢ (Functor.prod F H).map f ≫ (fun X => (app α X.fst, app β X.snd)) Y =
    (fun X => (app α X.fst, app β X.snd)) X ≫ (Functor.prod G I).map f
[PROOFSTEP]
cases X
[GOAL]
case mk
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 G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
Y : A × C
fst✝ : A
snd✝ : C
f : (fst✝, snd✝) ⟶ Y
⊢ (Functor.prod F H).map f ≫ (fun X => (app α X.fst, app β X.snd)) Y =
    (fun X => (app α X.fst, app β X.snd)) (fst✝, snd✝) ≫ (Functor.prod G I).map f
[PROOFSTEP]
cases Y
[GOAL]
case mk.mk
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 G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ (Functor.prod F H).map f ≫ (fun X => (app α X.fst, app β X.snd)) (fst✝, snd✝) =
    (fun X => (app α X.fst, app β X.snd)) (fst✝¹, snd✝¹) ≫ (Functor.prod G I).map f
[PROOFSTEP]
simp only [Functor.prod_map, prod_comp]
[GOAL]
case mk.mk
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 G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ (F.map f.fst ≫ app α fst✝, H.map f.snd ≫ app β snd✝) = (app α fst✝¹ ≫ G.map f.fst, app β snd✝¹ ≫ I.map f.snd)
[PROOFSTEP]
rw [Prod.mk.inj_iff]
[GOAL]
case mk.mk
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 G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ F.map f.fst ≫ app α fst✝ = app α fst✝¹ ≫ G.map f.fst ∧ H.map f.snd ≫ app β snd✝ = app β snd✝¹ ≫ I.map f.snd
[PROOFSTEP]
constructor
[GOAL]
case mk.mk.left
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 G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ F.map f.fst ≫ app α fst✝ = app α fst✝¹ ≫ G.map f.fst
case mk.mk.right
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 G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ H.map f.snd ≫ app β snd✝ = app β snd✝¹ ≫ I.map f.snd
[PROOFSTEP]
repeat {rw [naturality]
}
[GOAL]
case mk.mk.left
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 G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ F.map f.fst ≫ app α fst✝ = app α fst✝¹ ≫ G.map f.fst
case mk.mk.right
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 G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ H.map f.snd ≫ app β snd✝ = app β snd✝¹ ≫ I.map f.snd
[PROOFSTEP]
{rw [naturality]
}
[GOAL]
case mk.mk.left
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 G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ F.map f.fst ≫ app α fst✝ = app α fst✝¹ ≫ G.map f.fst
[PROOFSTEP]
rw [naturality]
[GOAL]
case mk.mk.right
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 G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ H.map f.snd ≫ app β snd✝ = app β snd✝¹ ≫ I.map f.snd
[PROOFSTEP]
{rw [naturality]
}
[GOAL]
case mk.mk.right
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 G : A ⥤ B
H I : C ⥤ D
α : F ⟶ G
β : H ⟶ I
fst✝¹ : A
snd✝¹ : C
fst✝ : A
snd✝ : C
f : (fst✝¹, snd✝¹) ⟶ (fst✝, snd✝)
⊢ H.map f.snd ≫ app β snd✝ = app β snd✝¹ ≫ I.map f.snd
[PROOFSTEP]
rw [naturality]
[GOAL]

[PROOFSTEP]
{rw [naturality]
}
[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
X✝ Y✝ : A ⥤ B × C
α : X✝ ⟶ Y✝
X Y : A
f : X ⟶ Y
⊢ ((fun F => (F ⋙ Prod.fst B C, F ⋙ Prod.snd B C)) X✝).fst.map f ≫ (fun X => (NatTrans.app α X).fst) Y =
    (fun X => (NatTrans.app α X).fst) X ≫ ((fun F => (F ⋙ Prod.fst B C, F ⋙ Prod.snd B C)) Y✝).fst.map f
[PROOFSTEP]
simp only [Functor.comp_map, Prod.fst_map, ← prod_comp_fst, α.naturality]
[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
X✝ Y✝ : A ⥤ B × C
α : X✝ ⟶ Y✝
X Y : A
f : X ⟶ Y
⊢ ((fun F => (F ⋙ Prod.fst B C, F ⋙ Prod.snd B C)) X✝).snd.map f ≫ (fun X => (NatTrans.app α X).snd) Y =
    (fun X => (NatTrans.app α X).snd) X ≫ ((fun F => (F ⋙ Prod.fst B C, F ⋙ Prod.snd B C)) Y✝).snd.map f
[PROOFSTEP]
simp only [Functor.comp_map, Prod.snd_map, ← prod_comp_snd, α.naturality]
