mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
D' : Type u₃
inst✝³ : Category.{v₃, u₃} D'
L : C ⥤ D
inst✝² : L.IsLocalization W
L' : C ⥤ D'
inst✝¹ : L'.IsLocalization W
G : D ⥤ D'
e : L ⋙ G ≅ L'
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
⊢ (homEquiv W W.Q L') ((homEquiv W L W.Q) f) = e.inv.app X ≫ G.map f ≫ e.hom.app Y

Tactic:
homEquiv_trans

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
D' : Type u₃
inst✝³ : Category.{v₃, u₃} D'
L : C ⥤ D
inst✝² : L.IsLocalization W
L' : C ⥤ D'
inst✝¹ : L'.IsLocalization W
G : D ⥤ D'
e : L ⋙ G ≅ L'
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
⊢ (homEquiv W L L') f = e.inv.app X ≫ G.map f ≫ e.hom.app Y
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C✝ : Type u_1
inst✝⁵ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝⁴ : Category.{?u.7, u_2} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n✝ n i : ℤ
hi : n < i
⊢ 0 ≤ i - n

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C✝ : Type u_1
inst✝⁵ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝⁴ : Category.{?u.7, u_2} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n✝ n i : ℤ
hi : i < n
⊢ 0 ≤ n - i

Tactic:
by lia

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ IsIso (Q.map (inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s b))

pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ f =
    Q.map (inv (X.ιTruncLE b) ≫ CochainComplex.truncLEMap g b) ≫
      inv (Q.map (inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s b))

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ IsIso (Q.map (inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s b))
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ f =
    Q.map (inv (X.ιTruncLE b) ≫ CochainComplex.truncLEMap g b) ≫
      inv (Q.map (inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s b))

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ f =
    Q.map (inv (X.ιTruncLE b) ≫ CochainComplex.truncLEMap g b) ≫
      inv (Q.map (inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s b))
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
h : a < b
inst✝¹ : X.IsStrictlyLE a
inst✝ : Y.IsStrictlyGE b
X' : CochainComplex C ℤ
w✝¹ : X'.IsStrictlyLE a
s : X' ⟶ X
w✝ : IsIso (Q.map s)
g : X' ⟶ Y
i : ℤ
hi : a < i
⊢ g.f i = HomologicalComplex.Hom.f 0 i

pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
h : a < b
inst✝¹ : X.IsStrictlyLE a
inst✝ : Y.IsStrictlyGE b
X' : CochainComplex C ℤ
w✝¹ : X'.IsStrictlyLE a
s : X' ⟶ X
w✝ : IsIso (Q.map s)
g : X' ⟶ Y
i : ℤ
hi : ¬a < i
⊢ g.f i = HomologicalComplex.Hom.f 0 i

Tactic:
·

Goal state after:
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
h : a < b
inst✝¹ : X.IsStrictlyLE a
inst✝ : Y.IsStrictlyGE b
X' : CochainComplex C ℤ
w✝¹ : X'.IsStrictlyLE a
s : X' ⟶ X
w✝ : IsIso (Q.map s)
g : X' ⟶ Y
i : ℤ
hi : a < i
⊢ g.f i = HomologicalComplex.Hom.f 0 i
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
h : a < b
inst✝¹ : X.IsStrictlyLE a
inst✝ : Y.IsStrictlyGE b
X' : CochainComplex C ℤ
w✝¹ : X'.IsStrictlyLE a
s : X' ⟶ X
w✝ : IsIso (Q.map s)
g : X' ⟶ Y
i : ℤ
hi : ¬a < i
⊢ g.f i = HomologicalComplex.Hom.f 0 i

Tactic:
·

Goal state after:
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
h : a < b
inst✝¹ : X.IsStrictlyLE a
inst✝ : Y.IsStrictlyGE b
X' : CochainComplex C ℤ
w✝¹ : X'.IsStrictlyLE a
s : X' ⟶ X
w✝ : IsIso (Q.map s)
g : X' ⟶ Y
i : ℤ
hi : ¬a < i
⊢ g.f i = HomologicalComplex.Hom.f 0 i
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
h : a < b
inst✝¹ : X.IsStrictlyLE a
inst✝ : Y.IsStrictlyGE b
X' : CochainComplex C ℤ
w✝¹ : X'.IsStrictlyLE a
s : X' ⟶ X
w✝ : IsIso (Q.map s)
g : X' ⟶ Y
i : ℤ
hi : ¬a < i
⊢ i < b

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁴ : AddMonoid M
inst✝³ : HasShift C M
inst✝² : HasShift D M
L : C ⥤ D
inst✝¹ : L.IsLocalization W
inst✝ : L.CommShift M
X Y : C
eq :
  ∀ (a b : M),
    Small.{w, v₂} ((shiftFunctor C a ⋙ L).obj X ⟶ (shiftFunctor C b ⋙ L).obj Y) ↔
      Small.{w, v₂} ((L ⋙ shiftFunctor D a).obj X ⟶ (L ⋙ shiftFunctor D b).obj Y)
⊢ (∀ (a b : M), HasSmallLocalizedHom W ((shiftFunctor C a).obj X) ((shiftFunctor C b).obj Y)) ↔
    ∀ (a b : M), Small.{w, v₂} ((shiftFunctor D a).obj (L.obj X) ⟶ (shiftFunctor D b).obj (L.obj Y))

Tactic:
dsimp at eq

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁴ : AddMonoid M
inst✝³ : HasShift C M
inst✝² : HasShift D M
L : C ⥤ D
inst✝¹ : L.IsLocalization W
inst✝ : L.CommShift M
X Y : C
eq :
  ∀ (a b : M),
    Small.{w, v₂} (L.obj ((shiftFunctor C a).obj X) ⟶ L.obj ((shiftFunctor C b).obj Y)) ↔
      Small.{w, v₂} ((shiftFunctor D a).obj (L.obj X) ⟶ (shiftFunctor D b).obj (L.obj Y))
⊢ (∀ (a b : M), HasSmallLocalizedHom W ((shiftFunctor C a).obj X) ((shiftFunctor C b).obj Y)) ↔
    ∀ (a b : M), Small.{w, v₂} ((shiftFunctor D a).obj (L.obj X) ⟶ (shiftFunctor D b).obj (L.obj Y))
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₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
hi : ∃ j, c.Rel i j
⊢ Mono (homologyMap φ.τ₃ i)

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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
hi : ¬∃ j, c.Rel i j
⊢ Mono (homologyMap φ.τ₃ i)

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₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₁ i)
h₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
hi : ∃ j, c.Rel i j
⊢ Mono (homologyMap φ.τ₃ i)
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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ ((δlastFunctor ⋙ δ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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ ((δlastFunctor ⋙ δ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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δlastFunctor ⋙ δ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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δlastFunctor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 1
      mono_of_epi_of_mono_of_mono'._proof_11)

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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δlastFunctor ⋙ δ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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ ((δlastFunctor ⋙ δ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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ ((δlastFunctor ⋙ δ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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δlastFunctor ⋙ δ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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δlastFunctor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 1
      mono_of_epi_of_mono_of_mono'._proof_11)

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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δlastFunctor ⋙ δ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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ ((δlastFunctor ⋙ δ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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δlastFunctor ⋙ δ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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δlastFunctor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 1
      mono_of_epi_of_mono_of_mono'._proof_11)

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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δlastFunctor ⋙ δ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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Epi
    (app' ((δlastFunctor ⋙ δ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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δlastFunctor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 1
      mono_of_epi_of_mono_of_mono'._proof_11)

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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δlastFunctor ⋙ δ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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δlastFunctor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 1
      mono_of_epi_of_mono_of_mono'._proof_11)
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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δlastFunctor ⋙ δ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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ Mono
    (app' ((δlastFunctor ⋙ δ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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
hi : ¬∃ j, c.Rel i j
⊢ Mono (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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
hi : ¬∃ j, c.Rel i j
⊢ Mono (homologyMap φ.τ₃ i)
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₁ 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)

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 pos
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)