awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset
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 α))ᵒᵖ
dsimp :
  Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
    (Pi.lift fun (s : ↥(Opposite.unop S)) ↦ Pi.π f (↑s : Discrete α).as)
    (∑ a ∈ (Opposite.unop S).attach,
      CategoryStruct.comp (Y := f (↑a : Discrete α).as) (Pi.π f (↑a : Discrete α).as)
        (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) a))
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u}
        (Functor.obj (Functor.const (Finset (Discrete α))ᵒᵖ)
          (Cone.pt.{w, v, w, u} (F := liftToFinsetObj (Discrete.functor f)) (finiteSubproductsCone f)))
        S ⟶
      Functor.obj.{w, v, w, u} (liftToFinsetObj (Discrete.functor f)) S)
    (NatTrans.app (Cone.π (finiteSubproductsCone f)) S)
    (∑ a ∈ (Opposite.unop S).attach,
      CategoryStruct.comp (Y := f (↑a : Discrete α).as) (Pi.π f (↑a : Discrete α).as)
        (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) a))

Tactic:
dsimp only [finiteSubproductsCone_pt, Functor.const_obj_obj, liftToFinsetObj_obj,
    Discrete.functor_obj_eq_as, finiteSubproductsCone_π_app]

Premises used: CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj_obj, CategoryTheory.Discrete.functor_obj_eq_as, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_pt, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone_π_app, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset
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 α))ᵒᵖ
h :
  ∀ (v : ↥(Opposite.unop S)),
    Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
      (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
          (Pi.lift fun (s : ↥(Opposite.unop S)) ↦ Pi.π f (↑s : Discrete α).as)
          (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v) :
        piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
      (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
          (∑ a ∈ (Opposite.unop S).attach,
            CategoryStruct.comp (Y := f (↑a : Discrete α).as) (Pi.π f (↑a : Discrete α).as)
              (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) a))
          (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v) :
        piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
⊢ Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
    (Pi.lift fun (s : ↥(Opposite.unop S)) ↦ Pi.π f (↑s : Discrete α).as)
    (∑ a ∈ (Opposite.unop S).attach,
      CategoryStruct.comp (Y := f (↑a : Discrete α).as) (Pi.π f (↑a : Discrete α).as)
        (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) a))

Tactic:
ext v
-- Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset
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)
    (∑ 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)))
⊢ Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
    (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
        (Pi.lift fun (s : ↥(Opposite.unop S)) ↦ Pi.π f (↑s : Discrete α).as)
        (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v) :
      piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
    (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
        (∑ a ∈ (Opposite.unop S).attach,
          CategoryStruct.comp (Y := f (↑a : Discrete α).as) (Pi.π f (↑a : Discrete α).as)
            (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) a))
        (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v) :
      piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)

Tactic:
simp only [limit.lift_π, Fan.mk_pt, Fan.mk_π_app, Preadditive.sum_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Preadditive.sum_comp, CategoryTheory.Limits.Fan.mk_pt, CategoryTheory.Limits.limit.lift_π, CategoryTheory.Limits.Fan.mk_π_app
-- Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset
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
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
⊢ 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)))

Tactic:
rw [Finset.sum_eq_single v]

Premises used: Finset.sum_eq_single
-- Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset
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)
    (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:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset
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
h₁ h₂ : Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : 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

Tactic:
rw [Pi.ι_π_of_ne _ hb₁, comp_zero]

Premises used: CategoryTheory.Limits.Pi.ι_π_of_ne, CategoryTheory.Limits.comp_zero
-- Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset
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)
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y : Mat_ C
f : X.Hom Y
⊢ Hom.comp (Hom.id X) f = f

Tactic:
simp +unfoldPartialApp [dite_comp]

Premises used: CategoryTheory.dite_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y : Mat_ C
f : X.Hom Y
⊢ Hom.comp (Hom.id X) f = f

Tactic:
classical
    simp +unfoldPartialApp [dite_comp]

Premises used: CategoryTheory.dite_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y : Mat_ C
f : X.Hom Y
⊢ f.comp (Hom.id Y) = f

Tactic:
simp +unfoldPartialApp [comp_dite]

Premises used: CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
X Y : Mat_ C
f : X.Hom Y
⊢ f.comp (Hom.id Y) = f

