awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LiftToFinset (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteProducts.{v, u} C
α : Type w
inst_3 : DecidableEq α
f : α → C
inst_4 : HasProduct.{w, v, u} f
S : (Finset (Discrete α))ᵒᵖ
v : ↥(Opposite.unop S)
⊢ Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as) (Pi.π f (↑v : Discrete α).as)
    (∑ x ∈ (Opposite.unop S).attach,
      CategoryStruct.comp (Y := f (↑x : Discrete α).as) (Pi.π f (↑x : Discrete α).as)
        (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
          (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) x)
          (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v)))
have h : Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as) (Pi.π f (↑v : Discrete α).as)
  (CategoryStruct.comp (Y := f (↑v : Discrete α).as) (Pi.π f (↑v : Discrete α).as)
    (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
      (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) v)
      (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v)))
Tactic: rw [Finset.sum_eq_single v]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LiftToFinset (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteProducts.{v, u} C
α : Type w
inst_3 : DecidableEq α
f : α → C
inst_4 : HasProduct.{w, v, u} f
S : (Finset (Discrete α))ᵒᵖ
v : ↥(Opposite.unop S)
h :
  Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as) (Pi.π f (↑v : Discrete α).as)
    (CategoryStruct.comp (Y := f (↑v : Discrete α).as) (Pi.π f (↑v : Discrete α).as)
      (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
        (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) v)
        (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v)))
⊢ Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as) (Pi.π f (↑v : Discrete α).as)
    (∑ x ∈ (Opposite.unop S).attach,
      CategoryStruct.comp (Y := f (↑x : Discrete α).as) (Pi.π f (↑x : Discrete α).as)
        (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
          (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) x)
          (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v)))
have h₁ : ∀ b ∈ (Opposite.unop S).attach,
  b ≠ v →
    Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
      (CategoryStruct.comp (Y := f (↑b : Discrete α).as) (Pi.π f (↑b : Discrete α).as)
        (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
          (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) b)
          (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v)))
      0
Tactic: rw [Finset.sum_eq_single v]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LiftToFinset (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteProducts.{v, u} C
α : Type w
inst_3 : DecidableEq α
f : α → C
inst_4 : HasProduct.{w, v, u} f
S : (Finset (Discrete α))ᵒᵖ
v : ↥(Opposite.unop S)
h :
  Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as) (Pi.π f (↑v : Discrete α).as)
    (CategoryStruct.comp (Y := f (↑v : Discrete α).as) (Pi.π f (↑v : Discrete α).as)
      (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
        (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) v)
        (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v)))
h₁ :
  ∀ b ∈ (Opposite.unop S).attach,
    b ≠ v →
      Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
        (CategoryStruct.comp (Y := f (↑b : Discrete α).as) (Pi.π f (↑b : Discrete α).as)
          (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
            (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) b)
            (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v)))
        0
⊢ Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as) (Pi.π f (↑v : Discrete α).as)
    (∑ x ∈ (Opposite.unop S).attach,
      CategoryStruct.comp (Y := f (↑x : Discrete α).as) (Pi.π f (↑x : Discrete α).as)
        (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
          (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) x)
          (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v)))
have h₂ : v ∉ (Opposite.unop S).attach →
  Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
    (CategoryStruct.comp (Y := f (↑v : Discrete α).as) (Pi.π f (↑v : Discrete α).as)
      (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
        (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) v)
        (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v)))
    0
Tactic: rw [Finset.sum_eq_single v]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LiftToFinset (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteProducts.{v, u} C
α : Type w
inst_3 : DecidableEq α
f : α → C
inst_4 : HasProduct.{w, v, u} f
S : (Finset (Discrete α))ᵒᵖ
v b : ↥(Opposite.unop S)
hb : b ∈ (Opposite.unop S).attach
hb₁ : b ≠ v
⊢ Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
    (CategoryStruct.comp (Y := f (↑b : Discrete α).as) (Pi.π f (↑b : Discrete α).as)
      (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
        (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) b)
        (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v)))
    0
have h : Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
  (CategoryStruct.comp (Y := f (↑b : Discrete α).as) (Pi.π f (↑b : Discrete α).as) 0) 0
