awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 g x : G
h :
  Quotient.lift (fun (σ : G) ↦ HMul.hMul (α := G ⧸ N) (↑σ : G ⧸ N) (↑v : G ⧸ N)⁻¹) ⋯
      (HMul.hMul (α := G ⧸ N) (↑g : G ⧸ N) (↑x : G ⧸ N)) =
    g • HMul.hMul (α := G ⧸ N) (↑x : G ⧸ N) (↑v : G ⧸ N)⁻¹
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
    ((@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))
            _ _ _
            (CategoryStruct.comp (Y := V (ofMulAction G (FintypeCat.of (G ⧸ N))))
                ((ρ (ofMulAction G (FintypeCat.of (G ⧸ N))) : (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
                  g)
                (FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * v⁻¹⟧) ⋯)) :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
        ⟦x⟧ :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
    ((@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))
            _ _ _
            (CategoryStruct.comp (Y := V (ofMulAction G (FintypeCat.of (G ⧸ N))))
                (FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * v⁻¹⟧) ⋯))
                ((ρ (ofMulAction G (FintypeCat.of (G ⧸ N))) : (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
                  g) :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
        ⟦x⟧ :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))

Tactic:
dsimp
-- 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 g x : G
h :
  (↑g : G ⧸ N) * HMul.hMul (α := G ⧸ N) (↑x : G ⧸ N) (↑v : G ⧸ N)⁻¹ =
    g • HMul.hMul (α := G ⧸ N) (↑x : G ⧸ N) (↑v : G ⧸ N)⁻¹
⊢ HMul.hMul (α := G ⧸ N) (↑((fun (x1 x2 : G) ↦ x1 * x2) g x) : G ⧸ N) (↑v : G ⧸ N)⁻¹ =
    g • HMul.hMul (α := G ⧸ N) (↑x : G ⧸ N) (↑v : G ⧸ N)⁻¹

Tactic:
simp only [QuotientGroup.mk_mul, mul_assoc]

Premises used: mul_assoc, QuotientGroup.mk_mul
-- 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 g x : G
⊢ (↑g : G ⧸ N) * HMul.hMul (α := G ⧸ N) (↑x : G ⧸ N) (↑v : G ⧸ N)⁻¹ =
    g • HMul.hMul (α := G ⧸ N) (↑x : G ⧸ N) (↑v : G ⧸ N)⁻¹

Tactic:
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
h :
  Eq.{u_1 + 1} (α := V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N))))
    (Hom.hom { hom := FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * 1⁻¹⟧) ⋯), comm := ⋯ }) (Hom.hom 1)
⊢ Eq.{u_1 + 1} (α := End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N))))
    { hom := FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * 1⁻¹⟧) ⋯), comm := ⋯ } 1

Tactic:
apply Action.hom_ext

Premises used: Action.hom_ext
-- 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
h :
  ∀ (x : G ⧸ N),
    Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
      ((@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))
              _ _ _
              (Hom.hom { hom := FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * 1⁻¹⟧) ⋯), comm := ⋯ } :
                V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
      ((@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))
              _ _ _
              (Hom.hom 1 : V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
⊢ Eq.{u_1 + 1} (α := V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N))))
    (Hom.hom { hom := FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * 1⁻¹⟧) ⋯), comm := ⋯ }) (Hom.hom 1)

Tactic:
ext (x : G ⧸ N)
-- 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
a : G
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
    ((@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))
            _ _ _
            (Hom.hom { hom := FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * 1⁻¹⟧) ⋯), comm := ⋯ } :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
        ⟦a⟧ :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
    ((@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))
            _ _ _ (Hom.hom 1 : V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
        ⟦a⟧ :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))

