mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
n a b c : ℕ
h : a + b = c
⊢ ∀ (a_1 b_1 : Ext X Y a),
    AddMonoidHom.mk' (fun β ↦ (a_1 + b_1).comp β h) ⋯ =
      AddMonoidHom.mk' (fun β ↦ a_1.comp β h) ⋯ + AddMonoidHom.mk' (fun β ↦ b_1.comp β h) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
⊢ AddCommGrpCat.ofHom ((Ext.mk₀ (f ≫ f')).postcomp X ⋯) =
    AddCommGrpCat.ofHom ((Ext.mk₀ f).postcomp X ⋯) ≫ AddCommGrpCat.ofHom ((Ext.mk₀ f').postcomp X ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y : C
⊢ ∀ (a b : Ext (Opposite.unop X₁) Y n),
    (Ext.mk₀ f.unop).comp (a + b) ⋯ = (Ext.mk₀ f.unop).comp a ⋯ + (Ext.mk₀ f.unop).comp b ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ (extFunctorObj (Opposite.unop X₁) n).map g ≫
      AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α ↦ (Ext.mk₀ f.unop).comp α ⋯) ⋯) =
    AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α ↦ (Ext.mk₀ f.unop).comp α ⋯) ⋯) ≫
      (extFunctorObj (Opposite.unop X₂) n).map g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
n : ℕ
X₁ X₂ X₃ : Cᵒᵖ
f : X₁ ⟶ X₂
f' : X₂ ⟶ X₃
⊢ { app := fun Y ↦ AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α ↦ (Ext.mk₀ (f ≫ f').unop).comp α ⋯) ⋯),
      naturality := ⋯ } =
    { app := fun Y ↦ AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α ↦ (Ext.mk₀ f.unop).comp α ⋯) ⋯), naturality := ⋯ } ≫
      { app := fun Y ↦ AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α ↦ (Ext.mk₀ f'.unop).comp α ⋯) ⋯), naturality := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂✝ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃✝ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
g₁ : A ⟶ R₂.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11
A₁ : C
π₁ : A₁ ⟶ A
w✝³ : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
w✝² : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
h₄ : (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ = 0
A₃ : C
π₃ : A₃ ⟶ A₂
w✝¹ : Epi π₃
g₀ : A₃ ⟶ R₂.obj 0
h₅ : π₃ ≫ π₂ ≫ π₁ ≫ g₁ - π₃ ≫ f₁ ≫ φ.app 1 = g₀ ≫ R₂.map (homOfLE ⋯)
A₄ : C
π₄ : A₄ ⟶ A₃
w✝ : Epi π₄
f₀ : A₄ ⟶ R₁.obj' 0 mono_of_epi_of_mono_of_mono'._proof_13
h₆ : π₄ ≫ g₀ = f₀ ≫ app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13
⊢ R₁.obj' 0 mono_of_epi_of_mono_of_mono'._proof_13 ⟶ R₁.obj 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x : Ext c.pt Y n
⊢ (fun e ↦ ∑ i, (mk₀ (c.π i)).comp (e i) ⋯) ((fun e i ↦ (mk₀ (c.ι i)).comp e ⋯) x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x✝ : (i : J) → Ext (X i) Y n
i : J
⊢ i ∉ Finset.univ → (mk₀ (c.ι i ≫ c.π i)).comp (x✝ i) ⋯ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x✝ : (i : J) → Ext (X i) Y n
i : J
⊢ (mk₀ (c.ι i ≫ c.π i)).comp (x✝ i) ⋯ = x✝ i

pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x✝ : (i : J) → Ext (X i) Y n
i : J
⊢ ∀ b ∈ Finset.univ, b ≠ i → (mk₀ (c.ι i ≫ c.π b)).comp (x✝ b) ⋯ = 0

Tactic:
bicone_ι_π_self,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x✝ : (i : J) → Ext (X i) Y n
i : J
⊢ (mk₀ (𝟙 (X i))).comp (x✝ i) ⋯ = x✝ i

C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x✝ : (i : J) → Ext (X i) Y n
i : J
⊢ ∀ b ∈ Finset.univ, b ≠ i → (mk₀ (c.ι i ≫ c.π b)).comp (x✝ b) ⋯ = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x✝ : (i : J) → Ext (X i) Y n
⊢ (fun e i ↦ (mk₀ (c.ι i)).comp e ⋯) ((fun e ↦ ∑ i, (mk₀ (c.π i)).comp (e i) ⋯) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x✝¹ x✝ : Ext c.pt Y n
⊢ (fun i ↦ (mk₀ (c.ι i)).comp (x✝¹ + x✝) ⋯) = (fun i ↦ (mk₀ (c.ι i)).comp x✝¹ ⋯) + fun i ↦ (mk₀ (c.ι i)).comp x✝ ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X : C
J : Type u_1
inst✝ : Fintype J
Y : J → C
c : Bicone Y
hc : c.IsBilimit
n : ℕ
x✝ : Ext X c.pt n
⊢ (fun e ↦ ∑ i, (e i).comp (mk₀ (c.ι i)) ⋯) ((fun e i ↦ e.comp (mk₀ (c.π i)) ⋯) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X : C
J : Type u_1
inst✝ : Fintype J
Y : J → C
c : Bicone Y
hc : c.IsBilimit
n : ℕ
x✝ : (i : J) → Ext X (Y i) n
i : J
⊢ i ∉ Finset.univ → (x✝ i).comp (mk₀ (c.ι i ≫ c.π i)) ⋯ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X : C
J : Type u_1
inst✝ : Fintype J
Y : J → C
c : Bicone Y
hc : c.IsBilimit
n : ℕ
x✝ : (i : J) → Ext X (Y i) n
i : J
⊢ (x✝ i).comp (mk₀ (c.ι i ≫ c.π i)) ⋯ = x✝ i

pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X : C
J : Type u_1
inst✝ : Fintype J
Y : J → C
c : Bicone Y
hc : c.IsBilimit
n : ℕ
x✝ : (i : J) → Ext X (Y i) n
i : J
⊢ ∀ b ∈ Finset.univ, b ≠ i → (x✝ b).comp (mk₀ (c.ι b ≫ c.π i)) ⋯ = 0

Tactic:
bicone_ι_π_self,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X : C
J : Type u_1
inst✝ : Fintype J
Y : J → C
c : Bicone Y
hc : c.IsBilimit
n : ℕ
x✝ : (i : J) → Ext X (Y i) n
i : J
⊢ (x✝ i).comp (mk₀ (𝟙 (Y i))) ⋯ = x✝ i

C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X : C
J : Type u_1
inst✝ : Fintype J
Y : J → C
c : Bicone Y
hc : c.IsBilimit
n : ℕ
x✝ : (i : J) → Ext X (Y i) n
i : J
⊢ ∀ b ∈ Finset.univ, b ≠ i → (x✝ b).comp (mk₀ (c.ι b ≫ c.π i)) ⋯ = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X : C
J : Type u_1
inst✝ : Fintype J
Y : J → C
c : Bicone Y
hc : c.IsBilimit
n : ℕ
x✝ : (i : J) → Ext X (Y i) n
⊢ (fun e i ↦ e.comp (mk₀ (c.π i)) ⋯) ((fun e ↦ ∑ i, (e i).comp (mk₀ (c.ι i)) ⋯) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w :
  a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (-(↑(fst S.f)).v n₀ n₁ h ≫ S.X₁.d n₁ (n₁ + 1)) = 0 ∧
    (a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (mappingCone S.f).d n₀ n₁ + b ≫ S.X₂.d n₀ n₁ ≫ (inr S.f).f n₁) ≫ (snd S.f).v n₁ n₁ ⋯ =
      0 ≫ (snd S.f).v n₁ n₁ ⋯
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h

Tactic:
comp_neg,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w :
  a ≫ (-(inl S.f).v n₁ n₀ ⋯ ≫ (↑(fst S.f)).v n₀ n₁ h ≫ S.X₁.d n₁ (n₁ + 1)) = 0 ∧
    (a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (mappingCone S.f).d n₀ n₁ + b ≫ S.X₂.d n₀ n₁ ≫ (inr S.f).f n₁) ≫ (snd S.f).v n₁ n₁ ⋯ =
      0 ≫ (snd S.f).v n₁ n₁ ⋯
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X : C
J : Type u_1
inst✝ : Fintype J
Y : J → C
c : Bicone Y
hc : c.IsBilimit
n : ℕ
x✝¹ x✝ : Ext X c.pt n
⊢ (fun i ↦ (x✝¹ + x✝).comp (mk₀ (c.π i)) ⋯) = (fun i ↦ x✝¹.comp (mk₀ (c.π i)) ⋯) + fun i ↦ x✝.comp (mk₀ (c.π i)) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w :
  a ≫ (-S.X₁.d n₁ (n₁ + 1)) = 0 ∧
    (a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (mappingCone S.f).d n₀ n₁ + b ≫ S.X₂.d n₀ n₁ ≫ (inr S.f).f n₁) ≫ (snd S.f).v n₁ n₁ ⋯ =
      0 ≫ (snd S.f).v n₁ n₁ ⋯
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h

Tactic:
comp_neg,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w :
  -a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧
    (a ≫ (inl S.f).v n₁ n₀ ⋯ ≫ (mappingCone S.f).d n₀ n₁ + b ≫ S.X₂.d n₀ n₁ ≫ (inr S.f).f n₁) ≫ (snd S.f).v n₁ n₁ ⋯ =
      0 ≫ (snd S.f).v n₁ n₁ ⋯
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X₁ X₂ Y : C
n : ℕ
x✝ : Ext (X₁ ⊞ X₂) Y n
⊢ (fun e ↦ (mk₀ biprod.fst).comp e.1 ⋯ + (mk₀ biprod.snd).comp e.2 ⋯)
      ((fun e ↦ ((mk₀ biprod.inl).comp e ⋯, (mk₀ biprod.inr).comp e ⋯)) x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X₁ X₂ Y : C
n : ℕ
x✝ : Ext X₁ Y n × Ext X₂ Y n
⊢ (fun e ↦ ((mk₀ biprod.inl).comp e ⋯, (mk₀ biprod.inr).comp e ⋯))
      ((fun e ↦ (mk₀ biprod.fst).comp e.1 ⋯ + (mk₀ biprod.snd).comp e.2 ⋯) x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X₁ X₂ Y : C
n : ℕ
⊢ ∀ (x y : Ext (X₁ ⊞ X₂) Y n),
    ((mk₀ biprod.inl).comp (x + y) ⋯, (mk₀ biprod.inr).comp (x + y) ⋯) =
      ((mk₀ biprod.inl).comp x ⋯, (mk₀ biprod.inr).comp x ⋯) + ((mk₀ biprod.inl).comp y ⋯, (mk₀ biprod.inr).comp y ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y₁ Y₂ : C
n : ℕ
e : Ext X (Y₁ ⊞ Y₂) n
⊢ (fun e ↦ e.1.comp (mk₀ biprod.inl) ⋯ + e.2.comp (mk₀ biprod.inr) ⋯)
      ((fun e ↦ (e.comp (mk₀ biprod.fst) ⋯, e.comp (mk₀ biprod.snd) ⋯)) e) =
    e

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y₁ Y₂ : C
n : ℕ
x✝ : Ext X Y₁ n × Ext X Y₂ n
⊢ (fun e ↦ (e.comp (mk₀ biprod.fst) ⋯, e.comp (mk₀ biprod.snd) ⋯))
      ((fun e ↦ e.1.comp (mk₀ biprod.inl) ⋯ + e.2.comp (mk₀ biprod.inr) ⋯) x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y₁ Y₂ : C
n : ℕ
⊢ ∀ (x y : Ext X (Y₁ ⊞ Y₂) n),
    ((x + y).comp (mk₀ biprod.fst) ⋯, (x + y).comp (mk₀ biprod.snd) ⋯) =
      (x.comp (mk₀ biprod.fst) ⋯, x.comp (mk₀ biprod.snd) ⋯) + (y.comp (mk₀ biprod.fst) ⋯, y.comp (mk₀ biprod.snd) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasExt C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
e : Ext X Y n
⊢ homEquiv (chgUniv e) = homEquiv e

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
this : HasDerivedCategory C := HasDerivedCategory.standard C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w', max u v}
        ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
n : ℕ
⊢ 0 ≤ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
⊢ Epi (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
⊢ HasExt C ↔ ∀ (X Y : C) (n : ℕ), Small.{w', w} (Ext X Y n)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
⊢ R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (φ.app 0)
h₁ : IsIso (φ.app 1)
h₃ : IsIso (φ.app 3)
h₄ : Mono (φ.app 4)
⊢ Mono (app' φ 2 ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (φ.app 0)
h₁ : IsIso (φ.app 1)
h₃ : IsIso (φ.app 3)
h₄ : Mono (φ.app 4)
this : Mono (app' φ 2 ⋯)
⊢ Epi (app' φ 2 ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
⊢ (Ext.mk₀ S.f).comp (Ext.mk₀ S.g) ⋯ = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (app' φ 0 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2)
h₁ : IsIso (app' φ 1 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4)
h₃ : IsIso (app' φ 3 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6)
h₄ : Mono (app' φ 4 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7)
⊢ IsIso (app' φ 2 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_9)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ HasSmallLocalizedShiftedHom W ℤ (S.map (CochainComplex.singleFunctor C 0)).X₃
    (S.map (CochainComplex.singleFunctor C 0)).X₁

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ HasSmallLocalizedHom W (S.map (CochainComplex.singleFunctor C 0)).X₃
    (CochainComplex.mappingCone (S.map (CochainComplex.singleFunctor C 0)).f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n k : ℕ
h : k + 3 ≤ n
R₁ R₂ : ComposableArrows C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ k₁ k₂ k₃ : ℕ
hk₀ : k₀ = k
hk₁ : k₁ = k + 1
hk₂ : k₂ = k + 2
hk₃ : k₃ = k + 3
h₀ : Epi (app' φ k₀ ⋯)
h₁ : Mono (app' φ k₁ ⋯)
h₃ : Mono (app' φ k₃ ⋯)
⊢ Mono (app' φ k₂ ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ HasSmallLocalizedShiftedHom W ℤ (CochainComplex.mappingCone (S.map (CochainComplex.singleFunctor C 0)).f)
    (S.map (CochainComplex.singleFunctor C 0)).X₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n k : ℕ
h : k + 3 ≤ n
R₁ R₂ : ComposableArrows C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ k₁ k₂ k₃ : ℕ
hk₀ : k₀ = k
hk₁ : k₁ = k + 1
hk₂ : k₂ = k + 2
hk₃ : k₃ = k + 3
h₀ : Epi (app' φ k₀ ⋯)
h₂ : Epi (app' φ k₂ ⋯)
h₃ : Mono (app' φ k₃ ⋯)
⊢ Epi (app' φ k₁ ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ Ext S.X₃ S.X₁ 1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n k : ℕ
h : k + 4 ≤ n
R₁ R₂ : ComposableArrows C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ k₁ k₂ k₃ k₄ : ℕ
hk₀ : k₀ = k
hk₁ : k₁ = k + 1
hk₂ : k₂ = k + 2
hk₃ : k₃ = k + 3
hk₄ : k₄ = k + 4
h₀ : Epi (app' φ k₀ ⋯)
h₁ : IsIso (app' φ k₁ ⋯)
h₃ : IsIso (app' φ k₃ ⋯)
h₄ : Mono (app' φ k₄ ⋯)
⊢ IsIso (app' φ k₂ ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_epi_mono'._proof_1 = 0
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂ : R₂.Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
⊢ (mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 _proof_299✝ _proof_300✝ ≫
      𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 _proof_300✝) =
    app' φ 2 ⋯ ≫ (mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0).map' 2 3 _proof_299✝ _proof_300✝

Tactic:
by

Goal state after: