mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos.hR₁
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ ((δ₀Functor ⋙ δlastFunctor).obj (composableArrows₅ hS₁ i j hij)).Exact

pp: case pos.hR₂
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ ((δ₀Functor ⋙ δlastFunctor).obj (composableArrows₅ hS₂ i j hij)).Exact

pp: case pos.h₀
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 0
      mono_of_epi_of_mono_of_mono'._proof_13)

pp: case pos.h₂
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 2
      mono_of_epi_of_mono_of_mono'._proof_4)

pp: case pos.h₃
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 3
      mono_of_epi_of_mono_of_mono'._proof_7)

Tactic:
·

Goal state after:
case pos.hR₁
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ ((δ₀Functor ⋙ δlastFunctor).obj (composableArrows₅ hS₁ i j hij)).Exact
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos.hR₂
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ ((δ₀Functor ⋙ δlastFunctor).obj (composableArrows₅ hS₂ i j hij)).Exact

pp: case pos.h₀
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 0
      mono_of_epi_of_mono_of_mono'._proof_13)

pp: case pos.h₂
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 2
      mono_of_epi_of_mono_of_mono'._proof_4)

pp: case pos.h₃
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 3
      mono_of_epi_of_mono_of_mono'._proof_7)

Tactic:
·

Goal state after:
case pos.hR₂
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ ((δ₀Functor ⋙ δlastFunctor).obj (composableArrows₅ hS₂ i j hij)).Exact
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos.h₀
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 0
      mono_of_epi_of_mono_of_mono'._proof_13)

pp: case pos.h₂
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 2
      mono_of_epi_of_mono_of_mono'._proof_4)

pp: case pos.h₃
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 3
      mono_of_epi_of_mono_of_mono'._proof_7)

Tactic:
·

Goal state after:
case pos.h₀
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 0
      mono_of_epi_of_mono_of_mono'._proof_13)
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos.h₂
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 2
      mono_of_epi_of_mono_of_mono'._proof_4)

pp: case pos.h₃
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 3
      mono_of_epi_of_mono_of_mono'._proof_7)

Tactic:
·

Goal state after:
case pos.h₂
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 2
      mono_of_epi_of_mono_of_mono'._proof_4)
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos.h₃
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 3
      mono_of_epi_of_mono_of_mono'._proof_7)

Tactic:
·

Goal state after:
case pos.h₃
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 3
      mono_of_epi_of_mono_of_mono'._proof_7)
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
hi : ¬∃ j, c.Rel i j
⊢ Epi (homologyMap φ.τ₃ i)

Tactic:
·

Goal state after:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
hi : ¬∃ j, c.Rel i j
⊢ Epi (homologyMap φ.τ₃ i)
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
hi : ¬∃ j, c.Rel i j
this : Epi S₂.g
eq : (homologyFunctor C c i).map (φ.τ₂ ≫ S₂.g) = (homologyFunctor C c i).map (S₁.g ≫ φ.τ₃)
⊢ Epi (homologyMap φ.τ₃ i)

Tactic:
dsimp at eq

Goal state after:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
hi : ¬∃ j, c.Rel i j
this : Epi S₂.g
eq : homologyMap (φ.τ₂ ≫ S₂.g) i = homologyMap (S₁.g ≫ φ.τ₃) i
⊢ Epi (homologyMap φ.τ₃ i)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (∀ (X Y : C) (a b : ℤ),
      Small.{w, w'}
        ((shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
          (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y)))) →
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))

pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'}
          ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))) →
    ∀ (X Y : C) (a b : ℤ),
      Small.{w, w'}
        ((shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
          (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y)))

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (∀ (X Y : C) (a b : ℤ),
      Small.{w, w'}
        ((shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
          (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y)))) →
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'}
          ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))) →
    ∀ (X Y : C) (a b : ℤ),
      Small.{w, w'}
        ((shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
          (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y)))

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w, w'}
          ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))) →
    ∀ (X Y : C) (a b : ℤ),
      Small.{w, w'}
        ((shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
          (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y)))
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case mpr.inl
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : a ≤ b
⊢ Small.{w, w'}
    ((shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
      (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y)))

pp: case mpr.inr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
⊢ Small.{w, w'}
    ((shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
      (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y)))

Tactic:
·

Goal state after:
case mpr.inl
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : a ≤ b
⊢ Small.{w, w'}
    ((shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
      (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y)))
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case mpr.inr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
⊢ Small.{w, w'}
    ((shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
      (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y)))

Tactic:
·

Goal state after:
case mpr.inr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
⊢ Small.{w, w'}
    ((shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
      (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y)))
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
x y :
  (shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
    (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))
⊢ a + -a = 0

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
j : ι
h₁ : Mono (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (HomologicalComplex.homologyMap S.g i)
hj : ∃ i, c.Rel i j
⊢ IsZero (S.X₁.homology j)

pp: case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
j : ι
h₁ : Mono (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (HomologicalComplex.homologyMap S.g i)
hj : ∀ (i : ι), ¬c.Rel i j
⊢ IsZero (S.X₁.homology j)

Tactic:
·

Goal state after:
case pos
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
j : ι
h₁ : Mono (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (HomologicalComplex.homologyMap S.g i)
hj : ∃ i, c.Rel i j
⊢ IsZero (S.X₁.homology j)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
h :
  ∀ (X Y : C) (n : ℤ),
    0 ≤ n →
      Small.{w, w'} ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
X Y : C
a b : ℤ
hab : b < a
x y :
  (shiftFunctor (DerivedCategory C) a).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj X)) ⟶
    (shiftFunctor (DerivedCategory C) b).obj (Q.obj ((CochainComplex.singleFunctor C 0).obj Y))
this : ((shiftFunctor (CochainComplex C ℤ) a).obj ((CochainComplex.singleFunctor C 0).obj X)).IsStrictlyLE (-a)
⊢ b + -b = 0

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos.hf
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
j : ι
h₁ : Mono (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (HomologicalComplex.homologyMap S.g i)
i : ι
hij : c.Rel i j
this : Epi (HomologicalComplex.homologyMap S.g i)
⊢ { X₁ := S.X₃.homology i, X₂ := S.X₁.homology j, X₃ := S.X₂.homology j, f := hS.δ i j hij,
        g := HomologicalComplex.homologyMap S.f j, zero := ⋯ }.f =
    0

pp: case pos.hg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
j : ι
h₁ : Mono (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (HomologicalComplex.homologyMap S.g i)
i : ι
hij : c.Rel i j
this : Epi (HomologicalComplex.homologyMap S.g i)
⊢ { X₁ := S.X₃.homology i, X₂ := S.X₁.homology j, X₃ := S.X₂.homology j, f := hS.δ i j hij,
        g := HomologicalComplex.homologyMap S.f j, zero := ⋯ }.g =
    0

Tactic:
·

Goal state after:
case pos.hf
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
j : ι
h₁ : Mono (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (HomologicalComplex.homologyMap S.g i)
i : ι
hij : c.Rel i j
this : Epi (HomologicalComplex.homologyMap S.g i)
⊢ { X₁ := S.X₃.homology i, X₂ := S.X₁.homology j, X₃ := S.X₂.homology j, f := hS.δ i j hij,
        g := HomologicalComplex.homologyMap S.f j, zero := ⋯ }.f =
    0
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos.hg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
j : ι
h₁ : Mono (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (HomologicalComplex.homologyMap S.g i)
i : ι
hij : c.Rel i j
this : Epi (HomologicalComplex.homologyMap S.g i)
⊢ { X₁ := S.X₃.homology i, X₂ := S.X₁.homology j, X₃ := S.X₂.homology j, f := hS.δ i j hij,
        g := HomologicalComplex.homologyMap S.f j, zero := ⋯ }.g =
    0

Tactic:
·

Goal state after:
case pos.hg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
j : ι
h₁ : Mono (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (HomologicalComplex.homologyMap S.g i)
i : ι
hij : c.Rel i j
this : Epi (HomologicalComplex.homologyMap S.g i)
⊢ { X₁ := S.X₃.homology i, X₂ := S.X₁.homology j, X₃ := S.X₂.homology j, f := hS.δ i j hij,
        g := HomologicalComplex.homologyMap S.f j, zero := ⋯ }.g =
    0
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
j : ι
h₁ : Mono (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (HomologicalComplex.homologyMap S.g i)
hj : ∀ (i : ι), ¬c.Rel i j
⊢ IsZero (S.X₁.homology j)

Tactic:
·

Goal state after:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
j : ι
h₁ : Mono (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (HomologicalComplex.homologyMap S.g i)
hj : ∀ (i : ι), ¬c.Rel i j
⊢ IsZero (S.X₁.homology j)
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
a b : ℕ
α : Ext X Y a
β : Ext Y Z b
c : ℕ
h : a + b = c
⊢ ↑b + ↑a = ↑c

Tactic:
by lia

Goal state after: