[GOAL]
M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
⊢ Category.{?u.1482, u} (ActionCategory M X)
[PROOFSTEP]
dsimp only [ActionCategory]
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
⊢ Category.{?u.1482, u} (Functor.Elements (actionAsFunctor M X))
[PROOFSTEP]
infer_instance
[GOAL]
M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
x : ActionCategory M X
⊢ { fst := (), snd := ActionCategory.back x } = x
[PROOFSTEP]
cases x
[GOAL]
case mk
M : Type u_1
inst✝¹ : Monoid M
X : Type u
inst✝ : MulAction M X
fst✝ : SingleObj M
snd✝ : (actionAsFunctor M X).obj fst✝
⊢ { fst := (), snd := ActionCategory.back { fst := fst✝, snd := snd✝ } } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : 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 : ActionCategory G X
f : a ⟶ b
⊢ P f
[PROOFSTEP]
refine' cast _ (hyp b.back f.val)
[GOAL]
M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : 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 : ActionCategory G X
f : a ⟶ b
⊢ P (homOfPair (ActionCategory.back b) ↑f) = P f
[PROOFSTEP]
rcases a with ⟨⟨⟩, a : X⟩
[GOAL]
case mk.unit
M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
P : ⦃a b : ActionCategory G X⦄ → (a ⟶ b) → Sort u_3
hyp : (t : X) → (g : G) → P (homOfPair t g)
b : ActionCategory G X
a : X
f : { fst := PUnit.unit, snd := a } ⟶ b
⊢ P (homOfPair (ActionCategory.back b) ↑f) = P f
[PROOFSTEP]
rcases b with ⟨⟨⟩, b : X⟩
[GOAL]
case mk.unit.mk.unit
M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : 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 : { fst := PUnit.unit, snd := a } ⟶ { fst := PUnit.unit, snd := b }
⊢ P (homOfPair (ActionCategory.back { fst := PUnit.unit, snd := b }) ↑f) = P f
[PROOFSTEP]
rcases f with ⟨g : G, h : g • a = b⟩
[GOAL]
case mk.unit.mk.unit.mk
M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : 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 (homOfPair (ActionCategory.back { fst := PUnit.unit, snd := b }) ↑{ val := g, property := h }) =
    P { val := g, property := h }
[PROOFSTEP]
cases inv_smul_eq_iff.mpr h.symm
[GOAL]
case mk.unit.mk.unit.mk.refl
M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
P : ⦃a b : ActionCategory G X⦄ → (a ⟶ b) → Sort u_3
hyp : (t : X) → (g : G) → P (homOfPair t g)
b : X
g : G
h : g • g⁻¹ • b = b
⊢ P (homOfPair (ActionCategory.back { fst := PUnit.unit, snd := b }) ↑{ val := g, property := h }) =
    P { val := g, property := h }
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a' b' : ActionCategory G X
f : a' ⟶ b'
a b : X
g : G
ha : a' = { fst := (), snd := a }
hb : b' = { fst := (), snd := b }
hg : a = g⁻¹ • b
⊢ a' = { fst := (), snd := g⁻¹ • b }
[PROOFSTEP]
rw [ha, hg]
[GOAL]
M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a' b' : ActionCategory G X
f : a' ⟶ b'
a b : X
g : G
ha : a' = { fst := (), snd := a }
hb : b' = { fst := (), snd := b }
hg : a = g⁻¹ • b
⊢ { fst := (), snd := b } = b'
[PROOFSTEP]
rw [hb]
[GOAL]
M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a' b' : ActionCategory G X
f : a' ⟶ b'
⊢ ∃ a b g ha hb hg,
    f = eqToHom (_ : a' = { fst := (), snd := g⁻¹ • b }) ≫ homOfPair b g ≫ eqToHom (_ : { fst := (), snd := b } = b')
[PROOFSTEP]
revert a' b' f
[GOAL]
M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
⊢ ∀ ⦃a' b' : ActionCategory G X⦄ (f : a' ⟶ b'),
    ∃ a b g ha hb hg,
      f = eqToHom (_ : a' = { fst := (), snd := g⁻¹ • b }) ≫ homOfPair b g ≫ eqToHom (_ : { fst := (), snd := b } = b')
