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
j : Fin n
x : (f j).ι
y :
  ι.{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).ι)) }
h : y.fst (β := fun (j : Fin n) ↦ (f j).ι) = j
h' : Eq.ndrec (motive := fun (j : Fin n) ↦ (f j).ι) (y.snd (β := fun (j : Fin n) ↦ (f j).ι)) h = x
p :
  (f j).X x =
    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).ι)) }
      y
⊢ (fun (i : (f j).ι)
        (j_1 :
          ι.{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₁} ((f j).X 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_1))
    x y

Tactic:
apply eqToHom

Premises used: CategoryTheory.eqToHom
-- 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
j : Fin n
x : (f j).ι
y :
  ι.{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).ι)) }
h : y.fst (β := fun (j : Fin n) ↦ (f j).ι) = j
h' : Eq.ndrec (motive := fun (j : Fin n) ↦ (f j).ι) (y.snd (β := fun (j : Fin n) ↦ (f j).ι)) h = x
p :
  (f (y.fst (β := fun (j : Fin n) ↦ (f j).ι))).X
      (Eq.ndrec (motive := fun (j : Fin n) ↦ (f j).ι) (y.snd (β := fun (j : Fin n) ↦ (f j).ι)) ⋯) =
    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).ι)) }
      y
⊢ (f j).X x =
    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).ι)) }
      y

Tactic:
substs h 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
y :
  ι.{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).ι)) }
⊢ (f (y.fst (β := fun (j : Fin n) ↦ (f j).ι))).X
      (Eq.ndrec (motive := fun (j : Fin n) ↦ (f j).ι) (y.snd (β := fun (j : Fin n) ↦ (f j).ι)) ⋯) =
    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).ι)) }
      y

