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

Goal state before:
pp: case mp
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{v_1, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
⊢ IsZero K → K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e

pp: case mpr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{v_1, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
⊢ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e → IsZero K

Tactic:
·

Goal state after:
case mp
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{v_1, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
⊢ IsZero K → K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e
Module: Mathlib.Algebra.Homology.Embedding.IsSupported

Goal state before:
pp: case mpr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{v_1, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
⊢ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e → IsZero K

Tactic:
·

Goal state after:
case mpr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{v_1, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
⊢ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e → IsZero K
Module: Mathlib.Algebra.Homology.Embedding.IsSupported

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{v_1, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
hn : ∃ i, e.f i = n
⊢ IsZero (K.X n)

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{v_1, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
hn : ¬∃ i, e.f i = n
⊢ IsZero (K.X n)

Tactic:
·

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{v_1, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
hn : ∃ i, e.f i = n
⊢ IsZero (K.X n)
Module: Mathlib.Algebra.Homology.Embedding.IsSupported

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{v_1, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
hn : ¬∃ i, e.f i = n
⊢ IsZero (K.X n)

Tactic:
·

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{v_1, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
hn : ¬∃ i, e.f i = n
⊢ IsZero (K.X n)
Module: Mathlib.Algebra.Homology.Embedding.IsSupported

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : Category.{v_2, u_4} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
K : HomologicalComplex C c'
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
e : c.Embedding c'
inst✝ : F.Faithful
x✝ : ((F.mapHomologicalComplex c').obj K).IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ 𝟙 (K.X i') = 0

Tactic:
exact F.map_injective ((isZero_X_of_isStrictlySupported
    ((F.mapHomologicalComplex c').obj K) e i' hi').eq_of_src _ _)

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
n : ℤ
⊢ n + 1 = n + 1

Tactic:
by lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
n : ℤ
⊢ n + 1 + -1 = n

Tactic:
by lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
n : ℤ
⊢ n + 2 + -2 = n

Tactic:
by lia

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
n : ℤ
⊢ n + 2 + -1 = n + 1

Tactic:
by lia

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

Goal state before:
pp: case inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
hi' : e.r i' = none
⊢ extend.d K (e.r i') (e.r j') = 0

pp: case inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
⊢ extend.d K (e.r i') (e.r j') = 0

Tactic:
·

Goal state after:
case inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
hi' : e.r i' = none
⊢ extend.d K (e.r i') (e.r j') = 0
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
⊢ extend.d K (e.r i') (e.r j') = 0

Tactic:
·

Goal state after:
case inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
⊢ extend.d K (e.r i') (e.r j') = 0
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr.inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
hj' : e.r j' = none
⊢ extend.d K (e.r i') (e.r j') = 0

pp: case inr.inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ extend.d K (e.r i') (e.r j') = 0

Tactic:
·

Goal state after:
case inr.inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
hj' : e.r j' = none
⊢ extend.d K (e.r i') (e.r j') = 0
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr.inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ extend.d K (e.r i') (e.r j') = 0

Tactic:
·

Goal state after:
case inr.inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ extend.d K (e.r i') (e.r j') = 0
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝³ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝² : HasZeroMorphisms V
K L : HomologicalComplex Vᵒᵖ c
φ : K ⟶ L
inst✝¹ : ∀ (i : ι), K.HasHomology i
inst✝ : ∀ (i : ι), L.HasHomology i
⊢ QuasiIso ((unopFunctor V c).map φ.op) ↔ QuasiIso φ

Tactic:
by
  simp only [quasiIso_iff, quasiIsoAt_unopFunctor_map_iff]

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

Goal state before:
pp: case inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
hi' : e.r i' = none
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0

pp: case inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0

Tactic:
·

Goal state after:
case inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
hi' : e.r i' = none
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: case pos
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : c.Rel j i
⊢ (K.opcyclesOpIso i).hom ≫ (K.toCycles j i).op = K.op.fromOpcycles i j

pp: case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel j i
⊢ (K.opcyclesOpIso i).hom ≫ (K.toCycles j i).op = K.op.fromOpcycles i j

Tactic:
·

Goal state after:
case pos
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : c.Rel j i
⊢ (K.opcyclesOpIso i).hom ≫ (K.toCycles j i).op = K.op.fromOpcycles i j
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0

Tactic:
·

Goal state after:
case inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr.inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
hj' : e.r j' = none
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0

pp: case inr.inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0

Tactic:
·

Goal state after:
case inr.inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
hj' : e.r j' = none
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel j i
⊢ (K.opcyclesOpIso i).hom ≫ (K.toCycles j i).op = K.op.fromOpcycles i j

Tactic:
·

Goal state after:
case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel j i
⊢ (K.opcyclesOpIso i).hom ≫ (K.toCycles j i).op = K.op.fromOpcycles i j
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr.inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0

Tactic:
·

Goal state after:
case inr.inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: case pos
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : c.Rel i j
⊢ (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i

pp: case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel i j
⊢ (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i

Tactic:
·

Goal state after:
case pos
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : c.Rel i j
⊢ (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr.inr.inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
hk' : e.r k' = none
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0

pp: case inr.inr.inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0

Tactic:
·

Goal state after:
case inr.inr.inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
hk' : e.r k' = none
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel i j
⊢ (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i

Tactic:
·

Goal state after:
case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel i j
⊢ (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr.inr.inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0

Tactic:
·

Goal state after:
case inr.inr.inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i j : ι
hi : e.f i = i'
hj : e.f j = j'
⊢ (K.extend e).d i' j' = (K.extendXIso e hi).hom ≫ K.d i j ≫ (K.extendXIso e hj).inv

Tactic:
by
  apply extend.d_eq

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

Goal state before:
pp: case inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
hj' : e.r j' = none
⊢ (K.extend e).d i' j' = 0

pp: case inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
j : ι
hj : e.r j' = some j
⊢ (K.extend e).d i' j' = 0

Tactic:
·

Goal state after:
case inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
hj' : e.r j' = none
⊢ (K.extend e).d i' j' = 0
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
j : ι
hj : e.r j' = some j
⊢ (K.extend e).d i' j' = 0

Tactic:
·

Goal state after:
case inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
j : ι
hj : e.r j' = some j
⊢ (K.extend e).d i' j' = 0
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case left
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ c'.Rel (c'.prev (e.f j)) (e.f j)

pp: case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ ∀ (i : ι), ¬c'.Rel (e.f i) (e.f j)

Tactic:
·

Goal state after:
case left
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ c'.Rel (c'.prev (e.f j)) (e.f j)
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ ∀ (i : ι), ¬c'.Rel (e.f i) (e.f j)

Tactic:
·

Goal state after:
case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
j : ι
hj : c'.Rel i' (e.f j)
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ ∀ (i : ι), ¬c'.Rel (e.f i) (e.f j)
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
hjk : c.Rel j k
⊢ ¬e.BoundaryGE k

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
hjk : ¬c.Rel j k
⊢ ¬e.BoundaryGE k

Tactic:
·

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
hjk : c.Rel j k
⊢ ¬e.BoundaryGE k
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
hjk : ¬c.Rel j k
⊢ ¬e.BoundaryGE k

Tactic:
·

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
hjk : ¬c.Rel j k
⊢ ¬e.BoundaryGE k