Tactic: rw [Pi.ι_π_of_ne _ hb₁, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LiftToFinset (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteProducts.{v, u} C
α : Type w
inst_3 : DecidableEq α
f : α → C
inst_4 : HasProduct.{w, v, u} f
S : (Finset (Discrete α))ᵒᵖ
v b : ↥(Opposite.unop S)
hb : b ∈ (Opposite.unop S).attach
hb₁ : b ≠ v
h :
  Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
    (CategoryStruct.comp (Y := f (↑b : Discrete α).as) (Pi.π f (↑b : Discrete α).as) 0) 0
⊢ Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
    (CategoryStruct.comp (Y := f (↑b : Discrete α).as) (Pi.π f (↑b : Discrete α).as)
      (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
        (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) b)
        (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v)))
    0
have h₁ : Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as) 0 0
Tactic: rw [Pi.ι_π_of_ne _ hb₁, comp_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
W X Y Z : Mat_ C
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
⊢ (f.comp g).comp h = f.comp (g.comp h)
have a : ∀ (i : W.ι) (j : Z.ι), (f.comp g).comp h i j = f.comp (g.comp h) i j
Tactic: apply DMatrix.ext
-- 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
W X Y Z : Mat_ C
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
i : W.ι
j : Z.ι
⊢ (f.comp g).comp h i j = f.comp (g.comp h) i j
have a : Eq.{v₁ + 1} (α := W.X i ⟶ Z.X j) (∑ x : Y.ι, ∑ x_1 : X.ι, f i x_1 ≫ g x_1 x ≫ h x j)
  (∑ x : X.ι, ∑ j_1 : Y.ι, f i x ≫ g x j_1 ≫ h j_1 j)
Tactic: simp_rw [Hom.comp, sum_comp, comp_sum, Category.assoc]
-- 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
W X Y Z : Mat_ C
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
i : W.ι
j : Z.ι
⊢ Eq.{v₁ + 1} (α := W.X i ⟶ Z.X j) (∑ x : Y.ι, ∑ x_1 : X.ι, f i x_1 ≫ g x_1 x ≫ h x j)
    (∑ x : X.ι, ∑ j_1 : Y.ι, f i x ≫ g x j_1 ≫ h j_1 j)
have a : Eq.{v₁ + 1} (α := W.X i ⟶ Z.X j) (∑ y : X.ι, ∑ x : Y.ι, f i y ≫ g y x ≫ h x j)
  (∑ x : X.ι, ∑ j_1 : Y.ι, f i x ≫ g x j_1 ≫ h j_1 j)
Tactic: rw [Finset.sum_comm]
-- 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
M N K : Mat_ C
f f' : Quiver.Hom.{v₁, max 1 u₁} M N
g : Quiver.Hom.{v₁, max 1 u₁} N K
⊢ CategoryStruct.comp.{v₁, max 1 u₁} (f + f') g =
    CategoryStruct.comp.{v₁, max 1 u₁} f g + CategoryStruct.comp.{v₁, max 1 u₁} f' g
have H : ∀ (i : M.ι) (j : K.ι),
  CategoryStruct.comp.{v₁, max 1 u₁} (f + f') g i j =
    (CategoryStruct.comp.{v₁, max 1 u₁} f g + CategoryStruct.comp.{v₁, max 1 u₁} f' g) i j
Tactic: ext
-- 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
M N K : Mat_ C
f : Quiver.Hom.{v₁, max 1 u₁} M N
g g' : Quiver.Hom.{v₁, max 1 u₁} N K
⊢ CategoryStruct.comp.{v₁, max 1 u₁} f (g + g') =
    CategoryStruct.comp.{v₁, max 1 u₁} f g + CategoryStruct.comp.{v₁, max 1 u₁} f g'
have H : ∀ (i : M.ι) (j : K.ι),
  CategoryStruct.comp.{v₁, max 1 u₁} f (g + g') i j =
    (CategoryStruct.comp.{v₁, max 1 u₁} f g + CategoryStruct.comp.{v₁, max 1 u₁} f g') i j
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (hypothesis)
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 :
  ι.{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).ι
⊢ (fun
        (i :
          ι.{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).ι)) })
        (j_1 : (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)
        ((f j).X j_1))
    x y
have h : x.fst (β := fun (j : Fin n) ↦ (f j).ι) = j
Tactic: refine if h : x.1 = j then ?_ else 0
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (hypothesis)
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 :
  ι.{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).ι
h : x.fst (β := fun (j : Fin n) ↦ (f j).ι) = j
⊢ (fun
        (i :
          ι.{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).ι)) })
        (j_1 : (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)
        ((f j).X j_1))
    x y
have h' : Eq.ndrec (motive := fun (j : Fin n) ↦ (f j).ι) (x.snd (β := fun (j : Fin n) ↦ (f j).ι)) h = y
Tactic: refine if h' : @Eq.ndrec (Fin n) x.1 (fun j => (f j).ι) x.2 _ h = y then ?_ else 0
-- 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 :
  ι.{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).ι
h : x.fst (β := fun (j : Fin n) ↦ (f j).ι) = j
h' : Eq.ndrec (motive := fun (j : Fin n) ↦ (f j).ι) (x.snd (β := fun (j : Fin n) ↦ (f j).ι)) h = y
⊢ (fun
        (i :
          ι.{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).ι)) })
        (j_1 : (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)
        ((f j).X j_1))
    x y
have p : 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 }
    x =
  (f j).X y
Tactic: apply eqToHom
-- 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 :
  ι.{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).ι
h : x.fst (β := fun (j : Fin n) ↦ (f j).ι) = j
h' : Eq.ndrec (motive := fun (j : Fin n) ↦ (f j).ι) (x.snd (β := fun (j : Fin n) ↦ (f j).ι)) h = y
⊢ 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 }
      x =
    (f j).X y
have p : 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 }
    x =
  (f (x.fst (β := fun (j : Fin n) ↦ (f j).ι))).X
    (Eq.ndrec (motive := fun (j : Fin n) ↦ (f j).ι) (x.snd (β := fun (j : Fin n) ↦ (f j).ι)) sorry)
Tactic: substs h h'
Cleared hypotheses: j, y, h, h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (hypothesis)
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).ι)) }
⊢ (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
have h : y.fst (β := fun (j : Fin n) ↦ (f j).ι) = j
Tactic: refine if h : y.1 = j then ?_ else 0
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (hypothesis)
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
⊢ (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
have h' : Eq.ndrec (motive := fun (j : Fin n) ↦ (f j).ι) (y.snd (β := fun (j : Fin n) ↦ (f j).ι)) h = x
Tactic: refine if h' : @Eq.ndrec _ y.1 (fun j => (f j).ι) y.2 _ h = x then ?_ else 0
-- 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 : (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
⊢ (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
have 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
Tactic: apply eqToHom
-- 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 : (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
⊢ (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
have 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).ι)) sorry) =
  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'
Cleared hypotheses: j, x, 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').ι
⊢ 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)
have 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 sorry
        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 sorry
        else 0
      else 0))
  ((if h : j = j' then eqToHom.{v₁, max 1 u₁} sorry else 0) x y)
Tactic: dsimp