awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst_2 : (X Y : V) → FunLike.{u_3 + 1, u_4 + 1, u_4 + 1} (FV X Y) (CV X) (CV Y)
inst_3 : ConcreteCategory.{u_4, v_1, u_1, u_3} V FV (CC := CV)
X Y : Action.{v_1, u_1, u_2} V G
x : HomSubtype V G (FV := FV) (CV := CV) X Y
a :
  (↑(Subtype.mk (p := fun (f : FV X.V Y.V) ↦
          ∀ (g : G),
            Eq.{u_4 + 1} (α := CV X.V → CV Y.V)
              (Function.comp (β := CV X.V) (⇑f : (a : CV X.V) → CV Y.V)
                (⇑(@ConcreteCategory.hom.{u_4, v_1, u_1, u_3} _ inst FV CV _ _ _ _ ((X.ρ : (a : G) → End X.V) g)) :
                  (a : CV X.V) → CV X.V))
              (Function.comp (β := CV Y.V)
                (⇑(@ConcreteCategory.hom.{u_4, v_1, u_1, u_3} _ inst FV CV _ _ _ _ ((Y.ρ : (a : G) → End Y.V) g)) :
                  (a : CV Y.V) → CV Y.V)
                (⇑f : (a : CV X.V) → CV Y.V)))
          (@ConcreteCategory.hom.{u_4, v_1, u_1, u_3} _ inst FV CV _ _ _ _
            (ConcreteCategory.ofHom (FC := FV) (CC := CV) (↑x : FV X.V Y.V)))
          ⋯) :
      FV X.V Y.V) =
    (↑x : FV X.V Y.V)
⊢ Subtype.mk (p := fun (f : FV X.V Y.V) ↦
      ∀ (g : G),
        Eq.{u_4 + 1} (α := CV X.V → CV Y.V)
          (Function.comp (β := CV X.V) (⇑f : (a : CV X.V) → CV Y.V)
            (⇑(@ConcreteCategory.hom.{u_4, v_1, u_1, u_3} _ inst FV CV _ _ _ _ ((X.ρ : (a : G) → End X.V) g)) :
              (a : CV X.V) → CV X.V))
          (Function.comp (β := CV Y.V)
            (⇑(@ConcreteCategory.hom.{u_4, v_1, u_1, u_3} _ inst FV CV _ _ _ _ ((Y.ρ : (a : G) → End Y.V) g)) :
              (a : CV Y.V) → CV Y.V)
            (⇑f : (a : CV X.V) → CV Y.V)))
      (@ConcreteCategory.hom.{u_4, v_1, u_1, u_3} _ inst FV CV _ _ _ _
        (ConcreteCategory.ofHom (FC := FV) (CC := CV) (↑x : FV X.V Y.V)))
      ⋯ =
    x

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst_2 : (X Y : V) → FunLike.{u_3 + 1, u_4 + 1, u_4 + 1} (FV X Y) (CV X) (CV Y)
inst_3 : ConcreteCategory.{u_4, v_1, u_1, u_3} V FV (CC := CV)
X Y : Action.{v_1, u_1, u_2} V G
x : HomSubtype V G (FV := FV) (CV := CV) X Y
⊢ (↑(Subtype.mk (p := fun (f : FV X.V Y.V) ↦
          ∀ (g : G),
            Eq.{u_4 + 1} (α := CV X.V → CV Y.V)
              (Function.comp (β := CV X.V) (⇑f : (a : CV X.V) → CV Y.V)
                (⇑(@ConcreteCategory.hom.{u_4, v_1, u_1, u_3} _ inst FV CV _ _ _ _ ((X.ρ : (a : G) → End X.V) g)) :
                  (a : CV X.V) → CV X.V))
              (Function.comp (β := CV Y.V)
                (⇑(@ConcreteCategory.hom.{u_4, v_1, u_1, u_3} _ inst FV CV _ _ _ _ ((Y.ρ : (a : G) → End Y.V) g)) :
                  (a : CV Y.V) → CV Y.V)
                (⇑f : (a : CV X.V) → CV Y.V)))
          (@ConcreteCategory.hom.{u_4, v_1, u_1, u_3} _ inst FV CV _ _ _ _
            (ConcreteCategory.ofHom (FC := FV) (CC := CV) (↑x : FV X.V Y.V)))
          ⋯) :
      FV X.V Y.V) =
    (↑x : FV X.V Y.V)

