awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
X Y : Action.{v_1, u_1, u_3} V G
f : X ⟶ Y
g : G
dsimp : F.map ((X.ρ : (a : G) → End X.V) g) ≫ F.map f.hom = F.map f.hom ≫ F.map ((Y.ρ : (a : G) → End Y.V) g)
⊢ Eq.{v_2 + 1} (α :=
    Action.V.{v_2, u_2, u_3} (G := G)
        { V := F.obj X.V,
          ρ :=
            { toFun := fun (g : G) ↦ F.map ((X.ρ : (a : G) → End X.V) g), map_one' := ⋯, map_mul' := ⋯ :
              MonoidHom.{u_3, v_2} G (End (F.obj X.V)) } :
          Action.{v_2, u_2, u_3} W G } ⟶
      Action.V.{v_2, u_2, u_3} (G := G)
        { V := F.obj Y.V,
          ρ := { toFun := fun (g : G) ↦ F.map ((Y.ρ : (a : G) → End Y.V) g), map_one' := ⋯, map_mul' := ⋯ } })
    ((Action.ρ
              { V := F.obj X.V,
                ρ := { toFun := fun (g : G) ↦ F.map ((X.ρ : (a : G) → End X.V) g), map_one' := ⋯, map_mul' := ⋯ } } :
            (a : G) →
              End
                { V := F.obj X.V,
                    ρ :=
                      { toFun := fun (g : G) ↦ F.map ((X.ρ : (a : G) → End X.V) g), map_one' := ⋯, map_mul' := ⋯ } }.V)
          g ≫
        F.map f.hom :
      Action.V.{v_2, u_2, u_3} (G := G)
          { V := F.obj X.V,
            ρ :=
              { toFun := fun (g : G) ↦ F.map ((X.ρ : (a : G) → End X.V) g), map_one' := ⋯, map_mul' := ⋯ :
                MonoidHom.{u_3, v_2} G (End (F.obj X.V)) } :
            Action.{v_2, u_2, u_3} W G } ⟶
        Action.V.{v_2, u_2, u_3} (G := G)
          { V := F.obj Y.V,
            ρ := { toFun := fun (g : G) ↦ F.map ((Y.ρ : (a : G) → End Y.V) g), map_one' := ⋯, map_mul' := ⋯ } })
    (F.map f.hom ≫
        (Action.ρ
              { V := F.obj Y.V,
                ρ := { toFun := fun (g : G) ↦ F.map ((Y.ρ : (a : G) → End Y.V) g), map_one' := ⋯, map_mul' := ⋯ } } :
            (a : G) →
              End
                { V := F.obj Y.V,
                    ρ :=
                      { toFun := fun (g : G) ↦ F.map ((Y.ρ : (a : G) → End Y.V) g), map_one' := ⋯, map_mul' := ⋯ } }.V)
          g :
      Action.V.{v_2, u_2, u_3} (G := G)
          { V := F.obj X.V,
            ρ :=
              { toFun := fun (g : G) ↦ F.map ((X.ρ : (a : G) → End X.V) g), map_one' := ⋯, map_mul' := ⋯ :
                MonoidHom.{u_3, v_2} G (End (F.obj X.V)) } :
            Action.{v_2, u_2, u_3} W G } ⟶
        Action.V.{v_2, u_2, u_3} (G := G)
          { V := F.obj Y.V,
            ρ := { toFun := fun (g : G) ↦ F.map ((Y.ρ : (a : G) → End Y.V) g), map_one' := ⋯, map_mul' := ⋯ } })

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
X Y : Action.{v_1, u_1, u_3} V G
f : X ⟶ Y
g : G
rw :
  Eq (α := F.obj X.V ⟶ F.obj Y.V) (F.map ((X.ρ : (a : G) → End X.V) g ≫ f.hom))
    (F.map f.hom ≫ F.map ((Y.ρ : (a : G) → End Y.V) g))
rw₁ :
  Eq (α := F.obj X.V ⟶ F.obj Y.V) (F.map (f.hom ≫ (Y.ρ : (a : G) → End Y.V) g))
    (F.map f.hom ≫ F.map ((Y.ρ : (a : G) → End Y.V) g))
rw₂ rw₃ :
  Eq (α := F.obj X.V ⟶ F.obj Y.V) (F.map f.hom ≫ F.map ((Y.ρ : (a : G) → End Y.V) g))
    (F.map f.hom ≫ F.map ((Y.ρ : (a : G) → End Y.V) g))
