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

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

Tactic:
induction x using Fin.cases
    <;> simp_all [diagonalSuccIsoTensorTrivial, types_tensorObj_def]

Goal state after:
case succ.zero
G : Type u
inst✝ : Group G
n : ℕ
f : Fin (n + 1 + 1) → G
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
⊢ (Fin.consEquiv fun x ↦ G)
      ({ toFun := fun g ↦ (g.1, (ConcreteCategory.hom ((leftRegular G ⊗ trivial G (Fin n → G)).ρ g.1⁻¹)) g.2),
            invFun := fun g ↦ (g.1, (ConcreteCategory.hom ((leftRegular G ⊗ trivial G (Fin n → G)).ρ g.1)) g.2),
            left_inv := ⋯, right_inv := ⋯ }
          (((Fin.consEquiv fun a ↦ G).symm f).1, ((Fin.consEquiv fun a ↦ G).symm f).2 0, fun i ↦
            (((Fin.consEquiv fun a ↦ G).symm f).2 i.castSucc)⁻¹ * ((Fin.consEquiv fun a ↦ G).symm f).2 i.succ)).2
      0 =
    (f 0)⁻¹ * f 1

case succ.succ
G : Type u
inst✝ : Group G
n : ℕ
f : Fin (n + 1 + 1) → G
i✝ : Fin n
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
⊢ (Fin.consEquiv fun x ↦ G)
      ({ toFun := fun g ↦ (g.1, (ConcreteCategory.hom ((leftRegular G ⊗ trivial G (Fin n → G)).ρ g.1⁻¹)) g.2),
            invFun := fun g ↦ (g.1, (ConcreteCategory.hom ((leftRegular G ⊗ trivial G (Fin n → G)).ρ g.1)) g.2),
            left_inv := ⋯, right_inv := ⋯ }
          (((Fin.consEquiv fun a ↦ G).symm f).1, ((Fin.consEquiv fun a ↦ G).symm f).2 0, fun i ↦
            (((Fin.consEquiv fun a ↦ G).symm f).2 i.castSucc)⁻¹ * ((Fin.consEquiv fun a ↦ G).symm f).2 i.succ)).2
      i✝.succ =
    (f i✝.castSucc.succ)⁻¹ * f i✝.succ.succ
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: case succ.succ
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
i : Fin (n + 1)
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).inv.hom) (g, f) i.succ = (g • Fin.partialProd f) i.succ

Tactic:
| succ i =>

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

Goal state before:
pp: case refine_2
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))
this : ∀ (Y : B), Mono (adj₁.unit.app Y)
⊢ ↑((h X).lift' s.ι ⋯) ≫ (Fork.ofι (adj₁.unit.app X) ⋯).ι = s.ι

Tactic:
apply ((h X).lift' s.ι _).2

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✝ : X✝ ⟶ Y✝
⊢ ((Sigma.desc fun g ↦ Sigma.ι (fun x ↦ x✝) (g ≫ f✝)) ≫ Sigma.desc fun h ↦ f ≫ Sigma.ι (fun x ↦ d₂) h) =
    (Sigma.desc fun h ↦ f ≫ Sigma.ι (fun x ↦ d₂) h) ≫ Sigma.desc fun g ↦ Sigma.ι (fun x ↦ d₂) (g ≫ f✝)

Tactic:
ext

Goal state after:
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✝ : X✝ ⟶ Y✝
b✝ : c ⟶ X✝
⊢ (Sigma.ι (fun x ↦ x✝) b✝ ≫
      (Sigma.desc fun g ↦ Sigma.ι (fun x ↦ x✝) (g ≫ f✝)) ≫ Sigma.desc fun h ↦ f ≫ Sigma.ι (fun x ↦ d₂) h) =
    Sigma.ι (fun x ↦ x✝) b✝ ≫
      (Sigma.desc fun h ↦ f ≫ Sigma.ι (fun x ↦ d₂) h) ≫ Sigma.desc fun g ↦ Sigma.ι (fun x ↦ d₂) (g ≫ f✝)
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:
ext

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

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✝² 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).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 := ⋯ }).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✝ : 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:
ext

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

Goal state after:
case mp
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)

case mpr
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
⊢ (∀ (c : C), Mono (η.app c)) → Mono η
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:
ext

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

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.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✝).hom =
    ((F.mapAction G).map (x✝¹ ▷ x✝) ≫ { hom := δ F Y✝.V x✝.V, comm := ⋯ }).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.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:
ext

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.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✝).hom =
    ((F.mapAction G).map (x✝¹ ◁ x✝) ≫ { hom := δ F x✝¹.V Y✝.V, comm := ⋯ }).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.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:
ext

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.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).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 := ⋯ }).hom
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:
constructor

Goal state after:
case mp
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)

case mpr
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
⊢ (∀ (c : C), Epi (η.app c)) → Epi η
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✝ : Action V G
⊢ (λ_ ((F.mapAction G).obj x✝)).inv =
    (F.mapAction G).map (λ_ x✝).inv ≫
      { hom := δ F (𝟙_ (Action V G)).V x✝.V, comm := ⋯ } ≫ { hom := η F, comm := ⋯ } ▷ (F.mapAction G).obj x✝

Tactic:
ext

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.OplaxMonoidal
x✝ : Action V G
⊢ (λ_ ((F.mapAction G).obj x✝)).inv.hom =
    ((F.mapAction G).map (λ_ x✝).inv ≫
        { hom := δ F (𝟙_ (Action V G)).V x✝.V, comm := ⋯ } ≫ { hom := η F, comm := ⋯ } ▷ (F.mapAction G).obj 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.OplaxMonoidal
x✝ : Action V G
⊢ (ρ_ ((F.mapAction G).obj x✝)).inv =
    (F.mapAction G).map (ρ_ x✝).inv ≫
      { hom := δ F x✝.V (𝟙_ (Action V G)).V, comm := ⋯ } ≫ (F.mapAction G).obj x✝ ◁ { hom := η F, comm := ⋯ }

Tactic:
ext

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.OplaxMonoidal
x✝ : Action V G
⊢ (ρ_ ((F.mapAction G).obj x✝)).inv.hom =
    ((F.mapAction G).map (ρ_ x✝).inv ≫
        { hom := δ F x✝.V (𝟙_ (Action V G)).V, comm := ⋯ } ≫ (F.mapAction G).obj x✝ ◁ { hom := η F, comm := ⋯ }).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.Monoidal
⊢ ε (F.mapAction G) ≫ η (F.mapAction G) = 𝟙 (𝟙_ (Action W G))

Tactic:
ext

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.Monoidal
⊢ (ε (F.mapAction G) ≫ η (F.mapAction G)).hom = (𝟙 (𝟙_ (Action W G))).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.Monoidal
⊢ η (F.mapAction G) ≫ ε (F.mapAction G) = 𝟙 ((F.mapAction G).obj (𝟙_ (Action V G)))

Tactic:
ext

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.Monoidal
⊢ (η (F.mapAction G) ≫ ε (F.mapAction G)).hom = (𝟙 ((F.mapAction G).obj (𝟙_ (Action V G)))).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.Monoidal
x✝¹ x✝ : Action V G
⊢ μ (F.mapAction G) x✝¹ x✝ ≫ δ (F.mapAction G) x✝¹ x✝ = 𝟙 ((F.mapAction G).obj x✝¹ ⊗ (F.mapAction G).obj x✝)

Tactic:
ext

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.Monoidal
x✝¹ x✝ : Action V G
⊢ (μ (F.mapAction G) x✝¹ x✝ ≫ δ (F.mapAction G) x✝¹ x✝).hom = (𝟙 ((F.mapAction G).obj x✝¹ ⊗ (F.mapAction G).obj x✝)).hom
Module: Mathlib.CategoryTheory.Adjunction.Triple

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
adj : F ⋙ G ⊣ H ⋙ G := t.adj₁.comp t.adj₂
⊢ IsIso t.adj₁.unit ↔ IsIso t.adj₂.counit

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
adj : F ⋙ G ⊣ H ⋙ G := ⋯
⊢ IsIso t.adj₁.unit → IsIso t.adj₂.counit

case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
adj : F ⋙ G ⊣ H ⋙ G := ⋯
⊢ IsIso t.adj₂.counit → IsIso t.adj₁.unit
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.Monoidal
x✝¹ x✝ : Action V G
⊢ δ (F.mapAction G) x✝¹ x✝ ≫ μ (F.mapAction G) x✝¹ x✝ = 𝟙 ((F.mapAction G).obj (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
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.Monoidal
x✝¹ x✝ : Action V G
⊢ (δ (F.mapAction G) x✝¹ x✝ ≫ μ (F.mapAction G) x✝¹ x✝).hom = (𝟙 ((F.mapAction G).obj (x✝¹ ⊗ x✝))).hom
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
inst✝ : HasReflexiveCoequalizers A
h✝ : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ (adj₁.homEquiv (U.obj X) (R.obj Y')).symm
      ((adj₂.homEquiv (U.obj X) Y)
          ↑((Cofork.IsColimit.homIso
                (colimit.isColimit (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X))) Y)
              h) ≫
        (R ⋙ U).map g) =
    ↑((Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y))
          ((Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y)).symm
            ⟨(adj₁.homEquiv (U.obj X) (R.obj Y)).symm
                ((adj₂.homEquiv (U.obj X) Y)
                  ↑((Cofork.IsColimit.homIso
                        (colimit.isColimit
                          (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)))
                        Y)
                      h)),
              ⋯⟩)) ≫
      R.map g

Tactic:
simp_rw [Functor.comp_map]

Goal state after:
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
inst✝ : HasReflexiveCoequalizers A
h✝ : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
Y Y' : A
g : Y ⟶ Y'
h : constructLeftAdjointObj R F' adj₁ adj₂ X ⟶ Y
⊢ (adj₁.homEquiv (U.obj X) (R.obj Y')).symm
      ((adj₂.homEquiv (U.obj X) Y)
          ↑((Cofork.IsColimit.homIso
                (colimit.isColimit (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X))) Y)
              h) ≫
        U.map (R.map g)) =
    ↑((Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y))
          ((Cofork.IsColimit.homIso (counitCoequalises adj₁ h✝ X) (R.obj Y)).symm
            ⟨(adj₁.homEquiv (U.obj X) (R.obj Y)).symm
                ((adj₂.homEquiv (U.obj X) Y)
                  ↑((Cofork.IsColimit.homIso
                        (colimit.isColimit
                          (parallelPair (F'.map (U.map (adj₁.counit.app X))) (otherMap R F' adj₁ adj₂ X)))
                        Y)
                      h)),
              ⋯⟩)) ≫
      R.map g
Module: Mathlib.CategoryTheory.Adjunction.Triple

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : G.Full
inst✝ : G.Faithful
⊢ t.op.rightToLeft = NatTrans.op t.rightToLeft

Tactic:
ext

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : G.Full
inst✝ : G.Faithful
x✝ : Cᵒᵖ
⊢ t.op.rightToLeft.app x✝ = (NatTrans.op t.rightToLeft).app x✝
Module: Mathlib.CategoryTheory.Adjunction.Triple

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : H.Full
inst✝ : H.Faithful
⊢ t.op.leftToRight = NatTrans.op t.leftToRight

Tactic:
ext

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : H.Full
inst✝ : H.Faithful
x✝ : Cᵒᵖ
⊢ t.op.leftToRight.app x✝ = (NatTrans.op t.leftToRight).app x✝
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
e₁ : x = y
⊢ eqToHomTransIso e₁ ⋯ = (ρ_ (eqToHom e₁)).symm

Tactic:
ext

Goal state after:
B : Type u
inst✝ : Bicategory B
x y : B
e₁ : x = y
⊢ (eqToHomTransIso e₁ ⋯).hom = (ρ_ (eqToHom e₁)).symm.hom
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
e₁ : x = y
⊢ eqToHomTransIso ⋯ e₁ = (λ_ (eqToHom e₁)).symm

Tactic:
ext

Goal state after:
B : Type u
inst✝ : Bicategory B
x y : B
e₁ : x = y
⊢ (eqToHomTransIso ⋯ e₁).hom = (λ_ (eqToHom e₁)).symm.hom
Module: Mathlib.CategoryTheory.Bicategory.Free

Goal state before:
pp: case mk
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
f✝ : Quot Rel
η : Hom₂ f g
⊢ Quot.map₂ Hom₂.vcomp ⋯ ⋯ (Quot.mk Rel η) (Quot.mk Rel (Hom₂.id g)) = Quot.mk Rel η

Tactic:
exact Quot.sound (Rel.comp_id η)

Goal state after: