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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
i₁ i₁' : I₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
hj' : c₁.π c₂ c (i₁, i₂') = j
⊢ c₁.π c₂ c (i₁', i₂') = c.next j

Tactic:
by rw [← c.next_eq' (ComplexShape.rel_π₂ c₁ c i₁' hi₂), hj]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a : A
⊢ t.z a 0 = 1

Tactic:
simpa using t.assoc a 0 0

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_5
C₄ : Type u_6
inst✝¹⁹ : Category.{v_1, u_1} C₁
inst✝¹⁸ : Category.{v_2, u_2} C₂
inst✝¹⁷ : Category.{v_3, u_5} C₃
inst✝¹⁶ : Category.{v_4, u_6} C₄
inst✝¹⁵ : Category.{v_5, u_3} C₁₂
inst✝¹⁴ : HasZeroMorphisms C₁
inst✝¹³ : HasZeroMorphisms C₂
inst✝¹² : HasZeroMorphisms C₃
inst✝¹¹ : Preadditive C₁₂
inst✝¹⁰ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝⁹ : F₁₂.PreservesZeroMorphisms
inst✝⁸ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁷ : G.Additive
inst✝⁶ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁵ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c₄
inst✝² : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝¹ : DecidableEq ι₁₂
inst✝ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
i₁₂ : ι₁₂
j : ι₄
h₁₂ : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h : c₁₂.π c₃ c₄ (i₁₂, i₃) = j
⊢ ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j ⋯ =
    (G.map (K₁.ιMapBifunctor K₂ F₁₂ c₁₂ i₁ i₂ i₁₂ h₁₂)).app (K₃.X i₃) ≫
      (K₁.mapBifunctor K₂ F₁₂ c₁₂).ιMapBifunctor K₃ G c₄ i₁₂ i₃ j h

Tactic:
subst h₁₂
  rfl

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
this✝² : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this✝¹ : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this✝ : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
H : Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁ f₂' F c) :=
  (Homotopy.ofEq ⋯).trans
    ((((mapBifunctorMapHomotopy₁ h₂ f₁ F.flip c).compRight (L₁.mapBifunctorFlipIso L₂ F c).hom).compLeft
          (K₁.mapBifunctorFlipIso K₂ F c).inv).trans
      (Homotopy.ofEq ⋯))
⊢ hom₂ f₁ h₂ F c = H.hom

Tactic:
ext j j' i₁ i₂ hj

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
this✝² : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this✝¹ : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this✝ : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
H : Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁ f₂' F c) :=
  (Homotopy.ofEq ⋯).trans
    ((((mapBifunctorMapHomotopy₁ h₂ f₁ F.flip c).compRight (L₁.mapBifunctorFlipIso L₂ F c).hom).compLeft
          (K₁.mapBifunctorFlipIso K₂ F c).inv).trans
      (Homotopy.ofEq ⋯))
j j' : J
i₁ : I₁
i₂ : I₂
hj : c₁.π c₂ c (i₁, i₂) = j
⊢ K₁.ιMapBifunctor K₂ F c i₁ i₂ j hj ≫ hom₂ f₁ h₂ F c j j' = K₁.ιMapBifunctor K₂ F c i₁ i₂ j hj ≫ H.hom j j'
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
b' n' : ℤ
hb' : a + b' = n'
hn' : n' = n + y
⊢ K.ιTotal (up ℤ) a b' n' hb' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n n' hn').inv ≫ (K.totalShift₂Iso y).inv.f n =
    (a * y).negOnePow • (K.shiftFunctor₂XXIso a b y b' ⋯).inv ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h

Tactic:
subst hn'
  obtain rfl : b = b' - y := by lia
  dsimp [totalShift₂Iso, totalShift₂XIso, shiftFunctor₂XXIso, XXIsoOfEq]
  simp only [id_comp, ι_totalDesc]

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

Goal state before:
pp: case e'_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
⊢ f ≫ biprod.inl - g ≫ biprod.inr = biprod.lift f (-g)

pp: case e'_3
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
⊢ 0 = 0 ≫ s.π

Tactic:
<;>

Goal state after:
case e'_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
⊢ f ≫ biprod.inl - g ≫ biprod.inr = biprod.lift f (-g)

case e'_3
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
⊢ 0 = 0 ≫ s.π
Module: Mathlib.Algebra.Homology.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))
x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))
hx₁ :
  (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂
k : ι
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₁.d j k))) x₁ = 0

Tactic:
have := hS.mono_f

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))
x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))
hx₁ :
  (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂
k : ι
this : Mono S.f
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₁.d j k))) x₁ = 0
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: case e'_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (biprod.desc f (-g)) 0
⊢ biprod.fst ≫ f - biprod.snd ≫ g = biprod.desc f (-g)

pp: case e'_3
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (biprod.desc f (-g)) 0
⊢ 0 = s.ι ≫ 0

Tactic:
<;>

Goal state after:
case e'_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (biprod.desc f (-g)) 0
⊢ biprod.fst ≫ f - biprod.snd ≫ g = biprod.desc f (-g)

case e'_3
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
sq : CommSq fst snd f g
h : IsLimit (PullbackCone.mk fst snd ⋯)
s : Fork (biprod.desc f (-g)) 0
⊢ 0 = s.ι ≫ 0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

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✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij' : ¬c'.Rel (e.f j) (e.f i)
⊢ ¬c.Rel j i

Tactic:
← e.rel_iff

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✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij' : ¬c'.Rel (e.f j) (e.f i)
⊢ ¬c'.Rel (e.f j) (e.f i)
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

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✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (K.extendXIso e ⋯).hom ≫
      ((dNext i) h.hom ≫ (L.extendXIso e ⋯).inv + (prevD i) h.hom ≫ (L.extendXIso e ⋯).inv +
        g.f i ≫ (L.extendXIso e ⋯).inv) =
    (dNext (e.f i)) (extend.hom e h.hom) + (prevD (e.f i)) (extend.hom e h.hom) +
      (K.extendXIso e ⋯).hom ≫ g.f i ≫ (L.extendXIso e ⋯).inv

Tactic:
Preadditive.comp_add,

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✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (K.extendXIso e ⋯).hom ≫ ((dNext i) h.hom ≫ (L.extendXIso e ⋯).inv + (prevD i) h.hom ≫ (L.extendXIso e ⋯).inv) +
      (K.extendXIso e ⋯).hom ≫ g.f i ≫ (L.extendXIso e ⋯).inv =
    (dNext (e.f i)) (extend.hom e h.hom) + (prevD (e.f i)) (extend.hom e h.hom) +
      (K.extendXIso e ⋯).hom ≫ g.f i ≫ (L.extendXIso e ⋯).inv
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

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✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (K.extendXIso e ⋯).hom ≫ ((dNext i) h.hom ≫ (L.extendXIso e ⋯).inv + (prevD i) h.hom ≫ (L.extendXIso e ⋯).inv) +
      (K.extendXIso e ⋯).hom ≫ g.f i ≫ (L.extendXIso e ⋯).inv =
    (dNext (e.f i)) (extend.hom e h.hom) + (prevD (e.f i)) (extend.hom e h.hom) +
      (K.extendXIso e ⋯).hom ≫ g.f i ≫ (L.extendXIso e ⋯).inv