Tactic:
simp
-- 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
σ τ : G
h :
  Hom.hom { hom := FintypeCat.homMk (Quotient.lift (fun (σ_1 : G) ↦ ⟦σ_1 * (σ * τ)⁻¹⟧) ⋯), comm := ⋯ } =
    (HMul.hMul (α := End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N))))
        { hom := FintypeCat.homMk (Quotient.lift (fun (σ_1 : G) ↦ ⟦σ_1 * σ⁻¹⟧) ⋯), comm := ⋯ :
          Hom (ofMulAction G (FintypeCat.of (G ⧸ N))) (ofMulAction G (FintypeCat.of (G ⧸ N))) }
        { hom := FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * τ⁻¹⟧) ⋯), comm := ⋯ :
          Hom (ofMulAction G (FintypeCat.of (G ⧸ N))) (ofMulAction G (FintypeCat.of (G ⧸ N))) }).hom
⊢ { hom := FintypeCat.homMk (Quotient.lift (fun (σ_1 : G) ↦ ⟦σ_1 * (σ * τ)⁻¹⟧) ⋯), comm := ⋯ } =
    HMul.hMul (α := End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N))))
      { hom := FintypeCat.homMk (Quotient.lift (fun (σ_1 : G) ↦ ⟦σ_1 * σ⁻¹⟧) ⋯), comm := ⋯ :
        Hom (ofMulAction G (FintypeCat.of (G ⧸ N))) (ofMulAction G (FintypeCat.of (G ⧸ N))) }
      { hom := FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * τ⁻¹⟧) ⋯), comm := ⋯ :
        Hom (ofMulAction G (FintypeCat.of (G ⧸ N))) (ofMulAction G (FintypeCat.of (G ⧸ N))) }

Tactic:
apply Action.hom_ext

Premises used: Action.hom_ext
-- 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
σ τ x : G
h : ⟦x * (τ⁻¹ * σ⁻¹)⟧ = ⟦x * τ⁻¹ * σ⁻¹⟧
h₁ h₂ : ⟦x * (τ⁻¹ * σ⁻¹)⟧ = ⟦x * (τ⁻¹ * σ⁻¹)⟧
⊢ ⟦x * (σ * τ)⁻¹⟧ = ⟦x * τ⁻¹ * σ⁻¹⟧

Tactic:
rw [mul_inv_rev, mul_assoc]

Premises used: mul_assoc, mul_inv_rev
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : Fintype (G ⧸ N)
inst_2 : N.Normal
g h : G
⊢ (@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))
          _ _ _
          (Hom.hom
              (((toEndHom N : G →* End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
                  (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))))
                g) :
            V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
      ⟦h⟧ =
    ⟦h * g⁻¹⟧

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : Fintype (G ⧸ N)
inst_2 : N.Normal
n : G
hn : n ∈ N
h :
  Eq (α := V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N))))
    (Hom.hom
      (((toEndHom N : G →* End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))))
        n))
    (Hom.hom (𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N)))))
⊢ Eq (α := End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N))))
    (((toEndHom N : G →* End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))))
        n :
      End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N))))
    (𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N))) :
      Quiver.Hom (V := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N)))
        (ofMulAction G (FintypeCat.of (G ⧸ N))))

Tactic:
apply Action.hom_ext

Premises used: Action.hom_ext
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : Fintype (G ⧸ N)
inst_2 : N.Normal
n : G
hn : n ∈ N
h :
  ∀ (x : G ⧸ N),
    Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
      ((@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))
              _ _ _
              (Hom.hom
                  (((toEndHom N : G →* End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
                      (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))))
                    n) :
                V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
      ((@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))
              _ _ _
              (Hom.hom (𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
                V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
            (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
              (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
          x :
        (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
⊢ Eq (α := V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N))))
    (Hom.hom
      (((toEndHom N : G →* End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))))
        n))
    (Hom.hom (𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N)))))

Tactic:
ext (x : G ⧸ N)
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : Fintype (G ⧸ N)
inst_2 : N.Normal
n : G
hn : n ∈ N
a : G
⊢ (a * n⁻¹)⁻¹ * a ∈ N

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : Fintype (G ⧸ N)
inst_2 : N.Normal
n : G
hn : n ∈ N
a : G
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
    ((@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))
            _ _ _
            (Hom.hom
                (((toEndHom N : G →* End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
                    (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))))
                  n) :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
        ⟦a⟧ :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
    ((@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))
            _ _ _
            (Hom.hom (𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
        ⟦a⟧ :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))