Tactic:
simp [ConcreteCategory.hom_ofHom]

Premises used: CategoryTheory.ConcreteCategory.hom_ofHom
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst_2 : (X Y : V) → FunLike.{u_3 + 1, u_4 + 1, u_4 + 1} (FV X Y) (CV X) (CV Y)
inst_3 : ConcreteCategory.{u_4, v_1, u_1, u_3} V FV (CC := CV)
X Y : Action.{v_1, u_1, u_2} V G
x : X ⟶ Y
h :
  ConcreteCategory.hom (FC := FV) (CC := CV)
      {
          hom :=
            ConcreteCategory.ofHom (FC := FV) (CC := CV)
              (↑(Subtype.mk (p := fun (f : FV X.V Y.V) ↦
                    ∀ (g : G),
                      Eq.{u_4 + 1} (α := CV X.V → CV Y.V)
                        (Function.comp (β := CV X.V) (⇑f : (a : CV X.V) → CV Y.V)
                          (⇑(@ConcreteCategory.hom.{u_4, v_1, u_1, u_3} _ inst FV CV _ _ _ _
                                ((X.ρ : (a : G) → End X.V) g)) :
                            (a : CV X.V) → CV X.V))
                        (Function.comp (β := CV Y.V)
                          (⇑(@ConcreteCategory.hom.{u_4, v_1, u_1, u_3} _ inst FV CV _ _ _ _
                                ((Y.ρ : (a : G) → End Y.V) g)) :
                            (a : CV Y.V) → CV Y.V)
                          (⇑f : (a : CV X.V) → CV Y.V)))
                    (ConcreteCategory.hom (FC := FV) (CC := CV) x.hom) ⋯) :
                FV X.V Y.V),
          comm := ⋯ : X.Hom Y }.hom =
    ConcreteCategory.hom (FC := FV) (CC := CV) x.hom
⊢ {
      hom :=
        ConcreteCategory.ofHom (FC := FV) (CC := CV)
          (↑(Subtype.mk (p := fun (f : FV X.V Y.V) ↦
                ∀ (g : G),
                  Eq.{u_4 + 1} (α := CV X.V → CV Y.V)
                    (Function.comp (β := CV X.V) (⇑f : (a : CV X.V) → CV Y.V)
                      (⇑(@ConcreteCategory.hom.{u_4, v_1, u_1, u_3} _ inst FV CV _ _ _ _
                            ((X.ρ : (a : G) → End X.V) g)) :
                        (a : CV X.V) → CV X.V))
                    (Function.comp (β := CV Y.V)
                      (⇑(@ConcreteCategory.hom.{u_4, v_1, u_1, u_3} _ inst FV CV _ _ _ _
                            ((Y.ρ : (a : G) → End Y.V) g)) :
                        (a : CV Y.V) → CV Y.V)
                      (⇑f : (a : CV X.V) → CV Y.V)))
                (ConcreteCategory.hom (FC := FV) (CC := CV) x.hom) ⋯) :
            FV X.V Y.V),
      comm := ⋯ : X.Hom Y } =
    x

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst_2 : (X Y : V) → FunLike.{u_3 + 1, u_4 + 1, u_4 + 1} (FV X Y) (CV X) (CV Y)
inst_3 : ConcreteCategory.{u_4, v_1, u_1, u_3} V FV (CC := CV)
X Y : Action.{v_1, u_1, u_2} V G
x : X ⟶ Y
⊢ ConcreteCategory.hom (FC := FV) (CC := CV)
      {
          hom :=
            ConcreteCategory.ofHom (FC := FV) (CC := CV)
              (↑(Subtype.mk (p := fun (f : FV X.V Y.V) ↦
                    ∀ (g : G),
                      Eq.{u_4 + 1} (α := CV X.V → CV Y.V)
                        (Function.comp (β := CV X.V) (⇑f : (a : CV X.V) → CV Y.V)
                          (⇑(@ConcreteCategory.hom.{u_4, v_1, u_1, u_3} _ inst FV CV _ _ _ _
                                ((X.ρ : (a : G) → End X.V) g)) :
                            (a : CV X.V) → CV X.V))
                        (Function.comp (β := CV Y.V)
                          (⇑(@ConcreteCategory.hom.{u_4, v_1, u_1, u_3} _ inst FV CV _ _ _ _
                                ((Y.ρ : (a : G) → End Y.V) g)) :
                            (a : CV Y.V) → CV Y.V)
                          (⇑f : (a : CV X.V) → CV Y.V)))
                    (ConcreteCategory.hom (FC := FV) (CC := CV) x.hom) ⋯) :
                FV X.V Y.V),
          comm := ⋯ : X.Hom Y }.hom =
    ConcreteCategory.hom (FC := FV) (CC := CV) x.hom

