-- 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
g : G
h : g • a = b
refl :
  ∀ (h : g • g⁻¹ • b = 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
                              (g⁻¹ • b)) ⟶
                          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, g⁻¹ • b⟩.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
                              (g⁻¹ • b))) :
                        (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, g⁻¹ • b⟩.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
                          (g⁻¹ • b)) ⟶
                      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, g⁻¹ • b⟩.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
                          (g⁻¹ • b))) :
                    (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, g⁻¹ • b⟩.fst ⟶ ⟨PUnit.unit, b⟩.fst)) =
      P (a := Sigma.mk (β := fun (c : SingleObj G) ↦ Functor.obj (actionAsFunctor G X) c) PUnit.unit (g⁻¹ • b)) (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 (g⁻¹ • b)) ⟶
                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, g⁻¹ • b⟩.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 (g⁻¹ • b))) :
              (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)
          (↑(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)

Tactic:
cases inv_smul_eq_iff.mpr h.symm

Premises used: Iff.mpr, inv_smul_eq_iff, Eq.symm