Tactic:
exact Quotient.sound ((QuotientGroup.leftRel_apply).mpr <| by simpa)

Premises used: Iff.mpr, Quotient.sound, 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
x : ↥H
g : G
⊢ (@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))
          _ _ _
          (Hom.hom
              (((quotientToEndHom H N :
                    ↥H ⧸ N.subgroupOf H →* End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
                  (a : ↥H ⧸ N.subgroupOf H) → End (ofMulAction G (FintypeCat.of (G ⧸ N))))
                ⟦x⟧) :
            V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
      ⟦g⟧ =
    ⟦g * (↑x⁻¹ : G)⟧

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 : Fintype (G ⧸ H)
h : N ≤ H
g a : G
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ H)))))
    ((@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))
            _ _ _
            (CategoryStruct.comp (Y := V (ofMulAction G (FintypeCat.of (G ⧸ N))))
                ((ρ (ofMulAction G (FintypeCat.of (G ⧸ N))) : (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
                  g)
                (FintypeCat.homMk (Quotient.lift (fun (x : G) ↦ ⟦x⟧) ⋯)) :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ H)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ H))).V)
        ⟦a⟧ :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ H)))))
    ((@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))
            _ _ _
            (CategoryStruct.comp (Y := V (ofMulAction G (FintypeCat.of (G ⧸ H))))
                (FintypeCat.homMk (Quotient.lift (fun (x : G) ↦ ⟦x⟧) ⋯))
                ((ρ (ofMulAction G (FintypeCat.of (G ⧸ H))) : (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ H))).V)
                  g) :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ H)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ H))).V)
        ⟦a⟧ :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ H)))))

Tactic:
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 : Fintype (G ⧸ H)
h : N ≤ H
x : G
⊢ ((@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))
            _ _ _
            (Hom.hom (quotientToQuotientOfLE H N h) :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ H)))) :
          TypeCat.Fun (V (ofMulAction G (FintypeCat.of (G ⧸ N)))).obj (V (ofMulAction G (FintypeCat.of (G ⧸ H)))).obj) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ H))).V)
      ⟦x⟧ =
    ⟦x⟧

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
V : Type (u + 1)
inst : LargeCategory V
FV : V → V → Type u_1
CV : V → Type u_2
inst_1 : (X Y : V) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FV X Y) (CV X) (CV Y)
inst_2 : ConcreteCategory V FV (CC := CV)
G : Type u_3
inst_3 : Monoid G
X : Action V G
g h : G
x : ToType (FC := HomSubtype V G (FV := FV) (CV := CV)) (CC := fun (X : Action V G) ↦ CV X.V) X
change :
  Eq (α := CV X.V)
    ((@ConcreteCategory.hom _ inst FV CV _ _ _ _ ((X.ρ : (a : G) → End X.V) (g * h)) : (a : CV X.V) → CV X.V) x :
      CV X.V)
    ((@ConcreteCategory.hom _ inst FV CV _ _ _ _ ((X.ρ : (a : G) → End X.V) g) : (a : CV X.V) → CV X.V)
        ((@ConcreteCategory.hom _ inst FV CV _ _ _ _ ((X.ρ : (a : G) → End X.V) h) : (a : CV X.V) → CV X.V) x :
          CV X.V) :
      CV X.V)
⊢ (g * h) • x = g • h • x

Tactic:
change ConcreteCategory.hom (X.ρ (g * h)) x =
      ConcreteCategory.hom (X.ρ g) ((ConcreteCategory.hom (X.ρ h)) x)

Premises used: HMul.hMul, CategoryTheory.ConcreteCategory.hom, Action.ρ, DFunLike.coe