-- Mathlib/CategoryTheory/Closed/Ideal.lean
theorem bijection_natural (A B : C) (X X' : D) (f : (reflector i).obj (A ⊗ B) ⟶ X) (g : X ⟶ X') :
    bijection i _ _ _ (f ≫ g) = bijection i _ _ _ f ≫ g

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
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ i.fullyFaithfulOfReflective.preimage
      (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
        ((exp.adjunction (i.obj ((reflector i).obj A))).homEquiv (i.obj ((reflector i).obj B)) (i.obj X')).symm
            ((unitCompPartialBijective B ⋯)
              (((exp.adjunction (i.obj ((reflector i).obj A))).homEquiv B (i.obj X'))
                ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                  ((exp.adjunction B).homEquiv (i.obj ((reflector i).obj A)) (i.obj X')).symm
                      ((unitCompPartialBijective A ⋯)
                        (((exp.adjunction B).homEquiv A (i.obj X'))
                          ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫
                    𝟙 (i.obj X')))) ≫
          𝟙 (i.obj X')) =
    i.fullyFaithfulOfReflective.preimage
        (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
          ((exp.adjunction (i.obj ((reflector i).obj A))).homEquiv (i.obj ((reflector i).obj B)) (i.obj X)).symm
              ((unitCompPartialBijective B ⋯)
                (((exp.adjunction (i.obj ((reflector i).obj A))).homEquiv B (i.obj X))
                  ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                    ((exp.adjunction B).homEquiv (i.obj ((reflector i).obj A)) (i.obj X)).symm
                        ((unitCompPartialBijective A ⋯)
                          (((exp.adjunction B).homEquiv A (i.obj X))
                            ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                      𝟙 (i.obj X)))) ≫
            𝟙 (i.obj X)) ≫
      g

Tactic:
erw [homEquiv_symm_apply_eq, homEquiv_symm_apply_eq, homEquiv_apply_eq, homEquiv_apply_eq,
  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
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ i.fullyFaithfulOfReflective.preimage
      (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
        uncurry
            ((unitCompPartialBijective B ⋯)
              (curry
                ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                  uncurry
                      ((unitCompPartialBijective A ⋯)
                        (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫
                    𝟙 (i.obj X')))) ≫
          𝟙 (i.obj X')) =
    i.fullyFaithfulOfReflective.preimage
        (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
          uncurry
              ((unitCompPartialBijective B ⋯)
                (curry
                  ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                    uncurry
                        ((unitCompPartialBijective A ⋯)
                          (curry ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                      𝟙 (i.obj X)))) ≫
            𝟙 (i.obj X)) ≫
      g

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
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ (bijection i A B X') (f ≫ g) = (bijection i A B X) f ≫ g

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
X X' : D
f : (reflector i).obj (A ⊗ B) ⟶ X
g : X ⟶ X'
⊢ i.fullyFaithfulOfReflective.preimage
      (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
        ((exp.adjunction (i.obj ((reflector i).obj A))).homEquiv (i.obj ((reflector i).obj B)) (i.obj X')).symm
            ((unitCompPartialBijective B ⋯)
              (((exp.adjunction (i.obj ((reflector i).obj A))).homEquiv B (i.obj X'))
                ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                  ((exp.adjunction B).homEquiv (i.obj ((reflector i).obj A)) (i.obj X')).symm
                      ((unitCompPartialBijective A ⋯)
                        (((exp.adjunction B).homEquiv A (i.obj X'))
                          ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫
                    𝟙 (i.obj X')))) ≫
          𝟙 (i.obj X')) =
    i.fullyFaithfulOfReflective.preimage
        (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫
          ((exp.adjunction (i.obj ((reflector i).obj A))).homEquiv (i.obj ((reflector i).obj B)) (i.obj X)).symm
              ((unitCompPartialBijective B ⋯)
                (((exp.adjunction (i.obj ((reflector i).obj A))).homEquiv B (i.obj X))
                  ((β_ B (i.obj ((reflector i).obj A))).inv ≫
                    ((exp.adjunction B).homEquiv (i.obj ((reflector i).obj A)) (i.obj X)).symm
                        ((unitCompPartialBijective A ⋯)
                          (((exp.adjunction B).homEquiv A (i.obj X))
                            ((β_ A B).inv ≫ ((reflectorAdjunction i).homEquiv (A ⊗ B) X) f ≫ 𝟙 (i.obj X)))) ≫
                      𝟙 (i.obj X)))) ≫
            𝟙 (i.obj X)) ≫
      g