mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
b✝ : X ⟶ Y
⊢ 1 • b✝ = b✝

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
b✝ : X ⟶ Y
⊢ 1 • b✝ = b✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
b✝ : X ⟶ Y
⊢ (1 • b✝).hom = b✝.hom

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
b✝ : X ⟶ Y
⊢ (1 • b✝).hom = b✝.hom
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
a✝ : R
⊢ a✝ • 0 = 0

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
a✝ : R
⊢ a✝ • 0 = 0
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
a✝ : R
⊢ (a✝ • 0).hom = Hom.hom 0

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
a✝ : R
⊢ (a✝ • 0).hom = Hom.hom 0
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
a✝ : R
x✝ y✝ : X ⟶ Y
⊢ a✝ • (x✝ + y✝) = a✝ • x✝ + a✝ • y✝

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
a✝ : R
x✝ y✝ : X ⟶ Y
⊢ a✝ • (x✝ + y✝) = a✝ • x✝ + a✝ • y✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
a✝ : R
x✝ y✝ : X ⟶ Y
⊢ (a✝ • (x✝ + y✝)).hom = (a✝ • x✝ + a✝ • y✝).hom

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
a✝ : R
x✝ y✝ : X ⟶ Y
⊢ (a✝ • (x✝ + y✝)).hom = (a✝ • x✝ + a✝ • y✝).hom
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
r✝ s✝ : R
x✝ : X ⟶ Y
⊢ (r✝ + s✝) • x✝ = r✝ • x✝ + s✝ • x✝

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
r✝ s✝ : R
x✝ : X ⟶ Y
⊢ (r✝ + s✝) • x✝ = r✝ • x✝ + s✝ • x✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
r✝ s✝ : R
x✝ : X ⟶ Y
⊢ ((r✝ + s✝) • x✝).hom = (r✝ • x✝ + s✝ • x✝).hom

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
r✝ s✝ : R
x✝ : X ⟶ Y
⊢ ((r✝ + s✝) • x✝).hom = (r✝ • x✝ + s✝ • x✝).hom
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
x✝ : X ⟶ Y
⊢ 0 • x✝ = 0

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
x✝ : X ⟶ Y
⊢ 0 • x✝ = 0
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
x✝ : X ⟶ Y
⊢ (0 • x✝).hom = Hom.hom 0

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
x✝ : X ⟶ Y
⊢ (0 • x✝).hom = Hom.hom 0
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X✝ Y✝ : D
f : X✝ ⟶ Y✝
X' Y' : C
f' : X' ⟶ Y'
w✝ : Mono f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalMono f' := normalMonoOfMono f'
this : PreservesLimit (parallelPair NormalMono.g 0) L
⊢ L.map (f' ≫ NormalMono.g) = 0

Tactic:
;

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X✝ Y✝ : D
f : X✝ ⟶ Y✝
X' Y' : C
f' : X' ⟶ Y'
w✝ : Mono f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalMono f' := normalMonoOfMono f'
this : PreservesLimit (parallelPair NormalMono.g 0) L
⊢ L.map (f' ≫ NormalMono.g) = 0
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X✝ Y✝ Z✝ : Action V G
r✝ : R
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ (r✝ • f✝) ≫ g✝ = r✝ • f✝ ≫ g✝

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X✝ Y✝ Z✝ : Action V G
r✝ : R
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ (r✝ • f✝) ≫ g✝ = r✝ • f✝ ≫ g✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X✝ Y✝ Z✝ : Action V G
r✝ : R
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ ((r✝ • f✝) ≫ g✝).hom = (r✝ • f✝ ≫ g✝).hom

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X✝ Y✝ Z✝ : Action V G
r✝ : R
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ ((r✝ • f✝) ≫ g✝).hom = (r✝ • f✝ ≫ g✝).hom
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X✝ Y✝ Z✝ : Action V G
f✝ : X✝ ⟶ Y✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
⊢ f✝ ≫ (r✝ • g✝) = r✝ • f✝ ≫ g✝

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X✝ Y✝ Z✝ : Action V G
f✝ : X✝ ⟶ Y✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
⊢ f✝ ≫ (r✝ • g✝) = r✝ • f✝ ≫ g✝
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X✝ Y✝ Z✝ : Action V G
f✝ : X✝ ⟶ Y✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
⊢ (f✝ ≫ (r✝ • g✝)).hom = (r✝ • f✝ ≫ g✝).hom

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁴ : Category.{v_1, u_1} V
G : Type u_2
inst✝³ : Monoid G
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X✝ Y✝ Z✝ : Action V G
f✝ : X✝ ⟶ Y✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
⊢ (f✝ ≫ (r✝ • g✝)).hom = (r✝ • f✝ ≫ g✝).hom
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X✝ Y✝ : D
f : X✝ ⟶ Y✝
X' Y' : C
f' : X' ⟶ Y'
w✝ : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalEpi f' := normalEpiOfEpi f'
this : PreservesColimit (parallelPair NormalEpi.g 0) L
⊢ L.map (NormalEpi.g ≫ f') = 0

Tactic:
;

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X✝ Y✝ : D
f : X✝ ⟶ Y✝
X' Y' : C
f' : X' ⟶ Y'
w✝ : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
hf' : NormalEpi f' := normalEpiOfEpi f'
this : PreservesColimit (parallelPair NormalEpi.g 0) L
⊢ L.map (NormalEpi.g ≫ f') = 0
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ : Action V G
f : X✝ ⟶ Y✝
g : G
⊢ F.map (X✝.ρ g) ≫ F.map f.hom = F.map f.hom ≫ F.map (Y✝.ρ g)

Tactic:
;

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ : Action V G
f : X✝ ⟶ Y✝
g : G
⊢ F.map (X✝.ρ g) ≫ F.map f.hom = F.map f.hom ≫ F.map (Y✝.ρ g)
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝ : Monoid G
M : Action V G
⊢ { hom := F.map (𝟙 M).hom, comm := ⋯ }.hom =
    (𝟙 { V := F.obj M.V, ρ := { toFun := fun g ↦ F.map (M.ρ g), map_one' := ⋯, map_mul' := ⋯ } }).hom

Tactic:
;

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝ : Monoid G
M : Action V G
⊢ { hom := F.map (𝟙 M).hom, comm := ⋯ }.hom =
    (𝟙 { V := F.obj M.V, ρ := { toFun := fun g ↦ F.map (M.ρ g), map_one' := ⋯, map_mul' := ⋯ } }).hom
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝ : Monoid G
M : Action V G
⊢ { hom := F.map (𝟙 M).hom, comm := ⋯ }.hom =
    (𝟙 { V := F.obj M.V, ρ := { toFun := fun g ↦ F.map (M.ρ g), map_one' := ⋯, map_mul' := ⋯ } }).hom

Tactic:
simp only [Action.id_hom, F.map_id]

Goal state after:
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ Z✝ : Action V G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { hom := F.map (f ≫ g).hom, comm := ⋯ }.hom =
    ({ hom := F.map f.hom, comm := ⋯ } ≫ { hom := F.map g.hom, comm := ⋯ }).hom

Tactic:
;

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ Z✝ : Action V G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { hom := F.map (f ≫ g).hom, comm := ⋯ }.hom =
    ({ hom := F.map f.hom, comm := ⋯ } ≫ { hom := F.map g.hom, comm := ⋯ }).hom
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V✝ : Type u_1
inst✝³ : Category.{v_1, u_1} V✝
V : Type u_2
W : Type u_3
inst✝² : Category.{v_2, u_2} V
inst✝¹ : Category.{v_3, u_3} W
G : Type u_4
inst✝ : Monoid G
E : V ≌ W
X : Action V G
⊢ ((E.functor.mapAction G).map
          ((Functor.mapActionCongr G E.unitIso ≪≫ Functor.mapActionComp G E.functor E.inverse).hom.app X) ≫
        ((Functor.mapActionComp G E.inverse E.functor).symm ≪≫ Functor.mapActionCongr G E.counitIso).hom.app
          ((E.functor.mapAction G).obj X)).hom =
    (𝟙 ((E.functor.mapAction G).obj X)).hom

Tactic:
;

Goal state after:
V✝ : Type u_1
inst✝³ : Category.{v_1, u_1} V✝
V : Type u_2
W : Type u_3
inst✝² : Category.{v_2, u_2} V
inst✝¹ : Category.{v_3, u_3} W
G : Type u_4
inst✝ : Monoid G
E : V ≌ W
X : Action V G
⊢ ((E.functor.mapAction G).map
          ((Functor.mapActionCongr G E.unitIso ≪≫ Functor.mapActionComp G E.functor E.inverse).hom.app X) ≫
        ((Functor.mapActionComp G E.inverse E.functor).symm ≪≫ Functor.mapActionCongr G E.counitIso).hom.app
          ((E.functor.mapAction G).obj X)).hom =
    (𝟙 ((E.functor.mapAction G).obj X)).hom
Module: Mathlib.CategoryTheory.Action.Continuous

Goal state before:
pp: V : Type u_1
inst✝⁷ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁶ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁵ : ConcreteCategory V FV
inst✝⁴ : HasForget₂ V TopCat
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G →ₜ* H
x✝ : ContAction V H
⊢ ∀ (g : G),
    ((res V f).obj x✝).obj.ρ g ≫ (Iso.refl ((res V f).obj x✝).obj.V).hom =
      (Iso.refl ((res V f).obj x✝).obj.V).hom ≫ ((res V f).obj x✝).obj.ρ g

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁷ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁶ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁵ : ConcreteCategory V FV
inst✝⁴ : HasForget₂ V TopCat
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G →ₜ* H
x✝ : ContAction V H
⊢ ∀ (g : G),
    ((res V f).obj x✝).obj.ρ g ≫ (Iso.refl ((res V f).obj x✝).obj.V).hom =
      (Iso.refl ((res V f).obj x✝).obj.V).hom ≫ ((res V f).obj x✝).obj.ρ g
Module: Mathlib.CategoryTheory.Action.Continuous

Goal state before:
pp: V : Type u_1
inst✝⁷ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁶ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁵ : ConcreteCategory V FV
inst✝⁴ : HasForget₂ V TopCat
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G ≃ₜ* H
x✝ : H
⊢ (ContinuousMonoidHom.id H) x✝ = ((↑f).comp ↑f.symm) x✝

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁷ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁶ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁵ : ConcreteCategory V FV
inst✝⁴ : HasForget₂ V TopCat
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G ≃ₜ* H
x✝ : H
⊢ (ContinuousMonoidHom.id H) x✝ = ((↑f).comp ↑f.symm) x✝
Module: Mathlib.CategoryTheory.Action.Continuous

Goal state before:
pp: V : Type u_1
inst✝⁷ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁶ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁵ : ConcreteCategory V FV
inst✝⁴ : HasForget₂ V TopCat
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G ≃ₜ* H
x✝ : G
⊢ ((↑f.symm).comp ↑f) x✝ = (ContinuousMonoidHom.id G) x✝

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁷ : Category.{v_1, u_1} V
FV : V → V → Type u_2
CV : V → Type u_3
inst✝⁶ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁵ : ConcreteCategory V FV
inst✝⁴ : HasForget₂ V TopCat
G : Type u_4
inst✝³ : Monoid G
inst✝² : TopologicalSpace G
H : Type u_5
inst✝¹ : Monoid H
inst✝ : TopologicalSpace H
f : G ≃ₜ* H
x✝ : G
⊢ ((↑f.symm).comp ↑f) x✝ = (ContinuousMonoidHom.id G) x✝
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
s : BinaryCofan a b
⊢ (pullback.fst a.arrow b.arrow ≫ underlying.map (s.ι.app { as := WalkingPair.left })) ≫
      (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }).arrow =
    (pullback.snd a.arrow b.arrow ≫ underlying.map (s.ι.app { as := WalkingPair.right })) ≫
      (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }).arrow

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
s : BinaryCofan a b
⊢ (pullback.fst a.arrow b.arrow ≫ underlying.map (s.ι.app { as := WalkingPair.left })) ≫
      (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }).arrow =
    (pullback.snd a.arrow b.arrow ≫ underlying.map (s.ι.app { as := WalkingPair.right })) ≫
      (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }).arrow
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
s✝ : BinaryCofan a b
⊢ ⋯.hom ≫ ⋯.hom = s✝.inl

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
s✝ : BinaryCofan a b
⊢ ⋯.hom ≫ ⋯.hom = s✝.inl
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
s✝ : BinaryCofan a b
⊢ ⋯.hom ≫ ⋯.hom = s✝.inr

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
s✝ : BinaryCofan a b
⊢ ⋯.hom ≫ ⋯.hom = s✝.inr
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
s✝ : BinaryCofan a b
m✝ : Subobject.mk (pushout.desc a.arrow b.arrow ⋯) ⟶ s✝.pt
x✝¹ : ⋯.hom ≫ m✝ = s✝.inl
x✝ : ⋯.hom ≫ m✝ = s✝.inr
⊢ m✝ = ⋯.hom

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
a b : Subobject X
s✝ : BinaryCofan a b
m✝ : Subobject.mk (pushout.desc a.arrow b.arrow ⋯) ⟶ s✝.pt
x✝¹ : ⋯.hom ≫ m✝ = s✝.inl
x✝ : ⋯.hom ≫ m✝ = s✝.inr
⊢ m✝ = ⋯.hom
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
⊢ T.free.obj X.A ⟶ T.free.obj (T.obj X.A)

pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
⊢ ?m.21 ≫ FreeCoequalizer.topMap X = 𝟙 (T.free.obj X.A)

pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
⊢ ?m.21 ≫ FreeCoequalizer.bottomMap X = 𝟙 (T.free.obj X.A)

Tactic:
· apply (free T).map (T.η.app X.A)

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
⊢ T.free.map (T.η.app X.A) ≫ FreeCoequalizer.topMap X = 𝟙 (T.free.obj X.A)

C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
⊢ T.free.map (T.η.app X.A) ≫ FreeCoequalizer.bottomMap X = 𝟙 (T.free.obj X.A)
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ Xᘁ.ρ h = X.ρ (inv h)ᘁ

pp: case x
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ SingleObj H

pp: case y
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ SingleObj H

Tactic:
;

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ Xᘁ.ρ h = X.ρ (inv h)ᘁ

case x
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ SingleObj H

case y
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : RightRigidCategory V
h : H
⊢ SingleObj H
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ (ᘁX).ρ h = ᘁX.ρ (inv h)

pp: case x
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ SingleObj H

pp: case y
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ SingleObj H

Tactic:
;

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ (ᘁX).ρ h = ᘁX.ρ (inv h)

case x
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ SingleObj H

case y
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
X : Action V H
inst✝ : LeftRigidCategory V
h : H
⊢ SingleObj H
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: case zero
G : Type u
inst✝ : Group G
g : G
f : Fin 0 → G
x : Fin 1
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G 0).inv.hom) (g, f) x = (g • Fin.partialProd f) x

