mathlib-initiative/mathlib-tactics huggingface dataset:
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 ℤ)
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ (n₁ * y + x * y).negOnePow • K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ =
    (n₁ * y + x * y).negOnePow •
      (K.shiftFunctor₁XXIso n₁ x (n₁ + x) ⋯ (n₂ + y)).hom ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫
          (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x (n + y) (n + x + y) ⋯).inv ≫
            ((K.total (up ℤ)).XIsoOfEq ⋯).hom

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n₁ n₂ : ℤ
h : n₁ + n₂ = n
⊢ (n₁ * y + x * y).negOnePow • K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ =
    (n₁ * y + x * y).negOnePow •
      𝟙 ((K.X (n₁ + x)).X (n₂ + y)) ≫
        K.ιTotal (up ℤ) (n₁ + x) (n₂ + y) (n + x + y) ⋯ ≫
          ((K.total (up ℤ)).XIsoOfEq ⋯).inv ≫ ((K.total (up ℤ)).XIsoOfEq ⋯).hom
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ (ComplexShape.up ℤ).Rel (n - 1) n

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ n - 1 + 1 = n
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ (ComplexShape.up ℤ).Rel (-n) (-(n - 1))

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ -n + 1 = -(n - 1)
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ h.hom n (n - 1) ≫ ((HomologicalComplex.op K).restriction ComplexShape.embeddingUpIntDownInt).d (n - 1) n =
    (K.d (-n) (-(n - 1)) ≫
        (HomologicalComplex.XIsoOfEq K ⋯).hom ≫
          (h.hom (- -n) (- -(n - 1))).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom).op

Tactic:
dsimp

