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

Goal state before:
pp: case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| N.actRight ▷ 𝟙_ C ≫ N.X ◁ η

pp: case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| coequalizer.π (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ μ)

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| f.hom ▷ Y.X

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| (ρ_ (N.X ⊗ Y.X)).inv

Tactic:
← whisker_exchange

Goal state after:
case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| (N.X ⊗ Y.X) ◁ η ≫ N.actRight ▷ Y.X

case a.a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| coequalizer.π (N.actRight ▷ Y.X) ((α_ N.X Y.X Y.X).hom ≫ N.X ◁ μ)

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| f.hom ▷ Y.X

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
| (ρ_ (N.X ⊗ Y.X)).inv
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
| (α_ M.X N.X P.X).inv ≫ (α_ M.X N.X P.X).hom ≫ f.hom ▷ (N.X ⊗ P.X)

pp: case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
| M'.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
| coequalizer.π (M'.actRight ▷ TensorBimod.X N P)
    ((α_ M'.X X.X (TensorBimod.X N P)).hom ≫ M'.X ◁ TensorBimod.actLeft N P)

Tactic:
rw [Iso.inv_hom_id_assoc]

Goal state after:
case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
| f.hom ▷ (N.X ⊗ P.X)

case a.a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
| M'.X ◁ coequalizer.π (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft)

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
W X Y Z : Mon C
M M' : Bimod W X
f : M ⟶ M'
N : Bimod X Y
P : Bimod Y Z
| coequalizer.π (M'.actRight ▷ TensorBimod.X N P)
    ((α_ M'.X X.X (TensorBimod.X N P)).hom ≫ M'.X ◁ TensorBimod.actLeft N P)
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: case h₁
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ { left := (x✝¹ + 1) • x✝.left, right := (x✝¹ + 1) • x✝.right, w := ⋯ }.left =
    ({ left := x✝¹ • x✝.left, right := x✝¹ • x✝.right, w := ⋯ } + x✝).left

Tactic:
dsimp

Goal state after:
case h₁
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ (x✝¹ + 1) • x✝.left = x✝¹ • x✝.left + x✝.left
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: case h₂
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ { left := (x✝¹ + 1) • x✝.left, right := (x✝¹ + 1) • x✝.right, w := ⋯ }.right =
    ({ left := x✝¹ • x✝.left, right := x✝¹ • x✝.right, w := ⋯ } + x✝).right

Tactic:
dsimp

Goal state after:
case h₂
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ (x✝¹ + 1) • x✝.right = x✝¹ • x✝.right + x✝.right
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: case h₁
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ { left := ↑x✝¹.succ • x✝.left, right := ↑x✝¹.succ • x✝.right, w := ⋯ }.left =
    ({ left := ↑x✝¹ • x✝.left, right := ↑x✝¹ • x✝.right, w := ⋯ } + x✝).left

Tactic:
dsimp

Goal state after:
case h₁
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ (↑x✝¹ + 1) • x✝.left = ↑x✝¹ • x✝.left + x✝.left
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: case h₂
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ { left := ↑x✝¹.succ • x✝.left, right := ↑x✝¹.succ • x✝.right, w := ⋯ }.right =
    ({ left := ↑x✝¹ • x✝.left, right := ↑x✝¹ • x✝.right, w := ⋯ } + x✝).right

Tactic:
dsimp

Goal state after:
case h₂
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ (↑x✝¹ + 1) • x✝.right = ↑x✝¹ • x✝.right + x✝.right
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: case h₁
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ { left := Int.negSucc x✝¹ • x✝.left, right := Int.negSucc x✝¹ • x✝.right, w := ⋯ }.left =
    (-{ left := ↑x✝¹.succ • x✝.left, right := ↑x✝¹.succ • x✝.right, w := ⋯ }).left

Tactic:
dsimp

Goal state after:
case h₁
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ Int.negSucc x✝¹ • x✝.left = -((↑x✝¹ + 1) • x✝.left)
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: case h₂
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ { left := Int.negSucc x✝¹ • x✝.left, right := Int.negSucc x✝¹ • x✝.right, w := ⋯ }.right =
    (-{ left := ↑x✝¹.succ • x✝.left, right := ↑x✝¹.succ • x✝.right, w := ⋯ }).right

Tactic:
dsimp

Goal state after:
case h₂
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ Int.negSucc x✝¹ • x✝.right = -((↑x✝¹ + 1) • x✝.right)
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
f : End X
hf : f ≠ 0
⊢ (f * if h : f = 0 then 0 else inv f) = 1

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
f : End X
hf : f ≠ 0
⊢ (if h : f = 0 then 0 else inv f) ≫ f = 𝟙 X
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫ (M.whiskerLeft g ≫ whiskerRight f Q).hom =
    coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫ (whiskerRight f P ≫ N.whiskerLeft g).hom

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M N : Bimod X Y
P Q : Bimod Y Z
f : M ⟶ N
g : P ⟶ Q
⊢ coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫
      colimMap
          (parallelPairHom (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) (M.actRight ▷ Q.X)
            ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) ((M.X ⊗ Y.X) ◁ g.hom) (M.X ◁ g.hom) ⋯ ⋯) ≫
        colimMap
          (parallelPairHom (M.actRight ▷ Q.X) ((α_ M.X Y.X Q.X).hom ≫ M.X ◁ Q.actLeft) (N.actRight ▷ Q.X)
            ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) (f.hom ▷ Y.X ▷ Q.X) (f.hom ▷ Q.X) ⋯ ⋯) =
    coequalizer.π (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) ≫
      colimMap
          (parallelPairHom (M.actRight ▷ P.X) ((α_ M.X Y.X P.X).hom ≫ M.X ◁ P.actLeft) (N.actRight ▷ P.X)
            ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (f.hom ▷ Y.X ▷ P.X) (f.hom ▷ P.X) ⋯ ⋯) ≫
        colimMap
          (parallelPairHom (N.actRight ▷ P.X) ((α_ N.X Y.X P.X).hom ≫ N.X ◁ P.actLeft) (N.actRight ▷ Q.X)
            ((α_ N.X Y.X Q.X).hom ≫ N.X ◁ Q.actLeft) ((N.X ⊗ Y.X) ◁ g.hom) (N.X ◁ g.hom) ⋯ ⋯)
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝³ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
P : Set ↑J.obj → Prop
inst✝² : IsDirectedOrder (Subtype P)
inst✝¹ : Nonempty (Subtype P)
inst✝ : ∀ (S : Subtype P), IsCardinalFiltered (↑↑S) κ
S : Subtype P
⊢ PartOrdEmb.isCardinalFiltered κ ((PartOrdEmb.functorOfPredicateSet P).obj S)

Tactic:
dsimp

Goal state after:
κ : Cardinal.{u}
inst✝³ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
P : Set ↑J.obj → Prop
inst✝² : IsDirectedOrder (Subtype P)
inst✝¹ : Nonempty (Subtype P)
inst✝ : ∀ (S : Subtype P), IsCardinalFiltered (↑↑S) κ
S : Subtype P
⊢ PartOrdEmb.isCardinalFiltered κ { carrier := ↑↑S, str := Subtype.partialOrder fun x ↦ x ∈ ↑S }
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ ((fun x y ↦ if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0) ≫ fun x y ↦
        if h : x.fst = j' then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0)
      x y =
    (if h : j = j' then eqToHom ⋯ else 0) x y

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ j_1,
      (if h : j_1.fst = j then if h' : h ▸ j_1.snd = x then eqToHom ⋯ else 0 else 0) ≫
        if h : j_1.fst = j' then if h' : h ▸ j_1.snd = y then eqToHom ⋯ else 0 else 0) =
    (if h : j = j' then eqToHom ⋯ else 0) x y
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
⊢ ∑ j,
      { pt := { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd },
              π := fun j x y ↦ if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0,
              ι := fun j x y ↦ if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0, ι_π := ⋯ }.π
          j ≫
        { pt := { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd },
              π := fun j x y ↦ if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0,
              ι := fun j x y ↦ if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0, ι_π := ⋯ }.ι
          j =
    𝟙
      { pt := { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd },
          π := fun j x y ↦ if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0,
          ι := fun j x y ↦ if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0, ι_π := ⋯ }.pt

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
⊢ (∑ j,
      (fun x y ↦ if h : x.fst = j then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0) ≫ fun x y ↦
        if h : y.fst = j then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0) =
    𝟙 { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ ∑ c,
      ((fun x y ↦ if h : x.fst = c then if h' : h ▸ x.snd = y then eqToHom ⋯ else 0 else 0) ≫ fun x y ↦
          if h : y.fst = c then if h' : h ▸ y.snd = x then eqToHom ⋯ else 0 else 0)
        ⟨i, j⟩ ⟨i', j'⟩ =
    𝟙 { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd } ⟨i, j⟩ ⟨i', j'⟩

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
⊢ (∑ c,
      ∑ j_1,
        (if h : i = c then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
          if h : i' = c then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
    𝟙 { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd } ⟨i, j⟩ ⟨i', j'⟩
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j b : M.ι
a✝ : b ∈ Finset.univ
hb : b ≠ i
⊢ ((fun j x ↦ if h : j = b then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : b = k then eqToHom ⋯ else 0) i j = 0

Tactic:
dsimp

Goal state after:
case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j b : M.ι
a✝ : b ∈ Finset.univ
hb : b ≠ i
⊢ (∑ j_1, (if h : i = b then eqToHom ⋯ else 0) ≫ if h : b = j then eqToHom ⋯ else 0) = 0
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
j : J
x y : ↑(F.1 j)
k : J
x' y' : ↑(F.obj k)
hx : (ConcreteCategory.hom (c.ι.app k)) x' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } x
hy : (ConcreteCategory.hom (c.ι.app k)) y' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } y
h : x' ≤ y'
l₁ : J
a₁ : k ⟶ l₁
b₁ : j ⟶ l₁
hl₁ : (ConcreteCategory.hom (F.map a₁)) x' = (ConcreteCategory.hom (F.map b₁)) x
l₂ : J
a₂ : k ⟶ l₂
b₂ : j ⟶ l₂
hl₂ : (ConcreteCategory.hom (F.map a₂)) y' = (ConcreteCategory.hom (F.map b₂)) y
m : J
d : l₁ ⟶ m
d' : l₂ ⟶ m
h₁ : a₁ ≫ d = a₂ ≫ d'
h₂ : b₁ ≫ d = b₂ ≫ d'
⊢ x ≤ y

Tactic:
← (F.map (a₁ ≫ d)).le_iff_le

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
j : J
x y : ↑(F.1 j)
k : J
x' y' : ↑(F.obj k)
hx : (ConcreteCategory.hom (c.ι.app k)) x' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } x
hy : (ConcreteCategory.hom (c.ι.app k)) y' = { toFun := ⇑(ConcreteCategory.hom (c.ι.app j)), inj' := ⋯ } y
l₁ : J
a₁ : k ⟶ l₁
b₁ : j ⟶ l₁
hl₁ : (ConcreteCategory.hom (F.map a₁)) x' = (ConcreteCategory.hom (F.map b₁)) x
l₂ : J
a₂ : k ⟶ l₂
b₂ : j ⟶ l₂
hl₂ : (ConcreteCategory.hom (F.map a₂)) y' = (ConcreteCategory.hom (F.map b₂)) y
m : J
d : l₁ ⟶ m
h : (ConcreteCategory.hom (F.map (a₁ ≫ d))) x' ≤ (ConcreteCategory.hom (F.map (a₁ ≫ d))) y'
d' : l₂ ⟶ m
h₁ : a₁ ≫ d = a₂ ≫ d'
h₂ : b₁ ≫ d = b₂ ≫ d'
⊢ x ≤ y
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: case refine_1.refine_2
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
f : J ⟶ c.pt
j : ↑J.obj → A
g : (x : ↑J.obj) → (fun X ↦ X) ((F ⋙ forget (CardinalDirectedPoset κ)).obj (j x))
hg :
  ∀ (x : ↑J.obj),
    (ConcreteCategory.hom (((forget (CardinalDirectedPoset κ)).mapCocone c).ι.app (j x))) (g x) =
      (ConcreteCategory.hom f) x
m : A := IsCardinalFiltered.max j hJ
φ : ↑J.obj → ↑(F.obj m).obj := fun x ↦ (ConcreteCategory.hom (F.map (IsCardinalFiltered.toMax j hJ x))) (g x)
hφ : ∀ (x : ↑J.obj), (ConcreteCategory.hom f) x = (ConcreteCategory.hom (c.ι.app m)) (φ x)
⊢ f =
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op J)).mapCocone c).ι.app m))
      (ObjectProperty.homMk (PartOrdEmb.ofHom { toFun := φ, inj' := ⋯, map_rel_iff' := ⋯ }))

Tactic:
dsimp

Goal state after:
case refine_1.refine_2
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
f : J ⟶ c.pt
j : ↑J.obj → A
g : (x : ↑J.obj) → (fun X ↦ X) ((F ⋙ forget (CardinalDirectedPoset κ)).obj (j x))
hg :
  ∀ (x : ↑J.obj),
    (ConcreteCategory.hom (((forget (CardinalDirectedPoset κ)).mapCocone c).ι.app (j x))) (g x) =
      (ConcreteCategory.hom f) x
m : A := IsCardinalFiltered.max j hJ
φ : ↑J.obj → ↑(F.obj m).obj := fun x ↦ (ConcreteCategory.hom (F.map (IsCardinalFiltered.toMax j hJ x))) (g x)
hφ : ∀ (x : ↑J.obj), (ConcreteCategory.hom f) x = (ConcreteCategory.hom (c.ι.app m)) (φ x)
⊢ f = ObjectProperty.homMk (PartOrdEmb.ofHom { toFun := φ, inj' := ⋯, map_rel_iff' := ⋯ }) ≫ c.ι.app m
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case e_a.e_a
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : F.Additive
L : Mat_ C ⥤ D
inst✝ : L.Additive
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
j : X✝.ι
k : Y✝.ι
⊢ (L.map ((embedding C).map (f j k)) ≫ (α.app (Y✝.X k)).hom ≫ ((embeddingLiftIso F).symm.app (Y✝.X k)).hom) ≫
      biproduct.π (fun i ↦ F.obj (((embedding C).obj (Y✝.X k)).X i)) PUnit.unit =
    ((α.app (X✝.X j)).hom ≫ ((embeddingLiftIso F).symm.app (X✝.X j)).hom ≫ (lift F).map ((embedding C).map (f j k))) ≫
      biproduct.π (fun i ↦ F.obj (((embedding C).obj (Y✝.X k)).X i)) PUnit.unit

Tactic:
dsimp

Goal state after:
case e_a.e_a
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₁
inst✝⁴ : Category.{v₁, u₁} D
inst✝³ : Preadditive D
inst✝² : HasFiniteBiproducts D
F : C ⥤ D
inst✝¹ : F.Additive
L : Mat_ C ⥤ D
inst✝ : L.Additive
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
j : X✝.ι
k : Y✝.ι
⊢ (L.map ((embedding C).map (f j k)) ≫ α.hom.app (Y✝.X k) ≫ biproduct.lift fun x ↦ 𝟙 (F.obj (Y✝.X k))) ≫
      biproduct.π (fun i ↦ F.obj (Y✝.X k)) PUnit.unit =
    (α.hom.app (X✝.X j) ≫ (biproduct.lift fun x ↦ 𝟙 (F.obj (X✝.X j))) ≫ biproduct.matrix fun i j_1 ↦ F.map (f j k)) ≫
      biproduct.π (fun i ↦ F.obj (Y✝.X k)) PUnit.unit
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁴ : HasCoproduct D₁.obj₁
inst✝³ : HasCoproduct D₁.obj₂
inst✝² : HasPushouts C
inst✝¹ : MorphismProperty.IsSmall.{w, v, u} W
inst✝ : LocallySmall.{w, v, u} C
⊢ Small.{w, max u v} (D₂.multispanShape W Z).L

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁴ : HasCoproduct D₁.obj₁
inst✝³ : HasCoproduct D₁.obj₂
inst✝² : HasPushouts C
inst✝¹ : MorphismProperty.IsSmall.{w, v, u} W
inst✝ : LocallySmall.{w, v, u} C
⊢ Small.{w, max u v} (D₂ W Z)