mathlib-initiative/mathlib-tactics huggingface dataset:
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
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : c.Rel i j
⊢ c'.prev (e.f j) = e.f i

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : ¬c.Rel i j
⊢ c'.prev (e.f j) = e.f i

Tactic:
·

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : c.Rel i j
⊢ c'.prev (e.f j) = e.f i
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
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : ¬c.Rel i j
⊢ c'.prev (e.f j) = e.f i

Tactic:
·

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : ¬c.Rel i j
⊢ c'.prev (e.f j) = e.f i
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' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
hi' : e.r i' = 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' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
i : ι
hi : e.r i' = some i
⊢ (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' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
hi' : e.r i' = 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' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
i : ι
hi : e.r i' = some i
⊢ (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' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
i : ι
hi : e.r i' = some i
⊢ (K.extend e).d i' j' = 0
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
hi : ∃ i, e.f i = i'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
hi : ¬∃ i, e.f i = i'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
hi : ∃ i, e.f i = i'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
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'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
⊢ c'.Rel (e.f j) (c'.next (e.f j))

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

Tactic:
·

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

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ∃ j, e.f j = j'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ¬∃ j, e.f j = j'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ∃ j, e.f j = j'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r 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'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
⊢ ∀ (k : ι), ¬c'.Rel (e.f j) (e.f k)

Tactic:
·

Goal state after:
case right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
k' : ι'
j : ι
hj : c'.Rel (e.f j) k'
hk' : ∀ (i : ι), e.f i ≠ k'
⊢ ∀ (k : ι), ¬c'.Rel (e.f j) (e.f k)
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
i j : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
hij : c.Rel i j
⊢ ¬e.BoundaryLE i

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
hij : ¬c.Rel i j
⊢ ¬e.BoundaryLE i

Tactic:
·

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
hij : c.Rel i j
⊢ ¬e.BoundaryLE i
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
i j : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
hij : ¬c.Rel i j
⊢ ¬e.BoundaryLE i

Tactic:
·

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
hij : ¬c.Rel i j
⊢ ¬e.BoundaryLE i
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ¬∃ j, e.f j = j'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ¬∃ j, e.f j = j'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r 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 : ι
hjk : c.next j = k
hj : ¬e.BoundaryLE j
hjk' : c.Rel j k
⊢ c'.next (e.f j) = e.f k

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hjk : c.next j = k
hj : ¬e.BoundaryLE j
hjk' : ¬c.Rel j k
⊢ c'.next (e.f j) = e.f 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 : ι
hjk : c.next j = k
hj : ¬e.BoundaryLE j
hjk' : c.Rel j k
⊢ c'.next (e.f j) = e.f 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 : ι
hjk : c.next j = k
hj : ¬e.BoundaryLE j
hjk' : ¬c.Rel j k
⊢ c'.next (e.f j) = e.f 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 : ι
hjk : c.next j = k
hj : ¬e.BoundaryLE j
hjk' : ¬c.Rel j k
⊢ c'.next (e.f j) = e.f k
Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: case refine_5
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₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
α : mappingCone.triangle u₁₂ ⟶ mappingCone.triangle (u₁₂ ≫ u₂₃) := mappingCone.triangleMap u₁₂ (u₁₂ ≫ u₂₃) (𝟙 X₁) u₂₃ ⋯
β : mappingCone.triangle (u₁₂ ≫ u₂₃) ⟶ mappingCone.triangle u₂₃ := mappingCone.triangleMap (u₁₂ ≫ u₂₃) u₂₃ u₁₂ (𝟙 X₃) ⋯
⊢ Triangle.mk ((quotient C (ComplexShape.up ℤ)).map α.hom₃) ((quotient C (ComplexShape.up ℤ)).map β.hom₃)
      (((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₂₃).mor₃ ≫
          (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone.triangle u₂₃).obj₁) ≫
        (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
          ((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₂)) ∈
    distinguishedTriangles

Tactic:
·

Goal state after:
case refine_5
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₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
α : mappingCone.triangle u₁₂ ⟶ mappingCone.triangle (u₁₂ ≫ u₂₃) := mappingCone.triangleMap u₁₂ (u₁₂ ≫ u₂₃) (𝟙 X₁) u₂₃ ⋯
β : mappingCone.triangle (u₁₂ ≫ u₂₃) ⟶ mappingCone.triangle u₂₃ := mappingCone.triangleMap (u₁₂ ≫ u₂₃) u₂₃ u₁₂ (𝟙 X₃) ⋯
⊢ Triangle.mk ((quotient C (ComplexShape.up ℤ)).map α.hom₃) ((quotient C (ComplexShape.up ℤ)).map β.hom₃)
      (((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₂₃).mor₃ ≫
          (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone.triangle u₂₃).obj₁) ≫
        (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
          ((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₂)) ∈
    distinguishedTriangles
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
hi : ¬∃ i, e.f i = i'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
hi : ¬∃ i, e.f i = i'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap (φ ≫ φ') e).f i' = (extendMap φ e ≫ extendMap φ' e).f i'

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (φ ≫ φ') e).f i' = (extendMap φ e ≫ extendMap φ' e).f i'

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap (φ ≫ φ') e).f i' = (extendMap φ e ≫ extendMap φ' e).f i'
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (φ ≫ φ') e).f i' = (extendMap φ e ≫ extendMap φ' e).f i'

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (φ ≫ φ') e).f i' = (extendMap φ e ≫ extendMap φ' e).f i'
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')
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.IsTruncGE
j k : ι
hjk : c.next j = k
hj : c'.Rel (e.f j) (c'.next (e.f j))
⊢ c'.next (e.f j) = e.f k

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : ¬c'.Rel (e.f j) (c'.next (e.f j))
⊢ c'.next (e.f j) = e.f k

Tactic:
·

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : c'.Rel (e.f j) (c'.next (e.f j))
⊢ c'.next (e.f j) = e.f k
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap (𝟙 K) e).f i' = 𝟙 ((K.extend e).X i')
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.IsTruncGE
j k : ι
hjk : c.next j = k
hj : ¬c'.Rel (e.f j) (c'.next (e.f j))
⊢ c'.next (e.f j) = e.f k

Tactic:
·

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : ¬c'.Rel (e.f j) (c'.next (e.f j))
⊢ c'.next (e.f j) = e.f k
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mp
p : ℤ
n : ℕ
⊢ (embeddingUpIntGE p).BoundaryGE n → n = 0

pp: case mpr
p : ℤ
n : ℕ
⊢ n = 0 → (embeddingUpIntGE p).BoundaryGE n

Tactic:
·

Goal state after:
case mp
p : ℤ
n : ℕ
⊢ (embeddingUpIntGE p).BoundaryGE n → n = 0
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mp.zero
p : ℤ
h : (embeddingUpIntGE p).BoundaryGE 0
⊢ 0 = 0

pp: case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
⊢ n + 1 = 0

Tactic:
·

Goal state after:
case mp.zero
p : ℤ
h : (embeddingUpIntGE p).BoundaryGE 0
⊢ 0 = 0
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
⊢ n + 1 = 0

Tactic:
·

Goal state after:
case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
⊢ n + 1 = 0
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap 0 e).f i' = Hom.f 0 i'

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap 0 e).f i' = Hom.f 0 i'

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap 0 e).f i' = Hom.f 0 i'
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mpr
p : ℤ
n : ℕ
⊢ n = 0 → (embeddingUpIntGE p).BoundaryGE n