[PROOFSTEP]
exact ActionCategory.cases (fun t g => ⟨g⁻¹ • t, t, g, rfl, rfl, rfl, by simp⟩)
[GOAL]
M : Type u_1
inst✝³ : Monoid M
X : Type u
inst✝² : MulAction M X
x : X
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
t : X
g : G
⊢ homOfPair t g =
    eqToHom (_ : { fst := (), snd := g⁻¹ • t } = { fst := (), snd := g⁻¹ • t }) ≫
      homOfPair t g ≫ eqToHom (_ : { fst := (), snd := t } = { fst := (), snd := t })
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
⊢ ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair (ActionCategory.back b) ↑f)
[PROOFSTEP]
apply ActionCategory.cases
[GOAL]
case hyp
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
⊢ ∀ (t : X) (g : G),
    F.map (homOfPair t g) = F.map (homOfPair (ActionCategory.back { fst := (), snd := t }) ↑(homOfPair t g))
[PROOFSTEP]
intros
[GOAL]
case hyp
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
t✝ : X
g✝ : G
⊢ F.map (homOfPair t✝ g✝) = F.map (homOfPair (ActionCategory.back { fst := (), snd := t✝ }) ↑(homOfPair t✝ g✝))
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair (ActionCategory.back b) ↑f)
⊢ (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1
[PROOFSTEP]
congr
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair (ActionCategory.back b) ↑f)
⊢ (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1
[PROOFSTEP]
dsimp
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair (ActionCategory.back b) ↑f)
⊢ { left := fun b => F.map (homOfPair b 1), right := 1 } = 1
[PROOFSTEP]
ext1
[GOAL]
case left
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair (ActionCategory.back b) ↑f)
⊢ { left := fun b => F.map (homOfPair b 1), right := 1 }.left = 1.left
case right
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair (ActionCategory.back b) ↑f)
⊢ { left := fun b => F.map (homOfPair b 1), right := 1 }.right = 1.right
[PROOFSTEP]
ext b
[GOAL]
case left.h
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair (ActionCategory.back b) ↑f)
b : X
⊢ left { left := fun b => F.map (homOfPair b 1), right := 1 } b = left 1 b
case right
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair (ActionCategory.back b) ↑f)
⊢ { left := fun b => F.map (homOfPair b 1), right := 1 }.right = 1.right
[PROOFSTEP]
exact F_map_eq.symm.trans (F.map_id b)
[GOAL]
case right
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair (ActionCategory.back b) ↑f)
⊢ { left := fun b => F.map (homOfPair b 1), right := 1 }.right = 1.right
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair (ActionCategory.back b) ↑f)
⊢ ∀ (x y : G),
    OneHom.toFun
        { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
          map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
        (x * y) =
      OneHom.toFun
          { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
            map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
          x *
        OneHom.toFun
          { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
            map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
          y
[PROOFSTEP]
intro g h
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair (ActionCategory.back b) ↑f)
g h : G
⊢ OneHom.toFun
      { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
        map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
      (g * h) =
    OneHom.toFun
        { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
          map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
        g *
      OneHom.toFun
        { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
          map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
        h
[PROOFSTEP]
congr
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair (ActionCategory.back b) ↑f)
g h : G
⊢ OneHom.toFun
      { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
        map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
      (g * h) =
    OneHom.toFun
        { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
          map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
        g *
      OneHom.toFun
        { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
          map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
        h
[PROOFSTEP]
ext b
[GOAL]
case left.h
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair (ActionCategory.back b) ↑f)
g h : G
b : X
⊢ left
      (OneHom.toFun
        { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
          map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
        (g * h))
      b =
    left
      (OneHom.toFun
          { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
            map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
          g *
        OneHom.toFun
          { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
            map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
          h)
      b
case right
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair (ActionCategory.back b) ↑f)
g h : G
⊢ (OneHom.toFun
        { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
          map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
        (g * h)).right =
    (OneHom.toFun
          { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
            map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
          g *
        OneHom.toFun
          { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
            map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
          h).right
[PROOFSTEP]
exact F_map_eq.symm.trans (F.map_comp (homOfPair (g⁻¹ • b) h) (homOfPair b g))
[GOAL]
case right
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair (ActionCategory.back b) ↑f)
g h : G
⊢ (OneHom.toFun
        { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
          map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
        (g * h)).right =
    (OneHom.toFun
          { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
            map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
          g *
        OneHom.toFun
          { toFun := fun g => { left := fun b => F.map (homOfPair b g), right := g },
            map_one' := (_ : (fun g => { left := fun b => F.map (homOfPair b g), right := g }) 1 = 1) }
          h).right
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x✝ : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : G →* (X → H) ⋊[mulAutArrow] G
sane : ∀ (g : G), (↑F g).right = g
x : ActionCategory G X
⊢ { obj := fun x => (), map := fun {x b} f => left (↑F ↑f) (ActionCategory.back b) }.map (𝟙 x) =
    𝟙 ({ obj := fun x => (), map := fun {x b} f => left (↑F ↑f) (ActionCategory.back b) }.obj x)
[PROOFSTEP]
dsimp
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x✝ : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : G →* (X → H) ⋊[mulAutArrow] G
sane : ∀ (g : G), (↑F g).right = g
x : ActionCategory G X
⊢ left (↑F 1) (ActionCategory.back x) = 𝟙 ()
[PROOFSTEP]
rw [F.map_one]
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x✝ : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : G →* (X → H) ⋊[mulAutArrow] G
sane : ∀ (g : G), (↑F g).right = g
x : ActionCategory G X
⊢ left 1 (ActionCategory.back x) = 𝟙 ()
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : G →* (X → H) ⋊[mulAutArrow] G
sane : ∀ (g : G), (↑F g).right = g
X✝ Y✝ Z✝ : ActionCategory G X
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun x => (), map := fun {x b} f => left (↑F ↑f) (ActionCategory.back b) }.map (f ≫ g) =
    { obj := fun x => (), map := fun {x b} f => left (↑F ↑f) (ActionCategory.back b) }.map f ≫
      { obj := fun x => (), map := fun {x b} f => left (↑F ↑f) (ActionCategory.back b) }.map g
[PROOFSTEP]
obtain ⟨_, z, γ₁, rfl, rfl, rfl, rfl⟩ := ActionCategory.cases' g
[GOAL]
case intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : G →* (X → H) ⋊[mulAutArrow] G
sane : ∀ (g : G), (↑F g).right = g
X✝ : ActionCategory G X
z : X
γ₁ : G
f : X✝ ⟶ { fst := (), snd := γ₁⁻¹ • z }
⊢ { obj := fun x => (), map := fun {x b} f => left (↑F ↑f) (ActionCategory.back b) }.map
      (f ≫
        eqToHom (_ : { fst := (), snd := γ₁⁻¹ • z } = { fst := (), snd := γ₁⁻¹ • z }) ≫
          homOfPair z γ₁ ≫ eqToHom (_ : { fst := (), snd := z } = { fst := (), snd := z })) =
    { obj := fun x => (), map := fun {x b} f => left (↑F ↑f) (ActionCategory.back b) }.map f ≫
      { obj := fun x => (), map := fun {x b} f => left (↑F ↑f) (ActionCategory.back b) }.map
        (eqToHom (_ : { fst := (), snd := γ₁⁻¹ • z } = { fst := (), snd := γ₁⁻¹ • z }) ≫
          homOfPair z γ₁ ≫ eqToHom (_ : { fst := (), snd := z } = { fst := (), snd := z }))
[PROOFSTEP]
obtain ⟨_, y, γ₂, rfl, hy, rfl, rfl⟩ := ActionCategory.cases' f
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : G →* (X → H) ⋊[mulAutArrow] G
sane : ∀ (g : G), (↑F g).right = g
z : X
γ₁ : G
y : X
γ₂ : G
hy : { fst := (), snd := γ₁⁻¹ • z } = { fst := (), snd := y }
⊢ { obj := fun x => (), map := fun {x b} f => left (↑F ↑f) (ActionCategory.back b) }.map
      ((eqToHom (_ : { fst := (), snd := γ₂⁻¹ • y } = { fst := (), snd := γ₂⁻¹ • y }) ≫
          homOfPair y γ₂ ≫ eqToHom (_ : { fst := (), snd := y } = { fst := (), snd := γ₁⁻¹ • z })) ≫
        eqToHom (_ : { fst := (), snd := γ₁⁻¹ • z } = { fst := (), snd := γ₁⁻¹ • z }) ≫
          homOfPair z γ₁ ≫ eqToHom (_ : { fst := (), snd := z } = { fst := (), snd := z })) =
    { obj := fun x => (), map := fun {x b} f => left (↑F ↑f) (ActionCategory.back b) }.map
        (eqToHom (_ : { fst := (), snd := γ₂⁻¹ • y } = { fst := (), snd := γ₂⁻¹ • y }) ≫
          homOfPair y γ₂ ≫ eqToHom (_ : { fst := (), snd := y } = { fst := (), snd := γ₁⁻¹ • z })) ≫
      { obj := fun x => (), map := fun {x b} f => left (↑F ↑f) (ActionCategory.back b) }.map
        (eqToHom (_ : { fst := (), snd := γ₁⁻¹ • z } = { fst := (), snd := γ₁⁻¹ • z }) ≫
          homOfPair z γ₁ ≫ eqToHom (_ : { fst := (), snd := z } = { fst := (), snd := z }))
[PROOFSTEP]
obtain rfl : y = γ₁⁻¹ • z := congr_arg Sigma.snd hy.symm
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : G →* (X → H) ⋊[mulAutArrow] G
sane : ∀ (g : G), (↑F g).right = g
z : X
γ₁ γ₂ : G
hy : { fst := (), snd := γ₁⁻¹ • z } = { fst := (), snd := γ₁⁻¹ • z }
⊢ { obj := fun x => (), map := fun {x b} f => left (↑F ↑f) (ActionCategory.back b) }.map
      ((eqToHom (_ : { fst := (), snd := γ₂⁻¹ • γ₁⁻¹ • z } = { fst := (), snd := γ₂⁻¹ • γ₁⁻¹ • z }) ≫
          homOfPair (γ₁⁻¹ • z) γ₂ ≫ eqToHom (_ : { fst := (), snd := γ₁⁻¹ • z } = { fst := (), snd := γ₁⁻¹ • z })) ≫
        eqToHom (_ : { fst := (), snd := γ₁⁻¹ • z } = { fst := (), snd := γ₁⁻¹ • z }) ≫
          homOfPair z γ₁ ≫ eqToHom (_ : { fst := (), snd := z } = { fst := (), snd := z })) =
    { obj := fun x => (), map := fun {x b} f => left (↑F ↑f) (ActionCategory.back b) }.map
        (eqToHom (_ : { fst := (), snd := γ₂⁻¹ • γ₁⁻¹ • z } = { fst := (), snd := γ₂⁻¹ • γ₁⁻¹ • z }) ≫
          homOfPair (γ₁⁻¹ • z) γ₂ ≫ eqToHom (_ : { fst := (), snd := γ₁⁻¹ • z } = { fst := (), snd := γ₁⁻¹ • z })) ≫
      { obj := fun x => (), map := fun {x b} f => left (↑F ↑f) (ActionCategory.back b) }.map
        (eqToHom (_ : { fst := (), snd := γ₁⁻¹ • z } = { fst := (), snd := γ₁⁻¹ • z }) ≫
          homOfPair z γ₁ ≫ eqToHom (_ : { fst := (), snd := z } = { fst := (), snd := z }))
[PROOFSTEP]
simp [sane]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : G →* (X → H) ⋊[mulAutArrow] G
sane : ∀ (g : G), (↑F g).right = g
z : X
γ₁ γ₂ : G
hy : { fst := (), snd := γ₁⁻¹ • z } = { fst := (), snd := γ₁⁻¹ • z }
⊢ left (↑F γ₁) z * (γ₁ • (↑F γ₂).left) z = left (↑F γ₂) (γ₁⁻¹ • z) ≫ left (↑F γ₁) z
[PROOFSTEP]
rfl