Tactic:
classical
    simp +unfoldPartialApp [comp_dite]

Premises used: CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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
a : ∀ (i : W.ι) (j : Z.ι), (f.comp g).comp h i j = f.comp (g.comp h) i j
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
apply DMatrix.ext

Premises used: DMatrix.ext
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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.ι
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)
⊢ (f.comp g).comp h i j = f.comp (g.comp h) i j

Tactic:
simp_rw [Hom.comp, sum_comp, comp_sum, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Mat_.Hom.comp, CategoryTheory.Preadditive.sum_comp, CategoryTheory.Preadditive.comp_sum
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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.ι
a 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)
⊢ 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:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M N : Mat_ C
f g : Quiver.Hom.{v₁, max 1 u₁} M N
H : ∀ (i : M.ι) (j : N.ι), f i j = g i j
⊢ f = g

Tactic:
DMatrix.ext_iff.mp H

Premises used: DMatrix, CategoryTheory.Mat_.Hom, Iff.mp, DMatrix.ext_iff
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
⊢ Eq.{v₁ + 1} (α := Quiver.Hom.{v₁, max 1 u₁} M M) (CategoryStruct.id.{v₁, max 1 u₁} M) fun (i j : M.ι) ↦
    if h : i = j then eqToHom ⋯ else 0

Tactic:
rfl

Premises used: dite, CategoryTheory.Mat_.Hom.id, rfl
-- 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.ι
⊢ Eq.{v₁ + 1} (α := (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)
    (if h : i = j then eqToHom ⋯ else 0 : M.X i ⟶ M.X j)

Tactic:
rfl

Premises used: dite, CategoryTheory.Mat_.Hom.id, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
i : M.ι
⊢ Eq.{v₁ + 1} (α := (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i i)
    (CategoryStruct.id.{v₁, max 1 u₁} M i i : (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i i)
    (𝟙 (M.X i) : M.X i ⟶ M.X i)

Tactic:
simp [id_apply]

Premises used: CategoryTheory.Mat_.id_apply
-- 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 : i ≠ j
⊢ Eq.{v₁ + 1} (α := (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)
    (0 : (fun (i j : M.ι) ↦ Quiver.Hom.{v₁, u₁} (M.X i) (M.X j)) i j)

Tactic:
simp [id_apply, h]

Premises used: CategoryTheory.Mat_.id_apply
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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 : Quiver.Hom.{v₁, max 1 u₁} N K
⊢ CategoryStruct.comp.{v₁, max 1 u₁} f g = fun (i : M.ι) (k : K.ι) ↦ ∑ j : N.ι, f i j ≫ g j k

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, CategoryTheory.Mat_.Hom.comp, Finset.sum, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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 : Quiver.Hom.{v₁, max 1 u₁} N K
i : M.ι
k : K.ι
⊢ CategoryStruct.comp.{v₁, max 1 u₁} f g i k = ∑ j : N.ι, f i j ≫ g j k

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, CategoryTheory.Mat_.Hom.comp, Finset.sum, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M N : Mat_ C
f g : Quiver.Hom.{v₁, max 1 u₁} M N
i : M.ι
j : N.ι
⊢ (f + g) i j = f i j + g i j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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
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
⊢ 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

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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
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:
simp [Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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
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
⊢ 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'

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Mat
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
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:
simp [Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- 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 :
  ι.{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).ι
⊢ x.fst (β := fun (j : Fin n) ↦ (f j).ι) = j

Tactic:
refine if h : x.1 = j then ?_ else 0

Premises used: Sigma.fst
-- 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 :
  ι.{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
⊢ 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

Premises used: Eq.ndrec, Sigma.snd
-- 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 :
  ι.{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
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
⊢ (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

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 :
  ι.{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
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).ι)) ⋯)
⊢ 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:
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
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).ι)) }
⊢ 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).ι)) ⋯)

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 : 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).ι)) }
⊢ y.fst (β := fun (j : Fin n) ↦ (f j).ι) = j

Tactic:
refine if h : y.1 = j then ?_ else 0

Premises used: Sigma.fst
-- 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
⊢ 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

Premises used: Eq.ndrec, Sigma.snd