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

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁴ : (i : I) → Category.{v₁, u₁} (C i)
inst✝³ : (i : I) → MonoidalCategory (C i)
D : I → Type u₂
inst✝² : (i : I) → Category.{v₂, u₂} (D i)
inst✝¹ : (i : I) → MonoidalCategory (D i)
F : (i : I) → D i ⥤ C i
inst✝ : (i : I) → (F i).OplaxMonoidal
X : (i : I) → D i
i✝ : I
⊢ (ρ_ ((Functor.pi F).obj X)).inv i✝ =
    ((Functor.pi F).map (ρ_ X).inv ≫
        (fun i ↦ Functor.OplaxMonoidal.δ (F i) (X i) ((𝟙_ ((i : I) → D i)) i)) ≫
          (Functor.pi F).obj X ◁ fun i ↦ Functor.OplaxMonoidal.η (F i))
      i✝

Tactic:
;

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝⁴ : (i : I) → Category.{v₁, u₁} (C i)
inst✝³ : (i : I) → MonoidalCategory (C i)
D : I → Type u₂
inst✝² : (i : I) → Category.{v₂, u₂} (D i)
inst✝¹ : (i : I) → MonoidalCategory (D i)
F : (i : I) → D i ⥤ C i
inst✝ : (i : I) → (F i).OplaxMonoidal
X : (i : I) → D i
i✝ : I
⊢ (ρ_ ((Functor.pi F).obj X)).inv i✝ =
    ((Functor.pi F).map (ρ_ X).inv ≫
        (fun i ↦ Functor.OplaxMonoidal.δ (F i) (X i) ((𝟙_ ((i : I) → D i)) i)) ≫
          (Functor.pi F).obj X ◁ fun i ↦ Functor.OplaxMonoidal.η (F i))
      i✝
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
inst✝⁴ : (i : I) → BraidedCategory (C i)
D : I → Type u₂
inst✝³ : (i : I) → Category.{v₂, u₂} (D i)
inst✝² : (i : I) → MonoidalCategory (D i)
inst✝¹ : (i : I) → BraidedCategory (D i)
F : (i : I) → D i ⥤ C i
inst✝ : (i : I) → (F i).LaxBraided
X✝ Y✝ : (i : I) → D i
⊢ Functor.LaxMonoidal.μ (Functor.pi F) X✝ Y✝ ≫ (Functor.pi F).map (β_ X✝ Y✝).hom =
    (β_ ((Functor.pi F).obj X✝) ((Functor.pi F).obj Y✝)).hom ≫ Functor.LaxMonoidal.μ (Functor.pi F) Y✝ X✝

Tactic:
;

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
inst✝⁴ : (i : I) → BraidedCategory (C i)
D : I → Type u₂
inst✝³ : (i : I) → Category.{v₂, u₂} (D i)
inst✝² : (i : I) → MonoidalCategory (D i)
inst✝¹ : (i : I) → BraidedCategory (D i)
F : (i : I) → D i ⥤ C i
inst✝ : (i : I) → (F i).LaxBraided
X✝ Y✝ : (i : I) → D i
⊢ Functor.LaxMonoidal.μ (Functor.pi F) X✝ Y✝ ≫ (Functor.pi F).map (β_ X✝ Y✝).hom =
    (β_ ((Functor.pi F).obj X✝) ((Functor.pi F).obj Y✝)).hom ≫ Functor.LaxMonoidal.μ (Functor.pi F) Y✝ X✝
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
inst✝⁴ : (i : I) → BraidedCategory (C i)
D : I → Type u₂
inst✝³ : (i : I) → Category.{v₂, u₂} (D i)
inst✝² : (i : I) → MonoidalCategory (D i)
inst✝¹ : (i : I) → BraidedCategory (D i)
F : (i : I) → D i ⥤ C i
inst✝ : (i : I) → (F i).LaxBraided
X✝ Y✝ : (i : I) → D i
i : I
⊢ (Functor.LaxMonoidal.μ (Functor.pi F) X✝ Y✝ ≫ (Functor.pi F).map (β_ X✝ Y✝).hom) i =
    ((β_ ((Functor.pi F).obj X✝) ((Functor.pi F).obj Y✝)).hom ≫ Functor.LaxMonoidal.μ (Functor.pi F) Y✝ X✝) i