Tactic:
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
j j' : Fin n
x : (f j).ι
y : (f j').ι
H :
  Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y)
    (∑ j_1 : (j : Fin n) × (f j).ι,
      CategoryStruct.comp (Y :=
        (f (j_1.fst (β := fun (j : Fin n) ↦ (f j).ι))).X (j_1.snd (β := fun (j : Fin n) ↦ (f j).ι)))
        (if h : j_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = j then
          if h' :
              Eq.rec (motive := fun (x : Fin n) (x_1 : j_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = x) ↦ (f x).ι)
                  (j_1.snd (β := fun (j : Fin n) ↦ (f j).ι)) h =
                x then
            eqToHom ⋯
          else 0
        else 0)
        (if h : j_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = j' then
          if h' :
              Eq.rec (motive := fun (x : Fin n) (x_1 : j_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = x) ↦ (f x).ι)
                  (j_1.snd (β := fun (j : Fin n) ↦ (f j).ι)) h =
                y then
            eqToHom ⋯
          else 0
        else 0))
    ((if h : j = j' then eqToHom.{v₁, max 1 u₁} ⋯ else 0) x y)
⊢ Eq.{v₁ + 1} (α := (fun (i : (f j).ι) (j_1 : (f j').ι) ↦ Quiver.Hom.{v₁, u₁} ((f j).X i) ((f j').X j_1)) x y)
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y :=
      { ι := (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).ι)) })
      (fun (x : (f j).ι)
          (y :
            ι.{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).ι)) }) ↦
        if h : y.fst (β := fun (j : Fin n) ↦ (f j).ι) = j then
          if h' : Eq.ndrec (motive := fun (j : Fin n) ↦ (f j).ι) (y.snd (β := fun (j : Fin n) ↦ (f j).ι)) h = x then
            eqToHom ⋯
          else 0
        else 0)
      (fun
          (x :
            ι.{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).ι)) })
          (y : (f j').ι) ↦
        if h : x.fst (β := fun (j : Fin n) ↦ (f j).ι) = j' then
          if h' : Eq.ndrec (motive := fun (j : Fin n) ↦ (f j).ι) (x.snd (β := fun (j : Fin n) ↦ (f j).ι)) h = y then
            eqToHom ⋯
          else 0
        else 0)
      x y)
    ((if h : j = j' then eqToHom.{v₁, max 1 u₁} ⋯ else 0) x y)

Tactic:
dsimp
-- 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
j j' : Fin n
x : (f j).ι
y : (f j').ι
H :
  Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y)
    (∑ a : Fin n,
      ∑ s : (f a).ι,
        if h : Sigma.fst (β := fun (j : Fin n) ↦ (f j).ι) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) a s) = j then
          if h_1 :
              Eq.rec (motive :=
                  fun (x : Fin n)
                    (x_1 :
                      Sigma.fst (β := fun (j : Fin n) ↦ (f j).ι) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) a s) = x) ↦
                  (f x).ι) (Sigma.snd (β := fun (j : Fin n) ↦ (f j).ι) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) a s))
                  ⋯ =
                x then
            if h_2 :
                Sigma.fst (β := fun (j : Fin n) ↦ (f j).ι) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) a s) = j' then
              if h_3 :
                  Eq.rec (motive :=
                      fun (x : Fin n)
                        (x_1 :
                          Sigma.fst (β := fun (j : Fin n) ↦ (f j).ι) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) a s) =
                            x) ↦
                      (f x).ι)
                      (Sigma.snd (β := fun (j : Fin n) ↦ (f j).ι) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) a s)) ⋯ =
                    y then
                eqToHom ⋯
              else 0
            else 0
          else 0
        else 0)
    ((if h : j = j' then eqToHom.{v₁, max 1 u₁} ⋯ else 0) x y)
⊢ Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y)
    (∑ x_1 : (j : Fin n) × (f j).ι,
      if h : x_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = j then
        if h_1 :
            Eq.rec (motive := fun (x : Fin n) (x_2 : x_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = x) ↦ (f x).ι)
                (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι)) ⋯ =
              x then
          if h_2 : x_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = j' then
            if h_3 :
                Eq.rec (motive := fun (x : Fin n) (x_2 : x_1.fst (β := fun (j : Fin n) ↦ (f j).ι) = x) ↦ (f x).ι)
                    (x_1.snd (β := fun (j : Fin n) ↦ (f j).ι)) ⋯ =
                  y then
              eqToHom ⋯
            else 0
          else 0
        else 0
      else 0)
    ((if h : j = j' then eqToHom.{v₁, max 1 u₁} ⋯ else 0) x y)

Tactic:
rw [← Finset.univ_sigma_univ, Finset.sum_sigma]

Premises used: Finset.sum_sigma, Finset.univ_sigma_univ
-- 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
j j' : Fin n
x : (f j).ι
y : (f j').ι
H :
  Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y)
    (∑ a : Fin n,
      ∑ s : (f a).ι,
        if h : a = j then
          if h_1 : Eq.rec (motive := fun (x : Fin n) (x_1 : a = x) ↦ (f x).ι) s ⋯ = x then
            if h_2 : a = j' then
              if h_3 : Eq.rec (motive := fun (x : Fin n) (x_1 : a = x) ↦ (f x).ι) s ⋯ = y then eqToHom ⋯ else 0
            else 0
          else 0
        else 0)
    ((if h : j = j' then eqToHom.{v₁, max 1 u₁} ⋯ else 0) x y)
⊢ Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y)
    (∑ a : Fin n,
      ∑ s : (f a).ι,
        if h : Sigma.fst (β := fun (j : Fin n) ↦ (f j).ι) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) a s) = j then
          if h_1 :
              Eq.rec (motive :=
                  fun (x : Fin n)
                    (x_1 :
                      Sigma.fst (β := fun (j : Fin n) ↦ (f j).ι) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) a s) = x) ↦
                  (f x).ι) (Sigma.snd (β := fun (j : Fin n) ↦ (f j).ι) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) a s))
                  ⋯ =
                x then
            if h_2 :
                Sigma.fst (β := fun (j : Fin n) ↦ (f j).ι) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) a s) = j' then
              if h_3 :
                  Eq.rec (motive :=
                      fun (x : Fin n)
                        (x_1 :
                          Sigma.fst (β := fun (j : Fin n) ↦ (f j).ι) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) a s) =
                            x) ↦
                      (f x).ι)
                      (Sigma.snd (β := fun (j : Fin n) ↦ (f j).ι) (Sigma.mk (β := fun (j : Fin n) ↦ (f j).ι) a s)) ⋯ =
                    y then
                eqToHom ⋯
              else 0
            else 0
          else 0
        else 0)
    ((if h : j = j' then eqToHom.{v₁, max 1 u₁} ⋯ else 0) x y)

Tactic:
dsimp +instances
-- 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
j j' : Fin n
x : (f j).ι
y : (f j').ι
H :
  Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y)
    (if h : j = j' then
      if h_1 : Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x ⋯ = y then eqToHom ⋯ else 0
    else 0)
    ((if h : j = j' then eqToHom.{v₁, max 1 u₁} ⋯ else 0) x y)
⊢ Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y)
    (∑ a : Fin n,
      ∑ s : (f a).ι,
        if h : a = j then
          if h_1 : Eq.rec (motive := fun (x : Fin n) (x_1 : a = x) ↦ (f x).ι) s ⋯ = x then
            if h_2 : a = j' then
              if h_3 : Eq.rec (motive := fun (x : Fin n) (x_1 : a = x) ↦ (f x).ι) s ⋯ = y then eqToHom ⋯ else 0
            else 0
          else 0
        else 0)
    ((if h : j = j' then eqToHom.{v₁, max 1 u₁} ⋯ else 0) x y)

Tactic:
simp only [if_true, Finset.sum_dite_irrel, Finset.mem_univ,
                Finset.sum_const_zero, Finset.sum_dite_eq']

Premises used: Finset.mem_univ, Finset.sum_dite_irrel, if_true, Finset.sum_dite_eq', Finset.sum_const_zero
-- 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
j j' : Fin n
x : (f j).ι
y : (f j').ι
pos :
  ∀ (h : j = j') (h' : Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x ⋯ = y),
    Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y) (eqToHom ⋯ : (f j).X x ⟶ (f j').X y)
      (eqToHom.{v₁, max 1 u₁} ⋯ x y :
        (fun (i : (f j).ι) (j_1 : (f j').ι) ↦ Quiver.Hom.{v₁, u₁} ((f j).X i) ((f j').X j_1)) x y)
neg :
  ∀ (h : j = j') (h' : ¬Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x ⋯ = y),
    Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y) (0 : (f j).X x ⟶ (f j').X y)
      (eqToHom.{v₁, max 1 u₁} ⋯ x y :
        (fun (i : (f j).ι) (j_1 : (f j').ι) ↦ Quiver.Hom.{v₁, u₁} ((f j).X i) ((f j').X j_1)) x y)
neg₁ : ∀ (h : ¬j = j'), Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y) 0 (0 x y)
⊢ Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y)
    (if h : j = j' then
      if h_1 : Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x ⋯ = y then eqToHom ⋯ else 0
    else 0)
    ((if h : j = j' then eqToHom.{v₁, max 1 u₁} ⋯ else 0) x y)

Tactic:
split_ifs with h 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
j j' : Fin n
x : (f j).ι
y : (f j').ι
h : j = j'
h' : Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x ⋯ = y
pos :
  Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j).X (Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x ⋯))
    (eqToHom ⋯ : (f j).X x ⟶ (f j).X (Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x ⋯))
    (eqToHom.{v₁, max 1 u₁} ⋯ x (Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x ⋯) :
      (fun (i j_1 : (f j).ι) ↦ Quiver.Hom.{v₁, u₁} ((f j).X i) ((f j).X j_1)) x
        (Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x ⋯))
⊢ Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y) (eqToHom ⋯ : (f j).X x ⟶ (f j').X y)
    (eqToHom.{v₁, max 1 u₁} ⋯ x y :
      (fun (i : (f j).ι) (j_1 : (f j').ι) ↦ Quiver.Hom.{v₁, u₁} ((f j).X i) ((f j').X j_1)) x y)

Tactic:
substs h 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
j : Fin n
x : (f j).ι
⊢ Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j).X (Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x ⋯))
    (eqToHom ⋯ : (f j).X x ⟶ (f j).X (Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x ⋯))
    (eqToHom.{v₁, max 1 u₁} ⋯ x (Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x ⋯) :
      (fun (i j_1 : (f j).ι) ↦ Quiver.Hom.{v₁, u₁} ((f j).X i) ((f j).X j_1)) x
        (Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x ⋯))

Tactic:
simp only [CategoryTheory.eqToHom_refl, CategoryTheory.Mat_.id_apply_self]

Premises used: CategoryTheory.Mat_.id_apply_self, CategoryTheory.eqToHom_refl
-- 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
j j' : Fin n
x : (f j).ι
y : (f j').ι
h : j = j'
h' : ¬Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x ⋯ = y
neg :
  ∀ (y : (f j).ι) (h' : ¬Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x ⋯ = y),
    Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j).X y) (0 : (f j).X x ⟶ (f j).X y)
      (eqToHom.{v₁, max 1 u₁} ⋯ x y : (fun (i j_1 : (f j).ι) ↦ Quiver.Hom.{v₁, u₁} ((f j).X i) ((f j).X j_1)) x y)
⊢ Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y) (0 : (f j).X x ⟶ (f j').X y)
    (eqToHom.{v₁, max 1 u₁} ⋯ x y :
      (fun (i : (f j).ι) (j_1 : (f j').ι) ↦ Quiver.Hom.{v₁, u₁} ((f j).X i) ((f j').X j_1)) x y)

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
j : Fin n
x y : (f j).ι
h' : ¬Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x ⋯ = y
neg :
  Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j).X y) (0 : (f j).X x ⟶ (f j).X y)
    (CategoryStruct.id.{v₁, max 1 u₁} (f j) x y :
      (fun (i j_1 : (f j).ι) ↦ Quiver.Hom.{v₁, u₁} ((f j).X i) ((f j).X j_1)) x y)
neg₁ neg₂ : Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j).X y) 0 0
⊢ Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j).X y) (0 : (f j).X x ⟶ (f j).X y)
    (eqToHom.{v₁, max 1 u₁} ⋯ x y : (fun (i j_1 : (f j).ι) ↦ Quiver.Hom.{v₁, u₁} ((f j).X i) ((f j).X j_1)) x y)

Tactic:
rw [eqToHom_refl, id_apply_of_ne _ _ _ h']

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Mat_.id_apply_of_ne
-- 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
j j' : Fin n
x : (f j).ι
y : (f j').ι
h : ¬j = j'
⊢ Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y) 0 (0 x y)

Tactic:
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 : (f i).ι
i' : Fin n
j' : (f i').ι
b : Fin n
H :
  Membership.mem (γ := Finset (Fin n)) Finset.univ b →
    b ≠ i →
      Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
        (∑ j_1 : (f b).ι,
          CategoryStruct.comp (Y := (f b).X j_1)
            (if h : i = b then
              if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j h = j_1 then eqToHom ⋯ else 0
            else 0)
            (if h : i' = b then
              if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = j_1 then eqToHom ⋯ else 0
            else 0))
        0
⊢ Membership.mem (γ := Finset (Fin n)) Finset.univ b →
    b ≠ i →
      Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
        (∑ j_1 : (f b).ι,
          CategoryStruct.comp (Y := (f b).X j_1)
            (if h : i = b then
              if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j h = j_1 then eqToHom ⋯ else 0
            else 0)
            (if h : i' = b then
              if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = j_1 then eqToHom ⋯ else 0
            else 0))
        0

Tactic:
_
-- 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 : Fin n
h : Membership.mem (γ := Finset (Fin n)) Finset.univ b
hb : b ≠ i
H :
  ∀ (x : (f b).ι),
    Membership.mem (γ := Finset (f b).ι) Finset.univ x →
      Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
        (CategoryStruct.comp (Y := (f b).X x)
          (if h : i = b then
            if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j h = x then eqToHom ⋯ else 0
          else 0)
          (if h : i' = b then
            if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = x then eqToHom ⋯ else 0
          else 0))
        0
⊢ Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
    (∑ j_1 : (f b).ι,
      CategoryStruct.comp (Y := (f b).X j_1)
        (if h : i = b then
          if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j h = j_1 then eqToHom ⋯ else 0
        else 0)
        (if h : i' = b then
          if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = j_1 then eqToHom ⋯ else 0
        else 0))
    0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_eq_zero
-- 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 : Fin n
h : Membership.mem (γ := Finset (Fin n)) Finset.univ b
hb : b ≠ i
x : (f b).ι
H :
  Membership.mem (γ := Finset (f b).ι) Finset.univ x →
    Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
      (CategoryStruct.comp (Y := (f b).X x)
        (if h : i = b then
          if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j h = x then eqToHom ⋯ else 0
        else 0)
        (if h : i' = b then
          if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = x then eqToHom ⋯ else 0
        else 0))
      0
⊢ Membership.mem (γ := Finset (f b).ι) Finset.univ x →
    Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
      (CategoryStruct.comp (Y := (f b).X x)
        (if h : i = b then
          if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j h = x then eqToHom ⋯ else 0
        else 0)
        (if h : i' = b then
          if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = x then eqToHom ⋯ else 0
        else 0))
      0

Tactic:
_
-- 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 : Fin n
h : Membership.mem (γ := Finset (Fin n)) Finset.univ b
hb : b ≠ i
x : (f b).ι
h_1 : Membership.mem (γ := Finset (f b).ι) Finset.univ x
H :
  Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
    (CategoryStruct.comp (Y := (f b).X x) 0
      (if h : i' = b then
        if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = x then eqToHom ⋯ else 0
      else 0))
    0
H₁ H₂ : Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j') 0 0
⊢ Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
    (CategoryStruct.comp (Y := (f b).X x)
      (if h : i = b then
        if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j h = x then eqToHom ⋯ else 0
      else 0)
      (if h : i' = b then
        if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i' = x) ↦ (f x).ι) j' h = x then eqToHom ⋯ else 0
      else 0))
    0

Tactic:
rw [dif_neg hb.symm, zero_comp]

Premises used: Ne.symm, dif_neg, CategoryTheory.Limits.zero_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').ι
hi : i ∉ Finset.univ
⊢ Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
    (∑ j_1 : (f i).ι,
      CategoryStruct.comp (Y := (f i).X j_1)
        (if h : i = i then
          if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j h = j_1 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_1 then eqToHom ⋯ else 0
        else 0))
    0

Tactic:
simp at hi
-- 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 →
    b ≠ j →
      Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
        (CategoryStruct.comp (Y := (f i).X b)
          (if h : i = i then
            if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j h = b 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 = b then eqToHom ⋯ else 0
          else 0))
        0
⊢ Membership.mem (γ := Finset (f i).ι) Finset.univ b →
    b ≠ j →
      Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
        (CategoryStruct.comp (Y := (f i).X b)
          (if h : i = i then
            if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j h = b 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 = b then eqToHom ⋯ else 0
          else 0))
        0

Tactic:
_
-- 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 : ¬Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j ⋯ = b
⊢ Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j')
    (CategoryStruct.comp (Y := (f i).X b)
      (if h : i = i then
        if h' : Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j h = b 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 = b then eqToHom ⋯ else 0
      else 0))
    0

Tactic:
rw [dif_pos rfl, dif_neg, zero_comp]

Premises used: dif_pos, dif_neg, CategoryTheory.Limits.zero_comp, rfl