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
C : Type u_3
inst✝ : Category.{v_2, u_3} C
F : C ⥤ Action 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

Tactic:
constructor

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
C : Type u_3
inst✝ : Category.{v_2, u_3} C
F : C ⥤ Action V G
h : PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
⊢ autoParam (∀ {J : Type w₁} [inst : Category.{w₂, w₁} J], PreservesColimitsOfShape J F)
    PreservesColimitsOfSize.preservesColimitsOfShape._autoParam
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
f : X✝ ⟶ Y✝
g : G
⊢ ⇑(ConcreteCategory.hom f.hom) ∘ ⇑(ConcreteCategory.hom (X✝.ρ g)) =
    ⇑(ConcreteCategory.hom (Y✝.ρ g)) ∘ ⇑(ConcreteCategory.hom f.hom)

Tactic:
ext

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
f : X✝ ⟶ Y✝
g : G
x✝ : CV X✝.V
⊢ (⇑(ConcreteCategory.hom f.hom) ∘ ⇑(ConcreteCategory.hom (X✝.ρ g))) x✝ =
    (⇑(ConcreteCategory.hom (Y✝.ρ g)) ∘ ⇑(ConcreteCategory.hom f.hom)) 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
C : Type u_3
inst✝¹ : Category.{v_2, u_3} C
F : C ⥤ Action V G
h : PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
inst✝ : Category.{w₂, w₁} J
⊢ PreservesColimitsOfShape J F