⊢ F.map ((X.ρ : (a : G) → End X.V) g) ≫ F.map f.hom = F.map f.hom ≫ F.map ((Y.ρ : (a : G) → End Y.V) g)

Tactic:
rw [← F.map_comp, f.comm, F.map_comp]

Premises used: CategoryTheory.Functor.map_comp, Action.Hom.comm
-- 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
h :
  Eq.{v_2 + 1} (α :=
    Action.V.{v_2, u_2, u_3} (G := G)
        { V := F.obj M.V,
          ρ :=
            { toFun := fun (g : G) ↦ F.map ((M.ρ : (a : G) → End M.V) g), map_one' := ⋯, map_mul' := ⋯ :
              MonoidHom.{u_3, v_2} G (End (F.obj M.V)) } :
          Action.{v_2, u_2, u_3} W G } ⟶
      Action.V.{v_2, u_2, u_3} (G := G)
        { V := F.obj M.V,
          ρ := { toFun := fun (g : G) ↦ F.map ((M.ρ : (a : G) → End M.V) g), map_one' := ⋯, map_mul' := ⋯ } })
    (Action.Hom.hom { hom := F.map (Action.Hom.hom (𝟙 M)), comm := ⋯ })
    (Action.Hom.hom
      (𝟙
        { V := F.obj M.V,
          ρ := { toFun := fun (g : G) ↦ F.map ((M.ρ : (a : G) → End M.V) g), map_one' := ⋯, map_mul' := ⋯ } }))
⊢ Eq.{v_2 + 1} (α :=
    Quiver.Hom (V := Action.{v_2, u_2, u_3} W G)
      { V := F.obj M.V,
        ρ := { toFun := fun (g : G) ↦ F.map ((M.ρ : (a : G) → End M.V) g), map_one' := ⋯, map_mul' := ⋯ } }
      { V := F.obj M.V,
        ρ := { toFun := fun (g : G) ↦ F.map ((M.ρ : (a : G) → End M.V) g), map_one' := ⋯, map_mul' := ⋯ } })
    { hom := F.map (Action.Hom.hom (𝟙 M)), comm := ⋯ }
    (𝟙
      { V := F.obj M.V,
        ρ := { toFun := fun (g : G) ↦ F.map ((M.ρ : (a : G) → End M.V) g), map_one' := ⋯, map_mul' := ⋯ } })

Tactic:
ext
-- 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.{v_2 + 1} (α :=
    Action.V.{v_2, u_2, u_3} (G := G)
        { V := F.obj M.V,
          ρ :=
            { toFun := fun (g : G) ↦ F.map ((M.ρ : (a : G) → End M.V) g), map_one' := ⋯, map_mul' := ⋯ :
              MonoidHom.{u_3, v_2} G (End (F.obj M.V)) } :
          Action.{v_2, u_2, u_3} W G } ⟶
      Action.V.{v_2, u_2, u_3} (G := G)
        { V := F.obj M.V,
          ρ := { toFun := fun (g : G) ↦ F.map ((M.ρ : (a : G) → End M.V) g), map_one' := ⋯, map_mul' := ⋯ } })
    (Action.Hom.hom { hom := F.map (Action.Hom.hom (𝟙 M)), comm := ⋯ })
    (Action.Hom.hom
      (𝟙
        { V := F.obj M.V,
          ρ := { toFun := fun (g : G) ↦ F.map ((M.ρ : (a : G) → End M.V) g), map_one' := ⋯, map_mul' := ⋯ } }))

Tactic:
simp only [Action.id_hom, F.map_id]

Premises used: Action.id_hom, CategoryTheory.Functor.map_id
-- 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
X Y Z : Action.{v_1, u_1, u_3} V G
f : X ⟶ Y
g : Y ⟶ Z
h :
  Eq.{v_2 + 1} (α :=
    Action.V.{v_2, u_2, u_3} (G := G)
        { V := F.obj X.V,
          ρ :=
            { toFun := fun (g : G) ↦ F.map ((X.ρ : (a : G) → End X.V) g), map_one' := ⋯, map_mul' := ⋯ :
              MonoidHom.{u_3, v_2} G (End (F.obj X.V)) } :
          Action.{v_2, u_2, u_3} W G } ⟶
      Action.V.{v_2, u_2, u_3} (G := G)
        { V := F.obj Z.V,
          ρ := { toFun := fun (g : G) ↦ F.map ((Z.ρ : (a : G) → End Z.V) g), map_one' := ⋯, map_mul' := ⋯ } })
    (Action.Hom.hom { hom := F.map (f ≫ g).hom, comm := ⋯ })
    (Action.Hom.hom
      (CategoryStruct.comp (Y :=
        { V := F.obj Y.V,
          ρ := { toFun := fun (g : G) ↦ F.map ((Y.ρ : (a : G) → End Y.V) g), map_one' := ⋯, map_mul' := ⋯ } })
        { hom := F.map f.hom, comm := ⋯ } { hom := F.map g.hom, comm := ⋯ }))