Tactic:
simp [ConcreteCategory.ofHom_hom]

Premises used: CategoryTheory.ConcreteCategory.ofHom_hom
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasLimits.{v_1, u_1} V
⊢ PreservesLimits (C := Action.{v_1, u_1, u_2} V G) (forget V G)

Tactic:
Limits.preservesLimits_of_natIso (Action.functorCategoryEquivalenceCompEvaluation V G)

Premises used: Action.functorCategoryEquivalenceCompEvaluation, CategoryTheory.Limits.preservesLimits_of_natIso
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasColimits.{v_1, u_1} V
⊢ PreservesColimits (C := Action.{v_1, u_1, u_2} V G) (forget V G)

Tactic:
preservesColimits_of_natIso (Action.functorCategoryEquivalenceCompEvaluation V G)

Premises used: Action.functorCategoryEquivalenceCompEvaluation, CategoryTheory.Limits.preservesColimits_of_natIso
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M ≅ N
g : G
rw :
  Eq (α := Functor.obj (forget V G) M ⟶ N.V) (Iso.hom (Functor.mapIso (forget V G) f) ≫ (N.ρ : (a : G) → End N.V) g)
    ((M.ρ : (a : G) → End M.V) g ≫ Iso.hom (Functor.mapIso (forget V G) f))
⊢ Eq.{v_1 + 1} (α := End N.V) ((N.ρ : (a : G) → End N.V) g : End N.V)
    ((Iso.conj (Functor.mapIso (forget V G) f) : (a : End ((forget V G).obj M)) → End ((forget V G).obj N))
        ((M.ρ : (a : G) → End M.V) g : End M.V) :
      End (Functor.obj (forget V G) N))

Tactic:
rw [Iso.conj_apply, Iso.eq_inv_comp]

Premises used: CategoryTheory.Iso.eq_inv_comp, CategoryTheory.Iso.conj_apply
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M ≅ N
g : G
⊢ Eq (α := Functor.obj (forget V G) M ⟶ N.V) (Iso.hom (Functor.mapIso (forget V G) f) ≫ (N.ρ : (a : G) → End N.V) g)
    ((M.ρ : (a : G) → End M.V) g ≫ Iso.hom (Functor.mapIso (forget V G) f))

Tactic:
simp [f.hom.comm]