Tactic:
Preadditive.comp_add,

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✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
⊢ (K.extendXIso e ⋯).hom ≫ (dNext i) h.hom ≫ (L.extendXIso e ⋯).inv +
        (K.extendXIso e ⋯).hom ≫ (prevD i) h.hom ≫ (L.extendXIso e ⋯).inv +
      (K.extendXIso e ⋯).hom ≫ g.f i ≫ (L.extendXIso e ⋯).inv =
    (dNext (e.f i)) (extend.hom e h.hom) + (prevD (e.f i)) (extend.hom e h.hom) +
      (K.extendXIso e ⋯).hom ≫ g.f i ≫ (L.extendXIso e ⋯).inv
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst✝ : Injective (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
hp : n + 1 ≤ n + 1
hpq : n + 1 + 0 = n + 1
⊢ (δ (-1) 0 (α + Cochain.single β (-1))).v (n + 1) (n + 1) hpq = (Cochain.ofHom f).v (n + 1) (n + 1) hpq

Tactic:
rw [δ_v (-1) 0 (neg_add_cancel 1) _ (n + 1) (n + 1) (by lia) n (n + 2)
      (by lia) (by lia), Cochain.add_v,
      Cochain.single_v_eq_zero _ _ _ _ _ (by lia)]

Goal state after:
case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) n
hK : (HomologicalComplex.sc' K n (n + 1) (n + 2)).Exact
inst✝ : Injective (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
hp : n + 1 ≤ n + 1
hpq : n + 1 + 0 = n + 1
⊢ (α.v (n + 1) n ⋯ + 0) ≫ L.d n (n + 1) +
      Int.negOnePow 0 • K.d (n + 1) (n + 2) ≫ (α + Cochain.single β (-1)).v (n + 2) (n + 1) ⋯ =
    (Cochain.ofHom f).v (n + 1) (n + 1) hpq
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
X : C
n a n' : ℤ
hn' : a + n' = n
inst✝ : t.IsLE ((shiftFunctor C a).obj X) n'
⊢ t.IsLE X n

Tactic:
have h := t.isLE_shift (X⟦a⟧) n' (-a) n

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
X : C
n a n' : ℤ
hn' : a + n' = n
inst✝ : t.IsLE ((shiftFunctor C a).obj X) n'
h : t.IsLE ((shiftFunctor C (-a)).obj ((shiftFunctor C a).obj X)) n
⊢ t.IsLE X n
Module: Mathlib.Algebra.Homology.HomotopyFiber

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
α : Type u_2
c : ComplexShape α
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : DecidableRel c.Rel
inst✝ : HasHomotopyFiber φ
i j : α
hij : c.symm.Rel i j
⊢ HasBinaryBiproduct (((opFunctor C c).obj (op G)).X j) (((opFunctor C c).obj (op F)).X i)

Tactic:
have := HasHomotopyFiber.hasBinaryBiproduct φ j i hij

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
α : Type u_2
c : ComplexShape α
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : DecidableRel c.Rel
inst✝ : HasHomotopyFiber φ
i j : α
hij : c.symm.Rel i j
this : HasBinaryBiproduct (G.X j) (F.X i)
⊢ HasBinaryBiproduct (((opFunctor C c).obj (op G)).X j) (((opFunctor C c).obj (op F)).X i)
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
⊢ sq.HasLift

Tactic:
have w : (u ≫ s) ≫ g = f' ≫ v ≫ t := by
      rw [Category.assoc, h.toCommSq.w, ← Category.assoc, ← Category.assoc, sq.w]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
⊢ sq.HasLift
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : C
n : ℤ
e : (singleFunctor C n).obj X ≅ Q.obj ((CochainComplex.singleFunctor C n).obj X) := (singleFunctorIsoCompQ C n).app X
⊢ ((singleFunctor C n).obj X).IsGE n

Tactic:
exact TStructure.t.isGE_of_iso e.symm n

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
J : Type w
⊢ (fibrations C).llp.IsStableUnderCoproductsOfShape J

Tactic:
apply MorphismProperty.llp_isStableUnderCoproductsOfShape

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
J : Type w
⊢ (trivialFibrations C).llp.IsStableUnderCoproductsOfShape J

Tactic:
apply MorphismProperty.llp_isStableUnderCoproductsOfShape

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: case left
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
h₁ : cofibrations C f₁
h₂ : cofibrations C f₂
inst✝¹ : HasBinaryCoproduct X₁ X₂
inst✝ : HasBinaryCoproduct Y₁ Y₂
⊢ cofibrations C ((mapPair f₁ f₂).app { as := WalkingPair.left })

pp: case right
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
h₁ : cofibrations C f₁
h₂ : cofibrations C f₂
inst✝¹ : HasBinaryCoproduct X₁ X₂
inst✝ : HasBinaryCoproduct Y₁ Y₂
⊢ cofibrations C ((mapPair f₁ f₂).app { as := WalkingPair.right })

Tactic:
<;>

Goal state after:
case left
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
h₁ : cofibrations C f₁
h₂ : cofibrations C f₂
inst✝¹ : HasBinaryCoproduct X₁ X₂
inst✝ : HasBinaryCoproduct Y₁ Y₂
⊢ cofibrations C ((mapPair f₁ f₂).app { as := WalkingPair.left })

case right
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
h₁ : cofibrations C f₁
h₂ : cofibrations C f₂
inst✝¹ : HasBinaryCoproduct X₁ X₂
inst✝ : HasBinaryCoproduct Y₁ Y₂
⊢ cofibrations C ((mapPair f₁ f₂).app { as := WalkingPair.right })
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: case left
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
h₁ : fibrations C f₁
h₂ : fibrations C f₂
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : HasBinaryProduct Y₁ Y₂
⊢ fibrations C ((mapPair f₁ f₂).app { as := WalkingPair.left })

pp: case right
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
h₁ : fibrations C f₁
h₂ : fibrations C f₂
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : HasBinaryProduct Y₁ Y₂
⊢ fibrations C ((mapPair f₁ f₂).app { as := WalkingPair.right })

Tactic:
<;>

Goal state after:
case left
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
h₁ : fibrations C f₁
h₂ : fibrations C f₂
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : HasBinaryProduct Y₁ Y₂
⊢ fibrations C ((mapPair f₁ f₂).app { as := WalkingPair.left })

case right
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
h₁ : fibrations C f₁
h₂ : fibrations C f₂
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : HasBinaryProduct Y₁ Y₂
⊢ fibrations C ((mapPair f₁ f₂).app { as := WalkingPair.right })
Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : Cylinder A
inst✝² : IsCofibrant A
P P' : Cylinder A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : P.I ⨿ A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
⊢ (P.trans P').i = coprod.map P.i₀ (𝟙 A) ≫ ψ

Tactic:
simp [Precylinder.i, ψ]

Goal state after: