[GOAL]
T : Type u
inst✝ : Category.{v, u} T
f : Arrow T
⊢ mk f.hom = f
[PROOFSTEP]
cases f
[GOAL]
case mk
T : Type u
inst✝ : Category.{v, u} T
left✝ right✝ : T
hom✝ : (𝟭 T).obj left✝ ⟶ (𝟭 T).obj right✝
⊢ mk { left := left✝, right := right✝, hom := hom✝ }.hom = { left := left✝, right := right✝, hom := hom✝ }
[PROOFSTEP]
rfl
[GOAL]
T : Type u
inst✝ : Category.{v, u} T
A B : T
f g : A ⟶ B
h : mk f = mk g
⊢ f = g
[PROOFSTEP]
cases h
[GOAL]
case refl
T : Type u
inst✝ : Category.{v, u} T
A B : T
f : A ⟶ B
⊢ f = f
[PROOFSTEP]
rfl
[GOAL]
T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
⊢ ∃ inv, ff ≫ inv = 𝟙 f ∧ inv ≫ ff = 𝟙 g
[PROOFSTEP]
let inverse : g ⟶ f := ⟨inv ff.left, inv ff.right, (by simp)⟩
[GOAL]
T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
⊢ (𝟭 T).map (inv ff.left) ≫ f.hom = g.hom ≫ (𝟭 T).map (inv ff.right)
[PROOFSTEP]
simp
[GOAL]
T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
inverse : g ⟶ f := CommaMorphism.mk (inv ff.left) (inv ff.right)
⊢ ∃ inv, ff ≫ inv = 𝟙 f ∧ inv ≫ ff = 𝟙 g
[PROOFSTEP]
apply Exists.intro inverse
[GOAL]
T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
inverse : g ⟶ f := CommaMorphism.mk (inv ff.left) (inv ff.right)
⊢ ff ≫ inverse = 𝟙 f ∧ inverse ≫ ff = 𝟙 g
[PROOFSTEP]
aesop_cat
[GOAL]
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
φ₁ φ₂ : f ⟶ g
h : φ₁ = φ₂
⊢ φ₁.left = φ₂.left
[PROOFSTEP]
rw [h]
[GOAL]
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
φ₁ φ₂ : f ⟶ g
h : φ₁ = φ₂
⊢ φ₁.right = φ₂.right
[PROOFSTEP]
rw [h]
[GOAL]
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ g.hom = e.inv.left ≫ f.hom ≫ e.hom.right
[PROOFSTEP]
have eq := Arrow.hom.congr_right e.inv_hom_id
[GOAL]
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
eq : (e.inv ≫ e.hom).right = (𝟙 g).right
⊢ g.hom = e.inv.left ≫ f.hom ≫ e.hom.right
[PROOFSTEP]
rw [Arrow.comp_right, Arrow.id_right] at eq
[GOAL]
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
eq : e.inv.right ≫ e.hom.right = 𝟙 g.right
⊢ g.hom = e.inv.left ≫ f.hom ≫ e.hom.right
[PROOFSTEP]
erw [Arrow.w_assoc, eq, Category.comp_id]
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ ∃ inv, sq.left ≫ inv = 𝟙 f.left ∧ inv ≫ sq.left = 𝟙 g.left
[PROOFSTEP]
apply Exists.intro (inv sq).left
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ sq.left ≫ (inv sq).left = 𝟙 f.left ∧ (inv sq).left ≫ sq.left = 𝟙 g.left
[PROOFSTEP]
simp only [← Comma.comp_left, IsIso.hom_inv_id, IsIso.inv_hom_id, Arrow.id_left, eq_self_iff_true, and_self_iff]
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ (𝟙 f).left = 𝟙 f.left ∧ (𝟙 g).left = 𝟙 g.left
[PROOFSTEP]
simp
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ ∃ inv, sq.right ≫ inv = 𝟙 f.right ∧ inv ≫ sq.right = 𝟙 g.right
[PROOFSTEP]
apply Exists.intro (inv sq).right
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ sq.right ≫ (inv sq).right = 𝟙 f.right ∧ (inv sq).right ≫ sq.right = 𝟙 g.right
[PROOFSTEP]
simp only [← Comma.comp_right, IsIso.hom_inv_id, IsIso.inv_hom_id, Arrow.id_right, eq_self_iff_true, and_self_iff]
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ (𝟙 f).right = 𝟙 f.right ∧ (𝟙 g).right = 𝟙 g.right
[PROOFSTEP]
simp
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ sq.left ≫ (inv sq).left = 𝟙 f.left
[PROOFSTEP]
rw [← Comma.comp_left, IsIso.hom_inv_id, id_left]
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ sq.right ≫ (inv sq).right = 𝟙 f.right
[PROOFSTEP]
rw [← Comma.comp_right, IsIso.hom_inv_id, id_right]
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ sq.left ≫ g.hom ≫ inv sq.right = f.hom
[PROOFSTEP]
simp only [← Category.assoc, IsIso.comp_inv_eq, w]
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : IsIso sq
⊢ inv sq.left ≫ f.hom ≫ sq.right = g.hom
[PROOFSTEP]
simp only [w, IsIso.inv_comp_eq]
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
⊢ φ = ψ
[PROOFSTEP]
let aux : (Z ⟶ f.left) → (Arrow.mk (𝟙 Z) ⟶ f) := fun φ =>
  { left := φ
    right := φ ≫ f.hom }
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
⊢ φ = ψ
[PROOFSTEP]
have : ∀ g, (aux g).right = g ≫ f.hom := fun g => by dsimp
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g✝ : Arrow T
sq : f ⟶ g✝
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
g : Z ⟶ f.left
⊢ (aux g).right = g ≫ f.hom
[PROOFSTEP]
dsimp
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
this : ∀ (g : Z ⟶ f.left), (aux g).right = g ≫ f.hom
⊢ φ = ψ
[PROOFSTEP]
show (aux φ).left = (aux ψ).left
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
this : ∀ (g : Z ⟶ f.left), (aux g).right = g ≫ f.hom
⊢ (aux φ).left = (aux ψ).left
[PROOFSTEP]
congr 1
[GOAL]
case e_self
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
this : ∀ (g : Z ⟶ f.left), (aux g).right = g ≫ f.hom
⊢ aux φ = aux ψ
[PROOFSTEP]
rw [← cancel_mono sq]
[GOAL]
case e_self
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
this : ∀ (g : Z ⟶ f.left), (aux g).right = g ≫ f.hom
⊢ aux φ ≫ sq = aux ψ ≫ sq
[PROOFSTEP]
apply CommaMorphism.ext
[GOAL]
case e_self.left
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
this : ∀ (g : Z ⟶ f.left), (aux g).right = g ≫ f.hom
⊢ (aux φ ≫ sq).left = (aux ψ ≫ sq).left
[PROOFSTEP]
exact h
[GOAL]
case e_self.right
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
this : ∀ (g : Z ⟶ f.left), (aux g).right = g ≫ f.hom
⊢ (aux φ ≫ sq).right = (aux ψ ≫ sq).right
[PROOFSTEP]
rw [Comma.comp_right, Comma.comp_right, this, this, Category.assoc, Category.assoc]
[GOAL]
case e_self.right
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
this : ∀ (g : Z ⟶ f.left), (aux g).right = g ≫ f.hom
⊢ φ ≫ f.hom ≫ sq.right = ψ ≫ f.hom ≫ sq.right
[PROOFSTEP]
rw [← Arrow.w]
[GOAL]
case e_self.right
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ sq.left = ψ ≫ sq.left
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := fun φ => CommaMorphism.mk φ (φ ≫ f.hom)
this : ∀ (g : Z ⟶ f.left), (aux g).right = g ≫ f.hom
⊢ φ ≫ sq.left ≫ g.hom = ψ ≫ sq.left ≫ g.hom
[PROOFSTEP]
simp only [← Category.assoc, h]
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : sq.right ≫ φ = sq.right ≫ ψ
⊢ φ = ψ
[PROOFSTEP]
let aux : (g.right ⟶ Z) → (g ⟶ Arrow.mk (𝟙 Z)) := fun φ =>
  { right := φ
    left := g.hom ≫ φ }
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : sq.right ≫ φ = sq.right ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun φ => CommaMorphism.mk (g.hom ≫ φ) φ
⊢ φ = ψ
[PROOFSTEP]
show (aux φ).right = (aux ψ).right
[GOAL]
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : sq.right ≫ φ = sq.right ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun φ => CommaMorphism.mk (g.hom ≫ φ) φ
⊢ (aux φ).right = (aux ψ).right
[PROOFSTEP]
congr 1
[GOAL]
case e_self
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : sq.right ≫ φ = sq.right ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun φ => CommaMorphism.mk (g.hom ≫ φ) φ
⊢ aux φ = aux ψ
[PROOFSTEP]
rw [← cancel_epi sq]
[GOAL]
case e_self
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : sq.right ≫ φ = sq.right ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun φ => CommaMorphism.mk (g.hom ≫ φ) φ
⊢ sq ≫ aux φ = sq ≫ aux ψ
[PROOFSTEP]
apply CommaMorphism.ext
[GOAL]
case e_self.left
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : sq.right ≫ φ = sq.right ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun φ => CommaMorphism.mk (g.hom ≫ φ) φ
⊢ (sq ≫ aux φ).left = (sq ≫ aux ψ).left
[PROOFSTEP]
rw [Comma.comp_left, Comma.comp_left, Arrow.w_assoc, Arrow.w_assoc, h]
[GOAL]
case e_self.right
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Epi sq
Z : T
φ ψ : g.right ⟶ Z
h : sq.right ≫ φ = sq.right ≫ ψ
aux : (g.right ⟶ Z) → (g ⟶ mk (𝟙 Z)) := fun φ => CommaMorphism.mk (g.hom ≫ φ) φ
⊢ (sq ≫ aux φ).right = (sq ≫ aux ψ).right
[PROOFSTEP]
exact h
[GOAL]
T : Type u
inst✝ : Category.{v, u} T
i : Arrow T
X Y : T
p : X ≅ Y
sq : i ⟶ mk p.hom
⊢ i.hom ≫ sq.right ≫ p.inv = sq.left
[PROOFSTEP]
simpa only [Category.assoc] using (Iso.comp_inv_eq p).mpr (Arrow.w_mk_right sq).symm
[GOAL]
T : Type u
inst✝ : Category.{v, u} T
X Y : T
i : X ≅ Y
p : Arrow T
sq : mk i.hom ⟶ p
⊢ i.inv ≫ sq.left ≫ p.hom = sq.right
[PROOFSTEP]
simp only [Iso.inv_hom_id_assoc, Arrow.w, Arrow.mk_hom]
[GOAL]
T : Type u
inst✝² : Category.{v, u} T
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ : Arrow C
f : X✝ ⟶ Y✝
⊢ (𝟭 D).map (F.map f.left) ≫ ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) Y✝).hom =
    ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) X✝).hom ≫ (𝟭 D).map (F.map f.right)
