awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
n : ℕ
X_1 Y Z : C
f : X_1 ⟶ Y
f' : Y ⟶ Z
hf :
  ∀ (α : (↑(AddCommGrpCat.of (Ext.{w, v, u} X X_1 n)) : Type w)),
    Eq (α := (↑(AddCommGrpCat.of (Ext.{w, v, u} X Z n)) : Type w))
      ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (Ext.postcomp (Ext.mk₀ (f ≫ f')) X ⋯)) :
            (a : (↑(AddCommGrpCat.of (Ext X X_1 n)) : Type w)) → (↑(AddCommGrpCat.of (Ext X Z n)) : Type w))
          α :
        (↑(AddCommGrpCat.of (Ext.{w, v, u} X Z n)) : Type w))
      ((AddCommGrpCat.Hom.hom
              (AddCommGrpCat.ofHom (Ext.postcomp (Ext.mk₀ f) X ⋯) ≫
                AddCommGrpCat.ofHom (Ext.postcomp (Ext.mk₀ f') X ⋯)) :
            (a : (↑(AddCommGrpCat.of (Ext X X_1 n)) : Type w)) → (↑(AddCommGrpCat.of (Ext X Z n)) : Type w))
          α :
        (↑(AddCommGrpCat.of (Ext.{w, v, u} X Z n)) : Type w))
⊢ Eq.{w + 1} (α := AddCommGrpCat.of (Ext.{w, v, u} X X_1 n) ⟶ AddCommGrpCat.of (Ext.{w, v, u} X Z n))
    (AddCommGrpCat.ofHom (Ext.postcomp (Ext.mk₀ (f ≫ f')) X ⋯))
    (AddCommGrpCat.ofHom (Ext.postcomp (Ext.mk₀ f) X ⋯) ≫ AddCommGrpCat.ofHom (Ext.postcomp (Ext.mk₀ f') X ⋯))

Tactic:
ext α
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
n : ℕ
X_1 Y Z : C
f : X_1 ⟶ Y
f' : Y ⟶ Z
α : (↑(AddCommGrpCat.of (Ext.{w, v, u} X X_1 n)) : Type w)
hf :
  Eq (α := Ext.{w, v, u} X Z n) (Ext.comp α (Ext.comp (Ext.mk₀ f) (Ext.mk₀ f') ⋯) ⋯)
    (Ext.comp (Ext.comp α (Ext.mk₀ f) ⋯) (Ext.mk₀ f') ⋯)
⊢ Eq (α := Ext.{w, v, u} X Z n) (Ext.comp α (Ext.mk₀ (f ≫ f')) ⋯) (Ext.comp (Ext.comp α (Ext.mk₀ f) ⋯) (Ext.mk₀ f') ⋯)

Tactic:
rw [← Ext.mk₀_comp_mk₀]

Premises used: CategoryTheory.Abelian.Ext.mk₀_comp_mk₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
n : ℕ
X_1 Y Z : C
f : X_1 ⟶ Y
f' : Y ⟶ Z
α : (↑(AddCommGrpCat.of (Ext.{w, v, u} X X_1 n)) : Type w)
hf :
  Eq (α := Ext.{w, v, u} X Z n) (Ext.comp (Ext.comp α (Ext.mk₀ f) ⋯) (Ext.mk₀ f') ⋯)
    (Ext.comp α (Ext.comp (Ext.mk₀ f) (Ext.mk₀ f') ⋯) ⋯)
⊢ Eq (α := Ext.{w, v, u} X Z n) (Ext.comp α (Ext.comp (Ext.mk₀ f) (Ext.mk₀ f') ⋯) ⋯)
    (Ext.comp (Ext.comp α (Ext.mk₀ f) ⋯) (Ext.mk₀ f') ⋯)

Tactic:
symm
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
n : ℕ
X_1 Y Z : C
f : X_1 ⟶ Y
f' : Y ⟶ Z
α : (↑(AddCommGrpCat.of (Ext.{w, v, u} X X_1 n)) : Type w)
hf : n + 0 + 0 = n
⊢ Eq (α := Ext.{w, v, u} X Z n) (Ext.comp (Ext.comp α (Ext.mk₀ f) ⋯) (Ext.mk₀ f') ⋯)
    (Ext.comp α (Ext.comp (Ext.mk₀ f) (Ext.mk₀ f') ⋯) ⋯)

Tactic:
apply Ext.comp_assoc

Premises used: CategoryTheory.Abelian.Ext.comp_assoc
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
n : ℕ
X_1 Y Z : C
f : X_1 ⟶ Y
f' : Y ⟶ Z
α : (↑(AddCommGrpCat.of (Ext.{w, v, u} X X_1 n)) : Type w)
⊢ n + 0 + 0 = n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y : C
⊢ ∀ (a b : Ext.{w, v, u} (Opposite.unop X₁) Y n),
    (fun (α : Ext.{w, v, u} (Opposite.unop X₁) Y n) ↦ Ext.comp (Ext.mk₀ f.unop) α ⋯) (a + b) =
      HAdd.hAdd (α := Ext.{w, v, u} (Opposite.unop X₂) Y n)
        ((fun (α : Ext.{w, v, u} (Opposite.unop X₁) Y n) ↦ Ext.comp (Ext.mk₀ f.unop) α ⋯) a)
        ((fun (α : Ext.{w, v, u} (Opposite.unop X₁) Y n) ↦ Ext.comp (Ext.mk₀ f.unop) α ⋯) b)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
hf :
  ∀ (α : (↑(Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₁) n) Y₁) : Type w)),
    Eq (α := (↑(Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₂) n) Y₂) : Type w))
      ((AddCommGrpCat.Hom.hom
              (Functor.map (extFunctorObj (Opposite.unop X₁) n) g ≫
                AddCommGrpCat.ofHom
                  (AddMonoidHom.mk' (fun (α : Ext.{w, v, u} (Opposite.unop X₁) Y₂ n) ↦ Ext.comp (Ext.mk₀ f.unop) α ⋯)
                    ⋯)) :
            (a : (↑((extFunctorObj (Opposite.unop X₁) n).obj Y₁) : Type w)) →
              (↑((extFunctorObj (Opposite.unop X₂) n).obj Y₂) : Type w))
          α :
        (↑(Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₂) n) Y₂) : Type w))
      ((AddCommGrpCat.Hom.hom
              (AddCommGrpCat.ofHom
                  (AddMonoidHom.mk' (fun (α : Ext.{w, v, u} (Opposite.unop X₁) Y₁ n) ↦ Ext.comp (Ext.mk₀ f.unop) α ⋯)
                    ⋯) ≫
                Functor.map (extFunctorObj (Opposite.unop X₂) n) g) :
            (a : (↑((extFunctorObj (Opposite.unop X₁) n).obj Y₁) : Type w)) →
              (↑((extFunctorObj (Opposite.unop X₂) n).obj Y₂) : Type w))
          α :
        (↑(Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₂) n) Y₂) : Type w))
⊢ Eq.{w + 1} (α :=
    Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₁) n) Y₁ ⟶
      Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₂) n) Y₂)
    (Functor.map (extFunctorObj (Opposite.unop X₁) n) g ≫
        AddCommGrpCat.ofHom
          (AddMonoidHom.mk' (fun (α : Ext.{w, v, u} (Opposite.unop X₁) Y₂ n) ↦ Ext.comp (Ext.mk₀ f.unop) α ⋯) ⋯) :
      Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₁) n) Y₁ ⟶
        Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₂) n) Y₂)
    (AddCommGrpCat.ofHom
          (AddMonoidHom.mk' (fun (α : Ext.{w, v, u} (Opposite.unop X₁) Y₁ n) ↦ Ext.comp (Ext.mk₀ f.unop) α ⋯) ⋯) ≫
        Functor.map (extFunctorObj (Opposite.unop X₂) n) g :
      Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₁) n) Y₁ ⟶
        Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₂) n) Y₂)

Tactic:
ext α
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
α : (↑(Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₁) n) Y₁) : Type w)
hf :
  Eq (α := Ext.{w, v, u} (Opposite.unop X₂) Y₂ n) (Ext.comp (Ext.comp (Ext.mk₀ f.unop) α ⋯) (Ext.mk₀ g) ⋯)
    (Ext.comp (Ext.mk₀ f.unop) (Ext.comp α (Ext.mk₀ g) ⋯) ⋯)
⊢ Eq (α := Ext.{w, v, u} (Opposite.unop X₂) Y₂ n) (Ext.comp (Ext.mk₀ f.unop) (Ext.comp α (Ext.mk₀ g) ⋯) ⋯)
    (Ext.comp (Ext.comp (Ext.mk₀ f.unop) α ⋯) (Ext.mk₀ g) ⋯)

Tactic:
symm
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
α : (↑(Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₁) n) Y₁) : Type w)
hf : 0 + n + 0 = n
⊢ Eq (α := Ext.{w, v, u} (Opposite.unop X₂) Y₂ n) (Ext.comp (Ext.comp (Ext.mk₀ f.unop) α ⋯) (Ext.mk₀ g) ⋯)
    (Ext.comp (Ext.mk₀ f.unop) (Ext.comp α (Ext.mk₀ g) ⋯) ⋯)

Tactic:
apply Ext.comp_assoc

Premises used: CategoryTheory.Abelian.Ext.comp_assoc
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
α : (↑(Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₁) n) Y₁) : Type w)
⊢ 0 + n + 0 = n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
α : (↑(Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₁) n) Y₁) : Type w)
⊢ 0 + n + 0 = n

Tactic:
all_goals lia
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
n : ℕ
X₁ X₂ X₃ : Cᵒᵖ
f : X₁ ⟶ X₂
f' : X₂ ⟶ X₃
w :
  ∀ (Y : C) (α : (↑(Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₁) n) Y) : Type w)),
    Eq (α := (↑(Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₃) n) Y) : Type w))
      ((AddCommGrpCat.Hom.hom
              (NatTrans.app
                {
                  app := fun (Y : C) ↦
                    AddCommGrpCat.ofHom
                      (AddMonoidHom.mk'
                        (fun (α : Ext.{w, v, u} (Opposite.unop X₁) Y n) ↦ Ext.comp (Ext.mk₀ (f ≫ f').unop) α ⋯) ⋯),
                  naturality := ⋯ }
                Y) :
            (a : (↑((extFunctorObj (Opposite.unop X₁) n).obj Y) : Type w)) →
              (↑((extFunctorObj (Opposite.unop X₃) n).obj Y) : Type w))
          α :
        (↑(Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₃) n) Y) : Type w))
      ((AddCommGrpCat.Hom.hom
              (NatTrans.app
                (CategoryStruct.comp (Y := extFunctorObj (Opposite.unop X₂) n)
                  {
                    app := fun (Y : C) ↦
                      AddCommGrpCat.ofHom
                        (AddMonoidHom.mk'
                          (fun (α : Ext.{w, v, u} (Opposite.unop X₁) Y n) ↦ Ext.comp (Ext.mk₀ f.unop) α ⋯) ⋯),
                    naturality := ⋯ }
                  {
                    app := fun (Y : C) ↦
                      AddCommGrpCat.ofHom
                        (AddMonoidHom.mk'
                          (fun (α : Ext.{w, v, u} (Opposite.unop X₂) Y n) ↦ Ext.comp (Ext.mk₀ f'.unop) α ⋯) ⋯),
                    naturality := ⋯ })
                Y) :
            (a : (↑((extFunctorObj (Opposite.unop X₁) n).obj Y) : Type w)) →
              (↑((extFunctorObj (Opposite.unop X₃) n).obj Y) : Type w))
          α :
        (↑(Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₃) n) Y) : Type w))
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v, w, u, w + 1} C AddCommGrpCat) (extFunctorObj (Opposite.unop X₁) n)
      (extFunctorObj (Opposite.unop X₃) n))
    {
      app := fun (Y : C) ↦
        AddCommGrpCat.ofHom
          (AddMonoidHom.mk' (fun (α : Ext.{w, v, u} (Opposite.unop X₁) Y n) ↦ Ext.comp (Ext.mk₀ (f ≫ f').unop) α ⋯) ⋯),
      naturality := ⋯ }
    (CategoryStruct.comp (Y := extFunctorObj (Opposite.unop X₂) n)
      {
        app := fun (Y : C) ↦
          AddCommGrpCat.ofHom
            (AddMonoidHom.mk' (fun (α : Ext.{w, v, u} (Opposite.unop X₁) Y n) ↦ Ext.comp (Ext.mk₀ f.unop) α ⋯) ⋯),
        naturality := ⋯ }
      {
        app := fun (Y : C) ↦
          AddCommGrpCat.ofHom
            (AddMonoidHom.mk' (fun (α : Ext.{w, v, u} (Opposite.unop X₂) Y n) ↦ Ext.comp (Ext.mk₀ f'.unop) α ⋯) ⋯),
        naturality := ⋯ })

