mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n : M
X Y : C
f : X ⟶ (shiftFunctor C n).obj Y
a a' : M
h : n + a = a'
⊢ ((F.shift a).map (L.map f) ≫ (F.shift a).map ((commShiftIso L n).hom.app Y)) ≫
      (F.shift a).map ((commShiftIso L n).inv.app Y) ≫
        (e' a).hom.app ((shiftFunctor C n).obj Y) ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y =
    (e' a).hom.app X ≫ ((G.shift a).map f ≫ (G.shiftIso n a a' h).hom.app Y) ≫ (e' a').inv.app Y

Tactic:
assoc,

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n : M
X Y : C
f : X ⟶ (shiftFunctor C n).obj Y
a a' : M
h : n + a = a'
⊢ (F.shift a).map (L.map f) ≫
      (F.shift a).map ((commShiftIso L n).hom.app Y) ≫
        (F.shift a).map ((commShiftIso L n).inv.app Y) ≫
          (e' a).hom.app ((shiftFunctor C n).obj Y) ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y =
    (e' a).hom.app X ≫ ((G.shift a).map f ≫ (G.shiftIso n a a' h).hom.app Y) ≫ (e' a').inv.app Y
Module: Mathlib.CategoryTheory.Localization.Triangulated

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
Z₂ : C
σ : γ.Y' ⟶ Z₂
hσ : W σ
fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'
T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h
hT₃ : T₃ ∈ distinguishedTriangles
hβγσ : W (β.s ≫ γ.s ≫ σ)
ψ₃ : T₂.obj₃ ⟶ T₃.obj₃
hψ₃ : W ψ₃
hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s ≫ γ.s ≫ σ) ≫ T₃.mor₂
hψ₂ : T₂.mor₃ ≫ (shiftFunctor C 1).map α.s = ψ₃ ≫ T₃.mor₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ α.s (β.s ≫ γ.s ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (L.mapTriangle.map ψ)
⊢ ((L.mapTriangle.map (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ α.f (γ.f ≫ σ) ⋯) ≫
          inv (L.mapTriangle.map ψ)) ≫
        L.mapTriangle.map ψ).hom₂ =
    b ≫ (L.mapTriangle.map ψ).hom₂

Tactic:
assoc,

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
Z₂ : C
σ : γ.Y' ⟶ Z₂
hσ : W σ
fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'
T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h
hT₃ : T₃ ∈ distinguishedTriangles
hβγσ : W (β.s ≫ γ.s ≫ σ)
ψ₃ : T₂.obj₃ ⟶ T₃.obj₃
hψ₃ : W ψ₃
hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s ≫ γ.s ≫ σ) ≫ T₃.mor₂
hψ₂ : T₂.mor₃ ≫ (shiftFunctor C 1).map α.s = ψ₃ ≫ T₃.mor₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ α.s (β.s ≫ γ.s ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (L.mapTriangle.map ψ)
⊢ (L.mapTriangle.map (completeDistinguishedTriangleMorphism T₁ T₃ hT₁ hT₃ α.f (γ.f ≫ σ) ⋯) ≫
        inv (L.mapTriangle.map ψ) ≫ L.mapTriangle.map ψ).hom₂ =
    b ≫ (L.mapTriangle.map ψ).hom₂
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: case mpr
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
⊢ QuasiIsoAt φ' i → QuasiIsoAt (φ ≫ φ') i

Tactic:
intro
    infer_instance

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

Goal state before:
pp: case mpr
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : QuasiIsoAt φ' i
⊢ QuasiIsoAt φ i → QuasiIsoAt (φ ≫ φ') i

Tactic:
intro
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Shift.SingleFunctors

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Category.{v_3, u_3} E
inst✝⁴ : Category.{v_4, u_4} E'
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : HasShift E' A
F G H : SingleFunctors C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
⊢ ((G.shiftIso n a a' ha').hom ≫ (iso a).inv) ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom

Tactic:
assoc,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Category.{v_3, u_3} E
inst✝⁴ : Category.{v_4, u_4} E'
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : HasShift E' A
F G H : SingleFunctors C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
⊢ (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom
Module: Mathlib.CategoryTheory.Shift.SingleFunctors

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Category.{v_3, u_3} E
inst✝⁴ : Category.{v_4, u_4} E'
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : HasShift E' A
F G H : SingleFunctors C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
⊢ (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    (whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom) ≫ (iso a).hom

Tactic:
assoc,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Category.{v_3, u_3} E
inst✝⁴ : Category.{v_4, u_4} E'
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : HasShift E' A
F G H : SingleFunctors C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
⊢ (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : ObjectProperty C
inst✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
Z : C
g : X ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X'
H : Triangle.mk s g h ∈ distinguishedTriangles
mem : P Z
hf₁ : s ≫ f₁ = s ≫ f₂
hf₂ : s ≫ (f₁ - f₂) = 0
q : (Triangle.mk s g h).obj₃ ⟶ Y
hq : f₁ - f₂ = (Triangle.mk s g h).mor₂ ≫ q
Y' : C
r : Y ⟶ Y'
t : Y' ⟶ (shiftFunctor C 1).obj (Triangle.mk s g h).obj₃
mem' : Triangle.mk q r t ∈ distinguishedTriangles
eq : q ≫ r = 0
⊢ ((Triangle.mk s g h).mor₂ ≫ q) ≫ r = 0

Tactic:
assoc,

Goal state after:
case refine_2
C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : ObjectProperty C
inst✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
Z : C
g : X ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X'
H : Triangle.mk s g h ∈ distinguishedTriangles
mem : P Z
hf₁ : s ≫ f₁ = s ≫ f₂
hf₂ : s ≫ (f₁ - f₂) = 0
q : (Triangle.mk s g h).obj₃ ⟶ Y
hq : f₁ - f₂ = (Triangle.mk s g h).mor₂ ≫ q
Y' : C
r : Y ⟶ Y'
t : Y' ⟶ (shiftFunctor C 1).obj (Triangle.mk s g h).obj₃
mem' : Triangle.mk q r t ∈ distinguishedTriangles
eq : q ≫ r = 0
⊢ (Triangle.mk s g h).mor₂ ≫ q ≫ r = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : DerivedCategory C
f : K ⟶ L
hf : ∀ (n : ℤ), IsIso ((homologyFunctor C n).map f)
⊢ IsIso f

Tactic:
refine ((MorphismProperty.isomorphisms (DerivedCategory C)).arrow_iso_iff
    (Qh.mapArrow.objObjPreimageIso (Arrow.mk f))).1 ?_

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : DerivedCategory C
f : K ⟶ L
hf : ∀ (n : ℤ), IsIso ((homologyFunctor C n).map f)
⊢ MorphismProperty.isomorphisms (DerivedCategory C) (Qh.mapArrow.obj (Qh.mapArrow.objPreimage (Arrow.mk f))).hom
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.XIso K hi).hom ≫ K.d i j ≫ (extend.XIso K hj).inv) ≫
      (extend.XIso K hj).hom ≫ K.d j k ≫ (extend.XIso K hk).inv =
    0

Tactic:
assoc,

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.XIso K hi).hom ≫
      (K.d i j ≫ (extend.XIso K hj).inv) ≫ (extend.XIso K hj).hom ≫ K.d j k ≫ (extend.XIso K hk).inv =
    0
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.XIso K hi).hom ≫
      (K.d i j ≫ (extend.XIso K hj).inv) ≫ (extend.XIso K hj).hom ≫ K.d j k ≫ (extend.XIso K hk).inv =
    0