Premises used: CategoryTheory.Iso.hom, Action.Hom.comm
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
X Y : V
f : X ⟶ Y
x : PUnit.{u_3 + 1}
⊢ Eq.{v_1 + 1} (α :=
    Action.V.{v_1, u_1, u_3} (G := PUnit.{u_3 + 1}) { V := X, ρ := 1 : Action.{v_1, u_1, u_3} V PUnit.{u_3 + 1} } ⟶
      Action.V.{v_1, u_1, u_3} (G := PUnit.{u_3 + 1}) { V := Y, ρ := 1 })
    ((ρ { V := X, ρ := 1 } : (a : PUnit.{u_3 + 1}) → End { V := X, ρ := 1 }.V) PUnit.unit ≫ f :
      Action.V.{v_1, u_1, u_3} (G := PUnit.{u_3 + 1}) { V := X, ρ := 1 : Action.{v_1, u_1, u_3} V PUnit.{u_3 + 1} } ⟶
        Action.V.{v_1, u_1, u_3} (G := PUnit.{u_3 + 1}) { V := Y, ρ := 1 })
    (f ≫ (ρ { V := Y, ρ := 1 } : (a : PUnit.{u_3 + 1}) → End { V := Y, ρ := 1 }.V) PUnit.unit :
      Action.V.{v_1, u_1, u_3} (G := PUnit.{u_3 + 1}) { V := X, ρ := 1 : Action.{v_1, u_1, u_3} V PUnit.{u_3 + 1} } ⟶
        Action.V.{v_1, u_1, u_3} (G := PUnit.{u_3 + 1}) { V := Y, ρ := 1 })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
