-- Mathlib/CategoryTheory/ChosenFiniteProducts/FunctorCategory.lean
@[simp]
lemma associator_hom_app (F₁ F₂ F₃ : J ⥤ C) (j : J) :
    (α_ F₁ F₂ F₃).hom.app j = (α_ _ _ _).hom

Proof state:
case h_snd.h_snd
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (snd (F₁ ⊗ F₂) F₃).app j = snd (F₁.obj j ⊗ F₂.obj j) (F₃.obj j)

Tactic:
rfl

Result:
no goals

Proof state:
case h_snd.h_fst
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (fst (F₁ ⊗ F₂) F₃ ≫ snd F₁ F₂).app j = fst (F₁.obj j ⊗ F₂.obj j) (F₃.obj j) ≫ snd (F₁.obj j) (F₂.obj j)

Tactic:
rfl

Result:
no goals

Proof state:
case h_snd.h_fst
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (fst (F₁ ⊗ F₂) F₃ ≫ snd F₁ F₂).app j =
    (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j) ≫ fst (F₂.obj j) (F₃.obj j)

Tactic:
erw [associator_hom_snd_fst]

Result:
case h_snd.h_fst
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (fst (F₁ ⊗ F₂) F₃ ≫ snd F₁ F₂).app j = fst (F₁.obj j ⊗ F₂.obj j) (F₃.obj j) ≫ snd (F₁.obj j) (F₂.obj j)

Proof state:
case h_snd.h_snd
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ ((α_ F₁ F₂ F₃).hom.app j ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j)) ≫ snd (F₂.obj j) (F₃.obj j) =
    ((α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j)) ≫ snd (F₂.obj j) (F₃.obj j)

Tactic:
change (_ ≫ (snd F₁ (F₂ ⊗ F₃)).app j) ≫ (snd F₂ F₃).app j = _

Result:
case h_snd.h_snd
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ ((α_ F₁ F₂ F₃).hom.app j ≫ (snd F₁ (F₂ ⊗ F₃)).app j) ≫ (snd F₂ F₃).app j =
    ((α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j)) ≫ snd (F₂.obj j) (F₃.obj j)

Proof state:
case h_snd.h_fst
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ ((α_ F₁ F₂ F₃).hom.app j ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j)) ≫ fst (F₂.obj j) (F₃.obj j) =
    ((α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j)) ≫ fst (F₂.obj j) (F₃.obj j)

Tactic:
change (_ ≫ (snd F₁ (F₂ ⊗ F₃)).app j) ≫ (fst F₂ F₃).app j = _

Result:
case h_snd.h_fst
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ ((α_ F₁ F₂ F₃).hom.app j ≫ (snd F₁ (F₂ ⊗ F₃)).app j) ≫ (fst F₂ F₃).app j =
    ((α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j)) ≫ fst (F₂.obj j) (F₃.obj j)

Proof state:
case h_fst
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (fst (F₁ ⊗ F₂) F₃ ≫ fst F₁ F₂).app j = fst (F₁.obj j ⊗ F₂.obj j) (F₃.obj j) ≫ fst (F₁.obj j) (F₂.obj j)

Tactic:
rfl

Result:
no goals

Proof state:
case h_fst
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (α_ F₁ F₂ F₃).hom.app j ≫ fst (F₁.obj j) ((F₂ ⊗ F₃).obj j) =
    (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ fst (F₁.obj j) ((F₂ ⊗ F₃).obj j)

Tactic:
change _ ≫ (fst F₁ (F₂ ⊗ F₃)).app j = _

Result:
case h_fst
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (α_ F₁ F₂ F₃).hom.app j ≫ (fst F₁ (F₂ ⊗ F₃)).app j =
    (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ fst (F₁.obj j) ((F₂ ⊗ F₃).obj j)

Proof state:
case h_snd
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (α_ F₁ F₂ F₃).hom.app j ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j) =
    (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j)

Tactic:
apply hom_ext

Result:
case h_snd.h_fst
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ ((α_ F₁ F₂ F₃).hom.app j ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j)) ≫ fst (F₂.obj j) (F₃.obj j) =
    ((α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j)) ≫ fst (F₂.obj j) (F₃.obj j)

case h_snd.h_snd
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ ((α_ F₁ F₂ F₃).hom.app j ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j)) ≫ snd (F₂.obj j) (F₃.obj j) =
    ((α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j)) ≫ snd (F₂.obj j) (F₃.obj j)

Proof state:
case h_fst
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (α_ F₁ F₂ F₃).hom.app j ≫ (fst F₁ (F₂ ⊗ F₃)).app j =
    (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ fst (F₁.obj j) ((F₂ ⊗ F₃).obj j)

Tactic:
rw [← NatTrans.comp_app, associator_hom_fst]

Result:
case h_fst
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (fst (F₁ ⊗ F₂) F₃ ≫ fst F₁ F₂).app j = (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ fst (F₁.obj j) ((F₂ ⊗ F₃).obj j)

Proof state:
case h_snd.h_snd
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (snd (F₁ ⊗ F₂) F₃).app j =
    (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j) ≫ snd (F₂.obj j) (F₃.obj j)

Tactic:
erw [associator_hom_snd_snd]

Result:
case h_snd.h_snd
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (snd (F₁ ⊗ F₂) F₃).app j = snd (F₁.obj j ⊗ F₂.obj j) (F₃.obj j)

Proof state:
case h_snd.h_snd
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ ((α_ F₁ F₂ F₃).hom.app j ≫ (snd F₁ (F₂ ⊗ F₃)).app j) ≫ (snd F₂ F₃).app j =
    ((α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j)) ≫ snd (F₂.obj j) (F₃.obj j)

Tactic:
rw [← NatTrans.comp_app, ← NatTrans.comp_app, assoc, associator_hom_snd_snd, assoc]

Result:
case h_snd.h_snd
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (snd (F₁ ⊗ F₂) F₃).app j =
    (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ snd (F₁.obj j) ((F₂ ⊗ F₃).obj j) ≫ snd (F₂.obj j) (F₃.obj j)

Proof state:
case h_fst
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (fst (F₁ ⊗ F₂) F₃ ≫ fst F₁ F₂).app j = (α_ (F₁.obj j) (F₂.obj j) (F₃.obj j)).hom ≫ fst (F₁.obj j) ((F₂ ⊗ F₃).obj j)

Tactic:
erw [associator_hom_fst]

Result:
case h_fst
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F₁ F₂ F₃ : J ⥤ C
j : J
⊢ (fst (F₁ ⊗ F₂) F₃ ≫ fst F₁ F₂).app j = fst (F₁.obj j ⊗ F₂.obj j) (F₃.obj j) ≫ fst (F₁.obj j) (F₂.obj j)