-- Lean 4 proof step from Mathlib.CategoryTheory.LocallyCartesianClosed.Sections (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : CartesianMonoidalCategory.{v₁, u₁} C
I : C
inst_2 : Closed.{v₁, u₁} I
inst_3 :
  ChosenPullbacksAlong.{v₁, u₁} (Y := tensorUnit.{v₁, u₁} C (𝒞 := inst)) (X := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)
    (curryRightUnitorHom I)
inst_4 : BraidedCategory.{v₁, u₁} C
A : C
X' X : Over.{v₁, u₁} I
u : Functor.obj (toOver I) A ⟶ X'
g : X' ⟶ X
h₁ :
  CategoryStruct.comp (Y :=
      pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
        (curry (Iso.hom (ρ_ I))))
      (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u ≫ Hom.left g)) (toUnit A) ⋯)
      (ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))) =
    CategoryStruct.comp (Y :=
      pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
        (curry (Iso.hom (ρ_ I))))
      (CategoryStruct.comp (Y :=
        pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X'.left) (Functor.map (ihom I) X'.hom)
          (curry (Iso.hom (ρ_ I))))
        (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u)) (toUnit A) ⋯)
        (pullbackMap (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) X'.hom)
          (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) (Hom.left g)) (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
          (𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)) ⋯ ⋯))
      (ChosenPullbacksAlong.fst (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I))))
⊢ Eq (α :=
    A ⟶
      pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
        (curry (Iso.hom (ρ_ I))))
    (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u ≫ Hom.left g)) (toUnit A) ⋯)
    (CategoryStruct.comp (Y :=
      pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X'.left) (Functor.map (ihom I) X'.hom)
        (curry (Iso.hom (ρ_ I))))
      (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u)) (toUnit A) ⋯)
      (pullbackMap (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) X'.hom)
        (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) (Hom.left g)) (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)) ⋯ ⋯))
have h₂ : CategoryStruct.comp (Y :=
    pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
      (curry (Iso.hom (ρ_ I))))
    (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u ≫ Hom.left g)) (toUnit A) sorry)
    (ChosenPullbacksAlong.snd (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I)))) =
  CategoryStruct.comp (Y :=
    pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X.left) (Functor.map (ihom I) X.hom)
      (curry (Iso.hom (ρ_ I))))
    (CategoryStruct.comp (Y :=
      pullbackObj (Y := Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) X'.left) (Functor.map (ihom I) X'.hom)
        (curry (Iso.hom (ρ_ I))))
      (ChosenPullbacksAlong.lift (curry (Iso.hom (β_ I A) ≫ Hom.left u)) (toUnit A) sorry)
      (pullbackMap (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) X'.hom)
        (curry (Iso.hom (ρ_ I))) (Functor.map (ihom I) (Hom.left g)) (𝟙 (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (ihom I) I)) sorry sorry))
    (ChosenPullbacksAlong.snd (Functor.map (ihom I) X.hom) (curry (Iso.hom (ρ_ I))))
Tactic: apply ChosenPullbacksAlong.hom_ext