mathlib-initiative/mathlib-tactics huggingface dataset:
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:
simp

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

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

Tactic:
simp

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✝ : G
⊢ ((↑f.symm).comp ↑f) x✝ = (ContinuousMonoidHom.id G) x✝

Tactic:
simp

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✝
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:
simp

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

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

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

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
x✝ : (leftRegular G ⊗ X).V
⊢ (ConcreteCategory.hom
          (((leftRegular G).ρ x✝¹ ⊗ₘ 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
      x✝ =
    (ConcreteCategory.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).ρ x✝¹ ⊗ₘ (trivial G X.V).ρ x✝¹))).toFun
      x✝

Tactic:
simp [types_tensorObj_def]

Goal state after:
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
x✝ : (leftRegular G ⊗ X).V
⊢ (ConcreteCategory.hom (X.ρ x✝.1⁻¹)) x✝.2 = (ConcreteCategory.hom (1 x✝¹)) ((ConcreteCategory.hom (X.ρ x✝.1⁻¹)) x✝.2)
Module: Mathlib.CategoryTheory.Action.Monoidal

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

Tactic:
simp

Goal state after:
case succ.zero
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).inv.hom) (g, f) = g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).inv.hom) (g, f) 0 = g
Module: Mathlib.CategoryTheory.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✝
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✝)

Tactic:
simp

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

Tactic:
simp

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

