mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : P.IsTriangulated
T₁ T₂ : Triangle P.FullSubcategory
hT₁ : T₁ ∈ P.ι.mapTriangle.obj ⁻¹' distinguishedTriangles
hT₂ : T₂ ∈ P.ι.mapTriangle.obj ⁻¹' distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : (P.ι.mapTriangle.obj T₁).obj₃ ⟶ (P.ι.mapTriangle.obj T₂).obj₃
hc₁ : (P.ι.mapTriangle.obj T₁).mor₂ ≫ c = P.ι.map b ≫ (P.ι.mapTriangle.obj T₂).mor₂
hc₂ : (P.ι.mapTriangle.obj T₁).mor₃ ≫ (shiftFunctor C 1).map (P.ι.map a) = c ≫ (P.ι.mapTriangle.obj T₂).mor₃
⊢ T₁.mor₃ ≫ (shiftFunctor P.FullSubcategory 1).map a = P.fullyFaithfulι.preimage c ≫ T₂.mor₃

Tactic:
ext

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
inst✝ : P.IsTriangulated
T₁ T₂ : Triangle P.FullSubcategory
hT₁ : T₁ ∈ P.ι.mapTriangle.obj ⁻¹' distinguishedTriangles
hT₂ : T₂ ∈ P.ι.mapTriangle.obj ⁻¹' distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
comm : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
c : (P.ι.mapTriangle.obj T₁).obj₃ ⟶ (P.ι.mapTriangle.obj T₂).obj₃
hc₁ : (P.ι.mapTriangle.obj T₁).mor₂ ≫ c = P.ι.map b ≫ (P.ι.mapTriangle.obj T₂).mor₂
hc₂ : (P.ι.mapTriangle.obj T₁).mor₃ ≫ (shiftFunctor C 1).map (P.ι.map a) = c ≫ (P.ι.mapTriangle.obj T₂).mor₃
⊢ (T₁.mor₃ ≫ (shiftFunctor P.FullSubcategory 1).map a).hom = (P.fullyFaithfulι.preimage c ≫ T₂.mor₃).hom
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
⊢ IsIso f ↔ ∀ (n : ℤ), IsIso ((homologyFunctor C n).map f)

Tactic:
by
  refine ⟨fun hf n ↦ inferInstance, fun hf ↦ ?_⟩
  refine ((MorphismProperty.isomorphisms (DerivedCategory C)).arrow_iso_iff
    (Qh.mapArrow.objObjPreimageIso (Arrow.mk f))).1 ?_
  let g := Qh.mapArrow.objPreimage (Arrow.mk f)
  change IsIso (Qh.map g.hom)
  rw [isIso_Qh_map_iff, HomotopyCategory.mem_quasiIso_iff]
  intro n
  have e : Arrow.mk ((homologyFunctor C n).map f) ≅
      Arrow.mk ((HomotopyCategory.homologyFunctor _ _ n).map g.hom) :=
    ((homologyFunctor C n).mapArrow.mapIso
      ((Qh.mapArrow.objObjPreimageIso (Arrow.mk f)).symm)) ≪≫
      ((Functor.mapArrowFunctor _ _).mapIso (homologyFunctorFactorsh C n)).app (Arrow.mk g.hom)
  exact ((MorphismProperty.isomorphisms C).arrow_iso_iff e).1 (hf n)

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i₁ i₂ : ι
⊢ c'.Rel (e.f i₁) (e.f i₂) ↔ c.Rel i₁ i₂

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i₁ i₂ : ι
⊢ c'.Rel (e.f i₁) (e.f i₂) → c.Rel i₁ i₂

case mpr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i₁ i₂ : ι
⊢ c.Rel i₁ i₂ → c'.Rel (e.f i₁) (e.f i₂)
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i₁ i₂ : ι
⊢ c'.Rel (e.f i₁) (e.f i₂) ↔ c.Rel i₁ i₂

Tactic:
by
  constructor
  · apply IsRelIff.rel'
  · exact e.rel

Goal state after:
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 : ℤ
⊢ (DerivedCategory.homologyFunctor C n).map 0 ≫ (DerivedCategory.homologyFunctorFactors C n).hom.app T.obj₃ =
    (DerivedCategory.homologyFunctorFactors C n).hom.app T.obj₁ ≫ 0

