mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K).τ₃ =
    ((shortComplexFunctor C (up ℤ) a).map
          ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K) ≫
        (shiftShortComplexFunctorIso C n a a' ha').hom.app
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ≫
          (shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K).τ₃

Tactic:
dsimp

Goal state after:
case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ mn.negOnePow • (XIsoOfEq K ⋯).hom =
    ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K).f ((up ℤ).next a) ≫
      (n.negOnePow • (XIsoOfEq ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ⋯).hom) ≫
        (m.negOnePow • (XIsoOfEq K ⋯).hom)
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
i : ι
⊢ IsIso ((Q ⋙ homologyFunctor C c i).map f)

Tactic:
dsimp

Goal state after:
case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
i : ι
⊢ IsIso ((homologyFunctor C c i).map (Q.map f))
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: 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
X' X Y : C
e : X' ⟶ X
he : IsIso e
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
mem' : P Z
⊢ (Triangle.mk (e ≫ f) g (h ≫ (shiftFunctor C 1).map (inv e))).mor₃ ≫ (shiftFunctor C 1).map (asIso e).hom =
    (Iso.refl (Triangle.mk (e ≫ f) g (h ≫ (shiftFunctor C 1).map (inv e))).obj₃).hom ≫ (Triangle.mk f g h).mor₃

Tactic:
dsimp

Goal state after:
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
X' X Y : C
e : X' ⟶ X
he : IsIso e
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f g h ∈ distinguishedTriangles
mem' : P Z
⊢ (h ≫ (shiftFunctor C 1).map (inv e)) ≫ (shiftFunctor C 1).map e = 𝟙 Z ≫ h
Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
a : ℤ
x✝ : C
⊢ ((NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯).hom.app x✝).f a =
    (((single C (ComplexShape.up ℤ) a).isoWhiskerLeft (shiftFunctorZero (CochainComplex C ℤ) ℤ)).hom.app x✝).f a

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
a : ℤ
x✝ : C
⊢ eqToHom ⋯ = ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app ((single C (ComplexShape.up ℤ) a).obj x✝)).f a
Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x✝ : C
⊢ ((NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯).hom.app x✝).f a =
    (((single C (ComplexShape.up ℤ) a'').isoWhiskerLeft (shiftFunctorAdd (CochainComplex C ℤ) m n) ≪≫
                ((single C (ComplexShape.up ℤ) a'').associator (CategoryTheory.shiftFunctor (CochainComplex C ℤ) m)
                      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n)).symm ≪≫
                  Functor.isoWhiskerRight (NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯)
                      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n) ≪≫
                    NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯).hom.app
          x✝).f
      a

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x✝ : C
⊢ eqToHom ⋯ =
    ((shiftFunctorAdd (CochainComplex C ℤ) m n).hom.app ((single C (ComplexShape.up ℤ) a'').obj x✝)).f a ≫
      𝟙 (((single C (ComplexShape.up ℤ) a'').obj x✝).X (a + n + m)) ≫ eqToHom ⋯ ≫ eqToHom ⋯
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
G : D ⥤ E
inst✝ : G.CommShift A
a : A
X : C
⊢ ((F.functor a).associator G (shiftFunctor E 0) ≪≫
            (F.functor a).isoWhiskerLeft (commShiftIso G 0).symm ≪≫
              ((F.functor a).associator (shiftFunctor D 0) G).symm ≪≫ isoWhiskerRight (F.shiftIso 0 a a ⋯) G).hom.app
      X =
    ((F.functor a ⋙ G).isoWhiskerLeft (shiftFunctorZero E A)).hom.app X