X : Action.{v_1, u_1, u_3} V PUnit.{u_3 + 1}
x : PUnit.{u_3 + 1}
simp : Eq.{v_1 + 1} (α := X.V ⟶ X.V) ((X.ρ : (a : PUnit.{u_3 + 1}) → End X.V) PUnit.unit : End X.V) (𝟙 X.V : X.V ⟶ X.V)
⊢ Eq.{v_1 + 1} (α :=
    (Functor.obj (𝟭 (Action.{v_1, u_1, u_3} V PUnit.{u_3 + 1})) X).V ⟶
      Action.V.{v_1, u_1, u_3} (G := PUnit.{u_3 + 1})
        (Functor.obj
          (forget V PUnit.{u_3 + 1} ⋙
            { obj := fun (X : V) ↦ { V := X, ρ := 1 }, map := fun {X Y : V} (f : X ⟶ Y) ↦ { hom := f, comm := ⋯ },
              map_id := ⋯, map_comp := ⋯ })
          X))
    (((Functor.obj (𝟭 (Action.{v_1, u_1, u_3} V PUnit.{u_3 + 1})) X).ρ :
            (a : PUnit.{u_3 + 1}) → End ((𝟭 (Action V PUnit.{u_3 + 1})).obj X).V)
          PUnit.unit ≫
        Iso.hom (Iso.refl (Functor.obj (𝟭 (Action.{v_1, u_1, u_3} V PUnit.{u_3 + 1})) X).V) :
      (Functor.obj (𝟭 (Action.{v_1, u_1, u_3} V PUnit.{u_3 + 1})) X).V ⟶
        Action.V.{v_1, u_1, u_3} (G := PUnit.{u_3 + 1})
          (Functor.obj
            (forget V PUnit.{u_3 + 1} ⋙
              { obj := fun (X : V) ↦ { V := X, ρ := 1 }, map := fun {X Y : V} (f : X ⟶ Y) ↦ { hom := f, comm := ⋯ },
                map_id := ⋯, map_comp := ⋯ })
            X))
    (Iso.hom (Iso.refl (Functor.obj (𝟭 (Action.{v_1, u_1, u_3} V PUnit.{u_3 + 1})) X).V) ≫
        (ρ
              (Functor.obj
                (forget V PUnit.{u_3 + 1} ⋙
                  { obj := fun (X : V) ↦ { V := X, ρ := 1 }, map := fun {X Y : V} (f : X ⟶ Y) ↦ { hom := f, comm := ⋯ },
                    map_id := ⋯, map_comp := ⋯ })
                X) :
            (a : PUnit.{u_3 + 1}) →
              End
                ((forget V PUnit.{u_3 + 1} ⋙
                        { obj := fun (X : V) ↦ { V := X, ρ := 1 },
                          map := fun {X Y : V} (f : X ⟶ Y) ↦ { hom := f, comm := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
                    X).V)
          PUnit.unit :
      (Functor.obj (𝟭 (Action.{v_1, u_1, u_3} V PUnit.{u_3 + 1})) X).V ⟶
        Action.V.{v_1, u_1, u_3} (G := PUnit.{u_3 + 1})
          (Functor.obj
            (forget V PUnit.{u_3 + 1} ⋙
              { obj := fun (X : V) ↦ { V := X, ρ := 1 }, map := fun {X Y : V} (f : X ⟶ Y) ↦ { hom := f, comm := ⋯ },
                map_id := ⋯, map_comp := ⋯ })
            X))

Tactic:
simp only [Functor.id_obj, MonoidHom.one_apply, End.one_def, Functor.comp_obj,
        forget_obj, Iso.refl_hom, Category.comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.comp_id, Action.forget_obj, CategoryTheory.Functor.id_obj, CategoryTheory.End.one_def, MonoidHom.one_apply, CategoryTheory.Iso.refl_hom
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
X : Action.{v_1, u_1, u_3} V PUnit.{u_3 + 1}
x : PUnit.{u_3 + 1}
⊢ Eq.{v_1 + 1} (α := X.V ⟶ X.V) ((X.ρ : (a : PUnit.{u_3 + 1}) → End X.V) PUnit.unit : End X.V) (𝟙 X.V : X.V ⟶ X.V)

Tactic:
ρ_one X

Premises used: CategoryTheory.End, Action.ρ_one
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
X : Action.{v_1, u_1, u_3} V PUnit.{u_3 + 1}
x : PUnit.{u_3 + 1}
⊢ Eq.{v_1 + 1} (α := X.V ⟶ X.V) ((X.ρ : (a : PUnit.{u_3 + 1}) → End X.V) PUnit.unit : End X.V) (𝟙 X.V : X.V ⟶ X.V)

Tactic:
exact ρ_one X

Premises used: Action.ρ_one
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G_1 : Type u_2
inst_1 : Monoid G_1
G : Type u_3
H : Type u_4
inst_2 : Monoid G
inst_3 : Monoid H
f : G ≃* H
h :
  ∀ (x : H),
    Eq (α := H) ((MonoidHom.id H : (a : H) → H) x : H)
      ((MonoidHom.comp (↑f : G →* H) (↑f.symm : H →* G) : (a : H) → H) x : H)
⊢ Eq (α := H →* H) (MonoidHom.id H) (MonoidHom.comp (↑f : G →* H) (↑f.symm : H →* G))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G_1 : Type u_2
inst_1 : Monoid G_1
G : Type u_3
H : Type u_4
inst_2 : Monoid G
inst_3 : Monoid H
f : G ≃* H
x : H
⊢ Eq (α := H) ((MonoidHom.id H : (a : H) → H) x : H)
    ((MonoidHom.comp (↑f : G →* H) (↑f.symm : H →* G) : (a : H) → H) x : H)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G_1 : Type u_2
inst_1 : Monoid G_1
G : Type u_3
H : Type u_4
inst_2 : Monoid G
inst_3 : Monoid H
f : G ≃* H
h :
  ∀ (x : G),
    Eq (α := G) ((MonoidHom.comp (↑f.symm : H →* G) (↑f : G →* H) : (a : G) → G) x : G)
      ((MonoidHom.id G : (a : G) → G) x : G)
⊢ Eq (α := G →* G) (MonoidHom.comp (↑f.symm : H →* G) (↑f : G →* H)) (MonoidHom.id G)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G_1 : Type u_2
inst_1 : Monoid G_1
G : Type u_3
H : Type u_4
inst_2 : Monoid G
inst_3 : Monoid H
f : G ≃* H
x : G
⊢ Eq (α := G) ((MonoidHom.comp (↑f.symm : H →* G) (↑f : G →* H) : (a : G) → G) x : G)
    ((MonoidHom.id G : (a : G) → G) x : G)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G_1 : Type u_2
inst_1 : Monoid G_1
G : Type u_3
H : Type u_4
inst_2 : Monoid G
inst_3 : Monoid H
f : G →* H
X Y : Action.{v_1, u_1, u_4} V H
g₁ g₂ : X ⟶ Y
h :
  Eq (α := Functor.obj (res V f) X ⟶ Functor.obj (res V f) Y) (CategoryTheory.Functor.map (res V f) g₁)
    (CategoryTheory.Functor.map (res V f) g₂)
h₁ : g₁.hom = g₂.hom
⊢ g₁ = g₂

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G_1 : Type u_2
inst_1 : Monoid G_1
G : Type u_3
H : Type u_4
inst_2 : Monoid G
inst_3 : Monoid H
f : G →* H
X Y : Action.{v_1, u_1, u_4} V H
g₁ g₂ : X ⟶ Y
h :
  Eq (α := Functor.obj (res V f) X ⟶ Functor.obj (res V f) Y) (CategoryTheory.Functor.map (res V f) g₁)
    (CategoryTheory.Functor.map (res V f) g₂)
h₁ : Hom.hom (CategoryTheory.Functor.map (res V f) g₁) = g₂.hom
h₂ :
  Eq (α := X.V ⟶ Y.V)
    (Hom.hom (CategoryTheory.Functor.map (res V f) g₁) :
      { V := X.V, ρ := X.ρ.comp f : Action.{v_1, u_1, u_3} V G }.V ⟶
        { V := Y.V, ρ := Y.ρ.comp f : Action.{v_1, u_1, u_3} V G }.V)
    (Hom.hom (CategoryTheory.Functor.map (res V f) g₂) :
      { V := X.V, ρ := X.ρ.comp f : Action.{v_1, u_1, u_3} V G }.V ⟶
        { V := Y.V, ρ := Y.ρ.comp f : Action.{v_1, u_1, u_3} V G }.V)
h₃ h₄ :
  Eq (α := X.V ⟶ Y.V)
    (Hom.hom (CategoryTheory.Functor.map (res V f) g₂) :
      { V := X.V, ρ := X.ρ.comp f : Action.{v_1, u_1, u_3} V G }.V ⟶
        { V := Y.V, ρ := Y.ρ.comp f : Action.{v_1, u_1, u_3} V G }.V)
    (Hom.hom (CategoryTheory.Functor.map (res V f) g₂) :
      { V := X.V, ρ := X.ρ.comp f : Action.{v_1, u_1, u_3} V G }.V ⟶
        { V := Y.V, ρ := Y.ρ.comp f : Action.{v_1, u_1, u_3} V G }.V)
⊢ g₁.hom = g₂.hom

Tactic:
rw [← res_map_hom _ f g₁, ← res_map_hom _ f g₂, h]

Premises used: Action.res_map_hom
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst_1 : Monoid G
inst_2 : Monoid H
f : G →* H
f_surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
X Y : Action.{v_1, u_1, u_4} V H
g : Functor.obj (res V f) X ⟶ Functor.obj (res V f) Y
h : CategoryTheory.Functor.map (res V f) { hom := g.hom, comm := ⋯ } = g
w :
  ∀ (h : H),
    Eq.{v_1 + 1} (α := X.V ⟶ Y.V) ((X.ρ : (a : H) → End X.V) h ≫ g.hom : X.V ⟶ Y.V)
      (g.hom ≫ (Y.ρ : (a : H) → End Y.V) h : X.V ⟶ Y.V)
⊢ ∃ (a : X ⟶ Y), CategoryTheory.Functor.map (res V f) a = g

Tactic:
use ⟨g.hom, fun h ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst_1 : Monoid G
inst_2 : Monoid H
f : G →* H
f_surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
X Y : Action.{v_1, u_1, u_4} V H
g : Functor.obj (res V f) X ⟶ Functor.obj (res V f) Y
h : Hom.hom (CategoryTheory.Functor.map (res V f) { hom := g.hom, comm := ⋯ }) = g.hom
⊢ CategoryTheory.Functor.map (res V f) { hom := g.hom, comm := ⋯ } = g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst_1 : Monoid G
inst_2 : Monoid H
f : G →* H
f_surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
X Y : Action.{v_1, u_1, u_4} V H
g : Functor.obj (res V f) X ⟶ Functor.obj (res V f) Y
⊢ Hom.hom (CategoryTheory.Functor.map (res V f) { hom := g.hom, comm := ⋯ }) = g.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst_1 : Monoid G
inst_2 : Monoid H
f : G →* H
f_surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
X Y : Action.{v_1, u_1, u_4} V H
g : Functor.obj (res V f) X ⟶ Functor.obj (res V f) Y
h : H
w :
  ∀ (a : G),
    Eq.{v_1 + 1} (α := X.V ⟶ Y.V) ((X.ρ : (a : H) → End X.V) ((f : (a : G) → H) a) ≫ g.hom : X.V ⟶ Y.V)
      (g.hom ≫ (Y.ρ : (a : H) → End Y.V) ((f : (a : G) → H) a) : X.V ⟶ Y.V)
⊢ Eq.{v_1 + 1} (α := X.V ⟶ Y.V) ((X.ρ : (a : H) → End X.V) h ≫ g.hom : X.V ⟶ Y.V)
    (g.hom ≫ (Y.ρ : (a : H) → End Y.V) h : X.V ⟶ Y.V)

Tactic:
obtain ⟨a, rfl⟩ := f_surj h

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst_1 : Monoid G
inst_2 : Monoid H
f : G →* H
f_surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
X Y : Action.{v_1, u_1, u_4} V H
g : Functor.obj (res V f) X ⟶ Functor.obj (res V f) Y
a : G
⊢ Eq.{v_1 + 1} (α := End X.V) ((X.ρ : (a : H) → End X.V) ((f : (a : G) → H) a) : End X.V)
    (((Functor.obj (res V f) X).ρ : (a : G) → End ((res V f).obj X).V) a : End (Functor.obj (res V f) X).V)

Tactic:
have : X.ρ (f a) = ((res V f).obj X).ρ a := rfl
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst_1 : Monoid G
inst_2 : Monoid H
f : G →* H
f_surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
X Y : Action.{v_1, u_1, u_4} V H
g : Functor.obj (res V f) X ⟶ Functor.obj (res V f) Y
a : G
this :
  Eq.{v_1 + 1} (α := End X.V) ((X.ρ : (a : H) → End X.V) ((f : (a : G) → H) a) : End X.V)
    (((Functor.obj (res V f) X).ρ : (a : G) → End ((res V f).obj X).V) a : End (Functor.obj (res V f) X).V)
w :
  Eq (α := X.V ⟶ Y.V) (g.hom ≫ ((Functor.obj (res V f) Y).ρ : (a : G) → End ((res V f).obj Y).V) a)
    (g.hom ≫ (Y.ρ : (a : H) → End Y.V) ((f : (a : G) → H) a))
⊢ Eq.{v_1 + 1} (α := X.V ⟶ Y.V) ((X.ρ : (a : H) → End X.V) ((f : (a : G) → H) a) ≫ g.hom : X.V ⟶ Y.V)
    (g.hom ≫ (Y.ρ : (a : H) → End Y.V) ((f : (a : G) → H) a) : X.V ⟶ Y.V)

Tactic:
rw [this, g.comm a]

Premises used: Action.Hom.comm
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst_1 : Monoid G
inst_2 : Monoid H
f : G →* H
f_surj : Function.Surjective.{u_3 + 1, u_4 + 1} (α := G) (β := H) (⇑f : (a : G) → H)
X Y : Action.{v_1, u_1, u_4} V H
g : Functor.obj (res V f) X ⟶ Functor.obj (res V f) Y
a : G
this :
  Eq.{v_1 + 1} (α := End X.V) ((X.ρ : (a : H) → End X.V) ((f : (a : G) → H) a) : End X.V)
    (((Functor.obj (res V f) X).ρ : (a : G) → End ((res V f).obj X).V) a : End (Functor.obj (res V f) X).V)
⊢ Eq (α := X.V ⟶ Y.V) (g.hom ≫ ((Functor.obj (res V f) Y).ρ : (a : G) → End ((res V f).obj Y).V) a)
    (g.hom ≫ (Y.ρ : (a : H) → End Y.V) ((f : (a : G) → H) a))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
W : Type u_2
inst_1 : Category.{v_2, u_2} W
F : Functor.{v_1, v_2, u_1, u_2} V W
G : Type u_3
inst_2 : Monoid G
M : Action.{v_1, u_1, u_3} V G
⊢ Eq (α := End (F.obj M.V)) (F.map ((M.ρ : (a : G) → End M.V) 1)) 1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
W : Type u_2
inst_1 : Category.{v_2, u_2} W
F : Functor.{v_1, v_2, u_1, u_2} V W
G : Type u_3
inst_2 : Monoid G
M : Action.{v_1, u_1, u_3} V G
g h : G
dsimp :
  Eq (α := End (F.obj M.V)) (F.map ((M.ρ : (a : G) → End M.V) (g * h)))
    (CategoryStruct.comp (Y := F.obj M.V) (F.map ((M.ρ : (a : G) → End M.V) h)) (F.map ((M.ρ : (a : G) → End M.V) g)))
⊢ F.map ((M.ρ : (a : G) → End M.V) (g * h)) =
    HMul.hMul (α := End (F.obj M.V)) (F.map ((M.ρ : (a : G) → End M.V) g)) (F.map ((M.ρ : (a : G) → End M.V) h))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
W : Type u_2
inst_1 : Category.{v_2, u_2} W
F : Functor.{v_1, v_2, u_1, u_2} V W
G : Type u_3
inst_2 : Monoid G
M : Action.{v_1, u_1, u_3} V G
g h : G
rw :
  F.map
      (HMul.hMul (α := End M.V) (β := End M.V) ((M.ρ : (a : G) → End M.V) g : End M.V)
        ((M.ρ : (a : G) → End M.V) h : End M.V)) =
    CategoryStruct.comp (Y := F.obj M.V) (F.map ((M.ρ : (a : G) → End M.V) h)) (F.map ((M.ρ : (a : G) → End M.V) g))
rw₁ :
  Eq (α := End (F.obj M.V))
    (F.map (CategoryStruct.comp (Y := M.V) ((M.ρ : (a : G) → End M.V) h) ((M.ρ : (a : G) → End M.V) g)))
    (CategoryStruct.comp (Y := F.obj M.V) (F.map ((M.ρ : (a : G) → End M.V) h)) (F.map ((M.ρ : (a : G) → End M.V) g)))
rw₂ rw₃ :
  Eq (α := End (F.obj M.V))
    (CategoryStruct.comp (Y := F.obj M.V) (F.map ((M.ρ : (a : G) → End M.V) h)) (F.map ((M.ρ : (a : G) → End M.V) g)))
    (CategoryStruct.comp (Y := F.obj M.V) (F.map ((M.ρ : (a : G) → End M.V) h)) (F.map ((M.ρ : (a : G) → End M.V) g)))
⊢ Eq (α := End (F.obj M.V)) (F.map ((M.ρ : (a : G) → End M.V) (g * h)))
    (CategoryStruct.comp (Y := F.obj M.V) (F.map ((M.ρ : (a : G) → End M.V) h)) (F.map ((M.ρ : (a : G) → End M.V) g)))

Tactic:
rw [map_mul, End.mul_def, F.map_comp]

Premises used: CategoryTheory.End.mul_def, map_mul, CategoryTheory.Functor.map_comp