⊢ Eq.{v_2 + 1} (α :=
    Quiver.Hom (V := Action.{v_2, u_2, u_3} W G)
      { V := F.obj X.V,
        ρ := { toFun := fun (g : G) ↦ F.map ((X.ρ : (a : G) → End X.V) g), map_one' := ⋯, map_mul' := ⋯ } }
      { V := F.obj Z.V,
        ρ := { toFun := fun (g : G) ↦ F.map ((Z.ρ : (a : G) → End Z.V) g), map_one' := ⋯, map_mul' := ⋯ } })
    { hom := F.map (f ≫ g).hom, comm := ⋯ }
    (CategoryStruct.comp (Y :=
      { V := F.obj Y.V,
        ρ := { toFun := fun (g : G) ↦ F.map ((Y.ρ : (a : G) → End Y.V) g), map_one' := ⋯, map_mul' := ⋯ } })
      { hom := F.map f.hom, comm := ⋯ } { hom := F.map g.hom, comm := ⋯ })

Tactic:
ext
-- 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
X Y Z : Action.{v_1, u_1, u_3} V G
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v_2 + 1} (α :=
    Action.V.{v_2, u_2, u_3} (G := G)
        { V := F.obj X.V,
          ρ :=
            { toFun := fun (g : G) ↦ F.map ((X.ρ : (a : G) → End X.V) g), map_one' := ⋯, map_mul' := ⋯ :
              MonoidHom.{u_3, v_2} G (End (F.obj X.V)) } :
          Action.{v_2, u_2, u_3} W G } ⟶
      Action.V.{v_2, u_2, u_3} (G := G)
        { V := F.obj Z.V,
          ρ := { toFun := fun (g : G) ↦ F.map ((Z.ρ : (a : G) → End Z.V) g), map_one' := ⋯, map_mul' := ⋯ } })
    (Action.Hom.hom { hom := F.map (f ≫ g).hom, comm := ⋯ })
    (Action.Hom.hom
      (CategoryStruct.comp (Y :=
        { V := F.obj Y.V,
          ρ := { toFun := fun (g : G) ↦ F.map ((Y.ρ : (a : G) → End Y.V) g), map_one' := ⋯, map_mul' := ⋯ } })
        { hom := F.map f.hom, comm := ⋯ } { hom := F.map g.hom, comm := ⋯ }))

Tactic:
simp only [Action.comp_hom, F.map_comp]

Premises used: Action.comp_hom, CategoryTheory.Functor.map_comp
-- 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
inst_3 : F.Faithful
X Y : Action.{v_1, u_1, u_3} V G
a₁ a₂ : X ⟶ Y
eq : Eq (α := obj (F.mapAction G) X ⟶ obj (F.mapAction G) Y) (map (F.mapAction G) a₁) (map (F.mapAction G) a₂)
h : a₁.hom = a₂.hom
⊢ a₁ = a₂

Tactic:
ext
-- 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
inst_3 : F.Faithful
X Y : Action.{v_1, u_1, u_3} V G
a₁ a₂ : X ⟶ Y
eq : Eq (α := obj (F.mapAction G) X ⟶ obj (F.mapAction G) Y) (map (F.mapAction G) a₁) (map (F.mapAction G) a₂)
⊢ Eq (α := (obj (F.mapAction G) X).V ⟶ (obj (F.mapAction G) Y).V) (Action.Hom.hom (map (F.mapAction G) a₁))
    (Action.Hom.hom (map (F.mapAction G) a₂))

Tactic:
apply_fun (fun f ↦ f.hom) at eq
-- 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
inst_3 : F.Faithful
X Y : Action.{v_1, u_1, u_3} V G
a₁ a₂ : X ⟶ Y
eq :
  Eq (α := (obj (F.mapAction G) X).V ⟶ (obj (F.mapAction G) Y).V) (Action.Hom.hom (map (F.mapAction G) a₁))
    (Action.Hom.hom (map (F.mapAction G) a₂))
⊢ a₁.hom = a₂.hom

