awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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
⊢ ShortComplex.Exact (cm.op.map (Functor.obj preadditiveYoneda Y))

Tactic:
exact.op.map_of_mono_of_preservesKernel _ mono inferInstance

Premises used: inferInstance, CategoryTheory.ShortComplex.Exact.op, CategoryTheory.ShortComplex.Exact.map_of_mono_of_preservesKernel
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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
⊢ ShortComplex.Exact (cm.op.map (Functor.obj preadditiveYoneda Y))

Tactic:
exact exact.op.map_of_mono_of_preservesKernel _ mono inferInstance

Premises used: inferInstance, CategoryTheory.ShortComplex.Exact.op, CategoryTheory.ShortComplex.Exact.map_of_mono_of_preservesKernel
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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
⊢ 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)))))
    (Y :=
    ShortComplex.X₂
      (cm.op.map
        (Functor.comp (D := (ModuleCat (End G)ᵐᵒᵖ)ᵒᵖ) (Functor.op (preadditiveCoyonedaObj G))
          (Functor.obj preadditiveYoneda (Functor.obj (preadditiveCoyonedaObj G) Y)))))
    (Functor.map
        (Functor.comp (D := (ModuleCat (End G)ᵐᵒᵖ)ᵒᵖ) (Functor.op (preadditiveCoyonedaObj G))
          (Functor.obj preadditiveYoneda (Functor.obj (preadditiveCoyonedaObj G) Y)))
        cm.op.f :
      Functor.obj
          (Functor.comp (D := (ModuleCat (End G)ᵐᵒᵖ)ᵒᵖ) (Functor.op (preadditiveCoyonedaObj G))
            (Functor.obj preadditiveYoneda (Functor.obj (preadditiveCoyonedaObj G) Y)))
          cm.op.X₁ ⟶
        Functor.obj
          (Functor.comp (D := (ModuleCat (End G)ᵐᵒᵖ)ᵒᵖ) (Functor.op (preadditiveCoyonedaObj G))
            (Functor.obj preadditiveYoneda (Functor.obj (preadditiveCoyonedaObj G) Y)))
          cm.op.X₂)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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
this : Function.Surjective (α := cm.X₂ ⟶ Y) φ.map
⊢ 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)))

Tactic:
simpa [AddCommGrpCat.epi_iff_surjective, Functor.coe_mapAddHom]

Premises used: CategoryTheory.Functor.coe_mapAddHom, AddCommGrpCat.epi_iff_surjective
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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
h₀ : Function.Surjective (α := cm.X₂ ⟶ Y) φ.map
⊢ 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)))

Tactic:
suffices φ.map.Surjective by simpa [AddCommGrpCat.epi_iff_surjective, Functor.coe_mapAddHom]
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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
⊢ Function.Surjective (α := cm.X₂ ⟶ Y) φ.map

Tactic:
exact fun f => ⟨f (𝟙 G), by cat_disch⟩
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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
⊢ 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:
simp [AddCommGrpCat.mono_iff_injective, Functor.coe_mapAddHom, Functor.map_injective]

Premises used: CategoryTheory.Functor.coe_mapAddHom, AddCommGrpCat.mono_iff_injective, CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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)
obtain : ∀ (p : G ⟶ F.obj X), Epi p → ∃ (a : X ⟶ Y), Functor.map (F ⋙ preadditiveCoyonedaObj G) a = f
⊢ ∃ (a : X ⟶ Y), Functor.map (F ⋙ preadditiveCoyonedaObj G) a = f

Tactic:
obtain ⟨p, _⟩ := hG₂ X
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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
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)
⊢ ∃ (a : X ⟶ Y), Functor.map (F ⋙ preadditiveCoyonedaObj G) a = f

Tactic:
obtain ⟨f, rfl⟩ := preadditiveCoyonedaObj_map_surjective hG p f

Premises used: CategoryTheory.Abelian.preadditiveCoyonedaObj_map_surjective, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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
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))
⊢ ∃ (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⟩ := F.map_surjective f

Premises used: rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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 : 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:
⟨f, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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 : 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:
exact ⟨f, rfl⟩
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
A : Action.{v_1, u_1, u_2} V G
⊢ Eq.{v_1 + 1} (α := End A.V) ((A.ρ : (a : G) → End A.V) 1) (𝟙 A.V)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : 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)
rw₁ rw₂ : Eq.{v_1 + 1} (α := End A.V) (𝟙 A.V) (𝟙 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)

Tactic:
rw [inv_mul_cancel, ρ_one]

Premises used: inv_mul_cancel, Action.ρ_one
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : 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)
rw₁ rw₂ : Eq.{v_1 + 1} (α := End A.V) (𝟙 A.V) (𝟙 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)

Tactic:
rw [mul_inv_cancel, ρ_one]

Premises used: Action.ρ_one, mul_inv_cancel
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
⊢ Function.Injective.{v_1 + 1, v_1 + 1} (α := M.Hom N) Hom.hom

Tactic:
fun _ _ ↦ Hom.ext

Premises used: Action.Hom.ext, Function.Injective
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
φ₁ φ₂ : M ⟶ N
h : φ₁.hom = φ₂.hom
⊢ φ₁ = φ₂

Tactic:
Hom.ext h

