mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left.right.left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : C
a✝² : D
f : (left a✝³).Hom (right a✝²)
a✝¹ : C
g : (right a✝²).Hom (left a✝¹)
a✝ : D
h : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
simp only [Hom, comp, Category.assoc]

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

Goal state before:
pp: case left.right.right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : C
a✝² : D
f : (left a✝³).Hom (right a✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
simp only [Hom, comp, Category.assoc]

Goal state after:
case left.right.right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : C
a✝² : D
f : (left a✝³).Hom (right a✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ (match left a✝³, right a✝¹, left a✝, PUnit.unit, h with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }) =
    match left a✝³, right a✝², left a✝, f,
      match right a✝², right a✝¹, left a✝, g, h with
      | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
      | left _x, left _y, right _z, x, x_1 => PUnit.unit
      | left _x, right _y, right _z, x, x_1 => PUnit.unit
      | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down } with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case left.right.right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : C
a✝² : D
f : (left a✝³).Hom (right a✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
simp only [Hom, comp, Category.assoc]

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

Goal state before:
pp: case right.left.left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : D
a✝² : C
f : (right a✝³).Hom (left a✝²)
a✝¹ : C
g : (left a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
simp only [Hom, comp, Category.assoc]

Goal state after:
case right.left.left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : D
a✝² : C
f : (right a✝³).Hom (left a✝²)
a✝¹ : C
g : (left a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝¹).Hom (left a✝)
⊢ (match right a✝³, left a✝¹, left a✝,
      match right a✝³, left a✝², left a✝¹, f, g with
      | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
      | left _x, left _y, right _z, x, x_1 => PUnit.unit
      | left _x, right _y, right _z, x, x_1 => PUnit.unit
      | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down },
      h with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }) =
    match right a✝³, left a✝², left a✝, f, { down := g.down ≫ h.down } with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case right.left.left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : D
a✝² : C
f : (right a✝³).Hom (left a✝²)
a✝¹ : C
g : (left a✝²).Hom (left a✝¹)
a✝ : D
h : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
simp only [Hom, comp, Category.assoc]

Goal state after:
case right.left.left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : D
a✝² : C
f : (right a✝³).Hom (left a✝²)
a✝¹ : C
g : (left a✝²).Hom (left a✝¹)
a✝ : D
h : (left a✝¹).Hom (right a✝)
⊢ (match right a✝³, left a✝¹, right a✝,
      match right a✝³, left a✝², left a✝¹, f, g with
      | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
      | left _x, left _y, right _z, x, x_1 => PUnit.unit
      | left _x, right _y, right _z, x, x_1 => PUnit.unit
      | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down },
      h with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }) =
    match right a✝³, left a✝², right a✝, f, PUnit.unit with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case right.left.right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : D
a✝² : C
f : (right a✝³).Hom (left a✝²)
a✝¹ : D
g : (left a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
simp only [Hom, comp, Category.assoc]

Goal state after:
case right.left.right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : D
a✝² : C
f : (right a✝³).Hom (left a✝²)
a✝¹ : D
g : (left a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ (match right a✝³, right a✝¹, left a✝,
      match right a✝³, left a✝², right a✝¹, f, g with
      | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
      | left _x, left _y, right _z, x, x_1 => PUnit.unit
      | left _x, right _y, right _z, x, x_1 => PUnit.unit
      | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down },
      h with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }) =
    match right a✝³, left a✝², left a✝, f,
      match left a✝², right a✝¹, left a✝, g, h with
      | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
      | left _x, left _y, right _z, x, x_1 => PUnit.unit
      | left _x, right _y, right _z, x, x_1 => PUnit.unit
      | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down } with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case right.left.right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : D
a✝² : C
f : (right a✝³).Hom (left a✝²)
a✝¹ : D
g : (left a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
simp only [Hom, comp, Category.assoc]

Goal state after:
case right.left.right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ : D
a✝² : C
f : (right a✝³).Hom (left a✝²)
a✝¹ : D
g : (left a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝¹).Hom (right a✝)
⊢ {
      down :=
        (match right a✝³, left a✝², right a✝¹, f, g with
            | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
            | left _x, left _y, right _z, x, x_1 => PUnit.unit
            | left _x, right _y, right _z, x, x_1 => PUnit.unit
            | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }).down ≫
          h.down } =
    match right a✝³, left a✝², right a✝, f, PUnit.unit with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case right.right.left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ a✝² : D
