awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
J : Type u_4
inst_3 : Category.{v_3, u_4} J
h : PreservesColimitsOfShape.{v_3, u_4, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)
⊢ PreservesColimitsOfShape J F
have preservesColimit : autoParam (∀ {K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C}, PreservesColimit K F)
  PreservesColimitsOfShape.preservesColimit._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
J : Type u_4
inst_3 : Category.{v_3, u_4} J
h : PreservesColimitsOfShape.{v_3, u_4, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)
K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C
⊢ PreservesColimit K F
have preservesColimit : PreservesColimit K (F ⋙ forget V G)
Tactic: apply Action.preservesColimit_of_preserves
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
h : PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
⊢ PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, max (max u_1 u_2) v_1} F
have preservesColimitsOfShape : autoParam (∀ {J : Type w₁} [inst_3 : Category.{w₂, w₁} J], PreservesColimitsOfShape J F)
  PreservesColimitsOfSize.preservesColimitsOfShape._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ Action.{v_1, u_1, u_2} V G
h : PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
inst_3 : Category.{w₂, w₁} J
⊢ PreservesColimitsOfShape J F
have preservesColimitsOfShape : PreservesColimitsOfShape.{w₂, w₁, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)
Tactic: apply Action.preservesColimitsOfShape_of_preserves
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
J : Type u_3
inst_2 : Category.{v_2, u_3} J
K : J ⥤ Action.{v_1, u_1, u_2} V G
inst_3 : HasLimit (K ⋙ forget V G)
⊢ PreservesLimit K (forget V G)
have change : PreservesLimit K
  (Equivalence.functor (functorCategoryEquivalence V G) ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
Tactic: change PreservesLimit K ((Action.functorCategoryEquivalence V G).functor ⋙
    (evaluation (SingleObj G) V).obj (SingleObj.star G))
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (hypothesis)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
J : Type u_3
inst_2 : Category.{v_2, u_3} J
K : J ⥤ Action.{v_1, u_1, u_2} V G
inst_3 : HasLimit (K ⋙ forget V G)
⊢ PreservesLimit K
    (Equivalence.functor (functorCategoryEquivalence V G) ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
have this : ∀ (k : SingleObj G), HasLimit ((K ⋙ Equivalence.functor (functorCategoryEquivalence V G)).flip.obj k)
Tactic: have (k : SingleObj G) :
      HasLimit ((K ⋙ (functorCategoryEquivalence V G).functor).flip.obj k) :=
    inferInstanceAs (HasLimit (K ⋙ forget V G))
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
J : Type u_3
inst_2 : Category.{v_2, u_3} J
K : J ⥤ Action.{v_1, u_1, u_2} V G
inst_3 : HasColimit (K ⋙ forget V G)
⊢ PreservesColimit K (forget V G)
have change : PreservesColimit K
  (Equivalence.functor (functorCategoryEquivalence V G) ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
Tactic: change PreservesColimit K ((Action.functorCategoryEquivalence V G).functor ⋙
    (evaluation (SingleObj G) V).obj (SingleObj.star G))
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (hypothesis)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
J : Type u_3
inst_2 : Category.{v_2, u_3} J
K : J ⥤ Action.{v_1, u_1, u_2} V G
inst_3 : HasColimit (K ⋙ forget V G)
⊢ PreservesColimit K
    (Equivalence.functor (functorCategoryEquivalence V G) ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
have this : ∀ (k : SingleObj G), HasColimit ((K ⋙ Equivalence.functor (functorCategoryEquivalence V G)).flip.obj k)
Tactic: have (k : SingleObj G) :
      HasColimit ((K ⋙ (functorCategoryEquivalence V G).functor).flip.obj k) :=
    inferInstanceAs (HasColimit (K ⋙ forget V G))
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteLimits.{v_1, u_1} V
⊢ PreservesFiniteLimits (C := Action.{v_1, u_1, u_2} V G) (forget V G)
have change : PreservesFiniteLimits (C := Action.{v_1, u_1, u_2} V G)
  (Equivalence.functor (functorCategoryEquivalence V G) ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
Tactic: change PreservesFiniteLimits ((Action.functorCategoryEquivalence V G).functor ⋙
    (evaluation (SingleObj G) V).obj (SingleObj.star G))
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteLimits.{v_1, u_1} V
⊢ PreservesFiniteLimits (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V)
    (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
have preservesFiniteLimits : autoParam
  (∀ (J : Type) [inst_3 : SmallCategory J] [FinCategory J],
    PreservesLimitsOfShape (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V) J
      (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G)))
  PreservesFiniteLimits.preservesFiniteLimits._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (hypothesis)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteLimits.{v_1, u_1} V
⊢ PreservesFiniteLimits (C := Action.{v_1, u_1, u_2} V G)
    (Equivalence.functor (functorCategoryEquivalence V G) ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
have this : PreservesFiniteLimits (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V)
  (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
Tactic: have : PreservesFiniteLimits ((evaluation (SingleObj G) V).obj (SingleObj.star G)) := by
    constructor
    intro _ _ _
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteColimits.{v_1, u_1} V
⊢ PreservesFiniteColimits (C := Action.{v_1, u_1, u_2} V G) (forget V G)
have change : PreservesFiniteColimits (C := Action.{v_1, u_1, u_2} V G)
  (Equivalence.functor (functorCategoryEquivalence V G) ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
Tactic: change PreservesFiniteColimits ((Action.functorCategoryEquivalence V G).functor ⋙
    (evaluation (SingleObj G) V).obj (SingleObj.star G))
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteColimits.{v_1, u_1} V
⊢ PreservesFiniteColimits (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V)
    (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
have preservesFiniteColimits : autoParam
  (∀ (J : Type) [inst_3 : SmallCategory J] [FinCategory J],
    PreservesColimitsOfShape (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V) J
      (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G)))
  PreservesFiniteColimits.preservesFiniteColimits._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (hypothesis)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasFiniteColimits.{v_1, u_1} V
⊢ PreservesFiniteColimits (C := Action.{v_1, u_1, u_2} V G)
    (Equivalence.functor (functorCategoryEquivalence V G) ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
have this : PreservesFiniteColimits (C := CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V)
  (Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
Tactic: have : PreservesFiniteColimits ((evaluation (SingleObj G) V).obj (SingleObj.star G)) := by
    constructor
    intro _ _ _
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
J : Type u_3
inst_2 : Category.{v_2, u_3} J
F : J ⥤ Action.{v_1, u_1, u_2} V G
c : Cone F
h : IsLimit (F := F ⋙ forget V G) (Functor.mapCone (forget V G) c)
⊢ IsLimit c
have t : IsLimit (F := F ⋙ Equivalence.functor (functorCategoryEquivalence V G))
  (Functor.mapCone (Equivalence.functor (functorCategoryEquivalence V G)) c)
Tactic: apply isLimitOfReflects ((Action.functorCategoryEquivalence V G).functor)
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
J : Type u_3
inst_2 : Category.{v_2, u_3} J
F : J ⥤ Action.{v_1, u_1, u_2} V G
c : Cocone F
h : IsColimit (F := F ⋙ forget V G) (Functor.mapCocone (forget V G) c)
⊢ IsColimit c
have t : IsColimit (F := F ⋙ Equivalence.functor (functorCategoryEquivalence V G))
  (Functor.mapCocone (Equivalence.functor (functorCategoryEquivalence V G)) c)
Tactic: apply isColimitOfReflects ((Action.functorCategoryEquivalence V G).functor)
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : Preadditive.{v_1, u_1} V
X Y P Q R : Action.{v_1, u_1, u_2} V G
f f' : P ⟶ Q
g : Q ⟶ R
⊢ (f + f') ≫ g = f ≫ g + f' ≫ g
have h : ((f + f') ≫ g).hom = (f ≫ g + f' ≫ g).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : Preadditive.{v_1, u_1} V
X Y P Q R : Action.{v_1, u_1, u_2} V G
f : P ⟶ Q
g g' : Q ⟶ R
⊢ f ≫ (g + g') = f ≫ g + f ≫ g'
have h : (f ≫ (g + g')).hom = (f ≫ g + f ≫ g').hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
x y : R
b : X ⟶ Y
⊢ (x * y) • b = x • y • b
have h : ((x * y) • b).hom = (x • y • b).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
b : X ⟶ Y
⊢ HSMul.hSMul.{u_3, v_1, v_1} (α := R) 1 b = b
have h : (HSMul.hSMul.{u_3, v_1, v_1} (α := R) 1 b).hom = b.hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
a : R
⊢ HSMul.hSMul (β := X ⟶ Y) a 0 = 0
have h : (HSMul.hSMul (β := X ⟶ Y) a 0).hom = Hom.hom 0
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
a : R
x y : X ⟶ Y
⊢ a • (x + y) = a • x + a • y
have h : (a • (x + y)).hom = (a • x + a • y).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
r s : R
x : X ⟶ Y
⊢ (r + s) • x = r • x + s • x
have h : ((r + s) • x).hom = (r • x + s • x).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y : Action.{v_1, u_1, u_2} V G
x : X ⟶ Y
⊢ HSMul.hSMul.{u_3, v_1, v_1} (α := R) 0 x = 0
have h : (HSMul.hSMul.{u_3, v_1, v_1} (α := R) 0 x).hom = Hom.hom 0
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y Z : Action.{v_1, u_1, u_2} V G
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (r • f) ≫ g = r • f ≫ g
have h : ((r • f) ≫ g).hom = (r • f ≫ g).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Limits (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : Preadditive.{v_1, u_1} V
R : Type u_3
inst_3 : Semiring R
inst_4 : Linear.{u_3, v_1, u_1} R V
X Y Z : Action.{v_1, u_1, u_2} V G
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g
have h : (f ≫ (r • g)).hom = (r • f ≫ g).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : MonoidalCategory.{v_1, u_1} V
H : Type u_3
inst_2 : Group H
X : Action.{v_1, u_1, u_3} V H
inst_3 : RightRigidCategory.{v_1, u_1} V
h : H
⊢ Eq.{v_1 + 1} (α := End (@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).V)
    (((@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).ρ : (a : H) → End Xᘁ.V) h :
      End (@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).V)
    ((X.ρ : (a : H) → End X.V) h⁻¹ᘁ :
      @HasRightDual.rightDual.{v_1, u_1} _ inst inst_1 X.V _ ⟶ @HasRightDual.rightDual.{v_1, u_1} _ inst inst_1 X.V _)
have rw : Eq.{v_1 + 1} (α := End (@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).V)
  (((@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).ρ : (a : H) → End Xᘁ.V) h :
    End (@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).V)
  ((X.ρ : (a : H) → End X.V) (inv h)ᘁ :
    @HasRightDual.rightDual.{v_1, u_1} _ inst inst_1 X.V _ ⟶ @HasRightDual.rightDual.{v_1, u_1} _ inst inst_1 X.V _)
Tactic: rw [← SingleObj.inv_as_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : MonoidalCategory.{v_1, u_1} V
H : Type u_3
inst_2 : Group H
X : Action.{v_1, u_1, u_3} V H
inst_3 : RightRigidCategory.{v_1, u_1} V
h : H
rw :
  Eq.{v_1 + 1} (α := End (@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).V)
    (((@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).ρ : (a : H) → End Xᘁ.V) h :
      End (@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).V)
    ((X.ρ : (a : H) → End X.V) (inv h)ᘁ :
      @HasRightDual.rightDual.{v_1, u_1} _ inst inst_1 X.V _ ⟶ @HasRightDual.rightDual.{v_1, u_1} _ inst inst_1 X.V _)
⊢ Eq.{v_1 + 1} (α := End (@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).V)
    (((@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).ρ : (a : H) → End Xᘁ.V) h :
      End (@HasRightDual.rightDual _ instCategory instMonoidalCategory X _).V)
    ((X.ρ : (a : H) → End X.V) h⁻¹ᘁ :
      @HasRightDual.rightDual.{v_1, u_1} _ inst inst_1 X.V _ ⟶ @HasRightDual.rightDual.{v_1, u_1} _ inst inst_1 X.V _)
have x : SingleObj H
Tactic: rw [← SingleObj.inv_as_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : MonoidalCategory.{v_1, u_1} V
H : Type u_3
inst_2 : Group H
X : Action.{v_1, u_1, u_3} V H
inst_3 : LeftRigidCategory.{v_1, u_1} V
h : H
⊢ Eq.{v_1 + 1} (α := End (@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).V)
    (((@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).ρ : (a : H) → End (ᘁX).V) h :
      End (@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).V)
    (ᘁ(X.ρ : (a : H) → End X.V) h⁻¹ :
      @HasLeftDual.leftDual.{v_1, u_1} _ inst inst_1 X.V _ ⟶ @HasLeftDual.leftDual.{v_1, u_1} _ inst inst_1 X.V _)
have rw : Eq.{v_1 + 1} (α := End (@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).V)
  (((@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).ρ : (a : H) → End (ᘁX).V) h :
    End (@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).V)
  (ᘁ(X.ρ : (a : H) → End X.V) (inv h) :
    @HasLeftDual.leftDual.{v_1, u_1} _ inst inst_1 X.V _ ⟶ @HasLeftDual.leftDual.{v_1, u_1} _ inst inst_1 X.V _)
Tactic: rw [← SingleObj.inv_as_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
inst_1 : MonoidalCategory.{v_1, u_1} V
H : Type u_3
inst_2 : Group H
X : Action.{v_1, u_1, u_3} V H
inst_3 : LeftRigidCategory.{v_1, u_1} V
h : H
rw :
  Eq.{v_1 + 1} (α := End (@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).V)
    (((@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).ρ : (a : H) → End (ᘁX).V) h :
      End (@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).V)
    (ᘁ(X.ρ : (a : H) → End X.V) (inv h) :
      @HasLeftDual.leftDual.{v_1, u_1} _ inst inst_1 X.V _ ⟶ @HasLeftDual.leftDual.{v_1, u_1} _ inst inst_1 X.V _)
⊢ Eq.{v_1 + 1} (α := End (@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).V)
    (((@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).ρ : (a : H) → End (ᘁX).V) h :
      End (@HasLeftDual.leftDual _ instCategory instMonoidalCategory X _).V)
    (ᘁ(X.ρ : (a : H) → End X.V) h⁻¹ :
      @HasLeftDual.leftDual.{v_1, u_1} _ inst inst_1 X.V _ ⟶ @HasLeftDual.leftDual.{v_1, u_1} _ inst inst_1 X.V _)
have x : SingleObj H
Tactic: rw [← SingleObj.inv_as_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (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
inst_2 : Group G
X : Action (Type u) G
x : G
x_1 : (tensorObj (𝒞 := instCategory) (leftRegular G) X).V
⊢ Eq (α := tensorObj (𝒞 := types) (Action.V (leftRegular G)) (Action.V (trivial G X.V)))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := tensorObj (𝒞 := types) (Action.V (leftRegular G)) X.V)
          ((ρ (leftRegular G) : (a : G) → End (leftRegular G).V) x ⊗ₘ (X.ρ : (a : G) → End X.V) x)
          (Iso.hom
            (Equiv.toIso
              {
                toFun := fun (g : tensorObj (𝒞 := types) (Action.V (leftRegular G)) X.V) ↦
                  (g.1,
                    (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1⁻¹) :
                        (a : X.V) → X.V)
                      g.2),
                invFun := fun (g : tensorObj (𝒞 := types) (Action.V (leftRegular G)) (Action.V (trivial G X.V))) ↦
                  (g.1,
                    (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1) :
                        (a : X.V) → X.V)
                      g.2),
                left_inv := ⋯, right_inv := ⋯ :
                tensorObj (𝒞 := types) (Action.V (leftRegular G)) X.V ≃
                  tensorObj (𝒞 := types) (Action.V (leftRegular G)) (Action.V (trivial G X.V)) }))))
      x_1)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := tensorObj (𝒞 := types) (Action.V (leftRegular G)) (Action.V (trivial G X.V)))
          (Iso.hom
            (Equiv.toIso
              {
                toFun := fun (g : tensorObj (𝒞 := types) (Action.V (leftRegular G)) X.V) ↦
                  (g.1,
                    (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1⁻¹) :
                        (a : X.V) → X.V)
                      g.2),
                invFun := fun (g : tensorObj (𝒞 := types) (Action.V (leftRegular G)) (Action.V (trivial G X.V))) ↦
                  (g.1,
                    (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g.1) :
                        (a : X.V) → X.V)
                      g.2),
                left_inv := ⋯, right_inv := ⋯ :
                tensorObj (𝒞 := types) (Action.V (leftRegular G)) X.V ≃
                  tensorObj (𝒞 := types) (Action.V (leftRegular G)) (Action.V (trivial G X.V)) }))
          ((ρ (leftRegular G) : (a : G) → End (leftRegular G).V) x ⊗ₘ
            (ρ (trivial G X.V) : (a : G) → End (trivial G X.V).V) x)))
      x_1)
have h : Eq (α := X.V)
  ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) x_1.1⁻¹) : (a : X.V) → X.V) x_1.2 :
    X.V)
  ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((1 : (a : G) → End X.V) x) : (a : X.V) → X.V)
      ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) x_1.1⁻¹) : (a : X.V) → X.V)
          x_1.2 :
        X.V) :
    X.V)
