mathlib-initiative/mathlib-tactics huggingface dataset:
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✝
V : Type u_5
W : Type u_6
inst✝⁹ : Category.{v_2, u_5} V
FV : V → V → Type u_7
CV : V → Type u_8
inst✝⁸ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝⁷ : ConcreteCategory V FV
inst✝⁶ : HasForget₂ V TopCat
inst✝⁵ : Category.{v_3, u_6} W
FW : W → W → Type u_9
CW : W → Type u_10
inst✝⁴ : (X Y : W) → FunLike (FW X Y) (CW X) (CW Y)
inst✝³ : ConcreteCategory W FW
inst✝² : HasForget₂ W TopCat
G : Type u_11
inst✝¹ : Monoid G
inst✝ : TopologicalSpace G
F F' : V ⥤ W
e : F ≅ F'
H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous
H' : ∀ (X : ContAction V G), ((F'.mapAction G).obj X.obj).IsContinuous
X : ContAction V G
⊢ ∀ (g : G),
    ((mapContAction G F H).obj X).obj.ρ g ≫ (e.app X.obj.V).hom =
      (e.app X.obj.V).hom ≫ ((mapContAction G F' H').obj X).obj.ρ 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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
⊢ PreservesFiniteLimits (L ⋙ G) ↔ PreservesFiniteLimits 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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
this✝ : Abelian D := abelian L P
this : PreservesFiniteColimits L
x✝ : PreservesFiniteColimits (L ⋙ G)
⊢ (L ⋙ G).Additive

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
G : D ⥤ E
⊢ PreservesFiniteColimits (L ⋙ G) ↔ PreservesFiniteColimits 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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
⊢ exactFunctor C E (L ⋙ G) ↔ exactFunctor D E 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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G✝ : D ⥤ E
G : D ⥤ₑ E
⊢ exactFunctor C E (((exactFunctor D E).ι ⋙ (Functor.whiskeringLeft C D E).obj L).obj 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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
⊢ (whiskeringLeft L P E).essImage = fun G ↦ P.isoModSerre.IsInvertedBy G.obj

Tactic:
by

Goal state after:
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:
simp [pullback.condition]

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

Goal state after:
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
⊢ pushout.desc (underlying.map (s.ι.app { as := WalkingPair.left }))
        (underlying.map (s.ι.app { as := WalkingPair.right })) ⋯ ≫
      (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }).arrow =
    pushout.desc a.arrow b.arrow ⋯

Tactic:
by

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

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

Goal state after:
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),
    ⋯.hom ≫ m = s.inl → ⋯.hom ≫ m = s.inr → m = ⋯.hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Adhesive C
X : C
F : Discrete WalkingPair ⥤ Subobject X
⊢ HasColimit F

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
H : D ⥤ E
J : Type u
inst✝³ : Category.{v, u} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : G.Full
inst✝ : G.Faithful
⊢ PreservesColimitsOfShape J H ↔ PreservesColimitsOfShape J (F ⋙ H)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
⊢ IsReflexivePair (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
H : D ⥤ E
inst✝² : HasColimitsOfSize.{v, u, v₁, u₁} C
inst✝¹ : G.Full
inst✝ : G.Faithful
⊢ PreservesColimitsOfSize.{v, u, v₂, v₃, u₂, u₃} H ↔ PreservesColimitsOfSize.{v, u, v₁, v₃, u₁, u₃} (F ⋙ H)

Tactic:
by

Goal state after:
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
inst✝¹ : MonoidalCategory V
inst✝ : BraidedCategory V
X Y : Action V G
g : G
⊢ (X ⊗ Y).ρ g ≫ (β_ X.V Y.V).hom = (β_ X.V Y.V).hom ≫ (Y ⊗ X).ρ g

Tactic:
by

Goal state after:
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
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
inst✝ : RightRigidCategory V
⊢ RightRigidCategory (SingleObj H ⥤ V)

Tactic:
by

Goal state after:
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
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
inst✝ : LeftRigidCategory V
⊢ LeftRigidCategory (SingleObj H ⥤ V)

Tactic:
by

Goal state after:
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
inst✝² : MonoidalCategory V
H : Type u_3
inst✝¹ : Group H
inst✝ : RigidCategory V
⊢ RigidCategory (SingleObj H ⥤ V)

Tactic:
by

Goal state after:
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.ρ h⁻¹ᘁ

Tactic:
by

Goal state after:
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.ρ h⁻¹

Tactic:
by

Goal state after:
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✝
G : Type u
inst✝ : Group G
X : Action (Type u) G
x✝ : (leftRegular G ⊗ X).V
⊢ ((fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1)) g.2))
        ((fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2)) x✝)).2 =
    x✝.2

