awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
G : C
inst_2 : Projective.{v, u} G
hG : IsSeparator.{v, u} G
X : C
p : G ⟶ X
inst_3 : Epi p
Y : C
cm : ShortComplex.{v, u} C := ShortComplex.mk (X₁ := kernel p) (kernel.ι p) p ⋯
exact : cm.Exact
mono : Mono cm.op.f
φ : Functor.{v, v, u, v + 1} C (ModuleCat (End G)ᵐᵒᵖ) := preadditiveCoyonedaObj G
faithful : φ.Faithful
hR₁ : ShortComplex.Exact (cm.op.map (Functor.obj preadditiveYoneda Y))
hR₂' :
  Mono (X :=
    ShortComplex.X₁
      (cm.op.map
        (Functor.comp (D := (ModuleCat (End G)ᵐᵒᵖ)ᵒᵖ) (Functor.op (preadditiveCoyonedaObj G))
          (Functor.obj preadditiveYoneda (Functor.obj (preadditiveCoyonedaObj G) Y)))))
    (ShortComplex.f
      (cm.op.map
        (Functor.comp (D := (ModuleCat (End G)ᵐᵒᵖ)ᵒᵖ) (Functor.op (preadditiveCoyonedaObj G))
          (Functor.obj preadditiveYoneda (Functor.obj (preadditiveCoyonedaObj G) Y)))))
h₀ :
  Epi (X := ShortComplex.X₂ (cm.op.map (Functor.obj preadditiveYoneda Y))) (Y :=
    ShortComplex.X₂
      (cm.op.map
        (Functor.comp (D := (ModuleCat (End G)ᵐᵒᵖ)ᵒᵖ) (Functor.op (preadditiveCoyonedaObj G))
          (Functor.obj preadditiveYoneda (Functor.obj (preadditiveCoyonedaObj G) Y)))))
    (ShortComplex.Hom.τ₂ (cm.op.mapNatTrans (preadditiveYonedaMap (preadditiveCoyonedaObj G) Y)))
⊢ Epi.{v, v + 1} (X := AddCommGrpCat.of (X ⟶ Y)) (Y :=
    AddCommGrpCat.of
      (Quiver.Hom (V := ModuleCat (End G)ᵐᵒᵖ) (Functor.obj (preadditiveCoyonedaObj G) X)
        (Functor.obj (preadditiveCoyonedaObj G) Y)))
    (AddCommGrpCat.ofHom (Functor.mapAddHom (preadditiveCoyonedaObj G)))
have h₁ : Mono (X := ShortComplex.X₃ (cm.op.map (Functor.obj preadditiveYoneda Y))) (Y :=
  ShortComplex.X₃
    (cm.op.map
      (Functor.comp (D := (ModuleCat (End G)ᵐᵒᵖ)ᵒᵖ) (Functor.op (preadditiveCoyonedaObj G))
        (Functor.obj preadditiveYoneda (Functor.obj (preadditiveCoyonedaObj G) Y)))))
  (ShortComplex.Hom.τ₃ (cm.op.mapNatTrans (preadditiveYonedaMap (preadditiveCoyonedaObj G) Y)))
Tactic: apply ShortComplex.epi_of_mono_of_epi_of_mono (cm.op.mapNatTrans (preadditiveYonedaMap _ _))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
G : C
inst_2 : Projective.{v, u} G
hG : IsSeparator.{v, u} G
X : C
p : G ⟶ X
inst_3 : Epi p
Y : C
cm : ShortComplex.{v, u} C := ShortComplex.mk (X₁ := kernel p) (kernel.ι p) p ⋯
exact : cm.Exact
mono : Mono cm.op.f
φ : Functor.{v, v, u, v + 1} C (ModuleCat (End G)ᵐᵒᵖ) := preadditiveCoyonedaObj G
faithful : φ.Faithful
⊢ Epi (X := ShortComplex.X₂ (cm.op.map (Functor.obj preadditiveYoneda Y))) (Y :=
    ShortComplex.X₂
      (cm.op.map
        (Functor.comp (D := (ModuleCat (End G)ᵐᵒᵖ)ᵒᵖ) (Functor.op (preadditiveCoyonedaObj G))
          (Functor.obj preadditiveYoneda (Functor.obj (preadditiveCoyonedaObj G) Y)))))
    (ShortComplex.Hom.τ₂ (cm.op.mapNatTrans (preadditiveYonedaMap (preadditiveCoyonedaObj G) Y)))
have h₀ : Function.Surjective (α := cm.X₂ ⟶ Y) φ.map
Tactic: suffices φ.map.Surjective by simpa [AddCommGrpCat.epi_iff_surjective, Functor.coe_mapAddHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
F : Functor.{v', v, u', u} D C
inst_3 : F.Full
G : C
inst_4 : Projective.{v, u} G
hG : IsSeparator.{v, u} G
hG₂ : ∀ (X : D), ∃ (p : G ⟶ F.obj X), Epi p
X Y : D
f :
  Quiver.Hom (V := ModuleCat (End G)ᵐᵒᵖ) (Functor.obj (F ⋙ preadditiveCoyonedaObj G) X)
    (Functor.obj (F ⋙ preadditiveCoyonedaObj G) Y)
⊢ ∃ (a : X ⟶ Y), Functor.map (F ⋙ preadditiveCoyonedaObj G) a = f
have obtain : ∀ (p : G ⟶ F.obj X), Epi p → ∃ (a : X ⟶ Y), Functor.map (F ⋙ preadditiveCoyonedaObj G) a = f
Tactic: obtain ⟨p, _⟩ := hG₂ X
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
F : Functor.{v', v, u', u} D C
inst_3 : F.Full
G : C
inst_4 : Projective.{v, u} G
hG : IsSeparator.{v, u} G
hG₂ : ∀ (X : D), ∃ (p : G ⟶ F.obj X), Epi p
X Y : D
f :
  Quiver.Hom (V := ModuleCat (End G)ᵐᵒᵖ) (Functor.obj (F ⋙ preadditiveCoyonedaObj G) X)
    (Functor.obj (F ⋙ preadditiveCoyonedaObj G) Y)
p : G ⟶ F.obj X
h : Epi p
⊢ ∃ (a : X ⟶ Y), Functor.map (F ⋙ preadditiveCoyonedaObj G) a = f
have obtain : ∀ (f : F.obj X ⟶ F.obj Y),
  ∃ (a : X ⟶ Y),
    Eq (α :=
      Quiver.Hom (V := ModuleCat (End G)ᵐᵒᵖ) (Functor.obj (F ⋙ preadditiveCoyonedaObj G) X)
        (Functor.obj (F ⋙ preadditiveCoyonedaObj G) Y))
      (Functor.map (F ⋙ preadditiveCoyonedaObj G) a) (Functor.map (preadditiveCoyonedaObj G) f)
Tactic: obtain ⟨f, rfl⟩ := preadditiveCoyonedaObj_map_surjective hG p f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
F : Functor.{v', v, u', u} D C
inst_3 : F.Full
G : C
inst_4 : Projective.{v, u} G
hG : IsSeparator.{v, u} G
hG₂ : ∀ (X : D), ∃ (p : G ⟶ F.obj X), Epi p
X Y : D
p : G ⟶ F.obj X
h : Epi p
f : F.obj X ⟶ F.obj Y
⊢ ∃ (a : X ⟶ Y),
    Eq (α :=
      Quiver.Hom (V := ModuleCat (End G)ᵐᵒᵖ) (Functor.obj (F ⋙ preadditiveCoyonedaObj G) X)
        (Functor.obj (F ⋙ preadditiveCoyonedaObj G) Y))
      (Functor.map (F ⋙ preadditiveCoyonedaObj G) a) (Functor.map (preadditiveCoyonedaObj G) f)
have obtain : ∀ (f : X ⟶ Y),
  ∃ (a : X ⟶ Y),
    Eq (α :=
      Quiver.Hom (V := ModuleCat (End G)ᵐᵒᵖ) (Functor.obj (F ⋙ preadditiveCoyonedaObj G) X)
        (Functor.obj (F ⋙ preadditiveCoyonedaObj G) Y))
      (Functor.map (F ⋙ preadditiveCoyonedaObj G) a) (Functor.map (preadditiveCoyonedaObj G) (F.map f))
Tactic: obtain ⟨f, rfl⟩ := F.map_surjective f
Cleared hypotheses: f
-- 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_2
inst_1 : Group G
A : Action.{v_1, u_1, u_2} V G
g : G
⊢ Eq.{v_1 + 1} (α := End A.V) ((A.ρ : (a : G) → End A.V) (g⁻¹ * g) : End A.V) (𝟙 A.V : A.V ⟶ A.V)
have rw : Eq.{v_1 + 1} (α := End A.V) ((A.ρ : (a : G) → End A.V) 1) (𝟙 A.V)
Tactic: rw [inv_mul_cancel, ρ_one]
-- 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_2
inst_1 : Group G
A : Action.{v_1, u_1, u_2} V G
g : G
rw : Eq.{v_1 + 1} (α := End A.V) ((A.ρ : (a : G) → End A.V) 1) (𝟙 A.V)
⊢ Eq.{v_1 + 1} (α := End A.V) ((A.ρ : (a : G) → End A.V) (g⁻¹ * g) : End A.V) (𝟙 A.V : A.V ⟶ A.V)
have rw₁ : Eq.{v_1 + 1} (α := End A.V) (𝟙 A.V) (𝟙 A.V)
Tactic: rw [inv_mul_cancel, ρ_one]
-- 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_2
inst_1 : Group G
A : Action.{v_1, u_1, u_2} V G
g : G
⊢ Eq.{v_1 + 1} (α := End A.V) ((A.ρ : (a : G) → End A.V) (g * g⁻¹) : End A.V) (𝟙 A.V : A.V ⟶ A.V)
have rw : Eq.{v_1 + 1} (α := End A.V) ((A.ρ : (a : G) → End A.V) 1) (𝟙 A.V)
Tactic: rw [mul_inv_cancel, ρ_one]
-- 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_2
inst_1 : Group G
A : Action.{v_1, u_1, u_2} V G
g : G
rw : Eq.{v_1 + 1} (α := End A.V) ((A.ρ : (a : G) → End A.V) 1) (𝟙 A.V)
⊢ Eq.{v_1 + 1} (α := End A.V) ((A.ρ : (a : G) → End A.V) (g * g⁻¹) : End A.V) (𝟙 A.V : A.V ⟶ A.V)
have rw₁ : Eq.{v_1 + 1} (α := End A.V) (𝟙 A.V) (𝟙 A.V)
Tactic: rw [mul_inv_cancel, ρ_one]
-- 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_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M ≅ N
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 M.V
have rw : (f.hom ≫ f.inv).hom = 𝟙 M.V
Tactic: rw [← comp_hom, Iso.hom_inv_id, id_hom]
-- 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_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M ≅ N
rw : (f.hom ≫ f.inv).hom = 𝟙 M.V
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 M.V
have rw₁ : Hom.hom (𝟙 M) = 𝟙 M.V
Tactic: rw [← comp_hom, Iso.hom_inv_id, id_hom]
-- 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_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M ≅ N
rw : (f.hom ≫ f.inv).hom = 𝟙 M.V
rw₁ : Hom.hom (𝟙 M) = 𝟙 M.V
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 M.V
have rw₂ : Eq.{v_1 + 1} (α := M.V ⟶ M.V) (𝟙 M.V) (𝟙 M.V)
Tactic: rw [← comp_hom, Iso.hom_inv_id, id_hom]
-- 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_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M ≅ N
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 N.V
have rw : (f.inv ≫ f.hom).hom = 𝟙 N.V
Tactic: rw [← comp_hom, Iso.inv_hom_id, id_hom]
-- 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_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M ≅ N
rw : (f.inv ≫ f.hom).hom = 𝟙 N.V
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 N.V
have rw₁ : Hom.hom (𝟙 N) = 𝟙 N.V
Tactic: rw [← comp_hom, Iso.inv_hom_id, id_hom]
-- 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_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M ≅ N
rw : (f.inv ≫ f.hom).hom = 𝟙 N.V
rw₁ : Hom.hom (𝟙 N) = 𝟙 N.V
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 N.V
have rw₂ : Eq.{v_1 + 1} (α := N.V ⟶ N.V) (𝟙 N.V) (𝟙 N.V)
Tactic: rw [← comp_hom, Iso.inv_hom_id, id_hom]
-- 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_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M.V ≅ N.V
comm :
  ∀ (g : G),
    Eq.{v_1 + 1} (α := M.V ⟶ N.V) ((M.ρ : (a : G) → End M.V) g ≫ f.hom : M.V ⟶ N.V)
      (f.hom ≫ (N.ρ : (a : G) → End N.V) g : M.V ⟶ N.V)
g : G
⊢ Eq.{v_1 + 1} (α := N.V ⟶ M.V) ((N.ρ : (a : G) → End N.V) g ≫ f.inv : N.V ⟶ M.V)
    (f.inv ≫ (M.ρ : (a : G) → End M.V) g : N.V ⟶ M.V)
have w : ((M.ρ : (a : G) → End M.V) g ≫ f.hom) ≫ f.inv = (f.hom ≫ (N.ρ : (a : G) → End N.V) g) ≫ f.inv
Tactic: have w := comm g =≫ f.inv
-- 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_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M.V ≅ N.V
comm :
  ∀ (g : G),
    Eq.{v_1 + 1} (α := M.V ⟶ N.V) ((M.ρ : (a : G) → End M.V) g ≫ f.hom : M.V ⟶ N.V)
      (f.hom ≫ (N.ρ : (a : G) → End N.V) g : M.V ⟶ N.V)
g : G
w : ((M.ρ : (a : G) → End M.V) g ≫ f.hom) ≫ f.inv = (f.hom ≫ (N.ρ : (a : G) → End N.V) g) ≫ f.inv
⊢ Eq.{v_1 + 1} (α := N.V ⟶ M.V) ((N.ρ : (a : G) → End N.V) g ≫ f.inv : N.V ⟶ M.V)
    (f.inv ≫ (M.ρ : (a : G) → End M.V) g : N.V ⟶ M.V)
have w₁ : Eq.{v_1 + 1} (α := M.V ⟶ M.V) ((M.ρ : (a : G) → End M.V) g : End M.V)
  (f.hom ≫ (N.ρ : (a : G) → End N.V) g ≫ f.inv : M.V ⟶ M.V)
Tactic: simp at w
Cleared hypotheses: w
-- 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_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
f : X ⟶ Y
g : G
⊢ Eq.{u_4 + 1} (α := CV X.V → CV Y.V)
    (Function.comp (β := CV X.V) (⇑(ConcreteCategory.hom (FC := FV) (CC := CV) f.hom) : (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)
      (⇑(ConcreteCategory.hom (FC := FV) (CC := CV) f.hom) : (a : CV X.V) → CV Y.V))
have h : ∀ (x : CV X.V),
  Eq (α := CV Y.V)
    (Function.comp (β := CV X.V) (⇑(ConcreteCategory.hom (FC := FV) (CC := CV) f.hom) : (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)
      x)
    (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)
      (⇑(ConcreteCategory.hom (FC := FV) (CC := CV) f.hom) : (a : CV X.V) → CV Y.V) x)
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_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 (FC := FV) (CC := CV)
        { hom := ConcreteCategory.ofHom (FC := FV) (CC := CV) (↑x : FV X.V Y.V), comm := ⋯ : X.Hom Y }.hom)
      ⋯ =
    x
have dsimp : 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)))
    sorry =
  x
