awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Action.Concrete
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
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Action.Concrete
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
change : (@ConcreteCategory.hom _ inst FV CV _ _ _ _ ((X.ρ : (a : G) → End X.V) 1) : (a : CV X.V) → CV X.V) x = x
⊢ HSMul.hSMul.{u_3, u_2, u_2} (α := G) 1 x = x

Tactic:
change ConcreteCategory.hom (X.ρ 1) x = x

Premises used: CategoryTheory.ConcreteCategory.hom, Action.ρ, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Action.Concrete
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
⊢ (@ConcreteCategory.hom _ inst FV CV _ _ _ _ ((X.ρ : (a : G) → End X.V) 1) : (a : CV X.V) → CV X.V) x = x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Continuous
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)
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
⊢ HSMul.hSMul.{u_4, u_3, u_3} (α := G) 1 x = x

Tactic:
change ((CategoryTheory.forget₂ _ TopCat).map (X.ρ 1)) x = x

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.map, Action.ρ, CategoryTheory.forget₂, TopCat, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Action.Continuous
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)
⊢ (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:
simp
-- Module: Mathlib.CategoryTheory.Action.Continuous
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.IsContinuous (FV := FV) (CV := CV) ↔
    Continuous (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) :
        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))
                  X) :
              Type u_3)) ↦
      (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) p.1)) :
          (a : (↑((forget₂ V TopCat).obj X.V) : Type u_3)) → (↑((forget₂ V TopCat).obj X.V) : Type u_3))
        p.2

Tactic:
⟨fun h ↦ h.1, fun h ↦ ⟨h⟩⟩

Premises used: Iff.intro, ContinuousSMul.mk, ContinuousSMul.continuous_smul
-- Module: Mathlib.CategoryTheory.Action.Continuous
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
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
⊢ IsContinuous (FV := FV) (CV := CV)
    (Functor.obj (ObjectProperty.ι (IsContinuous (FV := FV) (CV := CV)) ⋙ Action.res V (↑f : G →* H)) X)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Action.Continuous
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
⊢ ∀ (g : G),
    Eq.{v_1 + 1} (α :=
      (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V ⟶
        (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V)
      (((Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).ρ :
              (a : G) → End ((res V f).obj x).obj.V)
            g ≫
          Iso.hom
            (Iso.refl (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V) :
        (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V ⟶
          (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V)
      (Iso.hom
            (Iso.refl (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V) ≫
          ((Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).ρ :
              (a : G) → End ((res V f).obj x).obj.V)
            g :
        (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V ⟶
          (Functor.obj (res V (FV := FV) (CV := CV) f) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Continuous
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_1 f' : G →ₜ* H
h : f_1 = f'
X Y : ContAction.{v_1, u_1, u_2, u_3, u_5} V (FV := FV) (CV := CV) H
f : X ⟶ Y
⊢ Eq (α :=
    (Functor.obj (res V (FV := FV) (CV := CV) f_1) X).obj (P := IsContinuous (FV := FV) (CV := CV)).V ⟶
      (Functor.obj (res V (FV := FV) (CV := CV) f') Y).obj (P := IsContinuous (FV := FV) (CV := CV)).V)
    (Hom.hom
      (InducedCategory.Hom.hom
        (CategoryTheory.Functor.map (res V (FV := FV) (CV := CV) f_1) f ≫
          Iso.hom
            ((fun (x : ContAction.{v_1, u_1, u_2, u_3, u_5} V (FV := FV) (CV := CV) H) ↦
                ObjectProperty.isoMk (IsContinuous (FV := FV) (CV := CV))
                  (mkIso
                    (Iso.refl
                      (Functor.obj (res V (FV := FV) (CV := CV) f_1) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V)
                    ⋯))
              Y))))
    (Hom.hom
      (InducedCategory.Hom.hom
        (Iso.hom
            ((fun (x : ContAction.{v_1, u_1, u_2, u_3, u_5} V (FV := FV) (CV := CV) H) ↦
                ObjectProperty.isoMk (IsContinuous (FV := FV) (CV := CV))
                  (mkIso
                    (Iso.refl
                      (Functor.obj (res V (FV := FV) (CV := CV) f_1) x).obj (P := IsContinuous (FV := FV) (CV := CV)).V)
                    ⋯))
              X) ≫
          CategoryTheory.Functor.map (res V (FV := FV) (CV := CV) f') f)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Action.Continuous
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
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)
⊢ Eq (α := H →ₜ* H) (ContinuousMonoidHom.id H) (ContinuousMonoidHom.comp (↑f : G →ₜ* H) (↑f.symm : H →ₜ* G))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Action.Continuous
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 : 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:
simp
-- Module: Mathlib.CategoryTheory.Action.Continuous
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
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)
⊢ Eq (α := G →ₜ* G) (ContinuousMonoidHom.comp (↑f.symm : H →ₜ* G) (↑f : G →ₜ* H)) (ContinuousMonoidHom.id G)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Action.Continuous
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 : 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:
simp
-- Module: Mathlib.CategoryTheory.Action.Continuous
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 : DiscreteContAction.{v_1, u_1, u_2, u_3, u_4} V (FV := FV) (CV := CV) G
⊢ DiscreteTopology.{u_3}
    (↑(Functor.obj
          (forget₂ (DiscreteContAction.{v_1, u_1, u_2, u_3, u_4} V (FV := FV) (CV := CV) G) (FC :=
            fun
              (X Y :
                ObjectProperty.FullSubcategory (C := ContAction.{v_1, u_1, u_2, u_3, u_4} V (FV := FV) (CV := CV) G)
                  (ContAction.IsDiscrete (FV := FV) (CV := CV))) ↦
            HomSubtype V G (FV := FV) (CV := CV)
              (X.obj (P := ContAction.IsDiscrete (FV := FV) (CV := CV)).obj (P := IsContinuous (FV := FV) (CV := CV)))
              (Y.obj (P := ContAction.IsDiscrete (FV := FV) (CV := CV)).obj (P := IsContinuous (FV := FV) (CV := CV))))
            (CC :=
            fun
              (X :
                ObjectProperty.FullSubcategory (C := ContAction.{v_1, u_1, u_2, u_3, u_4} V (FV := FV) (CV := CV) G)
                  (ContAction.IsDiscrete (FV := FV) (CV := CV))) ↦
            CV X.obj (P := ContAction.IsDiscrete (FV := FV) (CV := CV)).obj (P := IsContinuous (FV := FV) (CV := CV)).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)

Tactic:
X.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasLimits.{v_1, u_1} V
⊢ HasLimits (Action.{v_1, u_1, u_2} V G)

Tactic:
Adjunction.has_limits_of_equivalence (Action.functorCategoryEquivalence _ _).functor

Premises used: CategoryTheory.Adjunction.has_limits_of_equivalence, Action.functorCategoryEquivalence, CategoryTheory.Equivalence.functor
-- Module: Mathlib.CategoryTheory.Action.Limits
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
inst_3 : HasLimitsOfShape.{v_2, u_3, v_1, u_1} J V
⊢ HasLimitsOfShape J (Action.{v_1, u_1, u_2} V G)

Tactic:
Adjunction.hasLimitsOfShape_of_equivalence (Action.functorCategoryEquivalence _ _).functor

Premises used: CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence, Action.functorCategoryEquivalence, CategoryTheory.Equivalence.functor
-- Module: Mathlib.CategoryTheory.Action.Limits
Goal:
V : Type u_1
inst : Category.{v_1, u_1} V
G : Type u_2
inst_1 : Monoid G
inst_2 : HasColimits.{v_1, u_1} V
⊢ HasColimits (Action.{v_1, u_1, u_2} V G)

Tactic:
Adjunction.has_colimits_of_equivalence (Action.functorCategoryEquivalence _ _).functor

Premises used: Action.functorCategoryEquivalence, CategoryTheory.Equivalence.functor, CategoryTheory.Adjunction.has_colimits_of_equivalence
-- Module: Mathlib.CategoryTheory.Action.Limits
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
inst_3 : HasColimitsOfShape.{v_2, u_3, v_1, u_1} J V
⊢ HasColimitsOfShape J (Action.{v_1, u_1, u_2} V G)

Tactic:
Adjunction.hasColimitsOfShape_of_equivalence (Action.functorCategoryEquivalence _ _).functor

Premises used: CategoryTheory.Adjunction.hasColimitsOfShape_of_equivalence, Action.functorCategoryEquivalence, CategoryTheory.Equivalence.functor
-- Module: Mathlib.CategoryTheory.Action.Limits
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))
H : ∀ (k : SingleObj G), PreservesLimit K (F ⋙ Functor.obj (evaluation (SingleObj G) V) k)
⊢ PreservesLimit K F

Tactic:
apply preservesLimit_of_evaluation

Premises used: CategoryTheory.Limits.preservesLimit_of_evaluation
-- Module: Mathlib.CategoryTheory.Action.Limits
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))
k : SingleObj G
⊢ PreservesLimit K (F ⋙ Functor.obj (evaluation (SingleObj G) V) k)

Tactic:
h

Premises used: Quiver.SingleObj, Quiver.SingleObj.star
-- Module: Mathlib.CategoryTheory.Action.Limits
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))
k : SingleObj G
⊢ PreservesLimit K (F ⋙ Functor.obj (evaluation (SingleObj G) V) k)

Tactic:
exact h
-- Module: Mathlib.CategoryTheory.Action.Limits
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'

Tactic:
have : PreservesLimit K F' := SingleObj.preservesLimit _ _ h
-- Module: Mathlib.CategoryTheory.Action.Limits
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)
this : PreservesLimit K F'
⊢ PreservesLimit K F

Tactic:
apply preservesLimit_of_reflects_of_preserves F (Action.functorCategoryEquivalence V G).functor

Premises used: Action.functorCategoryEquivalence, CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves, CategoryTheory.Equivalence.functor