Goal state after:
case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ h.hom n (n - 1) ≫ (K.d (-n) (-(n - 1))).op =
    (((HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom (- -n) (- -(n - 1))) ≫
        (HomologicalComplex.XIsoOfEq K ⋯).hom.op) ≫
      (K.d (-n) (-(n - 1))).op
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ (ComplexShape.up ℤ).Rel n (n + 1)

Tactic:
dsimp

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

Goal state before:
pp: 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
⊢ Cofork.π sq.cokernelCofork ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = s.π

Tactic:
dsimp

Goal state after:
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
⊢ biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = s.π
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ ((HomologicalComplex.op L).restriction ComplexShape.embeddingUpIntDownInt).d n (n + 1) ≫ h.hom (n + 1) n =
    (((HomologicalComplex.XIsoOfEq K ⋯).hom ≫
          (h.hom (- -(n + 1)) (- -n)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom) ≫
        L.d (-(n + 1)) (-n)).op

Tactic:
dsimp

Goal state after:
case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ (L.d (-(n + 1)) (-n)).op ≫ h.hom (n + 1) n =
    (L.d (-(n + 1)) (-n)).op ≫
      ((HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom (- -(n + 1)) (- -n)) ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
p q p' q' : ℤ
hp : autoParam (p + p' = 0) homotopyUnop_hom_eq._auto_1
hq : autoParam (q + q' = 0) homotopyUnop_hom_eq._auto_3
⊢ p = ComplexShape.embeddingUpIntDownInt.f p'

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
p q p' q' : ℤ
hp : autoParam (p + p' = 0) homotopyUnop_hom_eq._auto_1
hq : autoParam (q + q' = 0) homotopyUnop_hom_eq._auto_3
⊢ p = -p'
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
p q p' q' : ℤ
hp : autoParam (p + p' = 0) homotopyUnop_hom_eq._auto_1
hq : autoParam (q + q' = 0) homotopyUnop_hom_eq._auto_3
⊢ ComplexShape.embeddingUpIntDownInt.f q' = q

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
p q p' q' : ℤ
hp : autoParam (p + p' = 0) homotopyUnop_hom_eq._auto_1
hq : autoParam (q + q' = 0) homotopyUnop_hom_eq._auto_3
⊢ -q' = q
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: 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 sq.cokernelCofork
s : PushoutCocone f g
⊢ inr ≫ h.desc (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯) = s.inr

Tactic:
by simpa using biprod.inr ≫=
                h.fac (CokernelCofork.ofπ (biprod.desc s.inl s.inr)
                  (by simp [s.condition])) .one

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
n : ℤ
⊢ ((NatIso.ofComponents (fun K₂ ↦ K₁.mapBifunctorShift₂Iso K₂ F 0) ⋯).hom.app K₂).f n =
    ((CommShift.isoZero (F.map₂CochainComplex.obj K₁) ℤ).hom.app K₂).f n

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
n : ℤ
⊢ (K₁.mapBifunctorShift₂Iso K₂ F 0).hom.f n = ((CommShift.isoZero (F.map₂CochainComplex.obj K₁) ℤ).hom.app K₂).f n
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ : CochainComplex C₁ ℤ
a b : ℤ
K₂ : CochainComplex C₂ ℤ
n : ℤ
⊢ ((NatIso.ofComponents (fun K₂ ↦ K₁.mapBifunctorShift₂Iso K₂ F (a + b)) ⋯).hom.app K₂).f n =
    ((CommShift.isoAdd (NatIso.ofComponents (fun K₂ ↦ K₁.mapBifunctorShift₂Iso K₂ F a) ⋯)
                (NatIso.ofComponents (fun K₂ ↦ K₁.mapBifunctorShift₂Iso K₂ F b) ⋯)).hom.app
          K₂).f
      n

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ : CochainComplex C₁ ℤ
a b : ℤ
K₂ : CochainComplex C₂ ℤ
n : ℤ
⊢ (K₁.mapBifunctorShift₂Iso K₂ F (a + b)).hom.f n =
    ((CommShift.isoAdd (NatIso.ofComponents (fun K₂ ↦ K₁.mapBifunctorShift₂Iso K₂ F a) ⋯)
                (NatIso.ofComponents (fun K₂ ↦ K₁.mapBifunctorShift₂Iso K₂ F b) ⋯)).hom.app
          K₂).f
      n
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ L₁ : CochainComplex C₁ ℤ
f : K₁ ⟶ L₁
n : ℤ
K₂ : CochainComplex C₂ ℤ
d : ℤ
⊢ (((commShiftIso (F.map₂CochainComplex.obj K₁) n).hom ≫
              whiskerRight (F.map₂CochainComplex.map f) (shiftFunctor (CochainComplex D ℤ) n)).app
          K₂).f
      d =
    (((shiftFunctor (CochainComplex C₂ ℤ) n).whiskerLeft (F.map₂CochainComplex.map f) ≫
              (commShiftIso (F.map₂CochainComplex.obj L₁) n).hom).app
          K₂).f
      d

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ L₁ : CochainComplex C₁ ℤ
f : K₁ ⟶ L₁
n : ℤ
K₂ : CochainComplex C₂ ℤ
d : ℤ
⊢ ((commShiftIso (F.map₂CochainComplex.obj K₁) n).hom.app K₂).f d ≫
      (mapBifunctorMap f (𝟙 K₂) F (ComplexShape.up ℤ)).f (d + n) =
    (mapBifunctorMap f (𝟙 ((shiftFunctor (CochainComplex C₂ ℤ) n).obj K₂)) F (ComplexShape.up ℤ)).f d ≫
      ((commShiftIso (F.map₂CochainComplex.obj L₁) n).hom.app K₂).f d
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: 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
⊢ PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ Fork.ι sq.kernelFork = s.ι

Tactic:
dsimp

Goal state after:
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
⊢ PullbackCone.IsLimit.lift h (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) ⋯ ≫ biprod.lift fst snd = s.ι
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂✝ : CochainComplex C₂ ℤ
K₂ : CochainComplex C₁ ℤ
n : ℤ
⊢ ((NatIso.ofComponents (fun K₁ ↦ K₁.mapBifunctorShift₁Iso K₂✝ F 0) ⋯).hom.app K₂).f n =
    ((CommShift.isoZero (F.map₂CochainComplex.flip.obj K₂✝) ℤ).hom.app K₂).f n

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂✝ : CochainComplex C₂ ℤ
K₂ : CochainComplex C₁ ℤ
n : ℤ
⊢ (K₂.mapBifunctorShift₁Iso K₂✝ F 0).hom.f n =
    ((CommShift.isoZero (F.map₂CochainComplex.flip.obj K₂✝) ℤ).hom.app K₂).f n
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂✝ : CochainComplex C₂ ℤ
a b : ℤ
K₂ : CochainComplex C₁ ℤ
n : ℤ
⊢ ((NatIso.ofComponents (fun K₁ ↦ K₁.mapBifunctorShift₁Iso K₂✝ F (a + b)) ⋯).hom.app K₂).f n =
    ((CommShift.isoAdd (NatIso.ofComponents (fun K₁ ↦ K₁.mapBifunctorShift₁Iso K₂✝ F a) ⋯)
                (NatIso.ofComponents (fun K₁ ↦ K₁.mapBifunctorShift₁Iso K₂✝ F b) ⋯)).hom.app
          K₂).f
      n

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂✝ : CochainComplex C₂ ℤ
a b : ℤ
K₂ : CochainComplex C₁ ℤ
n : ℤ
⊢ (K₂.mapBifunctorShift₁Iso K₂✝ F (a + b)).hom.f n =
    ((CommShift.isoAdd (NatIso.ofComponents (fun K₁ ↦ K₁.mapBifunctorShift₁Iso K₂✝ F a) ⋯)
                (NatIso.ofComponents (fun K₁ ↦ K₁.mapBifunctorShift₁Iso K₂✝ F b) ⋯)).hom.app
          K₂).f
      n
Module: Mathlib.Algebra.Homology.BifunctorShift

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂ L₂ : CochainComplex C₂ ℤ
g : K₂ ⟶ L₂
n : ℤ
K₁ : CochainComplex C₁ ℤ
d : ℤ
⊢ (((commShiftIso (F.map₂CochainComplex.flip.obj K₂) n).hom ≫
              whiskerRight (F.map₂CochainComplex.flip.map g) (shiftFunctor (CochainComplex D ℤ) n)).app
          K₁).f
      d =
    (((shiftFunctor (CochainComplex C₁ ℤ) n).whiskerLeft (F.map₂CochainComplex.flip.map g) ≫
              (commShiftIso (F.map₂CochainComplex.flip.obj L₂) n).hom).app
          K₁).f
      d

Tactic:
dsimp

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
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
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₂ L₂ : CochainComplex C₂ ℤ
g : K₂ ⟶ L₂
n : ℤ
K₁ : CochainComplex C₁ ℤ
d : ℤ
⊢ ((commShiftIso (F.map₂CochainComplex.flip.obj K₂) n).hom.app K₁).f d ≫
      (mapBifunctorMap (𝟙 K₁) g F (ComplexShape.up ℤ)).f (d + n) =
    (mapBifunctorMap (𝟙 ((shiftFunctor (CochainComplex C₁ ℤ) n).obj K₁)) g F (ComplexShape.up ℤ)).f d ≫
      ((commShiftIso (F.map₂CochainComplex.flip.obj L₂) n).hom.app K₁).f d
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m✝ p : ℤ
α₁ α₂ : Cocycle K L n
m : ℤ
hm : m + 1 = n
β₁ : Cochain K L m
hβ₁ : δ m n β₁ = ↑α₁
hm' : m + 1 = n
β₂ : Cochain K L m
hβ₂ : δ m n β₂ = ↑α₂
⊢ α₁ + α₂ ∈ {α | ∃ m, ∃ (_ : m + 1 = n), ∃ β, δ m n β = ↑α}

Tactic:
exact ⟨m, hm, β₁ + β₂, by aesop⟩

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
hm : n + 1 = m
hp : m + 1 = p
x : ↑(KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt
⊢ (AddCommGrpCat.Hom.hom
        ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯) ≫
          AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)))
      x =
    (AddCommGrpCat.Hom.hom 0) x

Tactic:
dsimp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
hm : n + 1 = m
hp : m + 1 = p
x : ↑(KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt
⊢ CohomologyClass.mk
      ((AddCommGrpCat.Hom.hom ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι ((K.HomComplex L).d n m) ⋯))) x) =
    0
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
x✝ : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ (shiftFunctor C 1).obj X₁
hT : Triangle.mk f g h ∈ distinguishedTriangles
hX₃ : P X₃
α : X₂ ⟶ Y
hα : f ≫ α = 0
⊢ α = 0

Tactic:
obtain ⟨β, rfl⟩ := Triangle.yoneda_exact₂ _ hT α hα

Goal state after:
case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
x✝ : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ (shiftFunctor C 1).obj X₁
hT : Triangle.mk f g h ∈ distinguishedTriangles
hX₃ : P X₃
β : (Triangle.mk f g h).obj₃ ⟶ Y
hα : f ≫ (Triangle.mk f g h).mor₂ ≫ β = 0
⊢ (Triangle.mk f g h).mor₂ ≫ β = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: 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
⊢ ∃ h, (δ (-1) 0 (α + Cochain.single h (-1))).EqUpTo (Cochain.ofHom f) (n + 1)

Tactic:
refine ⟨β, ?_⟩

Goal state after:
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
⊢ (δ (-1) 0 (α + Cochain.single β (-1))).EqUpTo (Cochain.ofHom f) (n + 1)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: case mpr
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
a n n' : ℤ
hn' : a + n = n'
X : C
⊢ t.ge n' X → (t.ge n).shift a X

Tactic:
intro hX
    exact t.ge_shift _ _ _ hn' X hX

Goal state after: