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

Tactic:
]

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hij' : ¬c.Rel j j
hj' : c'.Rel (c'.prev (e.f j)) (e.f j)
hj : c'.Rel (c'.prev (e.f j)) (e.f j) → ∃ x, c'.Rel (e.f x) (e.f j)
i : ι
hij : i = j
hi : c.Rel i j
⊢ False
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
⊢ 0 = 0

pp: case inr.a
ι : 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
⊢ ¬c.Rel i j

Tactic:
]

Goal state after:
case inr.a
ι : 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
⊢ ¬c.Rel i 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 : ι
hk : c'.Rel (e.f j) (e.f k)
⊢ e.f k = e.f k

Tactic:
]

Goal state after:
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'
j : ι
hj : e.f j = j'
⊢ ((extend.XIso K ⋯).hom ≫ φ.f i ≫ (extend.XIso L ⋯).inv) ≫
      (L.extendXIso e hi).hom ≫ L.d i j ≫ (L.extendXIso e hj).inv =
    ((K.extendXIso e hi).hom ≫ K.d i j ≫ (K.extendXIso e hj).inv) ≫
      (extend.XIso K ⋯).hom ≫ φ.f j ≫ (extend.XIso L ⋯).inv

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'
j : ι
hj : e.f j = j'
⊢ ((extend.XIso K ⋯).hom ≫ φ.f i ≫ (extend.XIso L ⋯).inv) ≫
      (L.extendXIso e hi).hom ≫ L.d i j ≫ (L.extendXIso e hj).inv =
    ((K.extendXIso e hi).hom ≫ K.d i j ≫ (K.extendXIso e hj).inv) ≫
      (extend.XIso K ⋯).hom ≫ φ.f j ≫ (extend.XIso L ⋯).inv
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'
hj' : e.r j' = none
⊢ 0 = 0

Tactic:
]

Goal state after:
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'
hi' : e.r i' = none
⊢ 0 = 0

Tactic:
]

Goal state after:
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 : ι
hjk : c.next j = j
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
hj : c'.Rel (e.f j) (c'.next (e.f j)) → ∃ x, c'.Rel (e.f j) (e.f x)
k : ι
hk : c.Rel j k
⊢ False

Tactic:
]

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hjk : c.next j = j
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
hj : c'.Rel (e.f j) (c'.next (e.f j)) → ∃ x, c'.Rel (e.f j) (e.f x)
k : ι
hk : c.Rel j k
⊢ False
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 L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
i : ι
i' : ι'
h : e.f i = i'
⊢ (extend.XIso K ⋯).hom ≫ φ.f i ≫ (extend.XIso L ⋯).inv = (K.extendXIso e h).hom ≫ φ.f i ≫ (L.extendXIso e h).inv

Tactic:
]

Goal state after:
ι : 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
φ : K ⟶ L
e : c.Embedding c'
i : ι
i' : ι'
h : e.f i = i'
⊢ (extend.XIso K ⋯).hom ≫ φ.f i ≫ (extend.XIso L ⋯).inv = (K.extendXIso e h).hom ≫ φ.f i ≫ (L.extendXIso e h).inv
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 L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
i : ι
i' : ι'
h : e.f i = i'
⊢ extend.mapX φ (e.r i') = (K.extendXIso e h).hom ≫ φ.f i ≫ (L.extendXIso e h).inv

Tactic:
rw [extend.mapX_some φ (e.r_eq_some h)]

Goal state after:
ι : 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
φ : K ⟶ L
e : c.Embedding c'
i : ι
i' : ι'
h : e.f i = i'
⊢ (extend.XIso K ⋯).hom ≫ φ.f i ≫ (extend.XIso L ⋯).inv = (K.extendXIso e h).hom ≫ φ.f i ≫ (L.extendXIso e h).inv
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 L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ 0 = 0

Tactic:
]

Goal state after:
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 : ι
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
hj : c'.Rel (e.f j) (c'.next (e.f j)) → ∃ x, c'.Rel (e.f j) (e.f x)
k : ι
hjk : k = j
hk : c.Rel j k
⊢ False

Tactic:
]

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hjk' : ¬c.Rel j j
hj' : c'.Rel (e.f j) (c'.next (e.f j))
hj : c'.Rel (e.f j) (c'.next (e.f j)) → ∃ x, c'.Rel (e.f j) (e.f x)
k : ι
hjk : k = j
hk : c.Rel j k
⊢ False
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
k' : ι
hj : c.Rel j k'
hk' : e.f k' = 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
k' : ι
hj : c.Rel j k'
hk' : e.f k' = c'.next (e.f j)
⊢ c'.next (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.IsTruncGE
j k : ι
hjk : c.next j = k
k' : ι
hj : c.Rel j k'
hk' : e.f k' = c'.next (e.f j)
⊢ e.f k = e.f k

Tactic:
]

Goal state after:
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))
⊢ e.f j = e.f j

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.Rel j (c.next j)

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.Rel j (c.next j)
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))
hj' : c'.Rel (e.f j) (e.f (c.next j))
⊢ c'.Rel (e.f j) (c'.next (e.f j))

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))
hj' : c'.Rel (e.f j) (e.f (c.next j))
⊢ c'.Rel (e.f j) (c'.next (e.f j))
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

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✝¹ : 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
⊢ e.f k = e.f k

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
i' : ι'
i : ι
hi : e.f i = i'
hi' : ∃ k, e.f k = i'
⊢ i' = i'

Tactic:
]

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

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
⊢ ((K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv) ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

Tactic:
]

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
⊢ ((K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv) ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'
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
hk' : e.f k = k'
⊢ φ ≫ K.d j k ≫ (K.extendXIso e hk').inv = 0 ↔ φ ≫ K.d j k ≫ (K.extendXIso e hk').inv = 0

Tactic:
]

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

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
j : ι
hj : e.f j = j'
⊢ ((K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv) ≫
      (L.extendXIso e hi).hom ≫ L.d i j ≫ (L.extendXIso e hj).inv =
    K.d i' j' ≫ (K.restrictionXIso e hj).inv ≫ φ.f j ≫ (L.extendXIso e hj).inv

Tactic:
]

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
j : ι
hj : e.f j = j'
⊢ ((K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv) ≫
      (L.extendXIso e hi).hom ≫ L.d i j ≫ (L.extendXIso e hj).inv =
    K.d i' j' ≫ (K.restrictionXIso e hj).inv ≫ φ.f j ≫ (L.extendXIso e hj).inv
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

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
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
⊢ 0 = 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
⊢ ¬c.Rel j (c.next 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✝¹ : 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
⊢ ¬c.Rel j (c.next j)
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' : ι'
this : (K.extendOpIso e).inv.f i' ≫ (K.op.extend e.op).d i' j' = ((K.extend e).d j' i').op ≫ (K.extendOpIso e).inv.f j'
⊢ (K.op.extend e.op).d i' j' = (K.op.extend e.op).d i' j'

Tactic:
]

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

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
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
⊢ ¬c.Rel j k

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
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
⊢ ¬c.Rel j k
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

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✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : c.Rel i j
⊢ e.f i = e.f i

Tactic:
]

Goal state after:
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'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi'✝ : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : c.Rel i j
hi' : e.f i = i'
⊢ (K.extendXIso e hi').hom ≫ K.d i j ≫ φ = 0 ↔ (K.extendXIso e hi').hom ≫ K.d i j ≫ φ = 0

Tactic:
]

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

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
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : ¬c.Rel i j
⊢ 0 = 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'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : ¬c.Rel i j
⊢ ¬c.Rel (c.prev j) 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✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : ¬c.Rel i j
⊢ ¬c.Rel (c.prev j) j
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

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
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : ¬c.Rel i j
⊢ ¬c.Rel i 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✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : ¬c.Rel i j
⊢ ¬c.Rel i j
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ i, e.f i = i'
this : (L.extend e).d i' j' = 0
⊢ 0 = K.d i' j' ≫ f φ j'

Tactic:
]

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ i, e.f i = i'
this : (L.extend e).d i' j' = 0
⊢ 0 = K.d i' j' ≫ f φ j'
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

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✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
hi' : ¬∃ i, e.f i = i'
j : ι
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ 0 = K.d i' (e.f j) ≫ (K.restrictionXIso e ⋯).inv ≫ φ.f j ≫ (L.extendXIso e ⋯).inv

Tactic:
]

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
hi' : ¬∃ i, e.f i = i'
j : ι
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ 0 = K.d i' (e.f j) ≫ (K.restrictionXIso e ⋯).inv ≫ φ.f j ≫ (L.extendXIso e ⋯).inv
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' : ι'
hi' : ¬∃ i, e.f i = i'
j : ι
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
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
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
j : ι
hj : e.f j = j'
hij : j = i
⊢ i' = i'

Tactic:
]

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

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✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ (K.extendXIso e hj').inv = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : c.Rel i j
⊢ e.f i = e.f i

Tactic:
]

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

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
hi' : ¬∃ i, e.f i = i'
this✝ : (L.extend e).d i' j' = 0
hj' : ¬∃ j, e.f j = j'
this : f φ j' = 0
⊢ 0 = 0

Tactic:
]

Goal state after: