awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 g x : G
⊢ Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _
            (CategoryStruct.comp (Y := V (ofMulAction G (FintypeCat.of (G ⧸ N))))
                ((ρ (ofMulAction G (FintypeCat.of (G ⧸ N))) : (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
                  g)
                (FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * v⁻¹⟧) ⋯)) :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
        ⟦x⟧ :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _
            (CategoryStruct.comp (Y := V (ofMulAction G (FintypeCat.of (G ⧸ N))))
                (FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * v⁻¹⟧) ⋯))
                ((ρ (ofMulAction G (FintypeCat.of (G ⧸ N))) : (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
                  g) :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
        ⟦x⟧ :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
have h : Quotient.lift (fun (σ : G) ↦ HMul.hMul (α := G ⧸ N) (↑σ : G ⧸ N) (↑v : G ⧸ N)⁻¹) sorry
    (HMul.hMul (α := G ⧸ N) (↑g : G ⧸ N) (↑x : G ⧸ N)) =
  g • HMul.hMul (α := G ⧸ N) (↑x : G ⧸ N) (↑v : G ⧸ N)⁻¹
Tactic: dsimp
-- 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 g x : G
⊢ HMul.hMul (α := G ⧸ N) (↑((fun (x1 x2 : G) ↦ x1 * x2) g x) : G ⧸ N) (↑v : G ⧸ N)⁻¹ =
    g • HMul.hMul (α := G ⧸ N) (↑x : G ⧸ N) (↑v : G ⧸ N)⁻¹
have h : (↑g : G ⧸ N) * HMul.hMul (α := G ⧸ N) (↑x : G ⧸ N) (↑v : G ⧸ N)⁻¹ =
  g • HMul.hMul (α := G ⧸ N) (↑x : G ⧸ N) (↑v : G ⧸ N)⁻¹
Tactic: simp only [QuotientGroup.mk_mul, mul_assoc]
-- 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
⊢ Eq.{u_1 + 1} (α := End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N))))
    { hom := FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * 1⁻¹⟧) ⋯), comm := ⋯ } 1
have h : Eq.{u_1 + 1} (α := V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N))))
  (Hom.hom { hom := FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * 1⁻¹⟧) sorry), comm := sorry }) (Hom.hom 1)
Tactic: apply Action.hom_ext
-- 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
⊢ Eq.{u_1 + 1} (α := V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N))))
    (Hom.hom { hom := FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * 1⁻¹⟧) ⋯), comm := ⋯ }) (Hom.hom 1)
have h : ∀ (x : G ⧸ N),
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _
            (Hom.hom { hom := FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * 1⁻¹⟧) sorry), comm := sorry } :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _ (Hom.hom 1 : V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
Tactic: ext (x : G ⧸ N)
-- 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
σ τ : G
⊢ { hom := FintypeCat.homMk (Quotient.lift (fun (σ_1 : G) ↦ ⟦σ_1 * (σ * τ)⁻¹⟧) ⋯), comm := ⋯ } =
    HMul.hMul (α := End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N))))
      { hom := FintypeCat.homMk (Quotient.lift (fun (σ_1 : G) ↦ ⟦σ_1 * σ⁻¹⟧) ⋯), comm := ⋯ :
        Hom (ofMulAction G (FintypeCat.of (G ⧸ N))) (ofMulAction G (FintypeCat.of (G ⧸ N))) }
      { hom := FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * τ⁻¹⟧) ⋯), comm := ⋯ :
        Hom (ofMulAction G (FintypeCat.of (G ⧸ N))) (ofMulAction G (FintypeCat.of (G ⧸ N))) }
have h : Hom.hom { hom := FintypeCat.homMk (Quotient.lift (fun (σ_1 : G) ↦ ⟦σ_1 * (σ * τ)⁻¹⟧) sorry), comm := sorry } =
  (HMul.hMul (α := End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N))))
      { hom := FintypeCat.homMk (Quotient.lift (fun (σ_1 : G) ↦ ⟦σ_1 * σ⁻¹⟧) sorry), comm := sorry :
        Hom (ofMulAction G (FintypeCat.of (G ⧸ N))) (ofMulAction G (FintypeCat.of (G ⧸ N))) }
      { hom := FintypeCat.homMk (Quotient.lift (fun (σ : G) ↦ ⟦σ * τ⁻¹⟧) sorry), comm := sorry :
        Hom (ofMulAction G (FintypeCat.of (G ⧸ N))) (ofMulAction G (FintypeCat.of (G ⧸ N))) }).hom
Tactic: apply Action.hom_ext
-- 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
σ τ x : G
⊢ ⟦x * (σ * τ)⁻¹⟧ = ⟦x * τ⁻¹ * σ⁻¹⟧
have h : ⟦x * (τ⁻¹ * σ⁻¹)⟧ = ⟦x * τ⁻¹ * σ⁻¹⟧
Tactic: rw [mul_inv_rev, mul_assoc]
-- 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
σ τ x : G
h : ⟦x * (τ⁻¹ * σ⁻¹)⟧ = ⟦x * τ⁻¹ * σ⁻¹⟧
⊢ ⟦x * (σ * τ)⁻¹⟧ = ⟦x * τ⁻¹ * σ⁻¹⟧
have h₁ : ⟦x * (τ⁻¹ * σ⁻¹)⟧ = ⟦x * (τ⁻¹ * σ⁻¹)⟧
Tactic: rw [mul_inv_rev, mul_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Concrete (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : Fintype (G ⧸ N)
inst_2 : N.Normal
n : G
hn : n ∈ N
⊢ Eq (α := End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N))))
    (((toEndHom N : G →* End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))))
        n :
      End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N))))
    (𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N))) :
      Quiver.Hom (V := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N)))
        (ofMulAction G (FintypeCat.of (G ⧸ N))))
have h : Eq (α := V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N))))
  (Hom.hom
    (((toEndHom N : G →* End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
        (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))))
      n))
  (Hom.hom (𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N)))))
Tactic: apply Action.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Concrete (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : Fintype (G ⧸ N)
inst_2 : N.Normal
n : G
hn : n ∈ N
⊢ Eq (α := V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N))))
    (Hom.hom
      (((toEndHom N : G →* End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))))
        n))
    (Hom.hom (𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N)))))