Premises used: Action.Hom.ext
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
M : Action.{v_1, u_1, u_2} V G
⊢ Hom.hom (𝟙 M) = 𝟙 M.V

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
M N K : Action.{v_1, u_1, u_2} V G
f : M ⟶ N
g : N ⟶ K
⊢ (f ≫ g).hom = f.hom ≫ g.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M ≅ N
rw : (f.hom ≫ f.inv).hom = 𝟙 M.V
rw₁ : Hom.hom (𝟙 M) = 𝟙 M.V
rw₂ rw₃ : Eq.{v_1 + 1} (α := M.V ⟶ M.V) (𝟙 M.V) (𝟙 M.V)
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 M.V

Tactic:
rw [← comp_hom, Iso.hom_inv_id, id_hom]

Premises used: Action.comp_hom, CategoryTheory.Iso.hom_inv_id, Action.id_hom
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
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
rw₂ rw₃ : Eq.{v_1 + 1} (α := N.V ⟶ N.V) (𝟙 N.V) (𝟙 N.V)
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 N.V

Tactic:
rw [← comp_hom, Iso.inv_hom_id, id_hom]

Premises used: CategoryTheory.Iso.inv_hom_id, Action.comp_hom, Action.id_hom
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
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
⊢ ((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
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M.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} (α := 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
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M.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 :
  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)
⊢ 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)

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M ⟶ N
inst_2 : IsIso f.hom
⊢ IsIso f

Tactic:
(mkIso (asIso f.hom) f.comm).isIso_hom

Premises used: Action.mkIso, CategoryTheory.Iso.isIso_hom, Action.Hom.hom, Action.Hom.comm, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M.V ⟶ N.V
inst_2 : IsIso f
w :
  ∀ (g : G),
    Eq.{v_1 + 1} (α := M.V ⟶ N.V) ((M.ρ : (a : G) → End M.V) g ≫ f : M.V ⟶ N.V)
      (f ≫ (N.ρ : (a : G) → End N.V) g : M.V ⟶ N.V)
⊢ IsIso (C := Action.{v_1, u_1, u_2} V G) (X := M) (Y := N) { hom := f, comm := w : M.Hom N }

Tactic:
(mkIso (asIso f) w).isIso_hom

Premises used: Action.mkIso, CategoryTheory.Iso.isIso_hom, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M ≅ N
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 M.V ∧ f.inv.hom ≫ f.hom.hom = 𝟙 N.V

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
M N : Action.{v_1, u_1, u_2} V G
f : M ≅ N
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 N.V ∧ f.hom.hom ≫ f.inv.hom = 𝟙 M.V

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
⊢ Functor.IsEquivalence (C := Action.{v_1, u_1, u_2} V G) functor

Tactic:
(functorCategoryEquivalence V G).isEquivalence_functor

Premises used: Action.FunctorCategoryEquivalence.functor, Action.functorCategoryEquivalence, CategoryTheory.Equivalence.isEquivalence_functor
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
⊢ Functor.IsEquivalence (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V) inverse

Tactic:
(functorCategoryEquivalence V G).isEquivalence_inverse

Premises used: CategoryTheory.Equivalence.isEquivalence_inverse, Action.functorCategoryEquivalence, Action.FunctorCategoryEquivalence.inverse
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst_2 : (X Y : V) → FunLike.{u_3 + 1, u_4 + 1, u_4 + 1} (FV X Y) (CV X) (CV Y)
inst_3 : ConcreteCategory.{u_4, v_1, u_1, u_3} V FV (CC := CV)
X Y : Action.{v_1, u_1, u_2} V G
f : X ⟶ Y
g : G
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)
⊢ 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))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst_2 : (X Y : V) → FunLike.{u_3 + 1, u_4 + 1, u_4 + 1} (FV X Y) (CV X) (CV Y)
inst_3 : ConcreteCategory.{u_4, v_1, u_1, u_3} V FV (CC := CV)
X Y : Action.{v_1, u_1, u_2} V G
f : X ⟶ Y
g : G
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:
simpa using CategoryTheory.congr_fun (f.2 g) _

Premises used: CategoryTheory.congr_fun, Action.Hom.comm
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
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 : HomSubtype V G (FV := FV) (CV := CV) X Y
g : G
x : CV X.V
⊢ Eq (α := CV Y.V)
    ((@ConcreteCategory.hom.{u_4, v_1, u_1, u_3} _ inst FV CV _ _ _ _
            ((X.ρ : (a : G) → End X.V) g ≫ ConcreteCategory.ofHom (FC := FV) (CC := CV) (↑f : FV X.V Y.V)) :
          (a : CV X.V) → CV Y.V)
        x :
      CV Y.V)
    ((@ConcreteCategory.hom.{u_4, v_1, u_1, u_3} _ inst FV CV _ _ _ _
            (ConcreteCategory.ofHom (FC := FV) (CC := CV) (↑f : FV X.V Y.V) ≫ (Y.ρ : (a : G) → End Y.V) g) :
          (a : CV X.V) → CV Y.V)
        x :
      CV Y.V)

Tactic:
simpa [ConcreteCategory.hom_ofHom] using congr_fun (f.2 g) x

Premises used: congr_fun, CategoryTheory.ConcreteCategory.hom_ofHom, Subtype.property
-- Module: Mathlib.CategoryTheory.Action.Basic
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst_2 : (X Y : V) → FunLike.{u_3 + 1, u_4 + 1, u_4 + 1} (FV X Y) (CV X) (CV Y)
inst_3 : ConcreteCategory.{u_4, v_1, u_1, u_3} V FV (CC := CV)
X Y : Action.{v_1, u_1, u_2} V G
x : HomSubtype V G (FV := FV) (CV := CV) X Y
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)))
      ⋯ =
    x
⊢ 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

Tactic:
dsimp