Tactic:
assoc,

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.XIso K hi).hom ≫
      K.d i j ≫ (extend.XIso K hj).inv ≫ (extend.XIso K hj).hom ≫ K.d j k ≫ (extend.XIso K hk).inv =
    0
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:
rw [c.next_eq' hk] at hjk

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.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.d i j ≫ φ = 0 ↔ ((K.extendXIso e hi').hom ≫ K.d i j ≫ (K.extendXIso e hj').inv) ≫ (K.extendXIso e hj').hom ≫ φ = 0

Tactic:
assoc,

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'
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.d i j ≫ φ = 0 ↔ (K.extendXIso e hi').hom ≫ (K.d i j ≫ (K.extendXIso e hj').inv) ≫ (K.extendXIso e hj').hom ≫ φ = 0
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.d i j ≫ φ = 0 ↔ (K.extendXIso e hi').hom ≫ (K.d i j ≫ (K.extendXIso e hj').inv) ≫ (K.extendXIso e hj').hom ≫ φ = 0

Tactic:
assoc,

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'
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.d i j ≫ φ = 0 ↔ (K.extendXIso e hi').hom ≫ K.d i j ≫ (K.extendXIso e hj').inv ≫ (K.extendXIso e hj').hom ≫ φ = 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
inst✝ : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
j' k' : ι'
hj : ¬∃ j, e.f j = j'
⊢ (((single C c i).obj X).extend e).d j' k' = 0

Tactic:
exact IsZero.eq_of_src (isZero_extend_X _ _ _ (by tauto)) _ _

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 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
⊢ (Fork.ι cone ≫ (K.extendXIso e hj').inv) ≫ (K.extend e).d j' k' = 0

Tactic:
assoc,

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✝¹ : 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
⊢ Fork.ι cone ≫ (K.extendXIso e hj').inv ≫ (K.extend e).d j' k' = 0
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'
⊢ f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

Tactic:
· have : (L.extend e).d i' j' = 0 := by
        apply (L.isZero_extend_X e i' (by simpa using hi')).eq_of_src
      rw [this, comp_zero]
      by_cases hj' : ∃ j, e.f j = j'
      · obtain ⟨j, rfl⟩ := hj'
        rw [f_eq φ rfl]
        dsimp [restrictionXIso]
        rw [id_comp, reassoc_of% (hφ j (e.boundaryGE hij'
          (by simpa using hi')) i' hij'), zero_comp]
      · have : f φ j' = 0 := by
          apply (L.isZero_extend_X e j' (by simpa using hj')).eq_of_tgt
        rw [this, comp_zero]

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
hi'' : e.f i = i'
⊢ ((K.extendXIso e hi'').hom ≫ f') ≫ Fork.ι cone = f'' ≫ Fork.ι cone

Tactic:
assoc,

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✝¹ : 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
hi'' : e.f i = i'
⊢ (K.extendXIso e hi'').hom ≫ f' ≫ Fork.ι cone = f'' ≫ Fork.ι cone
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
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
hj : ¬∃ j, e.f j = j'
⊢ (mkHomToSingle ((((single C c i).obj X).extendXIso e h).hom ≫ (singleObjXSelf c i X).hom) ⋯ ≫
          mkHomFromSingle ((singleObjXSelf c i X).inv ≫ (((single C c i).obj X).extendXIso e h).inv) ⋯).f
      j' =
    (𝟙 (((single C c i).obj X).extend e)).f j'

Tactic:
exact IsZero.eq_of_src (isZero_extend_X _ _ _ (by tauto)) _ _

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
hi'' : e.f i = i'
⊢ ((K.extendXIso e hi'').hom ≫ K.d i j) ≫ (K.extendXIso e hj').inv = (f'' ≫ Fork.ι cone) ≫ (K.extendXIso e hj').inv

Tactic:
assoc,

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✝¹ : 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
hi'' : e.f i = i'
⊢ (K.extendXIso e hi'').hom ≫ K.d i j ≫ (K.extendXIso e hj').inv = (f'' ≫ Fork.ι cone) ≫ (K.extendXIso e hj').inv
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
hi'' : e.f i = i'
⊢ (K.extendXIso e hi'').hom ≫ K.d i j ≫ (K.extendXIso e hj').inv = (f'' ≫ Fork.ι cone) ≫ (K.extendXIso e hj').inv

Tactic:
assoc,

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✝¹ : 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
hi'' : e.f i = i'
⊢ (K.extendXIso e hi'').hom ≫ K.d i j ≫ (K.extendXIso e hj').inv = f'' ≫ Fork.ι cone ≫ (K.extendXIso e hj').inv