Tactic:
dsimp

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
G : D ⥤ E
inst✝ : G.CommShift A
a : A
X : C
⊢ 𝟙 ((shiftFunctor E 0).obj (G.obj ((F.functor a).obj X))) ≫
      (commShiftIso G 0).inv.app ((F.functor a).obj X) ≫
        𝟙 (G.obj ((shiftFunctor D 0).obj ((F.functor a).obj X))) ≫ G.map ((F.shiftIso 0 a a ⋯).hom.app X) =
    (shiftFunctorZero E A).hom.app (G.obj ((F.functor a).obj X))
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
G : D ⥤ E
inst✝ : G.CommShift A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ ((F.functor a'').associator G (shiftFunctor E (m + n)) ≪≫
            (F.functor a'').isoWhiskerLeft (commShiftIso G (m + n)).symm ≪≫
              ((F.functor a'').associator (shiftFunctor D (m + n)) G).symm ≪≫
                isoWhiskerRight (F.shiftIso (m + n) a a'' ⋯) G).hom.app
      X =
    ((F.functor a'' ⋙ G).isoWhiskerLeft (shiftFunctorAdd E m n) ≪≫
            ((F.functor a'' ⋙ G).associator (shiftFunctor E m) (shiftFunctor E n)).symm ≪≫
              isoWhiskerRight
                  ((F.functor a'').associator G (shiftFunctor E m) ≪≫
                    (F.functor a'').isoWhiskerLeft (commShiftIso G m).symm ≪≫
                      ((F.functor a'').associator (shiftFunctor D m) G).symm ≪≫
                        isoWhiskerRight (F.shiftIso m a' a'' ha'') G)
                  (shiftFunctor E n) ≪≫
                (F.functor a').associator G (shiftFunctor E n) ≪≫
                  (F.functor a').isoWhiskerLeft (commShiftIso G n).symm ≪≫
                    ((F.functor a').associator (shiftFunctor D n) G).symm ≪≫
                      isoWhiskerRight (F.shiftIso n a a' ha') G).hom.app
      X

Tactic:
dsimp

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
G : D ⥤ E
inst✝ : G.CommShift A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ 𝟙 ((shiftFunctor E (m + n)).obj (G.obj ((F.functor a'').obj X))) ≫
      (commShiftIso G (m + n)).inv.app ((F.functor a'').obj X) ≫
        𝟙 (G.obj ((shiftFunctor D (m + n)).obj ((F.functor a'').obj X))) ≫
          G.map ((F.shiftIso (m + n) a a'' ⋯).hom.app X) =
    (shiftFunctorAdd E m n).hom.app (G.obj ((F.functor a'').obj X)) ≫
      𝟙 ((shiftFunctor E n).obj ((shiftFunctor E m).obj (G.obj ((F.functor a'').obj X)))) ≫
        (shiftFunctor E n).map
            (𝟙 ((shiftFunctor E m).obj (G.obj ((F.functor a'').obj X))) ≫
              (commShiftIso G m).inv.app ((F.functor a'').obj X) ≫
                𝟙 (G.obj ((shiftFunctor D m).obj ((F.functor a'').obj X))) ≫
                  G.map ((F.shiftIso m a' a'' ha'').hom.app X)) ≫
          𝟙 ((shiftFunctor E n).obj (G.obj ((F.functor a').obj X))) ≫
            (commShiftIso G n).inv.app ((F.functor a').obj X) ≫
              𝟙 (G.obj ((shiftFunctor D n).obj ((F.functor a').obj X))) ≫ G.map ((F.shiftIso n a a' ha').hom.app X)
Module: Mathlib.Algebra.Homology.DerivedCategory.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ Q.mapTriangle.obj (mappingCone.triangle φ) ∈ distinguishedTriangles

Tactic:
rw [mem_distTriang_iff]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ ∃ X Y f, Nonempty (Q.mapTriangle.obj (mappingCone.triangle φ) ≅ Q.mapTriangle.obj (mappingCone.triangle f))
Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : HomotopyCategory C (ComplexShape.up ℤ)
f : X ⟶ Y
hf : IsIso (Qh.map f)
n : ℤ
⊢ IsIso ((Qh ⋙ homologyFunctor C n).map f)

Tactic:
dsimp

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : HomotopyCategory C (ComplexShape.up ℤ)
f : X ⟶ Y
hf : IsIso (Qh.map f)
n : ℤ
⊢ IsIso ((homologyFunctor C n).map (Qh.map f))
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasBinaryBiproducts C
⊢ (triangle φ).rotate.mor₃ ≫
      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (Iso.refl (triangle φ).rotate.obj₁).hom =
    ((shiftFunctorCompIsoId (CochainComplex C ℤ) (-1) 1 triangle._proof_2).app (mappingCone φ)).hom ≫
      (mappingCone.triangle φ).mor₃

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasBinaryBiproducts C
⊢ (-(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (fst φ)) ≫
      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (𝟙 K) =
    (shiftFunctorCompIsoId (CochainComplex C ℤ) (-1) 1 triangle._proof_2).hom.app (mappingCone φ) ≫
      (mappingCone.triangle φ).mor₃
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst✝² : AddCommSemigroup A
inst✝¹ : IsRightCancelAdd A
inst✝ : One A
a b : A
⊢ ∀ (i₁ i₂ : A), (up' a).Rel i₁ i₂ ↔ (up' a).Rel (i₁ + b) (i₂ + b)

Tactic:
dsimp

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst✝² : AddCommSemigroup A
inst✝¹ : IsRightCancelAdd A
inst✝ : One A
a b : A
⊢ ∀ (i₁ i₂ : A), i₁ + a = i₂ ↔ i₁ + b + a = i₂ + b
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst✝² : AddCommSemigroup A
inst✝¹ : IsRightCancelAdd A
inst✝ : One A
a b : A
⊢ ∀ (i₁ i₂ : A), (down' a).Rel i₁ i₂ ↔ (down' a).Rel (i₁ + b) (i₂ + b)

Tactic:
dsimp

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst✝² : AddCommSemigroup A
inst✝¹ : IsRightCancelAdd A
inst✝ : One A
a b : A
⊢ ∀ (i₁ i₂ : A), i₂ + a = i₁ ↔ i₂ + b + a = i₁ + b
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
⊢ ∀ (i₁ i₂ : ℕ), (up ℕ).Rel i₁ i₂ ↔ (up ℤ).Rel ↑i₁ ↑i₂

Tactic:
dsimp

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
⊢ ∀ (i₁ i₂ : ℕ), i₁ + 1 = i₂ ↔ ↑i₁ + 1 = ↑i₂
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
⊢ ∀ (i₁ i₂ : ℕ), (down ℕ).Rel i₁ i₂ ↔ (up ℤ).Rel (-↑i₁) (-↑i₂)

Tactic:
dsimp

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
⊢ ∀ (i₁ i₂ : ℕ), i₂ + 1 = i₁ ↔ -↑i₁ + 1 = -↑i₂
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
⊢ ∀ (i₁ i₂ : ℕ), (up ℕ).Rel i₁ i₂ ↔ (up ℤ).Rel (p + ↑i₁) (p + ↑i₂)

Tactic:
dsimp

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
⊢ ∀ (i₁ i₂ : ℕ), i₁ + 1 = i₂ ↔ p + ↑i₁ + 1 = p + ↑i₂
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
⊢ ∀ (i₁ i₂ : ℕ), (down ℕ).Rel i₁ i₂ ↔ (up ℤ).Rel (p - ↑i₁) (p - ↑i₂)

Tactic:
dsimp

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
⊢ ∀ (i₁ i₂ : ℕ), i₂ + 1 = i₁ ↔ p - ↑i₁ + 1 = p - ↑i₂
Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (CochainComplex C ℤ)
hT : DerivedCategory.Q.mapTriangle.obj T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ DerivedCategory.HomologySequence.δ (DerivedCategory.Q.mapTriangle.obj T) n₀ n₁ ⋯ ≫
      (DerivedCategory.homologyFunctor C n₁).map (DerivedCategory.Q.map T.mor₁) ≫
        (DerivedCategory.homologyFunctorFactors C n₁).hom.app T.obj₂ =
    (DerivedCategory.homologyFunctorFactors C n₀).hom.app T.obj₃ ≫ 0

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (CochainComplex C ℤ)
hT : DerivedCategory.Q.mapTriangle.obj T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ DerivedCategory.HomologySequence.δ
        (Triangle.mk (DerivedCategory.Q.map T.mor₁) (DerivedCategory.Q.map T.mor₂)
          (DerivedCategory.Q.map T.mor₃ ≫ (Functor.commShiftIso DerivedCategory.Q 1).hom.app T.obj₁))
        n₀ n₁ ⋯ ≫
      (DerivedCategory.homologyFunctor C n₁).map (DerivedCategory.Q.map T.mor₁) ≫
        (DerivedCategory.homologyFunctorFactors C n₁).hom.app T.obj₂ =
    (DerivedCategory.homologyFunctorFactors C n₀).hom.app T.obj₃ ≫ 0
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: case mpr
p n : ℤ
a✝ : p < n
i✝ : ℕ
⊢ (embeddingUpIntLE p).f i✝ ≠ n

Tactic:
dsimp

Goal state after:
case mpr
p n : ℤ
a✝ : p < n
i✝ : ℕ
⊢ ¬p - ↑i✝ = n
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: case mpr
p n : ℤ
a✝ : n < p
i✝ : ℕ
⊢ (embeddingUpIntGE p).f i✝ ≠ n

Tactic:
dsimp

Goal state after:
case mpr
p n : ℤ
a✝ : n < p
i✝ : ℕ
⊢ ¬p + ↑i✝ = 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✝ : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ 𝟙 (((F.mapHomologicalComplex c').obj K).X i') = 0

Tactic:
dsimp

Goal state after:
ι : 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✝ : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ 𝟙 (F.obj (K.X i')) = 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 : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
⊢ ((opFunctor V c).obj (op K)).HasHomology i

Tactic:
dsimp

Goal state after:
ι : 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
⊢ K.op.HasHomology i
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 : HomologicalComplex Vᵒᵖ c
i : ι
inst✝ : K.HasHomology i
⊢ ((unopFunctor V c).obj (op K)).HasHomology i

Tactic:
dsimp

Goal state after:
ι : 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
⊢ K.unop.HasHomology i
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst✝ : Preadditive V
F G : HomologicalComplex V c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
⊢ (((opFunctor V c).map φ₁.op).f n).unop =
    ((((dNext n) fun i j ↦ (h.hom j i).op) + (prevD n) fun i j ↦ (h.hom j i).op) + ((opFunctor V c).map φ₂.op).f n).unop

Tactic:
dsimp

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst✝ : Preadditive V
F G : HomologicalComplex V c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
⊢ φ₁.f n = ((((dNext n) fun i j ↦ (h.hom j i).op) + (prevD n) fun i j ↦ (h.hom j i).op) + (φ₂.f n).op).unop
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst✝ : Preadditive V
F G : HomologicalComplex Vᵒᵖ c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
⊢ (((unopFunctor V c).map φ₁.op).f n).op =
    ((((dNext n) fun i j ↦ (h.hom j i).unop) + (prevD n) fun i j ↦ (h.hom j i).unop) +
        ((unopFunctor V c).map φ₂.op).f n).op

Tactic:
dsimp

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst✝ : Preadditive V
F G : HomologicalComplex Vᵒᵖ c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
⊢ φ₁.f n = ((((dNext n) fun i j ↦ (h.hom j i).unop) + (prevD n) fun i j ↦ (h.hom j i).unop) + (φ₂.f n).unop).op
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hi : c.Rel i j
⊢ ¬e.BoundaryLE i

Tactic:
dsimp [BoundaryLE]
  simp only [not_and, not_forall, not_not]
  intro
  exact ⟨j, by simpa only [e.rel_iff] using hi⟩

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'
⊢ 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) ⋯ =
    𝟙 (((single C c i).obj X).extend e)

Tactic:
ext j'

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
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
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'
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'
h : (K.sc' i j k).LeftHomologyData
⊢ (h.i ≫ (K.extendXIso e hj').inv) ≫ ((K.extend e).sc' i' j' k').g = 0

Tactic:
dsimp

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'
h : (K.sc' i j k).LeftHomologyData
⊢ (h.i ≫ (K.extendXIso e hj').inv) ≫ (K.extend e).d j' k' = 0
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'
h : (K.sc' i j k).LeftHomologyData
⊢ (isLimitKernelFork K e hj' hk hk' (KernelFork.ofι h.i ⋯) h.hi).lift (KernelFork.ofι ((K.extend e).sc' i' j' k').f ⋯) ≫
      h.π =
    0

Tactic:
dsimp

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'
h : (K.sc' i j k).LeftHomologyData
⊢ (isLimitKernelFork K e hj' hk hk' (KernelFork.ofι h.i ⋯) h.hi).lift (KernelFork.ofι ((K.extend e).d i' j') ⋯) ≫ h.π =
    0
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'
h : (K.sc' i j k).RightHomologyData
⊢ ((K.extend e).sc' i' j' k').f ≫ (K.extendXIso e hj').hom ≫ h.p = 0

Tactic:
dsimp

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'
h : (K.sc' i j k).RightHomologyData
⊢ (K.extend e).d i' j' ≫ (K.extendXIso e hj').hom ≫ h.p = 0