awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : (f i).ι
h : Membership.mem (γ := Finset (f i).ι) Finset.univ b
hb : b ≠ j
H : ¬j = b
⊢ ¬Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j ⋯ = b

Tactic:
simp only
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : (f i).ι
h : Membership.mem (γ := Finset (f i).ι) Finset.univ b
hb : b ≠ j
H H₁ H₂ H₃ H₄ H₅ H₆ H₇ : j = b → False
⊢ ¬j = b

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
hj : j ∉ Finset.univ
⊢ Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
    (CategoryStruct.comp (Y := (f i).X j)
      (if h : i = i then
        if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j h = j then eqToHom ⋯ else 0
      else 0)
      (if h : i' = i then
        if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = j then eqToHom ⋯ else 0
      else 0))
    0

Tactic:
simp at hj
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
H :
  Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
    (if h : i' = i then
      if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = j then eqToHom ⋯ else 0
    else 0)
    (if h : i = i' ∧ j ≍ j' then eqToHom ⋯ else 0)
⊢ Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
    (CategoryStruct.comp (Y := (f i).X j)
        (if h : i = i then
          if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j h = j then eqToHom ⋯ else 0
        else 0)
        (if h : i' = i then
          if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = j then eqToHom ⋯ else 0
        else 0) :
      (f i).X j ⟶ (f i').X j')
    (CategoryStruct.id.{v₁, max 1 u₁}
        { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype,
          X := fun (p : (j : Fin n) × (f j).ι) ↦
            (f (p.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (p.snd (β := fun (j : Fin n) ↦ (f j).ι)) }
        (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) i j) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) i' j') :
      (fun
            (i j :
              ι.{u₁} (C := C)
                { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype,
                  X := fun (p : (j : Fin n) × (f j).ι) ↦
                    (f (p.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (p.snd (β := fun (j : Fin n) ↦ (f j).ι)) }) ↦
          Quiver.Hom.{v₁, u₁}
            (X
              { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype,
                X := fun (p : (j : Fin n) × (f j).ι) ↦
                  (f (p.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (p.snd (β := fun (j : Fin n) ↦ (f j).ι)) :
                Mat_ C }
              i)
            (X
              { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype,
                X := fun (p : (j : Fin n) × (f j).ι) ↦
                  (f (p.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (p.snd (β := fun (j : Fin n) ↦ (f j).ι)) }
              j))
        (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) i j) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) i' j'))

Tactic:
simp only [eqToHom_refl, dite_eq_ite, ite_true, Category.id_comp,
              Sigma.mk.inj_iff, id_def]

Premises used: CategoryTheory.eqToHom_refl, ite_true, Sigma.mk.inj_iff, dite_eq_ite, CategoryTheory.Mat_.id_def, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
pos :
  ∀ (h : i' = i),
    Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
      (if h : i' = i then
        if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = j then eqToHom ⋯ else 0
      else 0)
      (if h : i = i' ∧ j ≍ j' then eqToHom ⋯ else 0)
neg :
  ∀ (h : ¬i' = i),
    Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
      (if h : i' = i then
        if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = j then eqToHom ⋯ else 0
      else 0)
      (if h : i = i' ∧ j ≍ j' then eqToHom ⋯ else 0)
⊢ Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
    (if h : i' = i then
      if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = j then eqToHom ⋯ else 0
    else 0)
    (if h : i = i' ∧ j ≍ j' then eqToHom ⋯ else 0)

Tactic:
by_cases h : i' = i
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
h : i' = i
pos :
  ∀ (j : (f i').ι),
    Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j')
      (if h : i' = i' then
        if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = j then eqToHom ⋯ else 0
      else 0)
      (if h : i' = i' ∧ j ≍ j' then eqToHom ⋯ else 0)
⊢ Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
    (if h : i' = i then
      if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = j then eqToHom ⋯ else 0
    else 0)
    (if h : i = i' ∧ j ≍ j' then eqToHom ⋯ else 0)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
pos :
  Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j')
    (if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' ⋯ = j then eqToHom ⋯ else 0)
    (if h : i' = i' ∧ j ≍ j' then eqToHom ⋯ else 0)
⊢ Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j')
    (if h : i' = i' then
      if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = j then eqToHom ⋯ else 0
    else 0)
    (if h : i' = i' ∧ j ≍ j' then eqToHom ⋯ else 0)

Tactic:
rw [dif_pos rfl]

Premises used: dif_pos, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
pos :
  Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j') (if h' : j' = j then eqToHom ⋯ else 0)
    (if h : j = j' then eqToHom ⋯ else 0)
⊢ Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j')
    (if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' ⋯ = j then eqToHom ⋯ else 0)
    (if h : i' = i' ∧ j ≍ j' then eqToHom ⋯ else 0)

Tactic:
simp only [heq_eq_eq, true_and]

Premises used: heq_eq_eq, true_and
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
pos :
  ∀ (h : j' = j),
    Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j') (if h' : j' = j then eqToHom ⋯ else 0)
      (if h : j = j' then eqToHom ⋯ else 0)
neg :
  ∀ (h : ¬j' = j),
    Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j') (if h' : j' = j then eqToHom ⋯ else 0)
      (if h : j = j' then eqToHom ⋯ else 0)
⊢ Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j') (if h' : j' = j then eqToHom ⋯ else 0)
    (if h : j = j' then eqToHom ⋯ else 0)

Tactic:
by_cases h : j' = j
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
h : j' = j
pos :
  Eq.{v₁ + 1} (α := (f i').X j' ⟶ (f i').X j') (if h' : j' = j' then eqToHom ⋯ else 0)
    (if h : j' = j' then eqToHom ⋯ else 0)
⊢ Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j') (if h' : j' = j then eqToHom ⋯ else 0)
    (if h : j = j' then eqToHom ⋯ else 0)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' : (f i').ι
⊢ Eq.{v₁ + 1} (α := (f i').X j' ⟶ (f i').X j') (if h' : j' = j' then eqToHom ⋯ else 0)
    (if h : j' = j' then eqToHom ⋯ else 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
h : ¬j' = j
neg : Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j') 0 (if h : j = j' then eqToHom ⋯ else 0)
neg₁ neg₂ : Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j') 0 0
⊢ Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j') (if h' : j' = j then eqToHom ⋯ else 0)
    (if h : j = j' then eqToHom ⋯ else 0)

Tactic:
rw [dif_neg h, dif_neg (Ne.symm h)]

Premises used: Ne.symm, dif_neg
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
h : ¬i' = i
neg : ¬(i = i' ∧ j ≍ j')
⊢ Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
    (if h : i' = i then
      if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = j then eqToHom ⋯ else 0
    else 0)
    (if h : i = i' ∧ j ≍ j' then eqToHom ⋯ else 0)

Tactic:
rw [dif_neg h, dif_neg]

Premises used: dif_neg
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
h : ¬i' = i
neg neg₁ neg₂ neg₃ neg₄ neg₅ neg₆ neg₇ : i = i' → j ≍ j' → False
⊢ ¬(i = i' ∧ j ≍ j')

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u_1
inst_2 : Category.{v₁, u_1} D
inst_3 : Preadditive.{v₁, u_1} D
M : Mat_ C
mk :
  ∀ (ι : Type) [fintype : Fintype ι] (X : ι → C),
    Eq.{(max 1 u₁) + 1}
      (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) { ι := ι, fintype := fintype, X := X : Mat_ C })
      (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C))
        { ι := ι, fintype := fintype, X := X : Mat_ C })
⊢ Eq.{(max 1 u₁) + 1} (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) M)
    (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C)) M)

Tactic:
cases M
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u_1
inst_2 : Category.{v₁, u_1} D
inst_3 : Preadditive.{v₁, u_1} D
ι : Type
fintype : Fintype ι
X : ι → C
⊢ Eq.{(max 1 u₁) + 1} (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (mapMat_ (𝟭 C)) { ι := ι, fintype := fintype, X := X : Mat_ C })
    (obj.{v₁, v₁, max 1 u₁, max 1 u₁} (Functor.id.{v₁, max 1 u₁} (Mat_ C))
      { ι := ι, fintype := fintype, X := X : Mat_ C })

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u_1
inst_2 : Category.{v₁, u_1} D
inst_3 : Preadditive.{v₁, u_1} D
E : Type u_2
inst_4 : Category.{v₁, u_2} E
inst_5 : Preadditive.{v₁, u_2} E
F : Functor.{v₁, v₁, u₁, u_1} C D
inst_6 : F.Additive
G : Functor.{v₁, v₁, u_1, u_2} D E
inst_7 : G.Additive
M : Mat_ C
mk :
  ∀ (ι : Type) [fintype : Fintype ι] (X : ι → C),
    Eq.{(max 1 u_2) + 1}
      (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ { ι := ι, fintype := fintype, X := X : Mat_ C })
      (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_)
        { ι := ι, fintype := fintype, X := X : Mat_ C })
⊢ Eq.{(max 1 u_2) + 1} (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ M)
    (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_) M)

Tactic:
cases M
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u_1
inst_2 : Category.{v₁, u_1} D
inst_3 : Preadditive.{v₁, u_1} D
E : Type u_2
inst_4 : Category.{v₁, u_2} E
inst_5 : Preadditive.{v₁, u_2} E
F : Functor.{v₁, v₁, u₁, u_1} C D
inst_6 : F.Additive
G : Functor.{v₁, v₁, u_1, u_2} D E
inst_7 : G.Additive
ι : Type
fintype : Fintype ι
X : ι → C
⊢ Eq.{(max 1 u_2) + 1}
    (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (F ⋙ G).mapMat_ { ι := ι, fintype := fintype, X := X : Mat_ C })
    (obj.{v₁, v₁, max 1 u₁, max 1 u_2} (comp.{v₁, v₁, v₁, max 1 u₁, max 1 u_1, max 1 u_2} F.mapMat_ G.mapMat_)
      { ι := ι, fintype := fintype, X := X : Mat_ C })

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
x : C
H :
  ∀ (j : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x }),
    Eq.{v₁ + 1} (α :=
      (fun (i j : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x }) ↦
          Quiver.Hom.{v₁, u₁}
            (X { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x : Mat_ C } i)
            (X { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x } j))
        PUnit.unit j)
      (𝟙 x)
      (CategoryStruct.id.{v₁, max 1 u₁} { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x }
        PUnit.unit j)
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, max 1 u₁} (V := Mat_ C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x }
      { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x })
    (fun (x_1 x_2 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_2 : PUnit.{1}) ↦ x }) ↦ 𝟙 x)
    (CategoryStruct.id.{v₁, max 1 u₁} { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x })

Tactic:
ext ⟨⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
x : C
j : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x }
⊢ Eq.{v₁ + 1} (α :=
    (fun (i j : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x }) ↦
        Quiver.Hom.{v₁, u₁} (X { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x : Mat_ C } i)
          (X { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x } j))
      PUnit.unit j)
    (𝟙 x)
    (CategoryStruct.id.{v₁, max 1 u₁} { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x_1 : PUnit.{1}) ↦ x }
      PUnit.unit j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y Z : C
x : X ⟶ Y
x_1 : Y ⟶ Z
H :
  ∀ (j : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Z }),
    x ≫ x_1 =
      CategoryStruct.comp.{v₁, max 1 u₁} (Y :=
        { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Y })
        (fun (x_2 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ X })
            (x_3 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Y }) ↦
          x)
        (fun (x : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Y })
            (x_2 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Z }) ↦
          x_1)
        PUnit.unit j
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, max 1 u₁} (V := Mat_ C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ X }
      { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Z })
    (fun (x_2 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ X })
        (x_3 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Z }) ↦
      x ≫ x_1)
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y :=
      { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Y })
      (fun (x_2 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ X })
          (x_3 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Y }) ↦
        x)
      fun (x : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Y })
        (x_2 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Z }) ↦
      x_1)

Tactic:
ext ⟨⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y Z : C
x : X ⟶ Y
x_1 : Y ⟶ Z
j : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Z }
⊢ x ≫ x_1 =
    CategoryStruct.comp.{v₁, max 1 u₁} (Y := { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Y })
      (fun (x_2 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ X })
          (x_3 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Y }) ↦
        x)
      (fun (x : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Y })
          (x_2 : ι.{u₁} (C := C) { ι := PUnit.{1}, fintype := PUnit.fintype, X := fun (x : PUnit.{1}) ↦ Z }) ↦
        x_1)
      PUnit.unit j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
simp :
  Eq.{v₁ + 1} (α := Quiver.Hom.{v₁, max 1 u₁} M M)
    (∑ j : M.ι,
      CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
        (fun (j_1 : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) ↦
          if h : j_1 = j then eqToHom ⋯ else 0)
        fun (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) (k : M.ι) ↦
        if h : j = k then eqToHom ⋯ else 0)
    (CategoryStruct.id.{v₁, max 1 u₁} M)
⊢ Eq.{v₁ + 1} (α := Quiver.Hom.{v₁, max 1 u₁} M M)
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y :=
      biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
      (biproduct.lift.{0, v₁, max 1 u₁}
        fun (i j : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) ↦
        if h : j = i then eqToHom ⋯ else 0)
      (biproduct.desc.{0, v₁, max 1 u₁}
        fun (i : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) (k : M.ι) ↦
        if h : i = k then eqToHom ⋯ else 0))
    (CategoryStruct.id.{v₁, max 1 u₁} M)

Tactic:
simp only [biproduct.lift_desc]

Premises used: CategoryTheory.Limits.biproduct.lift_desc
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
h :
  ∀ (i j : M.ι),
    Eq.{v₁ + 1} (α := (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)
      ((∑ j : M.ι,
            CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
              (fun (j_1 : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) ↦
                if h : j_1 = j then eqToHom ⋯ else 0)
              fun (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) (k : M.ι) ↦
              if h : j = k then eqToHom ⋯ else 0)
          i j :
        (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)
      (CategoryStruct.id.{v₁, max 1 u₁} M i j : (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)
⊢ Eq.{v₁ + 1} (α := Quiver.Hom.{v₁, max 1 u₁} M M)
    (∑ j : M.ι,
      CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
        (fun (j_1 : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) ↦
          if h : j_1 = j then eqToHom ⋯ else 0)
        fun (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) (k : M.ι) ↦
        if h : j = k then eqToHom ⋯ else 0)
    (CategoryStruct.id.{v₁, max 1 u₁} M)

Tactic:
funext i j
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
i j : M.ι
h :
  Eq.{v₁ + 1} (α := M.X i ⟶ M.X j)
    ((∑ j : M.ι,
        CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
          (fun (j_1 : M.ι) (x : PUnit.{1}) ↦ if h : j_1 = j then eqToHom ⋯ else 0) fun (x : PUnit.{1}) (k : M.ι) ↦
          if h : j = k then eqToHom ⋯ else 0)
      i j)
    (if h : i = j then eqToHom ⋯ else 0)
⊢ Eq.{v₁ + 1} (α := (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)
    ((∑ j : M.ι,
          CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
            (fun (j_1 : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) ↦
              if h : j_1 = j then eqToHom ⋯ else 0)
            fun (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) (k : M.ι) ↦
            if h : j = k then eqToHom ⋯ else 0)
        i j :
      (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)
    (CategoryStruct.id.{v₁, max 1 u₁} M i j : (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)

Tactic:
dsimp [id_def]

Premises used: CategoryTheory.Mat_.id_def
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
i j : M.ι
h :
  Eq.{v₁ + 1} (α := M.X i ⟶ M.X j)
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
      (fun (j : M.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0)
      (fun (x : PUnit.{1}) (k : M.ι) ↦ if h : i = k then eqToHom ⋯ else 0) i j)
    (if h : i = j then eqToHom ⋯ else 0)
h₁ :
  ∀ (b : M.ι),
    Membership.mem (γ := Finset M.ι) Finset.univ b →
      b ≠ i →
        Eq.{v₁ + 1} (α := (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)
          (CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X b))
            (fun (j : M.ι) (x : PUnit.{1}) ↦ if h : j = b then eqToHom ⋯ else 0)
            (fun (x : PUnit.{1}) (k : M.ι) ↦ if h : b = k then eqToHom ⋯ else 0) i j)
          0
h₂ :
  i ∉ Finset.univ →
    Eq.{v₁ + 1} (α := (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)
      (CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
        (fun (j : M.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0)
        (fun (x : PUnit.{1}) (k : M.ι) ↦ if h : i = k then eqToHom ⋯ else 0) i j)
      0
⊢ Eq.{v₁ + 1} (α := M.X i ⟶ M.X j)
    ((∑ j : M.ι,
        CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
          (fun (j_1 : M.ι) (x : PUnit.{1}) ↦ if h : j_1 = j then eqToHom ⋯ else 0) fun (x : PUnit.{1}) (k : M.ι) ↦
          if h : j = k then eqToHom ⋯ else 0)
      i j)
    (if h : i = j then eqToHom ⋯ else 0)

Tactic:
rw [Finset.sum_apply, Finset.sum_apply, Finset.sum_eq_single i]

Premises used: Finset.sum_apply, Finset.sum_eq_single
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
i j b : M.ι
h :
  Membership.mem (γ := Finset M.ι) Finset.univ b →
    b ≠ i →
      Eq.{v₁ + 1} (α := (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)
        (CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X b))
          (fun (j : M.ι) (x : PUnit.{1}) ↦ if h : j = b then eqToHom ⋯ else 0)
          (fun (x : PUnit.{1}) (k : M.ι) ↦ if h : b = k then eqToHom ⋯ else 0) i j)
        0
⊢ Membership.mem (γ := Finset M.ι) Finset.univ b →
    b ≠ i →
      Eq.{v₁ + 1} (α := (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)
        (CategoryStruct.comp.{v₁, max 1 u₁} (Y := Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X b))
          (fun (j : M.ι) (x : PUnit.{1}) ↦ if h : j = b then eqToHom ⋯ else 0)
          (fun (x : PUnit.{1}) (k : M.ι) ↦ if h : b = k then eqToHom ⋯ else 0) i j)
        0

Tactic:
_