Tactic:
by

Goal state after:
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✝
G : Type u
inst✝ : Group G
X : Action (Type u) G
x✝ : (leftRegular G ⊗ trivial G X.V).V
⊢ ((fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2))
        ((fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1)) g.2)) x✝)).2 =
    x✝.2

Tactic:
by

Goal state after:
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✝
G : Type u
inst✝ : Group G
X : Action (Type u) G
x✝ : G
⊢ (leftRegular G ⊗ X).ρ x✝ ≫
      { toFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2),
            invFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1)) g.2), left_inv := ⋯, right_inv := ⋯ }.toIso.hom =
    { toFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1⁻¹)) g.2),
            invFun := fun g ↦ (g.1, (ConcreteCategory.hom (X.ρ g.1)) g.2), left_inv := ⋯, right_inv := ⋯ }.toIso.hom ≫
      (leftRegular G ⊗ trivial G X.V).ρ x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
⊢ { l //
    (beckAlgebraCofork X).π ≫ l = s.π ∧
      ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt}, (beckAlgebraCofork X).π ≫ m = s.π → m = l }

Tactic:
by

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

Goal state before:
pp: G : Type u
inst✝ : Group G
n : ℕ
f : Fin (n + 1) → G
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)

Tactic:
by

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

Goal state before:
pp: G : Type u
inst✝ : Group G
n : ℕ
g : G
f : Fin n → G
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).inv.hom) (g, f) = g • Fin.partialProd f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
x✝ d₂ : D
f : x✝ ⟶ d₂
⊢ ∀ ⦃X Y : C⦄ (f_1 : X ⟶ Y),
    ({ obj := fun t ↦ ∐ fun x ↦ x✝, map := fun {X Y} f ↦ Sigma.desc fun g ↦ Sigma.ι (fun x ↦ x✝) (g ≫ f), map_id := ⋯,
              map_comp := ⋯ }.map
          f_1 ≫
        Sigma.desc fun h ↦ f ≫ Sigma.ι (fun x ↦ d₂) h) =
      (Sigma.desc fun h ↦ f ≫ Sigma.ι (fun x ↦ d₂) h) ≫
        { obj := fun t ↦ ∐ fun x ↦ d₂, map := fun {X Y} f ↦ Sigma.desc fun g ↦ Sigma.ι (fun x ↦ d₂) (g ≫ f),
              map_id := ⋯, map_comp := ⋯ }.map
          f_1

Tactic:
by

Goal state after:
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
g : G
⊢ (𝟙_ (Action W G)).ρ g ≫ ε F = ε F ≫ ((F.mapAction G).obj (𝟙_ (Action V G))).ρ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
⊢ { l //
    (Cofork.ofπ (adj₁.counit.app X) ⋯).π ≫ l = s.π ∧
      ∀ {m : (Cofork.ofπ (adj₁.counit.app X) ⋯).pt ⟶ s.pt}, (Cofork.ofπ (adj₁.counit.app X) ⋯).π ≫ m = s.π → m = l }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