[PROOFSTEP]
let w := f.w
[GOAL]
T : Type u
inst✝² : Category.{v, u} T
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ : Arrow C
f : X✝ ⟶ Y✝
w : (𝟭 C).map f.left ≫ Y✝.hom = X✝.hom ≫ (𝟭 C).map f.right := f.w
⊢ (𝟭 D).map (F.map f.left) ≫ ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) Y✝).hom =
    ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) X✝).hom ≫ (𝟭 D).map (F.map f.right)
[PROOFSTEP]
simp only [id_map] at w
[GOAL]
T : Type u
inst✝² : Category.{v, u} T
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ : Arrow C
f : X✝ ⟶ Y✝
w : f.left ≫ Y✝.hom = X✝.hom ≫ f.right := f.w
⊢ (𝟭 D).map (F.map f.left) ≫ ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) Y✝).hom =
    ((fun a => { left := F.obj a.left, right := F.obj a.right, hom := F.map a.hom }) X✝).hom ≫ (𝟭 D).map (F.map f.right)
[PROOFSTEP]
dsimp
[GOAL]
T : Type u
inst✝² : Category.{v, u} T
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ : Arrow C
f : X✝ ⟶ Y✝
w : f.left ≫ Y✝.hom = X✝.hom ≫ f.right := f.w
⊢ F.map f.left ≫ F.map Y✝.hom = F.map X✝.hom ≫ F.map f.right
[PROOFSTEP]
simp only [← F.map_comp, w]