Tactic: dsimp
-- 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_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)))
      ⋯ =
    x
have 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)))
        sorry) :
    FV X.V Y.V) =
  (↑x : FV X.V Y.V)
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_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
⊢ {
      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
have 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) sorry) :
              FV X.V Y.V),
        comm := sorry : X.Hom Y }.hom =
  ConcreteCategory.hom (FC := FV) (CC := CV) x.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_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M ≅ N
g : G
⊢ 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))
have 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))
Tactic: rw [Iso.conj_apply, Iso.eq_inv_comp]
-- 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_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} (α :=
    (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))
have 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)
Tactic: simp only [Functor.id_obj, MonoidHom.one_apply, End.one_def, Functor.comp_obj,
        forget_obj, Iso.refl_hom, Category.comp_id]
-- 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
⊢ Eq (α := H →* H) (MonoidHom.id H) (MonoidHom.comp (↑f : G →* H) (↑f.symm : H →* G))
have 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: ext
-- 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
⊢ Eq (α := G →* G) (MonoidHom.comp (↑f.symm : H →* G) (↑f : G →* H)) (MonoidHom.id G)
have 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: ext
-- 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₂)
⊢ g₁ = g₂
have h₁ : g₁.hom = 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_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₂)
⊢ g₁.hom = g₂.hom
have h₁ : Hom.hom (CategoryTheory.Functor.map (res V f) g₁) = g₂.hom
Tactic: rw [← res_map_hom _ f g₁, ← res_map_hom _ f g₂, h]