-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Closed.Ideal (goal)
Goal:
C : Type u₁
D : Type u₂
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₁, u₂} D
i : Functor.{v₁, v₁, u₂, u₁} D C
inst_2 : CartesianMonoidalCategory.{v₁, u₁} C
inst_3 : Reflective i
inst_4 : MonoidalClosed.{v₁, u₁} C
inst_5 : CartesianMonoidalCategory.{v₁, u₂} D
inst_6 : ExponentialIdeal i
inst_7 : BraidedCategory.{v₁, u₁} C
A B : C
X X' : D
f : (reflector i).obj (tensorObj.{v₁, u₁} (𝒞 := inst) A B) ⟶ X
g : X ⟶ X'
⊢ Eq (α := tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶ X')
    (i.fullyFaithfulOfReflective.preimage
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
        (prodComparison i ((reflector i).obj A) ((reflector i).obj B))
        ((Equiv.symm
                (Adjunction.homEquiv (ihom.adjunction (i.obj ((reflector i).obj A))) (i.obj ((reflector i).obj B))
                  (i.obj X')) :
              (a : i.obj ((reflector i).obj B) ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X') →
                i.obj ((reflector i).obj A) ⊗ i.obj ((reflector i).obj B) ⟶ i.obj X')
            ((unitCompPartialBijective B ⋯ :
                  (a : B ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X') →
                    i.obj ((reflector i).obj B) ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X')
                ((Adjunction.homEquiv (ihom.adjunction (i.obj ((reflector i).obj A))) B (i.obj X') :
                      (a : i.obj ((reflector i).obj A) ⊗ B ⟶ i.obj X') → B ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X')
                    (Iso.inv (β_ B (i.obj ((reflector i).obj A))) ≫
                      (Equiv.symm (Adjunction.homEquiv (ihom.adjunction B) (i.obj ((reflector i).obj A)) (i.obj X')) :
                            (a : i.obj ((reflector i).obj A) ⟶ B ⟹ i.obj X') →
                              B ⊗ i.obj ((reflector i).obj A) ⟶ i.obj X')
                          ((unitCompPartialBijective A ⋯ :
                                (a : A ⟶ B ⟹ i.obj X') → i.obj ((reflector i).obj A) ⟶ B ⟹ i.obj X')
                              ((Adjunction.homEquiv (ihom.adjunction B) A (i.obj X') :
                                    (a : B ⊗ A ⟶ i.obj X') → A ⟶ B ⟹ i.obj X')
                                  (Iso.inv (β_ A B) ≫
                                    (Adjunction.homEquiv (reflectorAdjunction i) (tensorObj.{v₁, u₁} (𝒞 := inst) A B)
                                            X' :
                                          (a : (reflector i).obj (A ⊗ B) ⟶ X') → A ⊗ B ⟶ i.obj X')
                                        (f ≫ g) ≫
                                      𝟙 (i.obj X')) :
                                A ⟶ B ⟹ i.obj X') :
                            i.obj ((reflector i).obj A) ⟶ B ⟹ i.obj X') ≫
                        𝟙 (i.obj X')) :
                  B ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X') :
              i.obj ((reflector i).obj B) ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X') ≫
          𝟙 (i.obj X'))))
    (i.fullyFaithfulOfReflective.preimage
        (CategoryStruct.comp (Y :=
          tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
          (prodComparison i ((reflector i).obj A) ((reflector i).obj B))
          ((Equiv.symm
                  (Adjunction.homEquiv (ihom.adjunction (i.obj ((reflector i).obj A))) (i.obj ((reflector i).obj B))
                    (i.obj X)) :
                (a : i.obj ((reflector i).obj B) ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X) →
                  i.obj ((reflector i).obj A) ⊗ i.obj ((reflector i).obj B) ⟶ i.obj X)
              ((unitCompPartialBijective B ⋯ :
                    (a : B ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X) →
                      i.obj ((reflector i).obj B) ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X)
                  ((Adjunction.homEquiv (ihom.adjunction (i.obj ((reflector i).obj A))) B (i.obj X) :
                        (a : i.obj ((reflector i).obj A) ⊗ B ⟶ i.obj X) → B ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X)
                      (Iso.inv (β_ B (i.obj ((reflector i).obj A))) ≫
                        (Equiv.symm (Adjunction.homEquiv (ihom.adjunction B) (i.obj ((reflector i).obj A)) (i.obj X)) :
                              (a : i.obj ((reflector i).obj A) ⟶ B ⟹ i.obj X) →
                                B ⊗ i.obj ((reflector i).obj A) ⟶ i.obj X)
                            ((unitCompPartialBijective A ⋯ :
                                  (a : A ⟶ B ⟹ i.obj X) → i.obj ((reflector i).obj A) ⟶ B ⟹ i.obj X)
                                ((Adjunction.homEquiv (ihom.adjunction B) A (i.obj X) :
                                      (a : B ⊗ A ⟶ i.obj X) → A ⟶ B ⟹ i.obj X)
                                    (Iso.inv (β_ A B) ≫
                                      (Adjunction.homEquiv (reflectorAdjunction i) (tensorObj.{v₁, u₁} (𝒞 := inst) A B)
                                              X :
                                            (a : (reflector i).obj (A ⊗ B) ⟶ X) → A ⊗ B ⟶ i.obj X)
                                          f ≫
                                        𝟙 (i.obj X)) :
                                  A ⟶ B ⟹ i.obj X) :
                              i.obj ((reflector i).obj A) ⟶ B ⟹ i.obj X) ≫
                          𝟙 (i.obj X)) :
                    B ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X) :
                i.obj ((reflector i).obj B) ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X) ≫
            𝟙 (i.obj X))) ≫
      g)
have erw : Eq (α := tensorObj.{v₁, u₂} (𝒞 := inst_1) ((reflector i).obj A) ((reflector i).obj B) ⟶ X')
  (i.fullyFaithfulOfReflective.preimage
    (CategoryStruct.comp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
      (prodComparison i ((reflector i).obj A) ((reflector i).obj B))
      (uncurry
          ((unitCompPartialBijective B sorry :
              (a : B ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X') →
                i.obj ((reflector i).obj B) ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X')
            (curry
              (Iso.inv (β_ B (i.obj ((reflector i).obj A))) ≫
                uncurry
                    ((unitCompPartialBijective A sorry :
                        (a : A ⟶ B ⟹ i.obj X') → i.obj ((reflector i).obj A) ⟶ B ⟹ i.obj X')
                      (curry
                        (Iso.inv (β_ A B) ≫
                          (Adjunction.homEquiv (reflectorAdjunction i) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) X' :
                                (a : (reflector i).obj (A ⊗ B) ⟶ X') → A ⊗ B ⟶ i.obj X')
                              (f ≫ g) ≫
                            𝟙 (i.obj X')))) ≫
                  𝟙 (i.obj X')))) ≫
        𝟙 (i.obj X'))))
  (i.fullyFaithfulOfReflective.preimage
      (CategoryStruct.comp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) (i.obj ((reflector i).obj A)) (i.obj ((reflector i).obj B)))
        (prodComparison i ((reflector i).obj A) ((reflector i).obj B))
        (uncurry
            ((unitCompPartialBijective B sorry :
                (a : B ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X) →
                  i.obj ((reflector i).obj B) ⟶ i.obj ((reflector i).obj A) ⟹ i.obj X)
              (curry
                (Iso.inv (β_ B (i.obj ((reflector i).obj A))) ≫
                  uncurry
                      ((unitCompPartialBijective A sorry :
                          (a : A ⟶ B ⟹ i.obj X) → i.obj ((reflector i).obj A) ⟶ B ⟹ i.obj X)
                        (curry
                          (Iso.inv (β_ A B) ≫
                            (Adjunction.homEquiv (reflectorAdjunction i) (tensorObj.{v₁, u₁} (𝒞 := inst) A B) X :
                                  (a : (reflector i).obj (A ⊗ B) ⟶ X) → A ⊗ B ⟶ i.obj 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]