f : (right a✝³).Hom (right a✝²)
a✝¹ : C
g : (right a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
simp only [Hom, comp, Category.assoc]

Goal state after:
case right.right.left.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ a✝² : D
f : (right a✝³).Hom (right a✝²)
a✝¹ : C
g : (right a✝²).Hom (left a✝¹)
a✝ : C
h : (left a✝¹).Hom (left a✝)
⊢ (match right a✝³, left a✝¹, left a✝,
      match right a✝³, right a✝², left a✝¹, f, g with
      | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
      | left _x, left _y, right _z, x, x_1 => PUnit.unit
      | left _x, right _y, right _z, x, x_1 => PUnit.unit
      | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down },
      h with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }) =
    match right a✝³, right a✝², left a✝, f,
      match right a✝², left a✝¹, left a✝, g, h with
      | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
      | left _x, left _y, right _z, x, x_1 => PUnit.unit
      | left _x, right _y, right _z, x, x_1 => PUnit.unit
      | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down } with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case right.right.left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ a✝² : D
f : (right a✝³).Hom (right a✝²)
a✝¹ : C
g : (right a✝²).Hom (left a✝¹)
a✝ : D
h : (left a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
simp only [Hom, comp, Category.assoc]

Goal state after:
case right.right.left.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ a✝² : D
f : (right a✝³).Hom (right a✝²)
a✝¹ : C
g : (right a✝²).Hom (left a✝¹)
a✝ : D
h : (left a✝¹).Hom (right a✝)
⊢ (match right a✝³, left a✝¹, right a✝,
      match right a✝³, right a✝², left a✝¹, f, g with
      | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
      | left _x, left _y, right _z, x, x_1 => PUnit.unit
      | left _x, right _y, right _z, x, x_1 => PUnit.unit
      | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down },
      h with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }) =
    {
      down :=
        f.down ≫
          (match right a✝², left a✝¹, right a✝, g, h with
            | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
            | left _x, left _y, right _z, x, x_1 => PUnit.unit
            | left _x, right _y, right _z, x, x_1 => PUnit.unit
            | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }).down }
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case right.right.right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ a✝² : D
f : (right a✝³).Hom (right a✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
simp only [Hom, comp, Category.assoc]

Goal state after:
case right.right.right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ a✝² : D
f : (right a✝³).Hom (right a✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : C
h : (right a✝¹).Hom (left a✝)
⊢ (match right a✝³, right a✝¹, left a✝, { down := f.down ≫ g.down }, h with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }) =
    match right a✝³, right a✝², left a✝, f,
      match right a✝², right a✝¹, left a✝, g, h with
      | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
      | left _x, left _y, right _z, x, x_1 => PUnit.unit
      | left _x, right _y, right _z, x, x_1 => PUnit.unit
      | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down } with
    | left _x, left _y, left _z, f, g => { down := f.down ≫ g.down }
    | left _x, left _y, right _z, x, x_1 => PUnit.unit
    | left _x, right _y, right _z, x, x_1 => PUnit.unit
    | right _x, right _y, right _z, f, g => { down := f.down ≫ g.down }
Module: Mathlib.CategoryTheory.Join.Basic

Goal state before:
pp: case right.right.right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
a✝³ a✝² : D
f : (right a✝³).Hom (right a✝²)
a✝¹ : D
g : (right a✝²).Hom (right a✝¹)
a✝ : D
h : (right a✝¹).Hom (right a✝)
⊢ comp (comp f g) h = comp f (comp g h)

Tactic:
simp only [Hom, comp, Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : FormalCoproduct C
f g : X ⟶ Y
h₁ : f.f = g.f
h₂ : ∀ (i : X.I), f.φ i ≫ eqToHom ⋯ = g.φ i
⊢ f = g

Tactic:
obtain ⟨f, F⟩ := f
  obtain ⟨g, G⟩ := g
  obtain rfl : f = g := h₁
  obtain rfl : F = G := by ext i; simpa using h₂ i
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.SmallComplete

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := ⋯
α : Cardinal.{u} := ⋯
yp : C := ⋯
⊢ #(X ⟶ Y) ^ α ≤ #(X ⟶ yp)

Tactic:
rw [Cardinal.power_def]

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun x ↦ Y
⊢ #(md → (X ⟶ Y)) ≤ #(X ⟶ yp)
Module: Mathlib.CategoryTheory.Localization.Pi

Goal state before:
pp: case h_empty
C : PEmpty.{w + 1} → Type u₁
D : PEmpty.{w + 1} → Type u₂
inst✝³ : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)
inst✝² : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
L : (j : PEmpty.{w + 1}) → C j ⥤ D j
W : (j : PEmpty.{w + 1}) → MorphismProperty (C j)
inst✝¹ : ∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities
inst✝ : ∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)
this : ∀ (j : PEmpty.{w + 1}), (L j).IsEquivalence
⊢ (Functor.pi L).IsLocalization (MorphismProperty.pi W)