Tactic:
F.map_injective eq

Premises used: CategoryTheory.Functor.map_injective
-- 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
inst_3 : F.Faithful
X Y : Action.{v_1, u_1, u_3} V G
a₁ a₂ : X ⟶ Y
eq :
  Eq (α := (obj (F.mapAction G) X).V ⟶ (obj (F.mapAction G) Y).V) (Action.Hom.hom (map (F.mapAction G) a₁))
    (Action.Hom.hom (map (F.mapAction G) a₂))
⊢ a₁.hom = a₂.hom

Tactic:
exact F.map_injective eq

Premises used: CategoryTheory.Functor.map_injective
-- 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
h : F.FullyFaithful
G : Type u_3
inst_2 : Monoid G
X Y : Action.{v_1, u_1, u_3} V G
f : obj (F.mapAction G) X ⟶ obj (F.mapAction G) Y
refine :
  ∀ (x : G),
    Eq (α := F.obj X.V ⟶ F.obj Y.V) (F.map ((X.ρ : (a : G) → End X.V) x ≫ h.preimage f.hom))
      (F.map (h.preimage f.hom ≫ (Y.ρ : (a : G) → End Y.V) x))
⊢ X ⟶ Y

Tactic:
refine ⟨h.preimage f.hom, fun _ ↦ h.map_injective ?_⟩
-- 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
h : F.FullyFaithful
G : Type u_3
inst_2 : Monoid G
X Y : Action.{v_1, u_1, u_3} V G
f : obj (F.mapAction G) X ⟶ obj (F.mapAction G) Y
x : G
simp : F.map ((X.ρ : (a : G) → End X.V) x) ≫ f.hom = f.hom ≫ F.map ((Y.ρ : (a : G) → End Y.V) x)
⊢ Eq (α := F.obj X.V ⟶ F.obj Y.V) (F.map ((X.ρ : (a : G) → End X.V) x ≫ h.preimage f.hom))
    (F.map (h.preimage f.hom ≫ (Y.ρ : (a : G) → End Y.V) x))

Tactic:
simp only [map_comp, map_preimage]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Functor.FullyFaithful.map_preimage
-- 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
h : F.FullyFaithful
G : Type u_3
inst_2 : Monoid G
X Y : Action.{v_1, u_1, u_3} V G
f : obj (F.mapAction G) X ⟶ obj (F.mapAction G) Y
x : G
⊢ F.map ((X.ρ : (a : G) → End X.V) x) ≫ f.hom = f.hom ≫ F.map ((Y.ρ : (a : G) → End Y.V) x)

Tactic:
f.comm _

Premises used: Action.Hom.comm
-- 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
h : F.FullyFaithful
G : Type u_3
inst_2 : Monoid G
X Y : Action.{v_1, u_1, u_3} V G
f : obj (F.mapAction G) X ⟶ obj (F.mapAction G) Y
x : G
⊢ F.map ((X.ρ : (a : G) → End X.V) x) ≫ f.hom = f.hom ≫ F.map ((Y.ρ : (a : G) → End Y.V) x)

Tactic:
exact f.comm _

Premises used: Action.Hom.comm
-- 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
inst_3 : F.Faithful
inst_4 : F.Full
⊢ Full (C := Action.{v_1, u_1, u_3} V G) (F.mapAction G)

Tactic:
((Functor.FullyFaithful.ofFullyFaithful F).mapAction G).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.Functor.FullyFaithful.mapAction, CategoryTheory.Functor.FullyFaithful.ofFullyFaithful
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V_1 : Type u_1
inst : Category.{v_1, u_1} V_1
V : Type u_2
W : Type u_3
inst_1 : Category.{v_2, u_2} V
inst_2 : Category.{v_3, u_3} W
G : Type u_4
inst_3 : Monoid G
E : Equivalence.{v_2, v_3, u_2, u_3} V W
X : Action.{v_2, u_2, u_4} V G
h :
  Action.Hom.hom
      (Functor.map (E.functor.mapAction G)
          (NatTrans.app (Iso.hom (Functor.mapActionCongr G E.unitIso ≪≫ Functor.mapActionComp G E.functor E.inverse))
            X) ≫
        NatTrans.app
          (Iso.hom (Iso.symm (Functor.mapActionComp G E.inverse E.functor) ≪≫ Functor.mapActionCongr G E.counitIso))
          (Functor.obj (E.functor.mapAction G) X)) =
    Action.Hom.hom (𝟙 (Functor.obj (E.functor.mapAction G) X))