Tactic:
simp [diagonalSuccIsoTensorTrivial, diagonalOneIsoLeftRegular, Subsingleton.elim x 0,
      ofMulAction_V, types_tensorObj_def, types_tensorUnit_def]

Goal state after:
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: case succ.zero
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).inv.hom) (g, f) = g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).inv.hom) (g, f) 0 = g

Tactic:
;

Goal state after:
case succ.zero
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).inv.hom) (g, f) = g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).inv.hom) (g, f) 0 = g
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
X✝ Y✝ : Action V G
x✝¹ : X✝ ⟶ Y✝
x✝ : Action V G
⊢ ((F.mapAction G).map x✝¹ ▷ (F.mapAction G).obj x✝ ≫ { hom := μ F Y✝.V x✝.V, comm := ⋯ }).hom =
    ({ hom := μ F X✝.V x✝.V, comm := ⋯ } ≫ (F.mapAction G).map (x✝¹ ▷ x✝)).hom

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
X✝ Y✝ : Action V G
x✝¹ : X✝ ⟶ Y✝
x✝ : Action V G
⊢ ((F.mapAction G).map x✝¹ ▷ (F.mapAction G).obj x✝ ≫ { hom := μ F Y✝.V x✝.V, comm := ⋯ }).hom =
    ({ hom := μ F X✝.V x✝.V, comm := ⋯ } ≫ (F.mapAction G).map (x✝¹ ▷ x✝)).hom
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
X✝ Y✝ x✝¹ : Action V G
x✝ : X✝ ⟶ Y✝
⊢ ((F.mapAction G).obj x✝¹ ◁ (F.mapAction G).map x✝ ≫ { hom := μ F x✝¹.V Y✝.V, comm := ⋯ }).hom =
    ({ hom := μ F x✝¹.V X✝.V, comm := ⋯ } ≫ (F.mapAction G).map (x✝¹ ◁ x✝)).hom

Tactic:
;

Goal state after:
V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
X✝ Y✝ x✝¹ : Action V G
x✝ : X✝ ⟶ Y✝
⊢ ((F.mapAction G).obj x✝¹ ◁ (F.mapAction G).map x✝ ≫ { hom := μ F x✝¹.V Y✝.V, comm := ⋯ }).hom =
    ({ hom := μ F x✝¹.V X✝.V, comm := ⋯ } ≫ (F.mapAction G).map (x✝¹ ◁ x✝)).hom