Tactic:
refine IsLocalization.of_isEquivalence _ _ (fun _ _ _ _ => ?_)

Goal state after:
case h_empty
C : PEmpty.{w + 1} → Type u₁
D : PEmpty.{w + 1} → Type u₂
inst✝³ : (j : PEmpty.{w + 1}) → Category.{v₁, u₁} (C j)
inst✝² : (j : PEmpty.{w + 1}) → Category.{v₂, u₂} (D j)
L : (j : PEmpty.{w + 1}) → C j ⥤ D j
W : (j : PEmpty.{w + 1}) → MorphismProperty (C j)
inst✝¹ : ∀ (j : PEmpty.{w + 1}), (W j).ContainsIdentities
inst✝ : ∀ (j : PEmpty.{w + 1}), (L j).IsLocalization (W j)
this : ∀ (j : PEmpty.{w + 1}), (L j).IsEquivalence
x✝³ x✝² : (i : PEmpty.{w + 1}) → C i
x✝¹ : x✝³ ⟶ x✝²
x✝ : MorphismProperty.pi W x✝¹
⊢ MorphismProperty.isomorphisms ((i : PEmpty.{w + 1}) → C i) x✝¹
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

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
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
S S' : CatCommSqOver F G X
eₗ : S.fst ≅ S'.fst
eᵣ : S.snd ≅ S'.snd
w : whiskerRight eₗ.hom F ≫ S'.iso.hom = S.iso.hom ≫ whiskerRight eᵣ.hom G
⊢ whiskerRight eₗ.inv F ≫ S.iso.hom = S'.iso.hom ≫ whiskerRight eᵣ.inv G

Tactic:
ext t
    simpa [← Functor.map_comp_assoc, ← Functor.map_comp] using
      congr_app (whiskerRight eₗ.inv F ≫= w.symm =≫ whiskerRight eᵣ.inv G) t

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Free.Basic

Goal state before:
pp: C : Type u
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rintro X Y ⟨f⟩
    exact Quotient.sound (id_comp f)

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided

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
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
X Y Z : C
⊢ (L'.obj X ◁ LaxMonoidal.μ L' Y Z ≫
        LaxMonoidal.μ L' X (Y ⊗ Z) ≫
          L'.map (α_ X Y Z).inv ≫ OplaxMonoidal.δ L' (X ⊗ Y) Z ≫ OplaxMonoidal.δ L' X Y ▷ L'.obj Z) ≫
      ((braidingNatIso L W ε).hom.app (L'.obj X ⊗ L'.obj Y)).app (L'.obj Z) ≫
        L'.obj Z ◁ LaxMonoidal.μ L' X Y ≫
          LaxMonoidal.μ L' Z (X ⊗ Y) ≫
            L'.map (α_ Z X Y).inv ≫ OplaxMonoidal.δ L' (Z ⊗ X) Y ≫ OplaxMonoidal.δ L' Z X ▷ L'.obj Y =
    L'.obj X ◁ (LaxMonoidal.μ L' Y Z ≫ L'.map (β_ Y Z).hom ≫ OplaxMonoidal.δ L' Z Y) ≫
      (L'.obj X ◁ LaxMonoidal.μ L' Z Y ≫
          LaxMonoidal.μ L' X (Z ⊗ Y) ≫
            L'.map (α_ X Z Y).inv ≫ OplaxMonoidal.δ L' (X ⊗ Z) Y ≫ OplaxMonoidal.δ L' X Z ▷ L'.obj Y) ≫
        (LaxMonoidal.μ L' X Z ≫ L'.map (β_ X Z).hom ≫ OplaxMonoidal.δ L' Z X) ▷ L'.obj Y

Tactic:
slice_rhs 0 4 =>
    simp only [Functor.flip_obj_obj, Functor.CoreMonoidal.toMonoidal_toLaxMonoidal,
      Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, MonoidalCategory.whiskerLeft_comp, assoc,
      Functor.Monoidal.whiskerLeft_δ_μ, comp_id]

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
L : C ⥤ D
W : MorphismProperty C
inst✝³ : MonoidalCategory C
inst✝² : W.IsMonoidal
inst✝¹ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
inst✝ : BraidedCategory C
X Y Z : C
⊢ (L'.obj X ◁ LaxMonoidal.μ L' Y Z ≫
        LaxMonoidal.μ L' X (Y ⊗ Z) ≫
          L'.map (α_ X Y Z).inv ≫ OplaxMonoidal.δ L' (X ⊗ Y) Z ≫ OplaxMonoidal.δ L' X Y ▷ L'.obj Z) ≫
      ((braidingNatIso L W ε).hom.app (L'.obj X ⊗ L'.obj Y)).app (L'.obj Z) ≫
        L'.obj Z ◁ LaxMonoidal.μ L' X Y ≫
          LaxMonoidal.μ L' Z (X ⊗ Y) ≫
            L'.map (α_ Z X Y).inv ≫ OplaxMonoidal.δ L' (Z ⊗ X) Y ≫ OplaxMonoidal.δ L' Z X ▷ L'.obj Y =
    ((((L'.obj X ◁ LaxMonoidal.μ L' Y Z ≫
              L'.obj X ◁ L'.map (β_ Y Z).hom ≫
                L'.obj X ◁ OplaxMonoidal.δ L' Z Y ≫ L'.obj X ◁ LaxMonoidal.μ L' Z Y ≫ LaxMonoidal.μ L' X (Z ⊗ Y)) ≫
            L'.map (α_ X Z Y).inv) ≫
          OplaxMonoidal.δ L' (X ⊗ Z) Y) ≫
        OplaxMonoidal.δ L' X Z ▷ L'.obj Y) ≫
      ((LaxMonoidal.μ L' X Z ≫ L'.map (β_ X Z).hom) ≫ OplaxMonoidal.δ L' Z X) ▷ L'.obj Y
Module: Mathlib.CategoryTheory.LocallyCartesianClosed.Sections

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
I : C
inst✝² : Closed I
inst✝¹ : ChosenPullbacksAlong (curryRightUnitorHom I)
inst✝ : BraidedCategory C
A' A : C
X : Over I
g : A' ⟶ A
v : A ⟶ (sections I).obj X
⊢ (β_ A' I).hom ≫ uncurry ((g ≫ v) ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom)) =
    g ▷ I ≫ (β_ A I).hom ≫ uncurry (v ≫ ChosenPullbacksAlong.fst ((ihom I).map X.hom) (curry (ρ_ I).hom))

Tactic:
simp [uncurry_natural_left]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ adj.unit.app A.A ≫ G.map f = G.map f ↔
    G.map (F.map (adj.unit.app A.A) ≫ F.map (G.map f) ≫ adj.counit.app B) = A.a ≫ adj.unit.app A.A ≫ G.map f

Tactic:
adj.counit_naturality,

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
B : D
inst✝ : HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ adj.unit.app A.A ≫ G.map f = G.map f ↔
    G.map (F.map (adj.unit.app A.A) ≫ adj.counit.app (F.obj A.A) ≫ f) = A.a ≫ adj.unit.app A.A ≫ G.map f
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)
this : HasCoequalizerOfIsSplitPair G
⊢ ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], PreservesColimit (parallelPair f g) G

Tactic:
intros; infer_instance

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
inst✝ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], HasColimit (parallelPair f g ⋙ G)
this✝ : HasCoequalizerOfIsSplitPair G
this : PreservesColimitOfIsSplitPair G
⊢ ∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g], ReflectsColimit (parallelPair f g) G

Tactic:
intros; infer_instance

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : MonoidalCategory C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : MonoidalLeftAction C D
c✝ c'✝ : Cᵒᵖ
d✝ d'✝ : Dᵒᵖ
f : unop c'✝ ⟶ unop c✝
g : unop d'✝ ⟶ unop d✝
⊢ (Quiver.Hom.unop (op f) ⊙ₗₘ Quiver.Hom.unop (op g)).op =
    (Quiver.Hom.unop (op f) ⊵ₗ unop d✝).op ≫ (unop c'✝ ⊴ₗ Quiver.Hom.unop (op g)).op

Tactic:
by
        apply Quiver.Hom.unop_inj
        simpa [MonoidalLeftAction.action_exchange] using
          MonoidalLeftAction.actionHom_def f g

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A B : Mon C
M : Bimod A B
X Y : Mon C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ Q.actRight = f.inv ▷ Y.X ≫ P.actRight ≫ f.hom

Tactic:
f_right_act_hom,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A B : Mon C
M : Bimod A B
X Y : Mon C
P Q : Bimod X Y
f : P.X ≅ Q.X
f_left_act_hom : P.actLeft ≫ f.hom = X.X ◁ f.hom ≫ Q.actLeft
f_right_act_hom : P.actRight ≫ f.hom = f.hom ▷ Y.X ≫ Q.actRight
⊢ Q.actRight = f.inv ▷ Y.X ≫ f.hom ▷ Y.X ≫ Q.actRight