⊢ Functor.map (E.functor.mapAction G)
        (NatTrans.app (Iso.hom (Functor.mapActionCongr G E.unitIso ≪≫ Functor.mapActionComp G E.functor E.inverse)) X) ≫
      NatTrans.app
        (Iso.hom (Iso.symm (Functor.mapActionComp G E.inverse E.functor) ≪≫ Functor.mapActionCongr G E.counitIso))
        (Functor.obj (E.functor.mapAction G) X) =
    𝟙 (Functor.obj (E.functor.mapAction G) X)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V_1 : Type u_1
inst : Category.{v_1, u_1} V_1
V : Type u_2
W : Type u_3
inst_1 : Category.{v_2, u_2} V
inst_2 : Category.{v_3, u_3} W
G : Type u_4
inst_3 : Monoid G
E : Equivalence.{v_2, v_3, u_2, u_3} V W
X : Action.{v_2, u_2, u_4} V G
⊢ Action.Hom.hom
      (Functor.map (E.functor.mapAction G)
          (NatTrans.app (Iso.hom (Functor.mapActionCongr G E.unitIso ≪≫ Functor.mapActionComp G E.functor E.inverse))
            X) ≫
        NatTrans.app
          (Iso.hom (Iso.symm (Functor.mapActionComp G E.inverse E.functor) ≪≫ Functor.mapActionCongr G E.counitIso))
          (Functor.obj (E.functor.mapAction G) X)) =
    Action.Hom.hom (𝟙 (Functor.obj (E.functor.mapAction G) X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
X : Type u
x : Function.End X
⊢ (fun (f : End X) ↦ ((⇑(ConcreteCategory.hom (FC := Fun) f) : (a : X) → X) : (a : X) → X))
      ((fun (f : Function.End X) ↦ ↾f) x) =
    x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
X : Type u
x : End X
⊢ (fun (f : Function.End X) ↦ ↾f)
      ((fun (f : End X) ↦ ((⇑(ConcreteCategory.hom (FC := Fun) f) : (a : X) → X) : (a : X) → X)) x) =
    x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
X : Type u
⊢ ∀ (x y : Function.End X), ↾(x * y) = ↾x * ↾y

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
G : Type u
inst : Group G
A : Action (Type u) G
g : G
x : A.V
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (HMul.hMul (α := End A.V) (β := End A.V) ((A.ρ : (a : G) → End A.V) g⁻¹ : End A.V)
            ((A.ρ : (a : G) → End A.V) g : End A.V)) :
        (a : A.V) → A.V)
      x =
    x

Tactic:
simp [← map_mul]

Premises used: map_mul
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
G : Type u
inst : Group G
A : Action (Type u) G
g : G
x : A.V
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (HMul.hMul (α := End A.V) (β := End A.V) ((A.ρ : (a : G) → End A.V) g : End A.V)
            ((A.ρ : (a : G) → End A.V) g⁻¹ : End A.V)) :
        (a : A.V) → A.V)
      x =
    x

Tactic:
simp [← map_mul]

Premises used: map_mul
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
G : Type u_1
H : Type u
inst : Monoid G
inst_1 : MulAction G H
⊢ MulAction G H

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
G : Type u_1
H : Type u_2
inst : Monoid G
inst_1 : MulAction G H
g : G
x : H
⊢ (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (((ρ (ofMulAction G H) : MonoidHom.{u_1, u_2} G (End (V (ofMulAction G H)))) :
              (a : G) → End (ofMulAction G H).V)
            g) :
        (a : (fun (X : Type u_2) ↦ X) (ofMulAction G H).V) → (fun (X : Type u_2) ↦ X) (ofMulAction G H).V)
      x =
    g • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
ι : Type v
G : Type (max v u)
inst : Monoid G
F : ι → Type (max v u)
inst_1 : (i : ι) → MulAction G (F i)
s : Cone (J := Discrete ι) (C := Action (Type (max u v)) G) (Discrete.functor fun (i : ι) ↦ ofMulAction G (F i))
f :
  s.pt ⟶
    Cone.pt (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ ofMulAction G (F i))
      { pt := ofMulAction G ((i : ι) → F i),
        π :=
          Discrete.natTrans fun (i : Discrete ι) ↦
            {
              hom :=
                ↾fun
                    (x : V (Functor.obj (Functor.obj (Functor.const (Discrete ι)) (ofMulAction G ((i : ι) → F i))) i)) ↦
                  x i.as,
              comm := ⋯ } }