Tactic:
·

Goal state after:
case mpr
p : ℤ
n : ℕ
⊢ n = 0 → (embeddingUpIntGE p).BoundaryGE n
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mpr.left
p : ℤ
⊢ (up ℤ).Rel ((up ℤ).prev ((embeddingUpIntGE p).f 0)) ((embeddingUpIntGE p).f 0)

pp: case mpr.right
p : ℤ
⊢ ∀ (i : ℕ), ¬(up ℤ).Rel ((embeddingUpIntGE p).f i) ((embeddingUpIntGE p).f 0)

Tactic:
·

Goal state after:
case mpr.left
p : ℤ
⊢ (up ℤ).Rel ((up ℤ).prev ((embeddingUpIntGE p).f 0)) ((embeddingUpIntGE p).f 0)
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mpr.right
p : ℤ
⊢ ∀ (i : ℕ), ¬(up ℤ).Rel ((embeddingUpIntGE p).f i) ((embeddingUpIntGE p).f 0)

Tactic:
·

Goal state after:
case mpr.right
p : ℤ
⊢ ∀ (i : ℕ), ¬(up ℤ).Rel ((embeddingUpIntGE p).f i) ((embeddingUpIntGE p).f 0)
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mp
p : ℤ
n : ℕ
⊢ (embeddingUpIntLE p).BoundaryLE n → n = 0

pp: case mpr
p : ℤ
n : ℕ
⊢ n = 0 → (embeddingUpIntLE p).BoundaryLE n

Tactic:
·

Goal state after:
case mp
p : ℤ
n : ℕ
⊢ (embeddingUpIntLE p).BoundaryLE n → n = 0
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap 0 e).f i' = Hom.f 0 i'

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap 0 e).f i' = Hom.f 0 i'
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mp.zero
p : ℤ
h : (embeddingUpIntLE p).BoundaryLE 0
⊢ 0 = 0

pp: case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntLE p).BoundaryLE (n + 1)
⊢ n + 1 = 0

Tactic:
·

Goal state after:
case mp.zero
p : ℤ
h : (embeddingUpIntLE p).BoundaryLE 0
⊢ 0 = 0
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntLE p).BoundaryLE (n + 1)
⊢ n + 1 = 0

Tactic:
·

Goal state after:
case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntLE p).BoundaryLE (n + 1)
⊢ n + 1 = 0
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mpr
p : ℤ
n : ℕ
⊢ n = 0 → (embeddingUpIntLE p).BoundaryLE n

Tactic:
·

Goal state after:
case mpr
p : ℤ
n : ℕ
⊢ n = 0 → (embeddingUpIntLE p).BoundaryLE n
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

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
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ (K.extendXIso e hj').inv ≫ (K.extend e).d j' k' = 0

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
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : ¬c.Rel j k
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ (K.extendXIso e hj').inv ≫ (K.extend e).d j' k' = 0

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
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ (K.extendXIso e hj').inv ≫ (K.extend e).d j' k' = 0