[GOAL]
C : Type u
inst✝ : Groupoid C
X Y : C
f : X ⟶ Y
⊢ inv (inv f) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Groupoid C
X Y : C
f : Y ⟶ X
⊢ inv (inv f) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Groupoid C
X Y a✝ b✝ : C
f : a✝ ⟶ b✝
⊢ Quiver.reverse (Quiver.reverse f) = f
[PROOFSTEP]
dsimp [Quiver.reverse]
[GOAL]
C : Type u
inst✝ : Groupoid C
X Y a✝ b✝ : C
f : a✝ ⟶ b✝
⊢ Groupoid.inv (Groupoid.inv f) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Groupoid C
X Y : C
D : Type u_1
inst✝ : Groupoid D
F : C ⥤ D
u✝ v✝ : C
f : u✝ ⟶ v✝
⊢ F.map (Quiver.reverse f) = Quiver.reverse (F.map f)
[PROOFSTEP]
simp only [Quiver.reverse, Quiver.HasReverse.reverse', Groupoid.inv_eq_inv, Functor.map_inv]
[GOAL]
C : Type u
inst✝ : Groupoid C
X Y : C
f : X ⟶ Y
⊢ f ≫ inv f = 𝟙 X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Groupoid C
X Y : C
f : X ⟶ Y
⊢ inv f ≫ f = 𝟙 Y
[PROOFSTEP]
aesop_cat
[GOAL]
I : Type u
J : I → Type u₂
inst✝ : (i : I) → Groupoid (J i)
X✝ Y✝ : (i : I) → J i
f : X✝ ⟶ Y✝
⊢ (fun {X Y} f i => Groupoid.inv (f i)) f ≫ f = 𝟙 Y✝
[PROOFSTEP]
funext i
[GOAL]
case h
I : Type u
J : I → Type u₂
inst✝ : (i : I) → Groupoid (J i)
X✝ Y✝ : (i : I) → J i
f : X✝ ⟶ Y✝
i : I
⊢ ((fun {X Y} f i => Groupoid.inv (f i)) f ≫ f) i = 𝟙 Y✝ i
[PROOFSTEP]
apply Groupoid.inv_comp
[GOAL]
I : Type u
J : I → Type u₂
inst✝ : (i : I) → Groupoid (J i)
X✝ Y✝ : (i : I) → J i
f : X✝ ⟶ Y✝
⊢ f ≫ (fun {X Y} f i => Groupoid.inv (f i)) f = 𝟙 X✝
[PROOFSTEP]
funext i
[GOAL]
case h
I : Type u
J : I → Type u₂
inst✝ : (i : I) → Groupoid (J i)
X✝ Y✝ : (i : I) → J i
f : X✝ ⟶ Y✝
i : I
⊢ (f ≫ (fun {X Y} f i => Groupoid.inv (f i)) f) i = 𝟙 X✝ i
[PROOFSTEP]
apply Groupoid.comp_inv


[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α β : F.NatTrans G
h : α = β
X : C
⊢ NatTrans.app α X = NatTrans.app β X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F.NatTrans G
X Y U V : C
f : X ⟶ Y
g : Y ⟶ U
h : U ⟶ V
⊢ app α X ≫ G.map f ≫ G.map g ≫ G.map h = F.map f ≫ F.map g ≫ F.map h ≫ app α V
[PROOFSTEP]
simp


[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