h : ∀ (j : Discrete ι), f ≫ { hom := ↾fun (x : V (ofMulAction G ((i : ι) → F i))) ↦ x j.as, comm := ⋯ } = s.π.app j
x : s.pt.V
j : ι
h₁ :
  Eq (α := F j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f.hom : (a : s.pt.V) → (ofMulAction G ((i : ι) → F i)).V) x j : F j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Hom.hom
              (f ≫
                { hom := ↾fun (x : V (ofMulAction G ((i : ι) → F i))) ↦ x { as := j : Discrete ι }.as, comm := ⋯ :
                  Hom (ofMulAction G ((i : ι) → F i)) (ofMulAction G (F { as := j : Discrete ι }.as)) })) :
          (a : s.pt.V) → (ofMulAction G (F j)).V)
        x :
      V (ofMulAction G (F j)))
⊢ Eq (α := F j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f.hom : (a : s.pt.V) → (ofMulAction G ((i : ι) → F i)).V) x j : F j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (s.π.app { as := j : Discrete ι })) :
          (a : s.pt.V) → (ofMulAction G (F j)).V)
        x :
      V (ofMulAction G (F j)))

Tactic:
rw [← h ⟨j⟩]

Premises used: CategoryTheory.Discrete.mk
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
ι : Type v
G : Type (max v u)
inst : Monoid G
F : ι → Type (max v u)
inst_1 : (i : ι) → MulAction G (F i)
s : Cone (J := Discrete ι) (C := Action (Type (max u v)) G) (Discrete.functor fun (i : ι) ↦ ofMulAction G (F i))
f :
  s.pt ⟶
    Cone.pt (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ ofMulAction G (F i))
      { pt := ofMulAction G ((i : ι) → F i),
        π :=
          Discrete.natTrans fun (i : Discrete ι) ↦
            {
              hom :=
                ↾fun
                    (x : V (Functor.obj (Functor.obj (Functor.const (Discrete ι)) (ofMulAction G ((i : ι) → F i))) i)) ↦
                  x i.as,
              comm := ⋯ } }
h : ∀ (j : Discrete ι), f ≫ { hom := ↾fun (x : V (ofMulAction G ((i : ι) → F i))) ↦ x j.as, comm := ⋯ } = s.π.app j
x : s.pt.V
j : ι
⊢ Eq (α := F j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f.hom : (a : s.pt.V) → (ofMulAction G ((i : ι) → F i)).V) x j : F j)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Hom.hom
              (f ≫
                { hom := ↾fun (x : V (ofMulAction G ((i : ι) → F i))) ↦ x { as := j : Discrete ι }.as, comm := ⋯ :
                  Hom (ofMulAction G ((i : ι) → F i)) (ofMulAction G (F { as := j : Discrete ι }.as)) })) :
          (a : s.pt.V) → (ofMulAction G (F j)).V)
        x :
      V (ofMulAction G (F j)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
G : Type u_1
H : FintypeCat
inst : Monoid G
inst_1 : MulAction.{u_1, u} G H.obj
g : G
x : H.obj
⊢ (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _
          (((ρ (ofMulAction G H) : MonoidHom.{u_1, u} G (End (V (ofMulAction G H)))) :
                (a : G) → End (ofMulAction G H).V)
              g :
            End (V (ofMulAction G H))) :
        (a : (ofMulAction G H).V.obj) → (ofMulAction G H).V.obj)
      x =
    g • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
G : Type u_1
inst : Group G
H N : Subgroup G
inst_1 : Fintype (G ⧸ N)
inst_2 : N.Normal
v a b : G
h : a ≈ b
apply : (a * v⁻¹)⁻¹ * (b * v⁻¹) ∈ N
⊢ a * v⁻¹ ≈ b * v⁻¹

Tactic:
apply (QuotientGroup.leftRel_apply).mpr

Premises used: Iff.mpr, QuotientGroup.leftRel_apply
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
G : Type u_1
inst : Group G
H N : Subgroup G
inst_1 : Fintype (G ⧸ N)
inst_2 : N.Normal
v a b : G
h : a ≈ b
⊢ (a * v⁻¹)⁻¹ * (b * v⁻¹) ∈ N

Tactic:
simpa [mul_assoc] using Subgroup.Normal.conj_mem ‹_› _ (QuotientGroup.leftRel_apply.mp h) _

Premises used: mul_assoc, Iff.mp, Subgroup.Normal.conj_mem, QuotientGroup.leftRel_apply