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

Goal state before:
pp: case pos
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₁ c₁₂ i₁ i₂ i₁₂

Tactic:
simp [totalAux.d₁_eq' _ c₁₂ h]

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

Goal state before:
pp: case neg
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.σ c₂ c i₁ i₂ • K.d₂ c i₁ i₂ j' =
    K.flip.d₁ c i₂ i₁ j' ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯

Tactic:
· rw [K.d₂_eq_zero _ _ _ _ h₂, K.flip.d₁_eq_zero _ _ _ _ h₂, smul_zero, zero_comp]

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

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

Tactic:
simp only [biprod.inl_desc_assoc]
          apply PushoutCocone.IsColimit.inl_desc h

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
m : ℤ
hK : HomologicalComplex.ExactAt K (-m)
hm : -m + m = 0
⊢ (ComplexShape.up ℤ).next (-m) = -(m - 1)

Tactic:
grind [next]

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 sq.cokernelCofork
s : PushoutCocone f g
m : X₄ ⟶ s.pt
hm₁ : inl ≫ m = s.inl
hm₂ : inr ≫ m = s.inr
⊢ m = h.desc (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯)

Tactic:
by
        apply Cofork.IsColimit.hom_ext h
        convert!
          (h.fac (CokernelCofork.ofπ (biprod.desc s.inl s.inr) (by simp [s.condition])) .one).symm
        cat_disch

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₁ L₁ : CochainComplex C₁ ℤ
f : K₁ ⟶ L₁
n : ℤ
K₂ : CochainComplex C₂ ℤ
d p q : ℤ
h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = d
⊢ ιMapBifunctor K₁ ((shiftFunctor (CochainComplex C₂ ℤ) n).obj K₂) F (ComplexShape.up ℤ) p q d h ≫
      ((commShiftIso (F.map₂CochainComplex.obj K₁) n).hom.app K₂).f d ≫
        (mapBifunctorMap f (𝟙 K₂) F (ComplexShape.up ℤ)).f (d + n) =
    ιMapBifunctor K₁ ((shiftFunctor (CochainComplex C₂ ℤ) n).obj K₂) F (ComplexShape.up ℤ) p q d h ≫
      (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

Tactic:
simp [commShiftIso_map₂CochainComplex_hom_app,
      CochainComplex.ι_mapBifunctorShift₂Iso_hom_f _ _ _ _ _ _ _ _ (q + n) (d + n) rfl rfl,
      CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc _ _ _ _ _ _ _ _ (q + n) (d + n) rfl rfl]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x y : Cocycle K L n
h : toHom (mk x) = toHom (mk y)
⊢ toHom (mk y) - toHom (mk y) = 0

Tactic:
sub_self

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x y : Cocycle K L n
h : toHom (mk x) = toHom (mk y)
⊢ 0 = 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.ExactAt K (n + 1)
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
⊢ ∃ h, (δ (-1) 0 (α + Cochain.single h (-1))).EqUpTo (Cochain.ofHom f) (n + 1)

Tactic:
K.exactAt_iff' n (n + 1) (n + 2) (by simp) (by simp; lia)

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
⊢ ∃ h, (δ (-1) 0 (α + Cochain.single h (-1))).EqUpTo (Cochain.ofHom f) (n + 1)
Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
A : C
inst✝⁴ : CategoryWithWeakEquivalences C
P : PathObject A
inst✝³ : HasBinaryProducts C
inst✝² : CategoryWithFibrations C
inst✝¹ : P.IsGood
inst✝ : (fibrations C).RespectsIso
hp : fibrations C P.p
⊢ fibrations C (P.p ≫ (prod.braiding A A).hom)

Tactic:
refine ((fibrations C).arrow_mk_iso_iff ?_).2 hp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
A : C
inst✝⁴ : CategoryWithWeakEquivalences C
P : PathObject A
inst✝³ : HasBinaryProducts C
inst✝² : CategoryWithFibrations C
inst✝¹ : P.IsGood
inst✝ : (fibrations C).RespectsIso
hp : fibrations C P.p
⊢ Arrow.mk (P.p ≫ (prod.braiding A A).hom) ≅ Arrow.mk P.p
Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsFibrant Y
h✝¹ : LeftHomotopyRel f g
Z : C
i : Z ⟶ X
P : Cylinder X
left✝ : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder Z
h✝ : Q.IsVeryGood
⊢ LeftHomotopyRel (i ≫ f) (i ≫ g)

Tactic:
have sq : CommSq (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i) := ⟨by aesop_cat⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsFibrant Y
h✝¹ : LeftHomotopyRel f g
Z : C
i : Z ⟶ X
P : Cylinder X
left✝ : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder Z
h✝ : Q.IsVeryGood
sq : CommSq (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)
⊢ LeftHomotopyRel (i ≫ f) (i ≫ g)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
⊢ ∀ (h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : X₃ ⟶ Z₁₃}
    {w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁} (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles),
    Nonempty (Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
h₂₃

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
⊢ ∀ {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁}
    (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles),
    Nonempty (Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
j : ℤ
hj : j + 1 = i
⊢ IsZero (K.X j)

Tactic:
exact K.isZero_of_isStrictlyGE n j

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangulated

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles
o : Triangulated.Octahedron' ⋯ ⋯ ⋯ ⋯ := Triangulated.someOctahedron' ⋯ ⋯ ⋯ ⋯
⊢ o.m₃.op ≫ w₁₃ = w₁₂

Tactic:
have eq₃ := congr($(o.comm₃).op)
      dsimp at eq₃
      rw [← Category.assoc, ← op_comp, ← Functor.map_comp,
        NatIso.cancel_natIso_inv_right (opShiftFunctorEquivalence C _).unitIso] at eq₃
      exact congr($(Functor.map_injective _ congr($(eq₃).unop)).op)

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
p : I ⟶ Z
hZ : IsZero Z
⊢ Injective I ↔ (MorphismProperty.monomorphisms C).rlp p

Tactic:
obtain rfl := hZ.eq_of_tgt p 0
  constructor
  · intro _ A B i (_ : Mono i)
    exact Injective.hasLiftingProperty_of_isZero i 0 hZ
  · intro h
    constructor
    intro A B f i hi
    have := h _ hi
    have sq : CommSq f i (0 : I ⟶ Z) 0 := ⟨by simp⟩
    exact ⟨sq.lift, by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: case h₃
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T T' : Triangle C
f₁ f₂ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f.hom₃ = TriangleMorphism.hom₃ 0

Tactic:
obtain ⟨g, hg⟩ := T.yoneda_exact₃ hT f.hom₃ (by cat_disch)
    simp [hg, t.zero_of_isLE_of_isGE g (a - 1) b (by lia)
      (t.isLE_shift _ a 1 (a - 1)) inferInstance]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: case zero.succ.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : 0 ≤ j + 1
k : ℕ
hjk : j + 1 ≤ k + 1 + 1
⊢ map f 0 (k + 1 + 1) ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) (k + 1 + 1) hjk

Tactic:
simp only [map, Nat.reduceAdd]

Goal state after:
case zero.succ.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : 0 ≤ j + 1
k : ℕ
hjk : j + 1 ≤ k + 1 + 1
⊢ f 0 ≫ map (fun n ↦ f (n + 1)) 0 (k + 1) ⋯ = map f 0 (j + 1) hij ≫ map (fun n ↦ f (n + 1)) j (k + 1) ⋯
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

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
inst✝ : EnoughInjectives C
n₀✝ n₁ : ℤ
hn₁ : n₀✝ + 1 = n₁
hf : ∀ i ≤ n₀✝, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
x✝ : x₁ ≫ K.d n₁ (n₁ + 1) = 0
y₀ : A ⟶ (mid K L n₁).X n₀
hy₀ : x₁ ≫ (ι f n₁).f n₁ = y₀ ≫ (mid K L n₁).d n₀ n₁
⊢ ∃ z₁, z₁ ≫ (σ K L n₁).f n₀ = y₀

Tactic:
refine ⟨y₀ ≫ (π K L n₁).f n₀, Eq.trans ?_ (Category.comp_id _)⟩

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n₀✝ n₁ : ℤ
hn₁ : n₀✝ + 1 = n₁
hf : ∀ i ≤ n₀✝, QuasiIsoAt f i
n₀ : ℤ := n₁ - 1
A : C
x₁ : A ⟶ K.X n₁
x✝ : x₁ ≫ K.d n₁ (n₁ + 1) = 0
y₀ : A ⟶ (mid K L n₁).X n₀
hy₀ : x₁ ≫ (ι f n₁).f n₁ = y₀ ≫ (mid K L n₁).d n₀ n₁
⊢ (y₀ ≫ (π K L n₁).f n₀) ≫ (σ K L n₁).f n₀ = y₀ ≫ 𝟙 ((mid K L n₁).X n₀)
Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁴ : Category.{v_1, u_1} C₁
inst✝³ : Category.{v_2, u_2} C₂
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
inst✝ : w.GuitartExact
α : L ≅ L'
β : R ≅ R'
⊢ (w.whiskerVertical α.hom β.inv).GuitartExact

Tactic:
by
  rw [guitartExact_iff_initial]
  intro X₂
  let e : structuredArrowDownwards (w.whiskerVertical α.hom β.inv) X₂ ≅
      w.structuredArrowDownwards X₂ ⋙ (StructuredArrow.mapIso (β.app X₂)).functor :=
    NatIso.ofComponents (fun f => StructuredArrow.isoMk (α.symm.app f.right) (by
      dsimp
      simp only [NatTrans.naturality_assoc, assoc, ← B.map_comp,
        Iso.hom_inv_id_app, B.map_id, comp_id]))
  rw [Functor.initial_natIso_iff e]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
R R' : Φ.RightResolution X₂
φ : R ⟶ R'
⊢ L.map (R.w ≫ Φ.functor.map φ.f) ≫ (isoOfHom L W₂ R'.w ⋯).inv ≫ y = y

Tactic:
φ.comm,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
R R' : Φ.RightResolution X₂
φ : R ⟶ R'
⊢ L.map R'.w ≫ (isoOfHom L W₂ R'.w ⋯).inv ≫ y = y
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
D₁ : Type u_1
D₂ : Type u_2
inst✝⁴ : Category.{v_1, u_1} D₁
inst✝³ : Category.{v_2, u_2} D₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝² : L₁.IsLocalization W₁
inst✝¹ : L₂.IsLocalization W₂
F : D₁ ⥤ D₂
inst✝ : Φ.IsLeftDerivabilityStructure
⊢ Φ.op.IsRightDerivabilityStructure

Tactic:
by
  rwa [← isLeftDerivabilityStructure_iff_op]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived

Goal state before:
pp: C : Type u_1
D : Type u_3
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} D
inst✝¹ : Category.{v_5, u_2} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
this : F.HasRightDerivedFunctor W ↔ W.Q.HasLeftKanExtension F
⊢ F.HasRightDerivedFunctor W ↔ L.HasLeftKanExtension F

Tactic:
rw [this, hasLeftExtension_iff_postcomp₁ (Localization.compUniqFunctor W.Q L W) F]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: case refine_2
C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
L : Plus C ⥤ H
inst✝ : L.IsLocalization (quasiIso C)
⊢ (homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C) ≤ CochainComplex.Plus.quasiIso C

Tactic:
intro K L f hf

Goal state after:
case refine_2
C : Type u_1
H : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : Category.{v_2, u_2} H
L✝ : Plus C ⥤ H
inst✝ : L✝.IsLocalization (quasiIso C)
K L : CochainComplex.Plus C
f : K ⟶ L
hf : (homotopyEquivalences C (ComplexShape.up ℤ)).inverseImage (CochainComplex.Plus.ι C) f
⊢ CochainComplex.Plus.quasiIso C f
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
f : P.complex ⟶ Q.complex
comm : f ≫ Q.π = 0
⊢ P.complex.d 1 0 ≫ f.f 0 - P.complex.d 1 0 ≫ f.f 0 = 0

Tactic:
sub_self

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
f : P.complex ⟶ Q.complex
comm : f ≫ Q.π = 0
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : Karoubi C ⥤ D
τ :
  ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj F ⟶
    ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj G
X : C
⊢ F.map (𝟙 ((toKaroubi C).obj X)) ≫
      τ.app X ≫ G.map (𝟙 { X := ((toKaroubi C).obj X).X, p := 𝟙 ((toKaroubi C).obj X).X, idem := ⋯ }) =
    τ.app X

Tactic:
Functor.map_id,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : Karoubi C ⥤ D
τ :
  ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj F ⟶
    ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj G
X : C
⊢ 𝟙 (F.obj ((toKaroubi C).obj X)) ≫
      τ.app X ≫ G.map (𝟙 { X := ((toKaroubi C).obj X).X, p := 𝟙 ((toKaroubi C).obj X).X, idem := ⋯ }) =
    τ.app X
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: case pos
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i₁ i₂ j : I
h₁ : c.Rel i₁ (c.next i₁)
h₂ : c.π c c (c.next i₁, i₂) = j
⊢ mapBifunctor.d₁ (tensorUnit C c) K (curriedTensor C) c i₁ i₂ j = 0

pp: case neg
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i₁ i₂ j : I
h₁ : c.Rel i₁ (c.next i₁)
h₂ : ¬c.π c c (c.next i₁, i₂) = j
⊢ mapBifunctor.d₁ (tensorUnit C c) K (curriedTensor C) c i₁ i₂ j = 0

Tactic:
· rw [mapBifunctor.d₁_eq _ _ _ _ h₁ _ _ h₂, single_obj_d, Functor.map_zero,
        zero_app, zero_comp, smul_zero]

Goal state after:
case neg
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i₁ i₂ j : I
h₁ : c.Rel i₁ (c.next i₁)
h₂ : ¬c.π c c (c.next i₁, i₂) = j
⊢ mapBifunctor.d₁ (tensorUnit C c) K (curriedTensor C) c i₁ i₂ j = 0
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : MonoidalCategory C
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : (curriedTensor C).Additive
inst✝⁴ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝³ : AddMonoid I
c : ComplexShape I
inst✝² : c.TensorSigns
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i₁ i₂ j : I
⊢ mapBifunctor.d₁ (tensorUnit C c) K (curriedTensor C) c i₁ i₂ j = 0

Tactic:
by
  by_cases h₁ : c.Rel i₁ (c.next i₁)
  · by_cases h₂ : ComplexShape.π c c c (c.next i₁, i₂) = j
    · rw [mapBifunctor.d₁_eq _ _ _ _ h₁ _ _ h₂, single_obj_d, Functor.map_zero,
        zero_app, zero_comp, smul_zero]
    · rw [mapBifunctor.d₁_eq_zero' _ _ _ _ h₁ _ _ h₂]
  · rw [mapBifunctor.d₁_eq_zero _ _ _ _ _ _ _ h₁]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝² : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p
j : J
⊢ φ j ≫
      e.inv.app (Y' j) ≫
        (F.map (singleObjApplyIso 0 X).inv).app (Y' j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯ =
    e.inv.app (Y j) ≫
      (F.map (singleObjApplyIso 0 X).inv).app (Y j) ≫
        (F.map (𝟙 ((single₀ I).obj X 0))).app (Y j) ≫
          (F.obj ((single₀ I).obj X 0)).map (φ j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯

Tactic:
Functor.map_id,

Goal state after:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝² : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p
j : J
⊢ φ j ≫
      e.inv.app (Y' j) ≫
        (F.map (singleObjApplyIso 0 X).inv).app (Y' j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯ =
    e.inv.app (Y j) ≫
      (F.map (singleObjApplyIso 0 X).inv).app (Y j) ≫
        (𝟙 (F.obj ((single₀ I).obj X 0))).app (Y j) ≫
          (F.obj ((single₀ I).obj X 0)).map (φ j) ≫ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y' 0 j j ⋯