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
X Y : Action V G
⊢ ∀ (P Q R : Action V G) (f : P ⟶ Q) (g g' : Q ⟶ R), f ≫ (g + g') = f ≫ g + f ≫ g'

Tactic:
by

Goal state after:
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 : R
f : X ⟶ Y
⊢ ∀ (g : G), X.ρ g ≫ (r • f.hom) = (r • f.hom) ≫ Y.ρ g

Tactic:
by

Goal state after:
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 : C
f : X ⟶ Y
this✝¹ : L.PreservesEpimorphisms
this✝ : L.EssSurj
Z : C
z : Y ⟶ Z
Z' : C
t : Z ⟶ Z'
ht : P.isoModSerre t
fac : f ≫ z ≫ t = 0
this : IsIso (L.map t)
⊢ L.map (cokernel.π f) ≫ L.map (cokernel.desc f (z ≫ t) fac) ≫ inv (L.map t) = L.map z ≫ eqToHom ⋯

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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 : C
f : X ⟶ Y
⊢ PreservesColimit (parallelPair f 0) L

Tactic:
by

Goal state after:
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:
by

Goal state after:
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✝
⊢ HasKernel f

Tactic:
by

Goal state after:
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:
by

Goal state after:
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✝
⊢ HasCokernel f

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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' ≫ L.map NormalMono.g = 0

Tactic:
by

Goal state after:
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✝
hf : Mono f
⊢ Nonempty (NormalMono f)

Tactic:
by

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

Goal state before:
pp: 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
⊢ ∃ a, (res V f).map a = g

Tactic:
by

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
M : Action V G
⊢ F.map (M.ρ 1) = 1

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

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
M : Action V G
g h : G
⊢ F.map (M.ρ (g * h)) = F.map (M.ρ g) * F.map (M.ρ h)

Tactic:
by

Goal state after:
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 ≫ L.map f' = 0

Tactic:
by

