-- Module: Mathlib.Condensed.Discrete.LocallyConstant
Goal:
P : TopCat.{u} → Prop
inst : ∀ (S : CompHausLike P) (p : (↑(S.toTop (P := P)) : Type u) → Prop), HasProp P (Subtype p)
S : CompHausLike P
Y : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_1 : HasProp P PUnit.{u + 1}
f : LocallyConstant (↑(S.toTop (P := P)) : Type u) (Y.obj (op (of P PUnit.{u + 1})))
X : (CompHausLike P)ᵒᵖ ⥤ Type (max u w)
inst_2 : PreservesFiniteProducts X
x y : X.obj (op S)
inst_3 : HasExplicitFiniteCoproducts P
a :
  Fiber (Y := (↑(S.toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
    (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))
h :
  Eq (α := (fun (X : Type (max u w)) ↦ X) (X.obj (op (fiber.{u, w} (P := P) f a))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (sigmaIncl (P := P) f a))) :
          (a_1 : (fun (X : Type (max u w)) ↦ X) (X.obj (op S))) →
            (fun (X : Type (max u w)) ↦ X) (X.obj (op (fiber f a))))
        x :
      (fun (X : Type (max u w)) ↦ X) (X.obj (op (fiber.{u, w} (P := P) f a))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (sigmaIncl (P := P) f a))) :
          (a_1 : (fun (X : Type (max u w)) ↦ X) (X.obj (op S))) →
            (fun (X : Type (max u w)) ↦ X) (X.obj (op (fiber f a))))
        y :
      (fun (X : Type (max u w)) ↦ X) (X.obj (op (fiber.{u, w} (P := P) f a))))
⊢ Eq (α := (fun (X : Type (max u w)) ↦ X) (X.obj (op (fiber.{u, w} (P := P) f a))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := X.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) f))))
              (Iso.hom (X.mapIso (Iso.op (sigmaIso (P := P) f))) :
                X.obj (op S) ⟶ X.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) f))))
              (CategoryStruct.comp (Y :=
                  (a :
                      Fiber (Y := (↑(S.toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
                        (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))) →
                    X.obj (op (of P (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u))))
                  (sigmaComparison.{u, w} (P := P) X
                    fun
                      (a :
                        Fiber (Y := (↑(S.toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
                          (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))) ↦
                    (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u))
                  (↾fun
                      (g :
                        (a :
                            Fiber (Y := (↑(S.toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
                              (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))) →
                          X.obj (op (of P (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u)))) ↦
                    g a) :
                X.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) f))) ⟶
                  X.obj (op (of P (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u))))) :
          (a_1 : (fun (X : Type (max u w)) ↦ X) (X.obj (op S))) →
            (fun (X : Type (max u w)) ↦ X) (X.obj (op (fiber f a))))
        x :
      (fun (X : Type (max u w)) ↦ X) (X.obj (op (fiber.{u, w} (P := P) f a))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := X.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) f))))
              (Iso.hom (X.mapIso (Iso.op (sigmaIso (P := P) f))) :
                X.obj (op S) ⟶ X.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) f))))
              (CategoryStruct.comp (Y :=
                  (a :
                      Fiber (Y := (↑(S.toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
                        (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))) →
                    X.obj (op (of P (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u))))
                  (sigmaComparison.{u, w} (P := P) X
                    fun
                      (a :
                        Fiber (Y := (↑(S.toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
                          (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))) ↦
                    (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u))
                  (↾fun
                      (g :
                        (a :
                            Fiber (Y := (↑(S.toTop (P := P)) : Type u)) (Z := Y.obj (op (of P PUnit.{u + 1})))
                              (⇑f : (a : (↑S.toTop : Type u)) → Y.obj (op (of P PUnit.{u + 1})))) →
                          X.obj (op (of P (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u)))) ↦
                    g a) :
                X.obj (op (finiteCoproduct (P := P) (fiber.{u, w} (P := P) f))) ⟶
                  X.obj (op (of P (↑((fiber.{u, w} (P := P) f a).toTop (P := P)) : Type u))))) :
          (a_1 : (fun (X : Type (max u w)) ↦ X) (X.obj (op S))) →
            (fun (X : Type (max u w)) ↦ X) (X.obj (op (fiber f a))))
        y :
      (fun (X : Type (max u w)) ↦ X) (X.obj (op (fiber.{u, w} (P := P) f a))))

Tactic:
rw [← sigmaComparison_comp_sigmaIso] at h

Premises used: CompHausLike.LocallyConstant.sigmaComparison_comp_sigmaIso