Tactic:
simp

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

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
⊢ adj₂.unit.app (U'.1 (F.obj X)) ≫
      U'.map
        (F.map (adj₁.unit.app (L.1 (U'.1 (F.obj X))) ≫ U.map (adj₂.counit.app (F.obj X))) ≫ adj₁.counit.app (F.obj X)) =
    𝟙 (U'.obj (F.obj ((𝟭 B).obj X)))

Tactic:
simp

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

Tactic:
simp

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

Tactic:
simp

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

Tactic:
simp

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

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

Tactic:
simp

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

Tactic:
simp

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

Tactic:
simp

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

Tactic:
simp

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'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
f : Y ⟶ U'.obj (F.obj X)
⊢ adj₂.unit.app Y ≫
        U'.map ((L ⋙ F).map f) ≫
          U'.map (F.map (adj₁.unit.app (L.1 (U'.1 (F.obj X))) ≫ U.map (adj₂.counit.app (F.obj X)))) =
      f ≫ U'.map (F.map (adj₁.unit.app X)) ↔
    adj₂.unit.app Y ≫ U'.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map ((L ⋙ F).map f ≫ adj₂.counit.app (F.obj X)))) =
      (adj₂.homEquiv Y (F.obj (U.obj (F.obj X))))
        ((adj₂.homEquiv Y (F.obj ((F ⋙ U).obj X))).symm (f ≫ U'.map (F.map (adj₁.unit.app X))))

Tactic:
simp

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

Tactic:
simp

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'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
g : F.obj (L.obj Y) ⟶ F.obj X
⊢ adj₁.unit.app ((𝟭 B).obj (L.obj Y)) ≫ U.map (g ≫ F.map (adj₁.unit.app X)) =
      adj₁.unit.app ((𝟭 B).obj (L.obj Y)) ≫ U.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map g)) ↔
    (adj₁.unit.app (L.obj Y) ≫ U.map g) ≫ U.map (F.map (adj₁.unit.app X)) =
      (adj₁.unit.app (L.obj Y) ≫ U.map g) ≫ adj₁.unit.app (U.obj (F.obj X))

Tactic:
simp

Goal state after:
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
x✝ : Cᵒᵖ
⊢ (F.op.leftUnitor.inv ≫
          whiskerRight t.op.adj₁.unit F.op ≫
            (H.op.associator G.op F.op).hom ≫ inv (H.op.whiskerLeft t.op.adj₂.unit) ≫ H.op.rightUnitor.hom).app
      x✝ =
    (NatTrans.op
          (H.rightUnitor.inv ≫
            inv (H.whiskerLeft t.adj₁.counit) ≫
              (H.associator G F).inv ≫ whiskerRight t.adj₂.counit F ≫ F.leftUnitor.hom)).app
      x✝

Tactic:
simp

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'
inst✝ : HasCoreflexiveEqualizers C
h✝ : (X : B) → RegularMono (adj₁.unit.app X)
X Y : C
Y' : B
g : X ⟶ Y
h : L.obj Y ⟶ Y'
⊢ g ≫
      (adj₂.homEquiv Y (F.obj Y'))
        (F.map ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj Y)) h) ≫ adj₁.counit.app (F.obj Y')) =
    g ≫
      ↑⟨(adj₂.homEquiv Y (F.obj Y'))
            (F.map ↑((Fork.IsLimit.homIso (unitEqualises adj₁ h✝ Y') (L.obj Y)) h) ≫ adj₁.counit.app (F.obj Y')),
          ⋯⟩

Tactic:
simp

Goal state after:
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
X : C
⊢ (whiskerRight t.adj₂.counit F).app X ≫ t.adj₂.unit.app (F.obj X) =
    F.map ((t.adj₂.counit.app ((𝟭 C).obj X) ≫ t.adj₁.unit.app X) ≫ G.map (t.adj₂.unit.app (F.obj X))) ≫
      t.adj₁.counit.app (((F ⋙ G) ⋙ H).obj X)

Tactic:
simp

Goal state after:
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
X : C
⊢ F.map (t.adj₂.counit.app X) ≫ t.leftToRight.app X = t.adj₁.counit.app (H.obj X)

Tactic:
simp

Goal state after:
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
x✝ : Cᵒᵖ
⊢ (H.op.rightUnitor.inv ≫
          H.op.whiskerLeft t.op.adj₂.unit ≫
            (H.op.associator G.op F.op).inv ≫ inv (whiskerRight t.op.adj₁.unit F.op) ≫ F.op.leftUnitor.hom).app
      x✝ =
    (NatTrans.op
          (F.leftUnitor.inv ≫
            inv (whiskerRight t.adj₂.counit F) ≫
              (H.associator G F).hom ≫ H.whiskerLeft t.adj₁.counit ≫ H.rightUnitor.hom)).app
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

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

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

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

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
t : B
⊢ (α_ (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯)).hom =
    (eqToHomTransIso ⋯ ⋯).inv ▷ eqToHom ⋯ ≫
      (eqToHomTransIso ⋯ ⋯).inv ≫ (eqToHomTransIso ⋯ ⋯).hom ≫ eqToHom ⋯ ◁ (eqToHomTransIso ⋯ ⋯).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
t : B
⊢ (α_ (eqToHom ⋯) (eqToHom ⋯) (eqToHom ⋯)).inv =
    eqToHom ⋯ ◁ (eqToHomTransIso ⋯ ⋯).inv ≫
      (eqToHomTransIso ⋯ ⋯).inv ≫ (eqToHomTransIso ⋯ ⋯).hom ≫ (eqToHomTransIso ⋯ ⋯).hom ▷ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y z t : B
f' : x ⟶ y
g' : y ⟶ z
h' : z ⟶ t
⊢ (α_ f' g' h').hom = eqToHom ⋯ ≫ (α_ f' g' h').hom ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y z t : B
f' : x ⟶ y
g' : y ⟶ z
h' : z ⟶ t
⊢ (α_ f' g' h').inv = eqToHom ⋯ ≫ (α_ f' g' h').inv ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
f : x ⟶ y
z : B
g g' : y ⟶ z
η : g ⟶ g'
⊢ f ◁ η = eqToHom ⋯ ≫ f ◁ η ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
y z : B
g : y ⟶ z
x : B
f f' : x ⟶ y
η : f ⟶ f'
⊢ η ▷ g = eqToHom ⋯ ≫ η ▷ g ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
f : x ⟶ y
⊢ (λ_ f).hom = 𝟙 x ◁ eqToHom ⋯ ≫ (λ_ f).hom ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
f : x ⟶ y
⊢ (λ_ f).inv = eqToHom ⋯ ≫ (λ_ f).inv ≫ 𝟙 x ◁ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
f : x ⟶ y
⊢ (ρ_ f).hom = eqToHom ⋯ ▷ 𝟙 y ≫ (ρ_ f).hom ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.EqToHom

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
x y : B
f : x ⟶ y
⊢ (ρ_ f).inv = eqToHom ⋯ ≫ (ρ_ f).inv ≫ eqToHom ⋯ ▷ 𝟙 y

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.id
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel (Hom₂.id f✝) ≫ (normalizeIso p f✝).hom =
    (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.vcomp
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
ihg :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ ((normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)) ≫ (preinclusion B).map₂ (eqToHom ⋯) =
    (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.whisker_left
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ h✝ : b✝ ⟶ c✝
η✝ : Hom₂ g✝ h✝
ih :
  ∀ (p : Path a b✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η✝ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (α_ ((preinclusion B).map { as := p }) f✝ g✝).inv ≫
      (normalizeIso p f✝).hom ▷ g✝ ≫ (normalizeIso (normalizeAux p f✝) g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯) =
    ((α_ ((preinclusion B).map { as := p }) f✝ g✝).inv ≫
        (normalizeIso p f✝).hom ▷ g✝ ≫ (normalizeIso (normalizeAux p f✝) g✝).hom) ≫
      eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.associator
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ c✝ d✝ : FreeBicategory B
f✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ c✝
h✝ : c✝ ⟶ d✝
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ Quot.mk Rel (Hom₂.associator f✝ g✝ h✝) ≫ (normalizeIso p (f✝ ≫ g✝ ≫ h✝)).hom =
    (normalizeIso p ((f✝ ≫ g✝) ≫ h✝)).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
simp

Goal state after: