awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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').ι
⊢ 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)
have 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))
                sorry =
              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)) sorry =
                  y then
              eqToHom sorry
            else 0
          else 0
        else 0
      else 0)
  ((if h : j = j' then eqToHom.{v₁, max 1 u₁} sorry else 0) x y)
Tactic: rw [← Finset.univ_sigma_univ, Finset.sum_sigma]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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').ι
⊢ 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)
have 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 sorry = 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 sorry = y then eqToHom sorry else 0
          else 0
        else 0
      else 0)
  ((if h : j = j' then eqToHom.{v₁, max 1 u₁} sorry else 0) x y)
Tactic: dsimp +instances
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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').ι
⊢ 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)
have 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 sorry = y then eqToHom sorry else 0
  else 0)
  ((if h : j = j' then eqToHom.{v₁, max 1 u₁} sorry else 0) x y)
Tactic: simp only [if_true, Finset.sum_dite_irrel, Finset.mem_univ,
                Finset.sum_const_zero, Finset.sum_dite_eq']
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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').ι
⊢ 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)
have pos : ∀ (h : j = j') (h' : Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x sorry = y),
  Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y) (eqToHom sorry : (f j).X x ⟶ (f j').X y)
    (eqToHom.{v₁, max 1 u₁} sorry 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: split_ifs with h h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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)
⊢ 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)
have neg : ∀ (h : j = j') (h' : ¬Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x sorry = 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₁} sorry 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: split_ifs with h h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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)
⊢ 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)
have neg₁ : ∀ (h : ¬j = j'), Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j').X y) 0 (0 x y)
Tactic: split_ifs with h h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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
⊢ 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)
have 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 sorry))
  (eqToHom sorry : (f j).X x ⟶ (f j).X (Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x sorry))
  (eqToHom.{v₁, max 1 u₁} sorry x (Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x sorry) :
    (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 sorry))
Tactic: substs h h'
Cleared hypotheses: j', y, h, h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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
⊢ 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)
have neg : ∀ (y : (f j).ι) (h' : ¬Eq.rec (motive := fun (x : Fin n) (x_1 : j = x) ↦ (f x).ι) x sorry = 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₁} sorry x y : (fun (i j_1 : (f j).ι) ↦ Quiver.Hom.{v₁, u₁} ((f j).X i) ((f j).X j_1)) x y)
Tactic: subst h
Cleared hypotheses: j', y, h, h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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
⊢ 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)
have 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)
Tactic: rw [eqToHom_refl, id_apply_of_ne _ _ _ h']
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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)
⊢ 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)
have neg₁ : Eq.{v₁ + 1} (α := (f j).X x ⟶ (f j).X y) 0 0
Tactic: rw [eqToHom_refl, id_apply_of_ne _ _ _ h']
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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
⊢ 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
have 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 sorry 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 sorry else 0
        else 0))
      0
Tactic: apply Finset.sum_eq_zero
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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
⊢ 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
have 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 sorry else 0
    else 0))
  0
Tactic: rw [dif_neg hb.symm, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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
⊢ 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
have H₁ : Eq.{v₁ + 1} (α := (f i).X j ⟶ (f i').X j') 0 0
Tactic: rw [dif_neg hb.symm, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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
⊢ 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
have H : ¬Eq.rec (motive := fun (x : Fin n) (x_1 : i = x) ↦ (f x).ι) j sorry = b
Tactic: rw [dif_pos rfl, dif_neg, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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').ι
⊢ 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'))
have 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 sorry else 0
  else 0)
  (if h : i = i' ∧ j ≍ j' then eqToHom sorry else 0)
Tactic: simp only [eqToHom_refl, dite_eq_ite, ite_true, Category.id_comp,
              Sigma.mk.inj_iff, id_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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').ι
⊢ 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)
have 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 sorry else 0
    else 0)
    (if h : i = i' ∧ j ≍ j' then eqToHom sorry else 0)
Tactic: by_cases h : i' = i
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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)
⊢ 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)
have 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 sorry else 0
    else 0)
    (if h : i = i' ∧ j ≍ j' then eqToHom sorry else 0)
Tactic: by_cases h : i' = i
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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
⊢ 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)
have 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 sorry else 0
    else 0)
    (if h : i' = i' ∧ j ≍ j' then eqToHom sorry else 0)
Tactic: subst h
Cleared hypotheses: i, j, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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').ι
⊢ 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)
have 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' sorry = j then eqToHom sorry else 0)
  (if h : i' = i' ∧ j ≍ j' then eqToHom sorry else 0)
Tactic: rw [dif_pos rfl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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').ι
⊢ 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)
have pos : Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j') (if h' : j' = j then eqToHom sorry else 0) (if h : j = j' then eqToHom sorry else 0)
Tactic: simp only [heq_eq_eq, true_and]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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').ι
⊢ 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)
have pos : ∀ (h : j' = j),
  Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j') (if h' : j' = j then eqToHom sorry else 0)
    (if h : j = j' then eqToHom sorry else 0)
Tactic: by_cases h : j' = j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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)
⊢ 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)
have neg : ∀ (h : ¬j' = j),
  Eq.{v₁ + 1} (α := (f i').X j ⟶ (f i').X j') (if h' : j' = j then eqToHom sorry else 0)
    (if h : j = j' then eqToHom sorry else 0)
Tactic: by_cases h : j' = j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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
⊢ 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)
have pos : Eq.{v₁ + 1} (α := (f i').X j' ⟶ (f i').X j') (if h' : j' = j' then eqToHom sorry else 0)
  (if h : j' = j' then eqToHom sorry else 0)
Tactic: subst h
Cleared hypotheses: j, h