Tactic:
Functor.map_zero,

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 : ℤ
⊢ 0 ≫ (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: p n : ℤ
⊢ (∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n) ↔ p < n

Tactic:
constructor

Goal state after:
case mp
p n : ℤ
⊢ (∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n) → p < n

case mpr
p n : ℤ
⊢ p < n → ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: p n : ℤ
⊢ (∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n) ↔ n < p

Tactic:
constructor

Goal state after:
case mp
p n : ℤ
⊢ (∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n) → n < p

case mpr
p n : ℤ
⊢ n < p → ∀ (i : ℕ), (embeddingUpIntGE p).f 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
inst✝¹ : Category.{v_1, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
⊢ IsZero K ↔ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e

Tactic:
constructor

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

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

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

Tactic:
constructor

Goal state after:
case mp.left
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{v_1, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
hK : IsZero K
⊢ K.IsStrictlySupported e

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

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

Tactic:
constructor

Goal state after:
case mp.left
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{v_1, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
hK : IsZero K
⊢ ∀ (i' : ι'), (∀ (i : ι), e.f i ≠ i') → IsZero (K.X i')
Module: Mathlib.Algebra.Homology.Embedding.IsSupported

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

Tactic:
constructor

Goal state after:
case mp.right
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{v_1, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
hK : IsZero K
⊢ ∀ (i : ι), IsZero (K.X (e.f i))
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.op f.op ⋯ =
    (imageSubobjectIso g.op ≪≫ (imageOpOp g).symm).hom ≫
      (cokernel.desc f (factorThruImage g) ⋯).op ≫ (kernelSubobjectIso f.op ≪≫ kernelOpOp f).inv

Tactic:
ext

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.op f.op ⋯ ≫ (kernelSubobject f.op).arrow =
    ((imageSubobjectIso g.op ≪≫ (imageOpOp g).symm).hom ≫
        (cokernel.desc f (factorThruImage g) ⋯).op ≫ (kernelSubobjectIso f.op ≪≫ kernelOpOp f).inv) ≫
      (kernelSubobject f.op).arrow
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.unop f.unop ⋯ =
    (imageSubobjectIso g.unop ≪≫ (imageUnopUnop g).symm).hom ≫
      (cokernel.desc f (factorThruImage g) ⋯).unop ≫ (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f).inv

Tactic:
ext

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.unop f.unop ⋯ ≫ (kernelSubobject f.unop).arrow =
    ((imageSubobjectIso g.unop ≪≫ (imageUnopUnop g).symm).hom ≫
        (cokernel.desc f (factorThruImage g) ⋯).unop ≫ (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f).inv) ≫
      (kernelSubobject f.unop).arrow
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
X : (HomologicalComplex V c)ᵒᵖ
⊢ (opFunctor V c).map ((opUnitIso V c).hom.app X) ≫ (opCounitIso V c).hom.app ((opFunctor V c).obj X) =
    𝟙 ((opFunctor V c).obj X)

Tactic:
ext

Goal state after:
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : (HomologicalComplex V c)ᵒᵖ
i✝ : ι
⊢ ((opFunctor V c).map ((opUnitIso V c).hom.app X) ≫ (opCounitIso V c).hom.app ((opFunctor V c).obj X)).f i✝ =
    (𝟙 ((opFunctor V c).obj X)).f 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
X : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
⊢ (unopFunctor V c).map ((unopUnitIso V c).hom.app X) ≫ (unopCounitIso V c).hom.app ((unopFunctor V c).obj X) =
    𝟙 ((unopFunctor V c).obj X)

Tactic:
ext

Goal state after:
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
i✝ : ι
⊢ ((unopFunctor V c).map ((unopUnitIso V c).hom.app X) ≫ (unopCounitIso V c).hom.app ((unopFunctor V c).obj X)).f i✝ =
    (𝟙 ((unopFunctor V c).obj X)).f i✝
Module: Mathlib.Algebra.Homology.Embedding.Boundary

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

Tactic:
constructor

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

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

Goal state before:
pp: ι : 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'
⊢ e.BoundaryLE j

Tactic:
constructor

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))

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.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'
⊢ extendMap (𝟙 K) e = 𝟙 (K.extend e)

Tactic:
ext

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 : HomologicalComplex C c
e : c.Embedding c'
i✝ : ι'
⊢ (extendMap (𝟙 K) e).f i✝ = (𝟙 (K.extend e)).f i✝
Module: Mathlib.Algebra.Homology.Embedding.Boundary

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

Tactic:
constructor

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

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

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

Tactic:
constructor

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

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: p : ℤ
n : ℕ
⊢ (embeddingUpIntLE p).BoundaryLE n ↔ n = 0

Tactic:
constructor

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

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

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

Tactic:
constructor

Goal state after:
case mpr.left
p : ℤ
⊢ (up ℤ).Rel ((embeddingUpIntLE p).f 0) ((up ℤ).next ((embeddingUpIntLE p).f 0))

case mpr.right
p : ℤ
⊢ ∀ (k : ℕ), ¬(up ℤ).Rel ((embeddingUpIntLE p).f 0) ((embeddingUpIntLE p).f k)
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 = 0 ↔ φ ≫ (K.extendXIso e hj').inv ≫ (K.extend e).d j' k' = 0

Tactic:
rw [K.extend_d_eq e hj' hk', Iso.inv_hom_id_assoc,
      ← cancel_mono (K.extendXIso e hk').inv, zero_comp, assoc]

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

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
⊢ ((if hij : c.Rel i j then
        if hi : e.BoundaryGE i then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (XIso K e ⋯).inv
        else (XIso K e hi).hom ≫ K.d (e.f i) (e.f j) ≫ (XIso K e ⋯).inv
      else 0) ≫
      if hij : c.Rel j k then
        if hi : e.BoundaryGE j then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f j) (e.f k) ≫ (XIso K e ⋯).inv
        else (XIso K e hi).hom ≫ K.d (e.f j) (e.f k) ≫ (XIso K e ⋯).inv
      else 0) =
    0

Tactic:
by_cases hjk : c.Rel j k
    · rw [dif_pos hij, dif_pos hjk, dif_neg (e.not_boundaryGE_next hij)]
      split_ifs <;> simp
    · rw [dif_neg hjk, comp_zero]

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

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ K.d i' j' ≫ (K.restrictionXIso e hj').inv ≫ (K.restriction e).pOpcycles j = 0

Tactic:
rw [← cancel_epi (K.restrictionXIso e hi').hom, ← restriction_d_eq_assoc,
        comp_zero, d_pOpcycles]

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

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
⊢ IsIso ((K.restrictionToTruncGE' e).f i)

Tactic:
K.restrictionToTruncGE'_f_eq_iso_hom_iso_inv e rfl hi

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryGE i
⊢ IsIso ((K.restrictionXIso e ⋯).hom ≫ (K.truncGE'XIso e ⋯ hi).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'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ K.pOpcycles j = (K.extendXIso e hj').inv ≫ (K.extend e).pOpcycles j' ≫ (K.extendOpcyclesIso e hj').hom

Tactic:
dsimp [extendOpcyclesIso, pOpcycles]

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'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.sc j).pOpcycles =
    (K.extendXIso e hj').inv ≫
      ((K.extend e).sc j').pOpcycles ≫
        (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).right.opcyclesIso.hom ≫
          (K.sc j).homologyData.right.opcyclesIso.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 L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
inst✝¹ : ∀ (j : ι), K.HasHomology j
inst✝ : ∀ (j : ι), L.HasHomology j
⊢ (∀ (i : ι'), QuasiIsoAt (extendMap φ e) i) ↔ ∀ (i : ι), QuasiIsoAt (extendMap φ e) (e.f i)

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
inst✝¹ : ∀ (j : ι), K.HasHomology j
inst✝ : ∀ (j : ι), L.HasHomology j
⊢ (∀ (i : ι'), QuasiIsoAt (extendMap φ e) i) → ∀ (i : ι), QuasiIsoAt (extendMap φ e) (e.f i)

case mpr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
inst✝¹ : ∀ (j : ι), K.HasHomology j
inst✝ : ∀ (j : ι), L.HasHomology j
⊢ (∀ (i : ι), QuasiIsoAt (extendMap φ e) (e.f i)) → ∀ (i : ι'), QuasiIsoAt (extendMap φ e) i
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁶ : Category.{v_1, u_3} C
inst✝⁵ : HasZeroMorphisms C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁴ : e.IsTruncGE
inst✝³ : ∀ (i' : ι'), K.HasHomology i'
inst✝² : ∀ (i' : ι'), L.HasHomology i'
inst✝¹ : ∀ (i' : ι'), M.HasHomology i'
inst✝ : K.IsStrictlySupported e
i : ι
hi : ¬e.BoundaryGE i
⊢ IsIso ((K.restrictionToTruncGE' e).f i)

Tactic:
K.restrictionToTruncGE'_f_eq_iso_hom_iso_inv e rfl hi

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁶ : Category.{v_1, u_3} C
inst✝⁵ : HasZeroMorphisms C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁴ : e.IsTruncGE
inst✝³ : ∀ (i' : ι'), K.HasHomology i'
inst✝² : ∀ (i' : ι'), L.HasHomology i'
inst✝¹ : ∀ (i' : ι'), M.HasHomology i'
inst✝ : K.IsStrictlySupported e
i : ι
hi : ¬e.BoundaryGE i
⊢ IsIso ((K.restrictionXIso e ⋯).hom ≫ (K.truncGE'XIso e ⋯ hi).inv)
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
⊢ QuasiIso (K.πTruncGE e) ↔ K.IsSupported e

Tactic:
constructor

Goal state after:
case mp
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
⊢ QuasiIso (K.πTruncGE e) → K.IsSupported e

case mpr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
⊢ K.IsSupported e → QuasiIso (K.πTruncGE e)
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
⊢ Function.Bijective (fromSum e₁ e₂)

Tactic:
constructor

Goal state after:
case left
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
⊢ Function.Injective (fromSum e₁ e₂)

case right
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
⊢ Function.Surjective (fromSum e₁ e₂)