Tactic: simp [types_tensorObj_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
G : Type u
inst : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    Eq (α := tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G n))) :
            (a : (diagonal G (n + 1)).V) → (leftRegular G).V ⊗ (Fin n → G))
          f :
        tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
      ((f 0, fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin n) → G))
f : Fin (n + 1 + 1) → G
⊢ Eq (α := tensorObj (𝒞 := types) (V (leftRegular G)) (Fin (n + 1) → G))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G (n + 1)))) :
          (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V ⊗ (Fin (n + 1) → G))
        f :
      tensorObj (𝒞 := types) (V (leftRegular G)) (Fin (n + 1) → G))
    ((f 0, fun (i : Fin (n + 1)) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin (n + 1)) → G))
have succ : ∀ (x : Fin (n + 1)),
  Eq (α := G)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G (n + 1)))) :
            (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V ⊗ (Fin (n + 1) → G))
          f).2
      x)
    ((f 0, fun (i : Fin (n + 1)) ↦ (f i.castSucc)⁻¹ * f i.succ).2 x)
Tactic: refine Prod.ext rfl (funext fun x => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Monoidal (goal)
Goal:
G : Type u
inst : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    Eq (α := tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G n))) :
            (a : (diagonal G (n + 1)).V) → (leftRegular G).V ⊗ (Fin n → G))
          f :
        tensorObj (𝒞 := types) (V (leftRegular G)) (Fin n → G))
      ((f 0, fun (i : Fin n) ↦ (f i.castSucc)⁻¹ * f i.succ) : G × ((i : Fin n) → G))
f : Fin (n + 1 + 1) → G
x : Fin (n + 1)
⊢ Eq (α := G)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G (n + 1)))) :
            (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V ⊗ (Fin (n + 1) → G))
          f).2
      x)
    ((f 0, fun (i : Fin (n + 1)) ↦ (f i.castSucc)⁻¹ * f i.succ).2 x)
have succ : Eq (α := G)
  (((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (Iso.hom (diagonalSuccIsoTensorTrivial G (n + 1)))) :
          (a : (diagonal G (n + 1 + 1)).V) → (leftRegular G).V ⊗ (Fin (n + 1) → G))
        f).2
    0)
  ((f 0, fun (i : Fin (n + 1)) ↦ (f i.castSucc)⁻¹ * f i.succ).2 0)
Tactic: induction x using Fin.cases
Cleared hypotheses: x