-- Mathlib/CategoryTheory/Closed/Ideal.lean
theorem bijection_symm_apply_id (A B : C) :
    (bijection i A B _).symm (𝟙 _) = prodComparison _ _ _

Proof state:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ ((reflectorAdjunction i).homEquiv (A ⊗ B) ((reflector i).obj A ⊗ (reflector i).obj B)).symm
      ((reflectorAdjunction i).unit.app A ▷ B ≫
        (β_ ((reflector i ⋙ i).obj A) B).hom ≫
          (β_ B (i.obj ((reflector i).obj A))).hom ≫
            i.obj ((reflector i).obj A) ◁ (reflectorAdjunction i).unit.app B ≫
              (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv) =
    prodComparison (reflector i) A B

Tactic:
erw [SymmetricCategory.symmetry_assoc, ← MonoidalCategory.whisker_exchange_assoc]

Result:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ ((reflectorAdjunction i).homEquiv (A ⊗ B) ((reflector i).obj A ⊗ (reflector i).obj B)).symm
      (A ◁ (reflectorAdjunction i).unit.app B ≫
        (reflectorAdjunction i).unit.app A ▷ (reflector i ⋙ i).obj B ≫
          (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv) =
    prodComparison (reflector i) A B

Proof state:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ (reflectorAdjunction i).unit.app A ⊗ (reflectorAdjunction i).unit.app B =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫
      i.map (prodComparison (reflector i) A B) ≫ (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).hom

Tactic:
rw [prodComparisonIso_hom i ((reflector i).obj A) ((reflector i).obj B)]

Result:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ (reflectorAdjunction i).unit.app A ⊗ (reflectorAdjunction i).unit.app B =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫
      i.map (prodComparison (reflector i) A B) ≫ prodComparison i ((reflector i).obj A) ((reflector i).obj B)

Proof state:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ (bijection i A B ((reflector i).obj A ⊗ (reflector i).obj B)).symm (𝟙 ((reflector i).obj A ⊗ (reflector i).obj B)) =
    prodComparison (reflector i) A B

Tactic:
dsimp [bijection]

Result:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ ((reflectorAdjunction i).homEquiv (A ⊗ B) ((reflector i).obj A ⊗ (reflector i).obj B)).symm
      ((β_ A B).hom ≫
        ((exp.adjunction B).homEquiv A (i.obj ((reflector i).obj A ⊗ (reflector i).obj B))).symm
            ((unitCompPartialBijective A ⋯).symm
              (((exp.adjunction B).homEquiv (i.obj ((reflector i).obj A))
                  (i.obj ((reflector i).obj A ⊗ (reflector i).obj B)))
                ((β_ B (i.obj ((reflector i).obj A))).hom ≫
                  ((exp.adjunction (i.obj ((reflector i).obj A))).homEquiv B
                          (i.obj ((reflector i).obj A ⊗ (reflector i).obj B))).symm
                      ((unitCompPartialBijective B ⋯).symm
                        (((exp.adjunction (i.obj ((reflector i).obj A))).homEquiv (i.obj ((reflector i).obj B))
                            (i.obj ((reflector i).obj A ⊗ (reflector i).obj B)))
                          ((prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv ≫
                            i.map (𝟙 ((reflector i).obj A ⊗ (reflector i).obj B)) ≫
                              𝟙 (i.obj ((reflector i).obj A ⊗ (reflector i).obj B))))) ≫
                    𝟙 (i.obj ((reflector i).obj A ⊗ (reflector i).obj B))))) ≫
          𝟙 (i.obj ((reflector i).obj A ⊗ (reflector i).obj B))) =
    prodComparison (reflector i) A B

Proof state:
case h_fst
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ ((reflectorAdjunction i).unit.app A ⊗ (reflectorAdjunction i).unit.app B) ≫
      fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)) =
    ((reflectorAdjunction i).unit.app (A ⊗ B) ≫
        i.map (prodComparison (reflector i) A B) ≫ prodComparison i ((reflector i).obj A) ((reflector i).obj B)) ≫
      fst (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))

Tactic:
rw [tensorHom_fst, assoc, assoc, prodComparison_fst, ← i.map_comp,
prodComparison_fst]

Result:
case h_fst
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ fst A B ≫ (reflectorAdjunction i).unit.app A =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map ((reflector i).map (fst A B))

Proof state:
case h_snd
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ ((reflectorAdjunction i).unit.app A ⊗ (reflectorAdjunction i).unit.app B) ≫
      snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)) =
    ((reflectorAdjunction i).unit.app (A ⊗ B) ≫
        i.map (prodComparison (reflector i) A B) ≫ prodComparison i ((reflector i).obj A) ((reflector i).obj B)) ≫
      snd (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B))

Tactic:
rw [tensorHom_snd, assoc, assoc, prodComparison_snd, ← i.map_comp,
prodComparison_snd]

Result:
case h_snd
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : ChosenFiniteProducts C
inst✝³ : Reflective i
inst✝² : CartesianClosed C
inst✝¹ : ChosenFiniteProducts D
inst✝ : ExponentialIdeal i
A B : C
⊢ snd A B ≫ (reflectorAdjunction i).unit.app B =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map ((reflector i).map (snd A B))