Tactic:
ext Y α
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
n : ℕ
X₁ X₂ X₃ : Cᵒᵖ
f : X₁ ⟶ X₂
f' : X₂ ⟶ X₃
Y : C
α : (↑(Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₁) n) Y) : Type w)
⊢ Eq (α := (↑(Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₃) n) Y) : Type w))
    ((AddCommGrpCat.Hom.hom
            (NatTrans.app
              {
                app := fun (Y : C) ↦
                  AddCommGrpCat.ofHom
                    (AddMonoidHom.mk'
                      (fun (α : Ext.{w, v, u} (Opposite.unop X₁) Y n) ↦ Ext.comp (Ext.mk₀ (f ≫ f').unop) α ⋯) ⋯),
                naturality := ⋯ }
              Y) :
          (a : (↑((extFunctorObj (Opposite.unop X₁) n).obj Y) : Type w)) →
            (↑((extFunctorObj (Opposite.unop X₃) n).obj Y) : Type w))
        α :
      (↑(Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₃) n) Y) : Type w))
    ((AddCommGrpCat.Hom.hom
            (NatTrans.app
              (CategoryStruct.comp (Y := extFunctorObj (Opposite.unop X₂) n)
                {
                  app := fun (Y : C) ↦
                    AddCommGrpCat.ofHom
                      (AddMonoidHom.mk' (fun (α : Ext.{w, v, u} (Opposite.unop X₁) Y n) ↦ Ext.comp (Ext.mk₀ f.unop) α ⋯)
                        ⋯),
                  naturality := ⋯ }
                {
                  app := fun (Y : C) ↦
                    AddCommGrpCat.ofHom
                      (AddMonoidHom.mk'
                        (fun (α : Ext.{w, v, u} (Opposite.unop X₂) Y n) ↦ Ext.comp (Ext.mk₀ f'.unop) α ⋯) ⋯),
                  naturality := ⋯ })
              Y) :
          (a : (↑((extFunctorObj (Opposite.unop X₁) n).obj Y) : Type w)) →
            (↑((extFunctorObj (Opposite.unop X₃) n).obj Y) : Type w))
        α :
      (↑(Functor.obj.{v, w, u, w + 1} (extFunctorObj (Opposite.unop X₃) n) Y) : Type w))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y Z : C
p : ℕ
α : Ext.{w, v, u} X Y p
ι : Type u_1
inst_3 : Fintype ι
q : ℕ
β : ι → Ext.{w, v, u} Y Z q
n : ℕ
h : p + q = n
⊢ Eq (α := Ext.{w, v, u} X Z n) (α.comp (∑ i : ι, β i) h) (∑ i : ι, α.comp (β i) h)

Tactic:
map_sum (α.precomp Z h) _ _

Premises used: CategoryTheory.Abelian.Ext.precomp, map_sum, CategoryTheory.Abelian.Ext.comp, CategoryTheory.Localization.SmallHom.comp, CategoryTheory.Localization.SmallShiftedHom.comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y Z : C
p : ℕ
ι : Type u_1
inst_3 : Fintype ι
α : ι → Ext.{w, v, u} X Y p
q : ℕ
β : Ext.{w, v, u} Y Z q
n : ℕ
h : p + q = n
⊢ Eq (α := Ext.{w, v, u} X Z n) (comp (∑ i : ι, α i) β h) (∑ i : ι, (α i).comp β h)

Tactic:
map_sum (β.postcomp X h) _ _

Premises used: CategoryTheory.Abelian.Ext.postcomp, map_sum, CategoryTheory.Abelian.Ext.comp, CategoryTheory.Localization.SmallHom.comp, CategoryTheory.Localization.SmallShiftedHom.comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X Y : C
ι : Type u_1
inst_3 : Fintype ι
f : ι → (X ⟶ Y)
⊢ Eq.{w + 1} (α := Ext.{w, v, u} X Y 0) (mk₀ (∑ i : ι, f i)) (∑ i : ι, mk₀ (f i))

Tactic:
map_sum addEquiv₀.symm _ _

Premises used: CategoryTheory.Localization.SmallHom.mk, map_sum, CategoryTheory.Localization.SmallShiftedHom.mk₀, CategoryTheory.Abelian.Ext.addEquiv₀, CategoryTheory.Localization.SmallShiftedHom.mk, CategoryTheory.Abelian.Ext.mk₀, AddEquiv.symm
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
J : Type u_1
inst_3 : Fintype J
X : J → C
c : Bicone.{u_1, v, u} X
hc : c.IsBilimit
Y : C
n : ℕ
x : Ext.{w, v, u} c.pt Y n
simp : ∑ x_1 : J, comp (mk₀ (c.π x_1 ≫ c.ι x_1)) x ⋯ = x
⊢ (fun (e : (i : J) → Ext.{w, v, u} (X i) Y n) ↦ (∑ i : J, comp (mk₀ (c.π i)) (e i) ⋯ : Ext.{w, v, u} c.pt Y n))
      ((fun (e : Ext.{w, v, u} c.pt Y n) (i : J) ↦ comp (mk₀ (c.ι i)) e ⋯) x) =
    x

Tactic:
simp only [← comp_assoc_of_second_deg_zero, mk₀_comp_mk₀]

Premises used: CategoryTheory.Abelian.Ext.comp_assoc_of_second_deg_zero, CategoryTheory.Abelian.Ext.mk₀_comp_mk₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
J : Type u_1
inst_3 : Fintype J
X : J → C
c : Bicone.{u_1, v, u} X
hc : c.IsBilimit
Y : C
n : ℕ
x : Ext.{w, v, u} c.pt Y n
rw : comp (∑ i : J, mk₀ (c.π i ≫ c.ι i)) x ⋯ = x
rw₁ : comp (mk₀ (∑ i : J, c.π i ≫ c.ι i)) x ⋯ = x
rw₂ : comp (mk₀ (𝟙 c.pt)) x ⋯ = x
rw₃ rw₄ : x = x
⊢ ∑ x_1 : J, comp (mk₀ (c.π x_1 ≫ c.ι x_1)) x ⋯ = x

Tactic:
rw [← Ext.sum_comp, ← Ext.mk₀_sum, IsBilimit.total hc, mk₀_id_comp]

Premises used: CategoryTheory.Abelian.Ext.sum_comp, CategoryTheory.Abelian.Ext.mk₀_id_comp, CategoryTheory.Limits.IsBilimit.total, CategoryTheory.Abelian.Ext.mk₀_sum
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
J : Type u_1
inst_3 : Fintype J
X : J → C
c : Bicone.{u_1, v, u} X
hc : c.IsBilimit
Y : C
n : ℕ
x : (i : J) → Ext.{w, v, u} (X i) Y n
h :
  ∀ (i : J),
    (fun (e : Ext.{w, v, u} c.pt Y n) (i : J) ↦ comp (mk₀ (c.ι i)) e ⋯)
        ((fun (e : (i : J) → Ext.{w, v, u} (X i) Y n) ↦ (∑ i : J, comp (mk₀ (c.π i)) (e i) ⋯ : Ext.{w, v, u} c.pt Y n))
          x)
        i =
      x i
⊢ (fun (e : Ext.{w, v, u} c.pt Y n) (i : J) ↦ comp (mk₀ (c.ι i)) e ⋯)
      ((fun (e : (i : J) → Ext.{w, v, u} (X i) Y n) ↦ (∑ i : J, comp (mk₀ (c.π i)) (e i) ⋯ : Ext.{w, v, u} c.pt Y n))
        x) =
    x

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
J : Type u_1
inst_3 : Fintype J
X : J → C
c : Bicone.{u_1, v, u} X
hc : c.IsBilimit
Y : C
n : ℕ
x : (i : J) → Ext.{w, v, u} (X i) Y n
i : J
h : ∑ x_1 : J, comp (mk₀ (c.ι i ≫ c.π x_1)) (x x_1) ⋯ = x i
⊢ (fun (e : Ext.{w, v, u} c.pt Y n) (i : J) ↦ comp (mk₀ (c.ι i)) e ⋯)
      ((fun (e : (i : J) → Ext.{w, v, u} (X i) Y n) ↦ (∑ i : J, comp (mk₀ (c.π i)) (e i) ⋯ : Ext.{w, v, u} c.pt Y n)) x)
      i =
    x i

Tactic:
simp only [Ext.comp_sum, ← comp_assoc_of_second_deg_zero, mk₀_comp_mk₀]

Premises used: CategoryTheory.Abelian.Ext.comp_sum, CategoryTheory.Abelian.Ext.comp_assoc_of_second_deg_zero, CategoryTheory.Abelian.Ext.mk₀_comp_mk₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
J : Type u_1
inst_3 : Fintype J
X : J → C
c : Bicone.{u_1, v, u} X
hc : c.IsBilimit
Y : C
n : ℕ
x : (i : J) → Ext.{w, v, u} (X i) Y n
i : J
⊢ i ∉ Finset.univ → comp (mk₀ (c.ι i ≫ c.π i)) (x i) ⋯ = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
J : Type u_1
inst_3 : Fintype J
X : J → C
c : Bicone.{u_1, v, u} X
hc : c.IsBilimit
Y : C
n : ℕ
x : (i : J) → Ext.{w, v, u} (X i) Y n
i : J
rw : ∀ (b : J), Membership.mem (γ := Finset J) Finset.univ b → b ≠ i → comp (mk₀ (c.ι i ≫ c.π b)) (x b) ⋯ = 0
⊢ ∑ x_1 : J, comp (mk₀ (c.ι i ≫ c.π x_1)) (x x_1) ⋯ = x i

Tactic:
rw [Finset.sum_eq_single i _ (by simp), bicone_ι_π_self, mk₀_id_comp]

Premises used: CategoryTheory.Abelian.Ext.mk₀_id_comp, Finset.sum_eq_single, CategoryTheory.Limits.bicone_ι_π_self
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
J : Type u_1
inst_3 : Fintype J
X : J → C
c : Bicone.{u_1, v, u} X
hc : c.IsBilimit
Y : C
n : ℕ
x : (i : J) → Ext.{w, v, u} (X i) Y n
i b : J
_ : Membership.mem (γ := Finset J) Finset.univ b → b ≠ i → comp (mk₀ (c.ι i ≫ c.π b)) (x b) ⋯ = 0
⊢ Membership.mem (γ := Finset J) Finset.univ b → b ≠ i → comp (mk₀ (c.ι i ≫ c.π b)) (x b) ⋯ = 0

Tactic:
_
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
J : Type u_1
inst_3 : Fintype J
X : J → C
c : Bicone.{u_1, v, u} X
hc : c.IsBilimit
Y : C
n : ℕ
x : (i : J) → Ext.{w, v, u} (X i) Y n
i b : J
h : Membership.mem (γ := Finset J) Finset.univ b
hij : b ≠ i
rw : Eq (α := Ext.{w, v, u} (X i) Y n) (comp (mk₀ (if h : i = b then eqToHom ⋯ else 0)) (x b) ⋯) 0
rw₁ : Eq (α := Ext.{w, v, u} (X i) Y n) (comp (mk₀ 0) (x b) ⋯) 0
rw₂ : Eq (α := Ext.{w, v, u} (X i) Y n) (comp 0 (x b) ⋯) 0
rw₃ rw₄ : Eq.{w + 1} (α := Ext.{w, v, u} (X i) Y n) 0 0
⊢ comp (mk₀ (c.ι i ≫ c.π b)) (x b) ⋯ = 0

Tactic:
rw [c.ι_π, dif_neg hij.symm, mk₀_zero, zero_comp]

Premises used: CategoryTheory.Abelian.Ext.zero_comp, Ne.symm, dif_neg, CategoryTheory.Abelian.Ext.mk₀_zero, CategoryTheory.Limits.Bicone.ι_π
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
J : Type u_1
inst_3 : Fintype J
X : J → C
c : Bicone.{u_1, v, u} X
hc : c.IsBilimit
Y : C
n : ℕ
x x_1 : Ext.{w, v, u} c.pt Y n
⊢ (fun (i : J) ↦ comp (mk₀ (c.ι i)) (x + x_1) ⋯) =
    HAdd.hAdd (α := (i : J) → Ext.{w, v, u} (X i) Y n) (fun (i : J) ↦ comp (mk₀ (c.ι i)) x ⋯) fun (i : J) ↦
      comp (mk₀ (c.ι i)) x_1 ⋯

Tactic:
simp only [comp_add, Pi.add_def]

Premises used: CategoryTheory.Abelian.Ext.comp_add, Pi.add_def
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
J : Type u_1
inst_3 : Fintype J
Y : J → C
c : Bicone.{u_1, v, u} Y
hc : c.IsBilimit
n : ℕ
x : Ext.{w, v, u} X c.pt n
⊢ (fun (e : (i : J) → Ext.{w, v, u} X (Y i) n) ↦ (∑ i : J, (e i).comp (mk₀ (c.ι i)) ⋯ : Ext.{w, v, u} X c.pt n))
      ((fun (e : Ext.{w, v, u} X c.pt n) (i : J) ↦ e.comp (mk₀ (c.π i)) ⋯) x) =
    x

Tactic:
simp only [comp_assoc_of_second_deg_zero, mk₀_comp_mk₀, ← Ext.comp_sum,
      ← Ext.mk₀_sum, IsBilimit.total hc, comp_mk₀_id]

Premises used: CategoryTheory.Abelian.Ext.comp_sum, CategoryTheory.Limits.IsBilimit.total, CategoryTheory.Abelian.Ext.comp_assoc_of_second_deg_zero, CategoryTheory.Abelian.Ext.comp_mk₀_id, CategoryTheory.Abelian.Ext.mk₀_sum, CategoryTheory.Abelian.Ext.mk₀_comp_mk₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
J : Type u_1
inst_3 : Fintype J
Y : J → C
c : Bicone.{u_1, v, u} Y
hc : c.IsBilimit
n : ℕ
x : (i : J) → Ext.{w, v, u} X (Y i) n
h :
  ∀ (i : J),
    (fun (e : Ext.{w, v, u} X c.pt n) (i : J) ↦ e.comp (mk₀ (c.π i)) ⋯)
        ((fun (e : (i : J) → Ext.{w, v, u} X (Y i) n) ↦ (∑ i : J, (e i).comp (mk₀ (c.ι i)) ⋯ : Ext.{w, v, u} X c.pt n))
          x)
        i =
      x i
⊢ (fun (e : Ext.{w, v, u} X c.pt n) (i : J) ↦ e.comp (mk₀ (c.π i)) ⋯)
      ((fun (e : (i : J) → Ext.{w, v, u} X (Y i) n) ↦ (∑ i : J, (e i).comp (mk₀ (c.ι i)) ⋯ : Ext.{w, v, u} X c.pt n))
        x) =
    x

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
J : Type u_1
inst_3 : Fintype J
Y : J → C
c : Bicone.{u_1, v, u} Y
hc : c.IsBilimit
n : ℕ
x : (i : J) → Ext.{w, v, u} X (Y i) n
i : J
h : ∑ x_1 : J, (x x_1).comp (mk₀ (c.ι x_1 ≫ c.π i)) ⋯ = x i
⊢ (fun (e : Ext.{w, v, u} X c.pt n) (i : J) ↦ e.comp (mk₀ (c.π i)) ⋯)
      ((fun (e : (i : J) → Ext.{w, v, u} X (Y i) n) ↦ (∑ i : J, (e i).comp (mk₀ (c.ι i)) ⋯ : Ext.{w, v, u} X c.pt n)) x)
      i =
    x i

Tactic:
simp only [Ext.sum_comp, comp_assoc_of_second_deg_zero, mk₀_comp_mk₀]

Premises used: CategoryTheory.Abelian.Ext.sum_comp, CategoryTheory.Abelian.Ext.comp_assoc_of_second_deg_zero, CategoryTheory.Abelian.Ext.mk₀_comp_mk₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
J : Type u_1
inst_3 : Fintype J
Y : J → C
c : Bicone.{u_1, v, u} Y
hc : c.IsBilimit
n : ℕ
x : (i : J) → Ext.{w, v, u} X (Y i) n
i : J
⊢ i ∉ Finset.univ → (x i).comp (mk₀ (c.ι i ≫ c.π i)) ⋯ = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X : C
J : Type u_1
inst_3 : Fintype J
Y : J → C
c : Bicone.{u_1, v, u} Y
hc : c.IsBilimit
n : ℕ
x : (i : J) → Ext.{w, v, u} X (Y i) n
i : J
rw : ∀ (b : J), Membership.mem (γ := Finset J) Finset.univ b → b ≠ i → (x b).comp (mk₀ (c.ι b ≫ c.π i)) ⋯ = 0
⊢ ∑ x_1 : J, (x x_1).comp (mk₀ (c.ι x_1 ≫ c.π i)) ⋯ = x i

Tactic:
rw [Finset.sum_eq_single i _ (by simp), bicone_ι_π_self, comp_mk₀_id]

Premises used: CategoryTheory.Abelian.Ext.comp_mk₀_id, Finset.sum_eq_single, CategoryTheory.Limits.bicone_ι_π_self