⊢ { l //
    (Cofork.ofπ (adj₁.counit.app X) ⋯).π ≫ l = s.π ∧
      ∀ {m : (Cofork.ofπ (adj₁.counit.app X) ⋯).pt ⟶ s.pt}, (Cofork.ofπ (adj₁.counit.app X) ⋯).π ≫ m = s.π → m = l }

Tactic:
by
    have := fun Y ↦ h Y |>.epi
    refine ⟨((h X).desc' s.π ?_).1, ?_, ?_⟩
    · rw [← cancel_epi (adj₁.counit.app (h X).W)]
      rw [← adj₁.counit_naturality_assoc (h X).left]
      dsimp
      rw [← dsimp% s.condition, ← F.map_comp_assoc, ← U.map_comp, RegularEpi.w, U.map_comp,
        F.map_comp_assoc, s.condition, ← adj₁.counit_naturality_assoc (h X).right]
    · apply ((h X).desc' s.π _).2
    · intro m hm
      rw [← cancel_epi (adj₁.counit.app X)]
      apply hm.trans ((h _).desc' s.π _).2.symm

Goal state after:
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 := μ F X✝.V x✝.V, comm := ⋯ } ≫ (F.mapAction G).map (x✝¹ ▷ x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
h : (X : B) → RegularMono (adj₁.unit.app X)
X : B
s : Fork (U.map (F.map (adj₁.unit.app X))) (adj₁.unit.app ((F ⋙ U).obj X))
⊢ { l //
    l ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι ∧
      ∀ {m : s.pt ⟶ (Fork.ofι (adj₁.unit.app X) ⋯).pt}, m ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι → m = l }

Tactic:
by

Goal state after:
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 := μ F x✝¹.V X✝.V, comm := ⋯ } ≫ (F.mapAction G).map (x✝¹ ◁ x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (adj₁.unit.app (U.obj X)) ≫ F'.map (U.map (adj₁.counit.app X)) = 𝟙 (F'.obj (U.obj ((𝟭 B).obj X)))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
X : B
⊢ U'.map (F.map (adj₁.unit.app X)) ≫ U'.map (adj₁.counit.app (F.obj X)) = 𝟙 (U'.obj (F.obj ((𝟭 B).obj X)))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
⊢ Function.LeftInverse (fun f ↦ { app := fun x ↦ Sigma.desc fun h ↦ f ≫ F.map h, naturality := ⋯ }) fun f ↦
    Sigma.ι (fun x ↦ d) (𝟙 c) ≫ f.app c

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
X : B
⊢ otherMap L U' adj₁ adj₂ X ≫ U'.map (adj₁.counit.app (F.obj X)) = 𝟙 (U'.obj (F.obj ((𝟭 B).obj X)))

Tactic:
by

Goal state after:
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✝² x✝¹ x✝ : Action V G
⊢ { hom := μ F x✝².V x✝¹.V, comm := ⋯ } ▷ (F.mapAction G).obj x✝ ≫
      { hom := μ F (x✝² ⊗ x✝¹).V x✝.V, comm := ⋯ } ≫ (F.mapAction G).map (α_ x✝² x✝¹ x✝).hom =
    (α_ ((F.mapAction G).obj x✝²) ((F.mapAction G).obj x✝¹) ((F.mapAction G).obj x✝)).hom ≫
      (F.mapAction G).obj x✝² ◁ { hom := μ F x✝¹.V x✝.V, comm := ⋯ } ≫ { hom := μ F x✝².V (x✝¹ ⊗ x✝).V, comm := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
f : d ⟶ ((evaluation C D).obj c).obj F
⊢ (fun f ↦ Sigma.ι (fun x ↦ d) (𝟙 c) ≫ f.app c)
      ((fun f ↦ { app := fun x ↦ Sigma.desc fun h ↦ f ≫ F.map h, naturality := ⋯ }) f) =
    f

Tactic:
by

Goal state after:
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✝ : Action V G
⊢ (λ_ ((F.mapAction G).obj x✝)).hom =
    { hom := ε F, comm := ⋯ } ▷ (F.mapAction G).obj x✝ ≫
      { hom := μ F (𝟙_ (Action V G)).V x✝.V, comm := ⋯ } ≫ (F.mapAction G).map (λ_ x✝).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
X : B
⊢ F'.map (adj₁.unit.app (U.obj X)) ≫ otherMap R F' adj₁ adj₂ X = 𝟙 (F'.obj (U.obj ((𝟭 B).obj X)))

Tactic:
by

Goal state after:
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✝ : Action V G
⊢ (ρ_ ((F.mapAction G).obj x✝)).hom =
    (F.mapAction G).obj x✝ ◁ { hom := ε F, comm := ⋯ } ≫
      { hom := μ F x✝.V (𝟙_ (Action V G)).V, comm := ⋯ } ≫ (F.mapAction G).map (ρ_ x✝).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Mono η ↔ ∀ (c : C), Mono (η.app c)

Tactic:
by

Goal state after:
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.OplaxMonoidal
g : G
⊢ ((F.mapAction G).obj (𝟙_ (Action V G))).ρ g ≫ η F = η F ≫ (𝟙_ (Action W G)).ρ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
f : ((evaluation C D).obj c).obj F ⟶ d
⊢ (fun f ↦ f.app c ≫ Pi.π (fun x ↦ d) (𝟙 c))
      ((fun f ↦ { app := fun x ↦ Pi.lift fun g ↦ F.map g ≫ f, naturality := ⋯ }) f) =
    f

Tactic:
by

Goal state after:
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.OplaxMonoidal
X✝ Y✝ : Action V G
x✝¹ : X✝ ⟶ Y✝
x✝ : Action V G
⊢ { hom := δ F X✝.V x✝.V, comm := ⋯ } ≫ (F.mapAction G).map x✝¹ ▷ (F.mapAction G).obj x✝ =
    (F.mapAction G).map (x✝¹ ▷ x✝) ≫ { hom := δ F Y✝.V x✝.V, comm := ⋯ }

Tactic:
by

Goal state after:
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.OplaxMonoidal
X✝ Y✝ x✝¹ : Action V G
x✝ : X✝ ⟶ Y✝
⊢ { hom := δ F x✝¹.V X✝.V, comm := ⋯ } ≫ (F.mapAction G).obj x✝¹ ◁ (F.mapAction G).map x✝ =
    (F.mapAction G).map (x✝¹ ◁ x✝) ≫ { hom := δ F x✝¹.V Y✝.V, comm := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
c : C
F : C ⥤ D
d : D
⊢ Function.RightInverse (fun f ↦ f.app c ≫ Pi.π (fun x ↦ d) (𝟙 c)) fun f ↦
    { app := fun x ↦ Pi.lift fun g ↦ F.map g ≫ f, naturality := ⋯ }

Tactic:
by

Goal state after:
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.OplaxMonoidal
x✝² x✝¹ x✝ : Action V G
⊢ { hom := δ F (x✝² ⊗ x✝¹).V x✝.V, comm := ⋯ } ≫
      { hom := δ F x✝².V x✝¹.V, comm := ⋯ } ▷ (F.mapAction G).obj x✝ ≫
        (α_ ((F.mapAction G).obj x✝²) ((F.mapAction G).obj x✝¹) ((F.mapAction G).obj x✝)).hom =
    (F.mapAction G).map (α_ x✝² x✝¹ x✝).hom ≫
      { hom := δ F x✝².V (x✝¹ ⊗ x✝).V, comm := ⋯ } ≫ (F.mapAction G).obj x✝² ◁ { hom := δ F x✝¹.V x✝.V, comm := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasProductsOfShape (a ⟶ b) D
F G : C ⥤ D
η : F ⟶ G
⊢ Epi η ↔ ∀ (c : C), Epi (η.app c)

Tactic:
by

Goal state after: