-- Lean 4 proof step from Mathlib.Condensed.Discrete.LocallyConstant (goal)
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
S_1 : CompHausLike P
Y_1 : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f_1 : LocallyConstant (↑(S_1.toTop (P := P)) : Type u) (Y_1.obj (op (of P PUnit.{u + 1})))
T_1 : CompHausLike P
g_1 : T_1 ⟶ S_1
inst_2 : HasExplicitFiniteCoproducts P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_3 : PreservesFiniteProducts Y
S T : (CompHausLike P)ᵒᵖ
g : S ⟶ T
f : Functor.obj (Functor.obj (functorToPresheaves.{u, w} (P := P)) (Y.obj (op (of P PUnit.{u + 1})))) S
a :
  Fiber (Y := (↑((unop T).toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
    (⇑(comap (TopCat.Hom.hom g.unop.hom) f) : (a : (↑(unop T).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
⊢ Eq (α := Y.obj (op (fiber.{u, w} (P := P) (comap (TopCat.Hom.hom g.unop.hom) f) a)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Y.map
              (Quiver.Hom.op
                (IsTerminal.from (isTerminalPUnit (P := P))
                  (fiber.{u, w} (P := P) (comap (TopCat.Hom.hom g.unop.hom) f) a)))) :
          (a_1 : Y.obj (op (of P PUnit.{u + 1}))) → Y.obj (op (fiber (comap (TopCat.Hom.hom g.unop.hom) f) a)))
        (Fiber.image
          (⇑(comap (TopCat.Hom.hom g.unop.hom) f) : (a : (↑(unop T).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
          a) :
      Y.obj (op (fiber.{u, w} (P := P) (comap (TopCat.Hom.hom g.unop.hom) f) a)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Y.map
              (Quiver.Hom.op
                (componentHom (P := P) f g.unop a ≫
                  IsTerminal.from (isTerminalPUnit (P := P))
                    (fiber.{u, w} (P := P) f
                      (Fiber.mk (⇑f : (a : (↑(unop S).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
                        ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC :=
                              fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) g.unop :
                            (a : (↑(unop T).toTop : Type u)) → (↑(unop S).toTop : Type u))
                          (preimage
                            (⇑(comap (TopCat.Hom.hom g.unop.hom) f) :
                              (a : (↑(unop T).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
                            a))))))) :
          (a_1 : Y.obj (op (of P PUnit.{u + 1}))) → Y.obj (op (fiber (comap (TopCat.Hom.hom g.unop.hom) f) a)))
        (Fiber.image (Y := (↑((unop S).toTop (P := P)) : Type u))
          ((⇑f : (a : (↑((unop S).toTop (P := P)) : Type u)) → Y.obj (op (of P PUnit.{u + 1}))) :
            (a : (↑((unop S).toTop (P := P)) : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
          (Fiber.mk (⇑f : (a : (↑(unop S).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
              ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
                    C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC :=
                    fun (X : CompHausLike P) ↦ (↑(X.toTop (P := P)) : Type u)) g.unop :
                  (a : (↑(unop T).toTop : Type u)) → (↑(unop S).toTop : Type u))
                (preimage
                  (⇑(comap (TopCat.Hom.hom g.unop.hom) f) :
                    (a : (↑(unop T).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
                  a)) :
            Fiber (Y := (↑((unop S).toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
              (⇑f : (a : (↑(unop S).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1}))))) :
      Y.obj (op (fiber.{u, w} (P := P) (comap (TopCat.Hom.hom g.unop.hom) f) a)))
have h : Fiber.image
    (⇑(comap (TopCat.Hom.hom g.unop.hom) f) : (a : (↑(unop T).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1}))) a =
  Fiber.image (Y := (↑((unop S).toTop (P := P)) : Type u))
    ((⇑f : (a : (↑((unop S).toTop (P := P)) : Type u)) → Y.obj (op (of P PUnit.{u + 1}))) :
      (a : (↑((unop S).toTop (P := P)) : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
    (Fiber.mk (⇑f : (a : (↑(unop S).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike P) ↦
              C((↑(x1.toTop (P := P)) : Type u), (↑(x2.toTop (P := P)) : Type u))) (CC := fun (X : CompHausLike P) ↦
              (↑(X.toTop (P := P)) : Type u)) g.unop :
            (a : (↑(unop T).toTop : Type u)) → (↑(unop S).toTop : Type u))
          (preimage
            (⇑(comap (TopCat.Hom.hom g.unop.hom) f) :
              (a : (↑(unop T).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
            a)) :
      Fiber (Y := (↑((unop S).toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
        (⇑f : (a : (↑(unop S).toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1}))))
Tactic: apply congrArg