-- Lean 4 proof step from Mathlib.CategoryTheory.Action (goal)
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
⊢ 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)
have 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)
Tactic: cases inv_smul_eq_iff.mpr h.symm
Cleared hypotheses: a, h