have h : ∀ (x : G ⧸ N),
  Eq (α := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _
            (Hom.hom
                (((toEndHom N : G →* End (C := Action FintypeCat G) (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
                    (a : G) → End (ofMulAction G (FintypeCat.of (G ⧸ N))))
                  n) :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
    ((@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
            (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
              (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
            _ _ _
            (Hom.hom (𝟙 (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
              V (ofMulAction G (FintypeCat.of (G ⧸ N))) ⟶ V (ofMulAction G (FintypeCat.of (G ⧸ N)))) :
          (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V) →
            (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (ofMulAction G (FintypeCat.of (G ⧸ N))).V)
        x :
      (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (V (ofMulAction G (FintypeCat.of (G ⧸ N)))))
Tactic: ext (x : G ⧸ N)
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Concrete (goal)
Goal:
V : Type (u + 1)
inst : LargeCategory V
FV : V → V → Type u_1
CV : V → Type u_2
inst_1 : (X Y : V) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FV X Y) (CV X) (CV Y)
inst_2 : ConcreteCategory V FV (CC := CV)
G : Type u_3
inst_3 : Monoid G
X : Action V G
g h : G
x : ToType (FC := HomSubtype V G (FV := FV) (CV := CV)) (CC := fun (X : Action V G) ↦ CV X.V) X
⊢ (g * h) • x = g • h • x
have change : Eq (α := CV X.V)
  ((@ConcreteCategory.hom _ inst FV CV _ _ _ _ ((X.ρ : (a : G) → End X.V) (g * h)) : (a : CV X.V) → CV X.V) x : CV X.V)
  ((@ConcreteCategory.hom _ inst FV CV _ _ _ _ ((X.ρ : (a : G) → End X.V) g) : (a : CV X.V) → CV X.V)
      ((@ConcreteCategory.hom _ inst FV CV _ _ _ _ ((X.ρ : (a : G) → End X.V) h) : (a : CV X.V) → CV X.V) x : CV X.V) :
    CV X.V)
Tactic: change ConcreteCategory.hom (X.ρ (g * h)) x =
      ConcreteCategory.hom (X.ρ g) ((ConcreteCategory.hom (X.ρ h)) x)
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Concrete (goal)
Goal:
V : Type (u + 1)
inst : LargeCategory V
FV : V → V → Type u_1
CV : V → Type u_2
inst_1 : (X Y : V) → FunLike.{u_1 + 1, u_2 + 1, u_2 + 1} (FV X Y) (CV X) (CV Y)
inst_2 : ConcreteCategory V FV (CC := CV)
G : Type u_3
inst_3 : Monoid G
X : Action V G
x : ToType (FC := HomSubtype V G (FV := FV) (CV := CV)) (CC := fun (X : Action V G) ↦ CV X.V) X
⊢ HSMul.hSMul.{u_3, u_2, u_2} (α := G) 1 x = x
have change : (@ConcreteCategory.hom _ inst FV CV _ _ _ _ ((X.ρ : (a : G) → End X.V) 1) : (a : CV X.V) → CV X.V) x = x
Tactic: change ConcreteCategory.hom (X.ρ 1) x = x
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Continuous (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst_1 : (X Y : V) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FV X Y) (CV X) (CV Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} V FV (CC := CV)
inst_3 :
  HasForget₂.{u_3, v_1, u_1, u_2, u_3, u_3 + 1, u_3} V (FC := FV) (CC := CV) TopCat (FD := fun (X Y : TopCat.{u_3}) ↦
    C((↑X : Type u_3), (↑Y : Type u_3))) (CD := TopCat.carrier)
G : Type u_4
inst_4 : Monoid G
inst_5 : TopologicalSpace G
X : Action.{v_1, u_1, u_4} V G
x :
  (↑(Functor.obj
        (forget₂ (Action.{v_1, u_1, u_4} V G) (FC := HomSubtype V G (FV := FV) (CV := CV)) (CC :=
          fun (X : Action.{v_1, u_1, u_4} V G) ↦ CV X.V) TopCat (FD := fun (X Y : TopCat.{u_3}) ↦
          C((↑X : Type u_3), (↑Y : Type u_3))) (CD := TopCat.carrier))
        X) :
    Type u_3)
⊢ HSMul.hSMul.{u_4, u_3, u_3} (α := G) 1 x = x
have change : (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_3}) ↦ C((↑X : Type u_3), (↑Y : Type u_3))) (CC := TopCat.carrier)
        (X :=
        Functor.obj.{v_1, u_3, u_1, u_3 + 1}
          (forget₂ V (FC := FV) (CC := CV) TopCat (FD := fun (X Y : TopCat.{u_3}) ↦ C((↑X : Type u_3), (↑Y : Type u_3)))
            (CD := TopCat.carrier))
          X.V)
        (Y :=
        Functor.obj.{v_1, u_3, u_1, u_3 + 1}
          (forget₂ V (FC := FV) (CC := CV) TopCat (FD := fun (X Y : TopCat.{u_3}) ↦ C((↑X : Type u_3), (↑Y : Type u_3)))
            (CD := TopCat.carrier))
          X.V)
        (CategoryTheory.Functor.map
          (forget₂ V (FC := FV) (CC := CV) TopCat (FD := fun (X Y : TopCat.{u_3}) ↦ C((↑X : Type u_3), (↑Y : Type u_3)))
            (CD := TopCat.carrier))
          ((X.ρ : (a : G) → End X.V) 1)) :
      (a : (↑((forget₂ V TopCat).obj X.V) : Type u_3)) → (↑((forget₂ V TopCat).obj X.V) : Type u_3))
    x =
  x
Tactic: change ((CategoryTheory.forget₂ _ TopCat).map (X.ρ 1)) x = x
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Continuous (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst_1 : (X Y : V) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FV X Y) (CV X) (CV Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} V FV (CC := CV)
inst_3 :
  HasForget₂.{u_3, v_1, u_1, u_2, u_3, u_3 + 1, u_3} V (FC := FV) (CC := CV) TopCat (FD := fun (X Y : TopCat.{u_3}) ↦
    C((↑X : Type u_3), (↑Y : Type u_3))) (CD := TopCat.carrier)
G : Type u_4
inst_4 : Monoid G
inst_5 : TopologicalSpace G
H : Type u_5
inst_6 : Monoid H
inst_7 : TopologicalSpace H
f : G →ₜ* H
X : ContAction.{v_1, u_1, u_2, u_3, u_5} V (FV := FV) (CV := CV) H
⊢ IsContinuous (FV := FV) (CV := CV)
    (Functor.obj (ObjectProperty.ι (IsContinuous (FV := FV) (CV := CV)) ⋙ Action.res V (↑f : G →* H)) X)
have continuous_smul : Continuous (Y :=
  (↑(Functor.obj
        (forget₂ (Action.{v_1, u_1, u_4} V G) (FC := HomSubtype V G (FV := FV) (CV := CV)) (CC :=
          fun (X : Action.{v_1, u_1, u_4} V G) ↦ CV X.V) TopCat (FD := fun (X Y : TopCat.{u_3}) ↦
          C((↑X : Type u_3), (↑Y : Type u_3))) (CD := TopCat.carrier))
        (Functor.obj (ObjectProperty.ι (IsContinuous (FV := FV) (CV := CV)) ⋙ Action.res V (↑f : G →* H)) X)) :
    Type u_3))
  fun
    (p :
      Prod.{u_4, u_3} G
        (↑(Functor.obj
              (forget₂ (Action.{v_1, u_1, u_4} V G) (FC := HomSubtype V G (FV := FV) (CV := CV)) (CC :=
                fun (X : Action.{v_1, u_1, u_4} V G) ↦ CV X.V) TopCat (FD := fun (X Y : TopCat.{u_3}) ↦
                C((↑X : Type u_3), (↑Y : Type u_3))) (CD := TopCat.carrier))
              (Functor.obj (ObjectProperty.ι (IsContinuous (FV := FV) (CV := CV)) ⋙ Action.res V (↑f : G →* H)) X)) :
          Type u_3)) ↦
  p.1 • p.2
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Continuous (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst_1 : (X Y : V) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FV X Y) (CV X) (CV Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} V FV (CC := CV)
inst_3 :
  HasForget₂.{u_3, v_1, u_1, u_2, u_3, u_3 + 1, u_3} V (FC := FV) (CC := CV) TopCat (FD := fun (X Y : TopCat.{u_3}) ↦
    C((↑X : Type u_3), (↑Y : Type u_3))) (CD := TopCat.carrier)
G : Type u_4
inst_4 : Monoid G
inst_5 : TopologicalSpace G
H : Type u_5
inst_6 : Monoid H
inst_7 : TopologicalSpace H
f : G ≃ₜ* H
⊢ Eq (α := H →ₜ* H) (ContinuousMonoidHom.id H) (ContinuousMonoidHom.comp (↑f : G →ₜ* H) (↑f.symm : H →ₜ* G))
have h : ∀ (x : H),
  Eq (α := H) ((ContinuousMonoidHom.id H : (a : H) → H) x : H)
    ((ContinuousMonoidHom.comp (↑f : G →ₜ* H) (↑f.symm : H →ₜ* G) : (a : H) → H) x : H)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Continuous (goal)
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst_1 : (X Y : V) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FV X Y) (CV X) (CV Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} V FV (CC := CV)
inst_3 :
  HasForget₂.{u_3, v_1, u_1, u_2, u_3, u_3 + 1, u_3} V (FC := FV) (CC := CV) TopCat (FD := fun (X Y : TopCat.{u_3}) ↦
    C((↑X : Type u_3), (↑Y : Type u_3))) (CD := TopCat.carrier)
G : Type u_4
inst_4 : Monoid G
inst_5 : TopologicalSpace G
H : Type u_5
inst_6 : Monoid H
inst_7 : TopologicalSpace H
f : G ≃ₜ* H
⊢ Eq (α := G →ₜ* G) (ContinuousMonoidHom.comp (↑f.symm : H →ₜ* G) (↑f : G →ₜ* H)) (ContinuousMonoidHom.id G)
have h : ∀ (x : G),
  Eq (α := G) ((ContinuousMonoidHom.comp (↑f.symm : H →ₜ* G) (↑f : G →ₜ* H) : (a : G) → G) x : G)
    ((ContinuousMonoidHom.id G : (a : G) → G) x : G)
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
C : Type u_3
inst_2 : Category.{v_2, u_3} C
F : C ⥤ CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V
J : Type u_4
inst_3 : Category.{v_3, u_4} J
K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C
h : PreservesLimit K (F ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
⊢ PreservesLimit K F
have H : ∀ (k : SingleObj G), PreservesLimit K (F ⋙ Functor.obj (evaluation (SingleObj G) V) k)
Tactic: apply preservesLimit_of_evaluation
-- 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
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
K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C
h : PreservesLimit K (F ⋙ forget V G)
F' : C ⥤ CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V :=
  F ⋙ Equivalence.functor (functorCategoryEquivalence V G)
⊢ PreservesLimit K F
have this : PreservesLimit K F'
Tactic: have : PreservesLimit K F' := SingleObj.preservesLimit _ _ h
-- 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 : PreservesLimitsOfShape.{v_3, u_4, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)
⊢ PreservesLimitsOfShape J F
have preservesLimit : autoParam (∀ {K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C}, PreservesLimit K F)
  PreservesLimitsOfShape.preservesLimit._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 : PreservesLimitsOfShape.{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
⊢ PreservesLimit K F
have preservesLimit : PreservesLimit K (F ⋙ forget V G)
Tactic: apply Action.preservesLimit_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 : PreservesLimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
⊢ PreservesLimitsOfSize.{w₂, w₁, v_2, v_1, u_3, max (max u_1 u_2) v_1} F
have preservesLimitsOfShape : autoParam (∀ {J : Type w₁} [inst_3 : Category.{w₂, w₁} J], PreservesLimitsOfShape J F)
  PreservesLimitsOfSize.preservesLimitsOfShape._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 : PreservesLimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
inst_3 : Category.{w₂, w₁} J
⊢ PreservesLimitsOfShape J F
have preservesLimitsOfShape : PreservesLimitsOfShape.{w₂, w₁, v_2, v_1, u_3, u_1} J (F ⋙ forget V G)
Tactic: apply Action.preservesLimitsOfShape_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 ⥤ CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V
J : Type u_4
inst_3 : Category.{v_3, u_4} J
K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C
h : PreservesColimit K (F ⋙ Functor.obj (evaluation (SingleObj G) V) (SingleObj.star G))
⊢ PreservesColimit K F
have H : ∀ (k : SingleObj G), PreservesColimit K (F ⋙ Functor.obj (evaluation (SingleObj G) V) k)
Tactic: apply preservesColimit_of_evaluation
-- 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
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
K : CategoryTheory.Functor.{v_3, v_2, u_4, u_3} J C
h : PreservesColimit K (F ⋙ forget V G)
F' : C ⥤ CategoryTheory.Functor.{u_2, v_1, 0, u_1} (SingleObj G) V :=
  F ⋙ Equivalence.functor (functorCategoryEquivalence V G)
⊢ PreservesColimit K F
have this : PreservesColimit K F'
Tactic: have : PreservesColimit K F' := SingleObj.preservesColimit _ _ h