Goal state after:
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✝
hf : Epi f
⊢ Nonempty (NormalEpi f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ F.map (inv (f ≫ g))ᘁ = F.map (inv f)ᘁ ≫ F.map (inv g)ᘁ

Tactic:
by

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✝ : Action V G
f : X✝ ⟶ Y✝
g : G
⊢ { V := F.obj X✝.V, ρ := { toFun := fun g ↦ F.map (X✝.ρ g), map_one' := ⋯, map_mul' := ⋯ } }.ρ g ≫ F.map f.hom =
    F.map f.hom ≫ { V := F.obj Y✝.V, ρ := { toFun := fun g ↦ F.map (Y✝.ρ g), map_one' := ⋯, map_mul' := ⋯ } }.ρ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (𝟙_ (C ⥤ D)).map f ≫
      η_ (F.obj Y)
        ({ obj := fun X ↦ (F.obj X)ᘁ, map := fun {X Y} f ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ }.obj Y) =
    η_ (F.obj X)
        ({ obj := fun X ↦ (F.obj X)ᘁ, map := fun {X Y} f ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ }.obj X) ≫
      (F ⊗ { obj := fun X ↦ (F.obj X)ᘁ, map := fun {X Y} f ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ }).map f

Tactic:
by

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

Goal state after:
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
⊢ Abelian D

Tactic:
by

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

Goal state after:
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
X : Action V G
g h : G
x : ↑((forget₂ (Action V G) TopCat).obj X)
⊢ (g * h) • x = g • h • x

Tactic:
by

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

Goal state after:
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
X : Action V G
x : ↑((forget₂ (Action V G) TopCat).obj X)
⊢ 1 • x = x

Tactic:
by

Goal state after:
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
v : G × ↑((forget₂ (ContAction V H) TopCat).obj X) → H × ↑((forget₂ (ContAction V H) TopCat).obj X) :=
  fun p ↦ (f p.1, p.2)
⊢ Continuous v

Tactic:
by

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
h : F.FullyFaithful
G : Type u_3
inst✝ : Monoid G
X✝ Y✝ : Action V G
f : (F.mapAction G).obj X✝ ⟶ (F.mapAction G).obj Y✝
⊢ X✝ ⟶ Y✝

Tactic:
by

Goal state after:
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
⊢ PreservesFiniteLimits L

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : RightRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ ({ obj := fun X ↦ (F.obj X)ᘁ, map := fun {X Y} f ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ } ⊗ F).map f ≫
      ε_ (F.obj Y)
        ({ obj := fun X ↦ (F.obj X)ᘁ, map := fun {X Y} f ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ }.obj Y) =
    ε_ (F.obj X)
        ({ obj := fun X ↦ (F.obj X)ᘁ, map := fun {X Y} f ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ }.obj X) ≫
      (𝟙_ (C ⥤ D)).map f

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
⊢ PreservesFiniteColimits L

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : LeftRigidCategory D
F : C ⥤ D
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (ᘁF.map (inv (f ≫ g))) = (ᘁF.map (inv f)) ≫ ᘁF.map (inv g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
X Y : C
eval : Y ⊗ X ⟶ 𝟙_ C
coeval : 𝟙_ C ⟶ X ⊗ Y
inst✝ : ExactPairing (F.obj X) (F.obj Y)
map_eval : F.map eval = δ F Y X ≫ ε_ (F.obj X) (F.obj Y) ≫ ε F
map_coeval : F.map coeval = η F ≫ η_ (F.obj X) (F.obj Y) ≫ μ F X Y
⊢ F.map (Y ◁ coeval ≫ (α_ Y X Y).inv ≫ eval ▷ Y) = F.map ((ρ_ Y).hom ≫ (λ_ Y).inv)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
X Y : C
eval : Y ⊗ X ⟶ 𝟙_ C
coeval : 𝟙_ C ⟶ X ⊗ Y
inst✝ : ExactPairing (F.obj X) (F.obj Y)
map_eval : F.map eval = δ F Y X ≫ ε_ (F.obj X) (F.obj Y) ≫ ε F
map_coeval : F.map coeval = η F ≫ η_ (F.obj X) (F.obj Y) ≫ μ F X Y
⊢ F.map (coeval ▷ X ≫ (α_ X Y X).hom ≫ X ◁ eval) = F.map ((λ_ X).hom ≫ (ρ_ X).inv)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : MonoidalCategory C
inst✝⁴ : MonoidalCategory D
F : C ⥤ D
inst✝³ : F.Monoidal
inst✝² : F.Full
inst✝¹ : F.Faithful
X Y : C
inst✝ : ExactPairing (F.obj X) (F.obj Y)
⊢ F.map (F.preimage (δ F Y X ≫ ε_ (F.obj X) (F.obj Y) ≫ ε F)) = δ F Y X ≫ ε_ (F.obj X) (F.obj Y) ≫ ε F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : MonoidalCategory C
inst✝⁴ : MonoidalCategory D
F : C ⥤ D
inst✝³ : F.Monoidal
inst✝² : F.Full
inst✝¹ : F.Faithful
X Y : C
inst✝ : ExactPairing (F.obj X) (F.obj Y)
⊢ F.map (F.preimage (η F ≫ η_ (F.obj X) (F.obj Y) ≫ μ F X Y)) = η F ≫ η_ (F.obj X) (F.obj Y) ≫ μ F X Y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.IsEquivalence
X : C
inst✝ : HasLeftDual (F.obj X)
⊢ ExactPairing (G.obj ᘁ(F.obj X)) X

Tactic:
by

Goal state after:
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 f' : G →ₜ* H
h : f = f'
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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : LeftRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (𝟙_ (C ⥤ D)).map f ≫
      η_ ({ obj := fun X ↦ ᘁ(F.obj X), map := fun {X Y} f ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ }.obj Y)
        (F.obj Y) =
    η_ ({ obj := fun X ↦ ᘁ(F.obj X), map := fun {X Y} f ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ }.obj X)
        (F.obj X) ≫
      ({ obj := fun X ↦ ᘁ(F.obj X), map := fun {X Y} f ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ } ⊗ F).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : F.IsEquivalence
X : C
inst✝ : HasRightDual (F.obj X)
⊢ ExactPairing X (G.obj (F.obj X)ᘁ)

Tactic:
by

Goal state after:
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✝ f' : G →ₜ* H
h : f✝ = f'
X✝ Y✝ : ContAction V H
f : X✝ ⟶ Y✝
⊢ ((res V f✝).map f ≫ (ObjectProperty.isoMk IsContinuous (mkIso (Iso.refl ((res V f✝).obj Y✝).obj.V) ⋯)).hom).hom.hom =
    ((ObjectProperty.isoMk IsContinuous (mkIso (Iso.refl ((res V f✝).obj X✝).obj.V) ⋯)).hom ≫ (res V f').map f).hom.hom

Tactic:
by

Goal state after:
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 : C
f : X ⟶ Y
⊢ IsIso (L.map f) ↔ P.isoModSerre f

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Groupoid C
inst✝² : Category.{v_1, u_2} D
inst✝¹ : MonoidalCategory D
inst✝ : LeftRigidCategory D
F : C ⥤ D
X Y : C
f : X ⟶ Y
⊢ (F ⊗ { obj := fun X ↦ ᘁ(F.obj X), map := fun {X Y} f ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ }).map f ≫
      ε_ ({ obj := fun X ↦ ᘁ(F.obj X), map := fun {X Y} f ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ }.obj Y)
        (F.obj Y) =
    ε_ ({ obj := fun X ↦ ᘁ(F.obj X), map := fun {X Y} f ↦ ᘁF.map (inv f), map_id := ⋯, map_comp := ⋯ }.obj X)
        (F.obj X) ≫
      (𝟙_ (C ⥤ D)).map f

Tactic:
by

Goal state after:
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:
by

Goal state after: