awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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
⊢ g₁.hom = g₂.hom
have 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)
Tactic: rw [← res_map_hom _ f g₁, ← res_map_hom _ f g₂, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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)
⊢ g₁.hom = g₂.hom
have 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)
Tactic: rw [← res_map_hom _ f g₁, ← res_map_hom _ f g₂, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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 : X ⟶ Y), CategoryTheory.Functor.map (res V f) a = g
have h : CategoryTheory.Functor.map (res V f) { hom := g.hom, comm := sorry } = g
Tactic: use ⟨g.hom, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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
⊢ ∃ (a : X ⟶ Y), CategoryTheory.Functor.map (res V f) a = g
have 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)
Tactic: use ⟨g.hom, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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
⊢ CategoryTheory.Functor.map (res V f) { hom := g.hom, comm := ⋯ } = g
have h : Hom.hom (CategoryTheory.Functor.map (res V f) { hom := g.hom, comm := sorry }) = g.hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨a, rfl⟩ := f_surj h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (hypothesis)
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} (α := 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)
have 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)
Tactic: have : X.ρ (f a) = ((res V f).obj X).ρ a := rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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.{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)
have 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))
Tactic: rw [this, g.comm a]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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
⊢ 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))
have 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)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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
⊢ 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)))
have 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))
Tactic: rw [map_mul, End.mul_def, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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))
⊢ 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)))
have 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)))
Tactic: rw [map_mul, End.mul_def, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rw [map_mul, End.mul_def, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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
⊢ 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' := ⋯ } })
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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
⊢ 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)
have 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))
Tactic: rw [← F.map_comp, f.comm, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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))
⊢ 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)
have 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))
Tactic: rw [← F.map_comp, f.comm, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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))
⊢ 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)
have 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))
Tactic: rw [← F.map_comp, f.comm, F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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} (α :=
    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' := ⋯ } })
have 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' := sorry, map_mul' := sorry :
            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' := sorry, map_mul' := sorry } })
  (Action.Hom.hom { hom := F.map (Action.Hom.hom (𝟙 M)), comm := sorry })
  (Action.Hom.hom
    (𝟙
      { V := F.obj M.V,
        ρ := { toFun := fun (g : G) ↦ F.map ((M.ρ : (a : G) → End M.V) g), map_one' := sorry, map_mul' := sorry } }))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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} (α :=
    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 := ⋯ })
have 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' := sorry, map_mul' := sorry :
            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' := sorry, map_mul' := sorry } })
  (Action.Hom.hom { hom := F.map (f ≫ g).hom, comm := sorry })
  (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' := sorry, map_mul' := sorry } })
      { hom := F.map f.hom, comm := sorry } { hom := F.map g.hom, comm := sorry }))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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₂)
⊢ a₁ = a₂
have h : a₁.hom = a₂.hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (hypothesis)
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₂)
⊢ a₁.hom = a₂.hom
have 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₂))
Tactic: apply_fun (fun f ↦ f.hom) at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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 ⟶ Y
have 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))
Tactic: refine ⟨h.preimage f.hom, fun _ ↦ h.map_injective ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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
⊢ 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))
have simp : F.map ((X.ρ : (a : G) → End X.V) x) ≫ f.hom = f.hom ≫ F.map ((Y.ρ : (a : G) → End Y.V) x)
Tactic: simp only [map_comp, map_preimage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Basic (goal)
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
⊢ 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)
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Concrete (goal)
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 (s.π.app { as := j : Discrete ι })) :
          (a : s.pt.V) → (ofMulAction G (F j)).V)
        x :
      V (ofMulAction G (F j)))
have 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 := sorry :
                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: rw [← h ⟨j⟩]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Concrete (goal)
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⁻¹
have apply : (a * v⁻¹)⁻¹ * (b * v⁻¹) ∈ N
Tactic: apply (QuotientGroup.leftRel_apply).mpr