Tactic:
apply Action.preservesColimitsOfShape_of_preserves

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
C : Type u_3
inst✝¹ : Category.{v_2, u_3} C
F : C ⥤ Action V G
h : PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
J : Type w₁
inst✝ : Category.{w₂, w₁} J
⊢ PreservesColimitsOfShape J (F ⋙ forget V 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✝ : HasFiniteLimits V
⊢ PreservesFiniteLimits ((evaluation (SingleObj G) V).obj (SingleObj.star G))

Tactic:
constructor

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : HasFiniteLimits V
⊢ autoParam
    (∀ (J : Type) [inst : SmallCategory J] [FinCategory J],
      PreservesLimitsOfShape J ((evaluation (SingleObj G) V).obj (SingleObj.star G)))
    PreservesFiniteLimits.preservesFiniteLimits._autoParam
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
x✝ : HomSubtype V G X✝ Y✝
⊢ ⟨ConcreteCategory.hom (ConcreteCategory.ofHom ↑x✝), ⋯⟩ = x✝

Tactic:
ext

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
x✝ : HomSubtype V G X✝ Y✝
⊢ ↑⟨ConcreteCategory.hom (ConcreteCategory.ofHom ↑x✝), ⋯⟩ = ↑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✝ : HasFiniteColimits V
⊢ PreservesFiniteColimits ((evaluation (SingleObj G) V).obj (SingleObj.star G))

Tactic:
constructor

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : HasFiniteColimits V
⊢ autoParam
    (∀ (J : Type) [inst : SmallCategory J] [FinCategory J],
      PreservesColimitsOfShape J ((evaluation (SingleObj G) V).obj (SingleObj.star G)))
    PreservesFiniteColimits.preservesFiniteColimits._autoParam
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
x✝ : X✝ ⟶ Y✝
⊢ { hom := ConcreteCategory.ofHom ↑⟨ConcreteCategory.hom x✝.hom, ⋯⟩, comm := ⋯ } = x✝

Tactic:
ext

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
x✝ : X✝ ⟶ Y✝
⊢ ConcreteCategory.hom { hom := ConcreteCategory.ofHom ↑⟨ConcreteCategory.hom x✝.hom, ⋯⟩, comm := ⋯ }.hom =
    ConcreteCategory.hom 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
X Y P✝ Q✝ R✝ : Action V G
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ (f✝ + f'✝) ≫ g✝ = f✝ ≫ g✝ + f'✝ ≫ g✝

Tactic:
ext

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : Preadditive V
X Y P✝ Q✝ R✝ : Action V G
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ ((f✝ + f'✝) ≫ g✝).hom = (f✝ ≫ g✝ + f'✝ ≫ g✝).hom
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝² : Monoid G✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G ≃* H
⊢ MonoidHom.id H = (↑f).comp ↑f.symm

Tactic:
ext

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝² : Monoid G✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G ≃* H
x✝ : H
⊢ (MonoidHom.id H) x✝ = ((↑f).comp ↑f.symm) x✝
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝² : Monoid G✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G ≃* H
⊢ (↑f.symm).comp ↑f = MonoidHom.id G

Tactic:
ext

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝² : Monoid G✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G ≃* H
x✝ : G
⊢ ((↑f.symm).comp ↑f) x✝ = (MonoidHom.id G) 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
X Y P✝ Q✝ R✝ : Action V G
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ f✝ ≫ (g✝ + g'✝) = f✝ ≫ g✝ + f✝ ≫ g'✝

Tactic:
ext

Goal state after:
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_2
inst✝¹ : Monoid G
inst✝ : Preadditive V
X Y P✝ Q✝ R✝ : Action V G
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ (f✝ ≫ (g✝ + g'✝)).hom = (f✝ ≫ g✝ + f✝ ≫ g'✝).hom
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝² : Monoid G✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
X Y : Action V H
g₁ g₂ : X ⟶ Y
h : (res V f).map g₁ = (res V f).map g₂
⊢ g₁ = g₂

Tactic:
ext

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G✝ : Type u_2
inst✝² : Monoid G✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
X Y : Action V H
g₁ g₂ : X ⟶ Y
h : (res V f).map g₁ = (res V f).map g₂
⊢ g₁.hom = 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 : Action V G
x✝ y✝ : R
b✝ : X ⟶ Y
⊢ (x✝ * y✝) • b✝ = x✝ • y✝ • b✝

Tactic:
ext

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✝ y✝ : R
b✝ : X ⟶ Y
⊢ ((x✝ * y✝) • b✝).hom = (x✝ • y✝ • 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
b✝ : X ⟶ Y
⊢ 1 • b✝ = b✝

Tactic:
ext

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.Basic

Goal state before:
pp: case h
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
⊢ (res V f).map { hom := g.hom, comm := ⋯ } = g

Tactic:
ext

Goal state after:
case h
V : Type u_1
inst✝² : Category.{v_1, u_1} V
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
f_surj : Function.Surjective ⇑f
X Y : Action V H
g : (res V f).obj X ⟶ (res V f).obj Y
⊢ ((res V f).map { hom := g.hom, comm := ⋯ }).hom = 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 : Action V G
a✝ : R
⊢ a✝ • 0 = 0

Tactic:
ext

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:
ext

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:
ext

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:
ext

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.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:
ext

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:
ext

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.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 := ⋯ } =
    𝟙 { V := F.obj M.V, ρ := { toFun := fun g ↦ F.map (M.ρ g), map_one' := ⋯, map_mul' := ⋯ } }

Tactic:
ext

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.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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
this✝³ : HasFiniteProducts D
this✝² : HasKernels D
this✝¹ : HasCokernels D
this✝ : IsNormalMonoCategory D
this : IsNormalEpiCategory D
⊢ Abelian D

Tactic:
constructor

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 := F.map f.hom, comm := ⋯ } ≫ { hom := F.map g.hom, comm := ⋯ }

Tactic:
ext

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
W : Type u_2
inst✝² : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝¹ : Monoid G
inst✝ : F.Faithful
X✝ Y✝ : Action V G
a₁✝ a₂✝ : X✝ ⟶ Y✝
eq : (F.mapAction G).map a₁✝ = (F.mapAction G).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext

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
inst✝ : F.Faithful
X✝ Y✝ : Action V G
a₁✝ a₂✝ : X✝ ⟶ Y✝
eq : (F.mapAction G).map a₁✝ = (F.mapAction G).map a₂✝
⊢ a₁✝.hom = a₂✝.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
⊢ ((ObjectProperty.ι IsContinuous ⋙ Action.res V ↑f).obj X).IsContinuous

Tactic:
constructor

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
⊢ Continuous fun p ↦ p.1 • p.2
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) =
    𝟙 ((E.functor.mapAction G).obj X)

Tactic:
ext

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
⊢ ContinuousMonoidHom.id H = (↑f).comp ↑f.symm

Tactic:
ext

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.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
⊢ (MorphismProperty.isomorphisms D).inverseImage L = P.isoModSerre

Tactic:
ext

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✝ : C
f✝ : X✝ ⟶ Y✝
⊢ (MorphismProperty.isomorphisms D).inverseImage L f✝ ↔ P.isoModSerre f✝
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
⊢ (↑f.symm).comp ↑f = ContinuousMonoidHom.id G

Tactic:
ext

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 }) =
    pullback.snd a.arrow b.arrow ≫ underlying.map (s.ι.app { as := WalkingPair.right })

Tactic:
ext

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.Monad.Coequalizer

Goal state before:
pp: 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)

Tactic:
ext

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).f = (𝟙 (T.free.obj X.A)).f
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.map (T.η.app X.A) ≫ FreeCoequalizer.bottomMap X = 𝟙 (T.free.obj X.A)

Tactic:
ext

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.bottomMap X).f = (𝟙 (T.free.obj X.A)).f
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ (beckAlgebraCofork X).π ≫ { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ } = s.π

Tactic:
ext

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
⊢ ((beckAlgebraCofork X).π ≫ { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ }).f = s.π.f
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
m : (beckAlgebraCofork X).pt ⟶ s.pt
hm : (beckAlgebraCofork X).π ≫ m = s.π
⊢ m = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ }

Tactic:
ext

Goal state after:
case refine_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
h₂ : T.map s.π.f ≫ s.pt.a = T.μ.app X.A ≫ s.π.f
m : (beckAlgebraCofork X).pt ⟶ s.pt
hm : (beckAlgebraCofork X).π ≫ m = s.π
⊢ m.f = { f := T.η.app (beckAlgebraCofork X).pt.1 ≫ s.π.f, h := ⋯ }.f