Tactic:
;

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
inst✝⁴ : (i : I) → BraidedCategory (C i)
D : I → Type u₂
inst✝³ : (i : I) → Category.{v₂, u₂} (D i)
inst✝² : (i : I) → MonoidalCategory (D i)
inst✝¹ : (i : I) → BraidedCategory (D i)
F : (i : I) → D i ⥤ C i
inst✝ : (i : I) → (F i).LaxBraided
X✝ Y✝ : (i : I) → D i
i : I
⊢ (Functor.LaxMonoidal.μ (Functor.pi F) X✝ Y✝ ≫ (Functor.pi F).map (β_ X✝ Y✝).hom) i =
    ((β_ ((Functor.pi F).obj X✝) ((Functor.pi F).obj Y✝)).hom ≫ Functor.LaxMonoidal.μ (Functor.pi F) Y✝ X✝) i
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : MonoidalCategory D
F G : D ⥤ ((i : I) → C i)
inst✝² : F.LaxMonoidal
inst✝¹ : G.LaxMonoidal
τ : (i : I) → F ⋙ eval C i ⟶ G ⋙ eval C i
inst✝ : ∀ (i : I), NatTrans.IsMonoidal (τ i)
i : I
⊢ (Functor.LaxMonoidal.ε F ≫ (NatTrans.pi' τ).app (𝟙_ D)) i = Functor.LaxMonoidal.ε G i

Tactic:
;

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : MonoidalCategory D
F G : D ⥤ ((i : I) → C i)
inst✝² : F.LaxMonoidal
inst✝¹ : G.LaxMonoidal
τ : (i : I) → F ⋙ eval C i ⟶ G ⋙ eval C i
inst✝ : ∀ (i : I), NatTrans.IsMonoidal (τ i)
i : I
⊢ (Functor.LaxMonoidal.ε F ≫ (NatTrans.pi' τ).app (𝟙_ D)) i = Functor.LaxMonoidal.ε G i
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: 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 : u ⟶ v), { left := 0 • x.left, right := 0 • x.right, w := ⋯ } = 0

Tactic:
;

Goal state after:
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 : u ⟶ v), { left := 0 • x.left, right := 0 • x.right, w := ⋯ } = 0
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : MonoidalCategory D
F G : D ⥤ ((i : I) → C i)
inst✝² : F.LaxMonoidal
inst✝¹ : G.LaxMonoidal
τ : (i : I) → F ⋙ eval C i ⟶ G ⋙ eval C i
inst✝ : ∀ (i : I), NatTrans.IsMonoidal (τ i)
X Y : D
i : I
⊢ (Functor.LaxMonoidal.μ F X Y ≫ (NatTrans.pi' τ).app (X ⊗ Y)) i =
    (((NatTrans.pi' τ).app X ⊗ₘ (NatTrans.pi' τ).app Y) ≫ Functor.LaxMonoidal.μ G X Y) i

Tactic:
;

Goal state after:
I : Type w₁
C : I → Type u₁
inst✝⁶ : (i : I) → Category.{v₁, u₁} (C i)
inst✝⁵ : (i : I) → MonoidalCategory (C i)
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : MonoidalCategory D
F G : D ⥤ ((i : I) → C i)
inst✝² : F.LaxMonoidal
inst✝¹ : G.LaxMonoidal
τ : (i : I) → F ⋙ eval C i ⟶ G ⋙ eval C i
inst✝ : ∀ (i : I), NatTrans.IsMonoidal (τ i)
X Y : D
i : I
⊢ (Functor.LaxMonoidal.μ F X Y ≫ (NatTrans.pi' τ).app (X ⊗ Y)) i =
    (((NatTrans.pi' τ).app X ⊗ₘ (NatTrans.pi' τ).app Y) ≫ Functor.LaxMonoidal.μ G X Y) i
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: 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 := x✝¹ • x✝.left, right := x✝¹ • x✝.right, w := ⋯ } + x✝

Tactic:
;

Goal state after:
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 := x✝¹ • x✝.left, right := x✝¹ • x✝.right, w := ⋯ } + x✝
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: 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
⊢ ∀ (a : u ⟶ v), { left := 0 • a.left, right := 0 • a.right, w := ⋯ } = 0

Tactic:
;

Goal state after:
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
⊢ ∀ (a : u ⟶ v), { left := 0 • a.left, right := 0 • a.right, w := ⋯ } = 0
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: 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 := ↑x✝¹ • x✝.left, right := ↑x✝¹ • x✝.right, w := ⋯ } + x✝

Tactic:
;

Goal state after:
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 := ↑x✝¹ • x✝.left, right := ↑x✝¹ • x✝.right, w := ⋯ } + x✝
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
M : DMatrix m n α
β : m → n → Type w
γ : m → n → Type z
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
g : ⦃i : m⦄ → ⦃j : n⦄ → β i j → γ i j
i✝ : m
j✝ : n
⊢ (M.map f).map g i✝ j✝ = M.map (fun x x_1 x_2 ↦ g (f x_2)) i✝ j✝

Tactic:
;

Goal state after:
m : Type u_1
n : Type u_2
α : m → n → Type v
M : DMatrix m n α
β : m → n → Type w
γ : m → n → Type z
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
g : ⦃i : m⦄ → ⦃j : n⦄ → β i j → γ i j
i✝ : m
j✝ : n
⊢ (M.map f).map g i✝ j✝ = M.map (fun x x_1 x_2 ↦ g (f x_2)) i✝ j✝
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → Zero (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → Zero (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
h : ∀ (i : m) (j : n), f 0 = 0
i✝ : m
j✝ : n
⊢ map 0 f i✝ j✝ = 0 i✝ j✝

Tactic:
;

Goal state after:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → Zero (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → Zero (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j
h : ∀ (i : m) (j : n), f 0 = 0
i✝ : m
j✝ : n
⊢ map 0 f i✝ j✝ = 0 i✝ j✝
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
i✝ : m
j✝ : n
⊢ (M + N).map (fun i j ↦ ⇑f) i✝ j✝ = ((M.map fun i j ↦ ⇑f) + N.map fun i j ↦ ⇑f) i✝ j✝

Tactic:
;

Goal state after:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddMonoid (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddMonoid (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
i✝ : m
j✝ : n
⊢ (M + N).map (fun i j ↦ ⇑f) i✝ j✝ = ((M.map fun i j ↦ ⇑f) + N.map fun i j ↦ ⇑f) i✝ j✝
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
i✝ : m
j✝ : n
⊢ (M - N).map (fun i j ↦ ⇑f) i✝ j✝ = ((M.map fun i j ↦ ⇑f) - N.map fun i j ↦ ⇑f) i✝ j✝

Tactic:
;

Goal state after:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝¹ : (i : m) → (j : n) → AddGroup (α i j)
β : m → n → Type w
inst✝ : (i : m) → (j : n) → AddGroup (β i j)
f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j
M N : DMatrix m n α
i✝ : m
j✝ : n
⊢ (M - N).map (fun i j ↦ ⇑f) i✝ j✝ = ((M.map fun i j ↦ ⇑f) - N.map fun i j ↦ ⇑f) i✝ j✝
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝ : IsEmpty m
M N : DMatrix m n α
i : m
j✝ : n
⊢ M i j✝ = N i j✝

Tactic:
exact isEmptyElim i

Goal state after:
Module: Mathlib.Data.Matrix.DMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝ : IsEmpty n
M N : DMatrix m n α
i : m
j : n
⊢ M i j = N i j

Tactic:
;

Goal state after:
m : Type u_1
n : Type u_2
α : m → n → Type v
inst✝ : IsEmpty n
M N : DMatrix m n α
i : m
j : n
⊢ M i j = N i j
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: case intro
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a ↦ s (f a)) ≅ ⨁ fun b ↦ s (g b)
c : ι
val✝ : Fintype α
⊢ Cardinal.mk ↑(f ⁻¹' {c}) = Cardinal.mk ↑(g ⁻¹' {c})

Tactic:
;

Goal state after:
case intro
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a ↦ s (f a)) ≅ ⨁ fun b ↦ s (g b)
c : ι
val✝ : Fintype α
⊢ Cardinal.mk ↑(f ⁻¹' {c}) = Cardinal.mk ↑(g ⁻¹' {c})
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y Z : C
f : X ⟶ Y
g h : Y ⟶ Z
⊢ f ≫ (g + h) = f ≫ g + f ≫ h

Tactic:
by
  simp only [add_eq_left_addition, ← Category.assoc]
  congr
  ext <;> simp

Goal state after:
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 κ { carrier := ↑↑S, str := Subtype.partialOrder fun x ↦ x ∈ ↑S }

Tactic:
;

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
M N K : Mat_ C
f f' : M ⟶ N
g : N ⟶ K
i✝ : M.ι
j✝ : K.ι
⊢ ((f + f') ≫ g) i✝ j✝ = (f ≫ g + f' ≫ g) i✝ j✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M N K : Mat_ C
f f' : M ⟶ N
g : N ⟶ K
i✝ : M.ι
j✝ : K.ι
⊢ ((f + f') ≫ g) i✝ j✝ = (f ≫ g + f' ≫ g) i✝ j✝
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M N K : Mat_ C
f : M ⟶ N
g g' : N ⟶ K
i✝ : M.ι
j✝ : K.ι
⊢ (f ≫ (g + g')) i✝ j✝ = (f ≫ g + f ≫ g') i✝ j✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M N K : Mat_ C
f : M ⟶ N
g g' : N ⟶ K
i✝ : M.ι
j✝ : K.ι
⊢ (f ≫ (g + g')) i✝ j✝ = (f ≫ g + f ≫ g') i✝ j✝
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').ι
⊢ (∑ j_1,
      (if h : i = i then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = i 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'⟩

pp: case h₀
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').ι
⊢ ∀ b ∈ Finset.univ,
    b ≠ i →
      (∑ j_1,
          (if h : i = b then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
            if h : i' = b then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
        0

pp: case h₁
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').ι
⊢ i ∉ Finset.univ →
    (∑ j_1,
        (if h : i = i then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
          if h : i' = i then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
      0

Tactic:
;

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').ι
⊢ (∑ j_1,
      (if h : i = i then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = i 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'⟩

case h₀
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').ι
⊢ ∀ b ∈ Finset.univ,
    b ≠ i →
      (∑ j_1,
          (if h : i = b then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
            if h : i' = b then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
        0

case h₁
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').ι
⊢ i ∉ Finset.univ →
    (∑ j_1,
        (if h : i = i then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
          if h : i' = i then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
      0
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').ι
⊢ ((if h : i = i then if h' : h ▸ j = j then eqToHom ⋯ else 0 else 0) ≫
      if h : i' = i then if h' : h ▸ j' = j 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'⟩

pp: case h₀
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').ι
⊢ ∀ b ∈ Finset.univ,
    b ≠ j →
      ((if h : i = i then if h' : h ▸ j = b then eqToHom ⋯ else 0 else 0) ≫
          if h : i' = i then if h' : h ▸ j' = b then eqToHom ⋯ else 0 else 0) =
        0

pp: case h₁
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').ι
⊢ j ∉ Finset.univ →
    ((if h : i = i then if h' : h ▸ j = j then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = j then eqToHom ⋯ else 0 else 0) =
      0

Tactic:
;

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').ι
⊢ ((if h : i = i then if h' : h ▸ j = j then eqToHom ⋯ else 0 else 0) ≫
      if h : i' = i then if h' : h ▸ j' = j 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'⟩

case h₀
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').ι
⊢ ∀ b ∈ Finset.univ,
    b ≠ j →
      ((if h : i = i then if h' : h ▸ j = b then eqToHom ⋯ else 0 else 0) ≫
          if h : i' = i then if h' : h ▸ j' = b then eqToHom ⋯ else 0 else 0) =
        0

case h₁
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').ι
⊢ j ∉ Finset.univ →
    ((if h : i = i then if h' : h ▸ j = j then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = j then eqToHom ⋯ else 0 else 0) =
      0
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: case refine_1
κ : 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
⊢ ∃ i xi, f = (ConcreteCategory.hom (((coyoneda.obj (Opposite.op J)).mapCocone c).ι.app i)) xi

Tactic:
let φ (x : J.obj) : (F.obj m).obj := F.map (IsCardinalFiltered.toMax j hJ x) (g x)

Goal state after:
case refine_1
κ : 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)
⊢ ∃ i xi, f = (ConcreteCategory.hom (((coyoneda.obj (Opposite.op J)).mapCocone c).ι.app i)) xi
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
D : Type u_1
inst✝¹ : Category.{v₁, u_1} D
inst✝ : Preadditive D
ι✝ : Type
fintype✝ : Fintype ι✝
X✝ : ι✝ → C
⊢ (𝟭 C).mapMat_.obj { ι := ι✝, fintype := fintype✝, X := X✝ } =
    (𝟭 (Mat_ C)).obj { ι := ι✝, fintype := fintype✝, X := X✝ }

Tactic:
;

Goal state after:
case mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
D : Type u_1
inst✝¹ : Category.{v₁, u_1} D
inst✝ : Preadditive D
ι✝ : Type
fintype✝ : Fintype ι✝
X✝ : ι✝ → C
⊢ (𝟭 C).mapMat_.obj { ι := ι✝, fintype := fintype✝, X := X✝ } =
    (𝟭 (Mat_ C)).obj { ι := ι✝, fintype := fintype✝, X := X✝ }
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
D : Type u_1
inst✝¹ : Category.{v₁, u_1} D
inst✝ : Preadditive D
N : Mat_ C
j✝ : ((𝟭 (Mat_ C)).obj N).ι
ι✝ : Type
fintype✝ : Fintype ι✝
X✝ : ι✝ → C
f : { ι := ι✝, fintype := fintype✝, X := X✝ } ⟶ N
i✝ : ((𝟭 C).mapMat_.obj { ι := ι✝, fintype := fintype✝, X := X✝ }).ι
⊢ ((𝟭 C).mapMat_.map f ≫ (eqToIso ⋯).hom) i✝ j✝ = ((eqToIso ⋯).hom ≫ (𝟭 (Mat_ C)).map f) i✝ j✝

Tactic:
;

Goal state after:
case mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
D : Type u_1
inst✝¹ : Category.{v₁, u_1} D
inst✝ : Preadditive D
N : Mat_ C
j✝ : ((𝟭 (Mat_ C)).obj N).ι
ι✝ : Type
fintype✝ : Fintype ι✝
X✝ : ι✝ → C
f : { ι := ι✝, fintype := fintype✝, X := X✝ } ⟶ N
i✝ : ((𝟭 C).mapMat_.obj { ι := ι✝, fintype := fintype✝, X := X✝ }).ι
⊢ ((𝟭 C).mapMat_.map f ≫ (eqToIso ⋯).hom) i✝ j✝ = ((eqToIso ⋯).hom ≫ (𝟭 (Mat_ C)).map f) i✝ j✝