-- 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
      (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

Tactic:
dsimp only [Functor.comp_obj]

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 ▷ i.obj ((reflector 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).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

Tactic:
erw [homEquiv_symm_apply_eq, homEquiv_symm_apply_eq, homEquiv_apply_eq, homEquiv_apply_eq]

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 ≫
        uncurry
            ((unitCompPartialBijective A ⋯).symm
              (curry
                ((β_ B (i.obj ((reflector i).obj A))).hom ≫
                  uncurry
                      ((unitCompPartialBijective B ⋯).symm
                        (curry
                          ((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:
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 ▷ i.obj ((reflector i).obj B) ≫
          (prodComparisonIso i ((reflector i).obj A) ((reflector i).obj B)).inv) =
    prodComparison (reflector i) A B

Tactic:
rw [← tensorHom_def'_assoc, Adjunction.homEquiv_symm_apply,
  ← Adjunction.eq_unit_comp_map_iff, Iso.comp_inv_eq, 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).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

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
⊢ snd A B ≫ (reflectorAdjunction i).unit.app B =
    (reflectorAdjunction i).unit.app (A ⊗ B) ≫ i.map ((reflector i).map (snd A B))

Tactic:
apply (reflectorAdjunction i).unit.naturality

Result:
no goals

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
      ((β_ A B).hom ≫
        uncurry
            ((unitCompPartialBijective A ⋯).symm
              (curry
                ((β_ B (i.obj ((reflector i).obj A))).hom ≫
                  uncurry
                      ((unitCompPartialBijective B ⋯).symm
                        (curry
                          ((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

Tactic:
rw [comp_id, comp_id, comp_id, i.map_id, comp_id, unitCompPartialBijective_symm_apply,
  unitCompPartialBijective_symm_apply, uncurry_natural_left, uncurry_curry,
  uncurry_natural_left, uncurry_curry, ← BraidedCategory.braiding_naturality_left_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
      ((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