-- Module: Mathlib.CategoryTheory.Action
Goal:
M : Type u_1
inst : Monoid M
X : Type u
inst_1 : MulAction M X
x : X
G : Type u_2
inst_2 : Group G
inst_3 : MulAction G X
P : ⦃a b : ActionCategory G X⦄ → (a ⟶ b) → Sort u_3
hyp : (t : X) → (g : G) → P (homOfPair t g)
a b : X
f :
  Quiver.Hom.{u_2, u} (V := ActionCategory G X)
    (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit a)
    (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b)
rcases :
  ∀ (g : G) (h : g • a = b),
    P (a :=
        Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) ()
          (HSMul.hSMul (β := X)
            (↑(Subtype.mk (p :=
                    fun
                      (f :
                        Sigma.fst (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                            (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit a) ⟶
                          Sigma.fst (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                            (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit
                              b)) ↦
                    Eq (α :=
                      (fun (X : Type u) ↦ X)
                        (Functor.obj (actionAsFunctor G X)
                          (Sigma.fst (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                            (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit
                              b))))
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (actionAsFunctor G X) f) :
                            (a : (fun (X : Type u) ↦ X) ((actionAsFunctor G X).obj ⟨PUnit.unit, a⟩.fst)) →
                              (fun (X : Type u) ↦ X) ((actionAsFunctor G X).obj ⟨PUnit.unit, b⟩.fst))
                          (Sigma.snd (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                            (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit
                              a)) :
                        (fun (X : Type u) ↦ X)
                          (Functor.obj (actionAsFunctor G X)
                            (Sigma.fst (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                              (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit
                                b))))
                      (Sigma.snd (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                          (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b) :
                        Functor.obj (actionAsFunctor G X)
                          (Sigma.fst (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                            (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit
                              b))))
                    g h) :
                ⟨PUnit.unit, a⟩.fst ⟶ ⟨PUnit.unit, b⟩.fst)⁻¹
            (ActionCategory.back.{u, u_2} (M := G)
              (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b))))
        (homOfPair
          (ActionCategory.back.{u, u_2} (M := G)
            (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b))
          (↑(Subtype.mk (p :=
                fun
                  (f :
                    Sigma.fst (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                        (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit a) ⟶
                      Sigma.fst (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                        (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b)) ↦
                Eq (α :=
                  (fun (X : Type u) ↦ X)
                    (Functor.obj (actionAsFunctor G X)
                      (Sigma.fst (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                        (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b))))
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (actionAsFunctor G X) f) :
                        (a : (fun (X : Type u) ↦ X) ((actionAsFunctor G X).obj ⟨PUnit.unit, a⟩.fst)) →
                          (fun (X : Type u) ↦ X) ((actionAsFunctor G X).obj ⟨PUnit.unit, b⟩.fst))
                      (Sigma.snd (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                        (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit a)) :
                    (fun (X : Type u) ↦ X)
                      (Functor.obj (actionAsFunctor G X)
                        (Sigma.fst (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                          (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b))))
                  (Sigma.snd (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                      (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b) :
                    Functor.obj (actionAsFunctor G X)
                      (Sigma.fst (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                        (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b))))
                g h) :
            ⟨PUnit.unit, a⟩.fst ⟶ ⟨PUnit.unit, b⟩.fst)) =
      P (a := Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit a) (b :=
        Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b)
        (Subtype.mk (p :=
          fun
            (f :
              Sigma.fst (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                  (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit a) ⟶
                Sigma.fst (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                  (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b)) ↦
          Eq (α :=
            (fun (X : Type u) ↦ X)
              (Functor.obj (actionAsFunctor G X)
                (Sigma.fst (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                  (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b))))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (actionAsFunctor G X) f) :
                  (a : (fun (X : Type u) ↦ X) ((actionAsFunctor G X).obj ⟨PUnit.unit, a⟩.fst)) →
                    (fun (X : Type u) ↦ X) ((actionAsFunctor G X).obj ⟨PUnit.unit, b⟩.fst))
                (Sigma.snd (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                  (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit a)) :
              (fun (X : Type u) ↦ X)
                (Functor.obj (actionAsFunctor G X)
                  (Sigma.fst (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                    (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b))))
            (Sigma.snd (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b) :
              Functor.obj (actionAsFunctor G X)
                (Sigma.fst (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c)
                  (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b))))
          g h)
⊢ P (a :=
      Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) ()
        (HSMul.hSMul (β := X) (↑f : ⟨PUnit.unit, a⟩.fst ⟶ ⟨PUnit.unit, b⟩.fst)⁻¹
          (ActionCategory.back.{u, u_2} (M := G)
            (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b))))
      (homOfPair
        (ActionCategory.back.{u, u_2} (M := G)
          (Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit b))
        (↑f : ⟨PUnit.unit, a⟩.fst ⟶ ⟨PUnit.unit, b⟩.fst)) =
    P f

Tactic:
rcases f with ⟨g : G, h : g • a = b⟩