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

Goal state before:
pp: case pos.h
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₄
j j' : ι₄
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₁₂ : ι₁₂ := c₁.π c₂ c₁₂ (i₁, i₂)
h₁ : c₁₂.Rel i₁₂ (c₁₂.next i₁₂)
h₂ : ¬c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (c₁.next i₁, i₂), i₃) = j'
⊢ c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (c₁.next i₁, i₂), i₃)

Tactic:
ComplexShape.next_π₁ c₂ c₁₂ h₃ i₂

Goal state after:
case pos.h
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₄
j j' : ι₄
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₁₂ : ι₁₂ := c₁.π c₂ c₁₂ (i₁, i₂)
h₁ : c₁₂.Rel i₁₂ (c₁₂.next i₁₂)
h₂ : ¬c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (c₁.next i₁, i₂), i₃) = j'
⊢ c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (c₁.next i₁, i₂), i₃) = c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (c₁.next i₁, i₂), i₃)
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: case pos.h
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₄
j j' : ι₄
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₁₂ : ι₁₂ := c₁.π c₂ c₁₂ (i₁, i₂)
h₁ : c₁₂.Rel i₁₂ (c₁₂.next i₁₂)
h₂ : ¬c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : c₂.Rel i₂ (c₂.next i₂)
h₄ : c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, c₂.next i₂), i₃) = j'
⊢ c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, c₂.next i₂), i₃)

Tactic:
ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃

Goal state after:
case pos.h
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₄
j j' : ι₄
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₁₂ : ι₁₂ := c₁.π c₂ c₁₂ (i₁, i₂)
h₁ : c₁₂.Rel i₁₂ (c₁₂.next i₁₂)
h₂ : ¬c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = j'
h₃ : c₂.Rel i₂ (c₂.next i₂)
h₄ : c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, c₂.next i₂), i₃) = j'
⊢ c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, c₂.next i₂), i₃) = c₁₂.π c₃ c₄ (c₁.π c₂ c₁₂ (i₁, c₂.next i₂), i₃)
Module: Mathlib.CategoryTheory.ObjectProperty.Orthogonal

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P : ObjectProperty C
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : P.leftOrthogonal X✝
Y : C
f : Y✝ ⟶ Y
hY : P Y
⊢ e.hom ≫ f = 0

Tactic:
exact h _ hY

Goal state after:
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 Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst✝¹ : t.IsLE X n₀
inst✝ : t.IsGE Y n₁
this : t.IsLE ((shiftFunctor C n₀).obj X) 0
⊢ f = 0

Tactic:
have := t.isGE_shift Y n₁ n₀ (n₁ - 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 Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst✝¹ : t.IsLE X n₀
inst✝ : t.IsGE Y n₁
this✝ : t.IsLE ((shiftFunctor C n₀).obj X) 0
this : t.IsGE ((shiftFunctor C n₀).obj Y) (n₁ - n₀)
⊢ f = 0
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.pushouts ≤ T.rlp.llp

Tactic:
exact T.pushouts_le_llp_rlp

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

Goal state before:
pp: case h₂
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.inr ≫ coprod.map P.i₁ (𝟙 A) ≫ ψ = coprod.inr ≫ P'.i ≫ pushout.inr P.i₁ P'.i₀

Tactic:
simp [ψ]

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

Goal state before:
pp: case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : PathObject A
inst✝² : IsFibrant A
P P' : PathObject A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : (P.trans P').P ⟶ P.P ⨯ A := ⋯
⊢ (ψ ≫ prod.map P.p₁ (𝟙 A)) ≫ prod.snd = (pullback.snd P.p₁ P'.p₀ ≫ P'.p) ≫ prod.snd

Tactic:
simp [ψ]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Quotient

Goal state before:
pp: case mk
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
homRel : HomRel C
W : MorphismProperty C
h : homRel.FactorsThroughLocalization W
W' : MorphismProperty (CategoryTheory.Quotient homRel)
hW : W = W'.inverseImage (Quotient.functor homRel)
E : Type u_3
inst✝ : Category.{v_3, u_3} E
L' : CategoryTheory.Quotient homRel ⥤ D
univ : StrictUniversalPropertyFixedTarget L' W' E
F : C ⥤ E
hF : W.IsInvertedBy F
K L : CategoryTheory.Quotient homRel
f✝ : K ⟶ L
f : K.as ⟶ L.as
hf : W' (Quot.mk (HomRel.CompClosure homRel) f)
⊢ IsIso ((CategoryTheory.Quotient.lift homRel F ⋯).map (Quot.mk (HomRel.CompClosure homRel) f))

Tactic:
exact hF _ (by simpa [hW] using! hf)

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

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
P : ObjectProperty C
inst✝² : P.IsTriangulated
t : TStructure C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P.HasInducedTStructure t
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
⊢ t.IsLE (((P.tStructure t).truncLE n₀).obj { obj := T.obj₂, property := h₂ }).obj n₀

Tactic:
← P.tStructure_isLE_iff

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
P : ObjectProperty C
inst✝² : P.IsTriangulated
t : TStructure C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P.HasInducedTStructure t
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
h₂ : P T.obj₂
h₃ : t.IsGE T.obj₃ n₁
⊢ (P.tStructure t).IsLE (((P.tStructure t).truncLE n₀).obj { obj := T.obj₂, property := h₂ }) n₀
Module: Mathlib.Algebra.Homology.DerivedCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K : CochainComplex C ℤ
hK : HomologicalComplex.Acyclic K
L : CochainComplex C ℤ
n : ℤ
hn : L.IsStrictlyGE n
φ : K ⟶ L
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (K.πTruncGE n) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.truncGEMap φ n ≫ inv (L.πTruncGE n)) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map φ

Tactic:
by simp [← Functor.map_comp]

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

Goal state before:
pp: 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
inst✝ : IsTriangulated C
a b : ℤ
X : C
⊢ (t.truncGEπ a).app ((t.truncLT b).obj X) ≫ (t.truncGELTToLTGE a b).app X ≫ (t.truncLTι b).app ((t.truncGE a).obj X) =
    (t.truncLTι b).app X ≫ (t.truncGEπ a).app X

Tactic:
simp [truncGELTToLTGE]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : IsFibrant Y
h✝ : RightHomotopyRel f g
Q : Cylinder X
inst✝ : Q.IsGood
P : PathObject Y := ⋯.choose
h : ⋯.choose.RightHomotopy f g
h' : ⋯.choose.IsGood
sq : CommSq (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
⊢ Q.i₀ ≫ sq.lift ≫ P.p₁ = f

Tactic:
have := coprod.inl ≫= sq.fac_left
      rw [Q.inl_i_assoc, coprod.inl_desc] at this
      simp [reassoc_of% this]

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
⊢ ∀ {X Y : Plus C} (f : X ⟶ Y), Nonempty ((trivialCofibrations (Plus C)).MapFactorizationData (fibrations (Plus C)) f)

Tactic:
by
    intro ⟨K, n, hn⟩ ⟨L, m, hm⟩ ⟨f⟩
    obtain ⟨d, _, _⟩ : ∃ (d : ℤ), K.IsStrictlyGE (d + 1) ∧ L.IsStrictlyGE d :=
      ⟨min (n - 1) m, K.isStrictlyGE_of_ge _ n (by grind),
        L.isStrictlyGE_of_ge _ m (by simp)⟩
    obtain ⟨K', _, i, p, _, _, hp, fac⟩ := cm5a f d
    exact ⟨{
      Z := ⟨K', d, inferInstance⟩
      i := ObjectProperty.homMk i
      p := ObjectProperty.homMk p
      hi :=
        ⟨by rwa [← HomotopicalAlgebra.cofibration_iff, cofibration_iff, Plus.mono_iff],
          by assumption⟩
      hp := hp }⟩

Goal state after:
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 i : ℤ
⊢ { X₁ := (S f n).X (i - 1), X₂ := (mid f n).X i, X₃ := L.X i, f := (↑(mappingCocone.inr (α f n))).v (i - 1) i ⋯,
            g := (π f n).f i, zero := ⋯ }.g ≫
        (mappingCocone.inl (α f n)).v i i ⋯ +
      (mappingCocone.snd (α f n)).v i (i - 1) ⋯ ≫
        { X₁ := (S f n).X (i - 1), X₂ := (mid f n).X i, X₃ := L.X i, f := (↑(mappingCocone.inr (α f n))).v (i - 1) i ⋯,
            g := (π f n).f i, zero := ⋯ }.f =
    𝟙
      { X₁ := (S f n).X (i - 1), X₂ := (mid f n).X i, X₃ := L.X i, f := (↑(mappingCocone.inr (α f n))).v (i - 1) i ⋯,
          g := (π f n).f i, zero := ⋯ }.X₂

Tactic:
simp [mappingCocone.id_X]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Resolution

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
inst✝⁴ : Category.{v_3, u_3} D₁
inst✝³ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝² : R.functor.EssSurj
inst✝¹ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : T.HasRightResolutions
Y₂ : D₂
⊢ Nonempty (B.RightResolution Y₂)

Tactic:
obtain ⟨X₂, ⟨e⟩⟩ := Functor.EssSurj.mem_essImage (F := R.functor) Y₂

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
inst✝⁴ : Category.{v_3, u_3} D₁
inst✝³ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝² : R.functor.EssSurj
inst✝¹ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : T.HasRightResolutions
Y₂ : D₂
X₂ : C₂
e : R.functor.obj X₂ ≅ Y₂
⊢ Nonempty (B.RightResolution Y₂)
Module: Mathlib.CategoryTheory.Localization.Resolution

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
inst✝⁴ : Category.{v_3, u_3} D₁
inst✝³ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝² : R.functor.EssSurj
inst✝¹ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : T.HasLeftResolutions
Y₂ : D₂
⊢ Nonempty (B.LeftResolution Y₂)

Tactic:
obtain ⟨X₂, ⟨e⟩⟩ := Functor.EssSurj.mem_essImage (F := R.functor) Y₂

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
inst✝⁴ : Category.{v_3, u_3} D₁
inst✝³ : Category.{v_4, u_4} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝² : R.functor.EssSurj
inst✝¹ : W₂'.RespectsIso
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : T.HasLeftResolutions
Y₂ : D₂
X₂ : C₂
e : R.functor.obj X₂ ≅ Y₂
⊢ Nonempty (B.LeftResolution Y₂)
Module: Mathlib.CategoryTheory.GuitartExact.KanExtension

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
D : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₃, u₃} C₃
inst✝³ : Category.{v₄, u₄} C₄
inst✝² : Category.{v₅, u₅} D
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
inst✝¹ : ∀ (F : C₁ ⥤ D), L.HasLeftKanExtension F
inst✝ : ∀ (F : C₂ ⥤ D), R.HasLeftKanExtension F
F₁ F₂ : C₂ ⥤ D
τ : F₁ ⟶ F₂
⊢ ((whiskeringLeft C₁ C₂ D).obj T ⋙ L.lan).map τ ≫
      ((L.lanAdjunction D).homEquiv (((whiskeringLeft C₁ C₂ D).obj T).obj F₂)
            ((R.lan ⋙ (whiskeringLeft C₃ C₄ D).obj B).obj F₂)).symm
        (StructuredArrow.hom ((LeftExtension.mk (R.lan.obj F₂) (R.lanUnit.app F₂)).compTwoSquare w)) =
    ((L.lanAdjunction D).homEquiv (((whiskeringLeft C₁ C₂ D).obj T).obj F₁)
            ((R.lan ⋙ (whiskeringLeft C₃ C₄ D).obj B).obj F₁)).symm
        (StructuredArrow.hom ((LeftExtension.mk (R.lan.obj F₁) (R.lanUnit.app F₁)).compTwoSquare w)) ≫
      (R.lan ⋙ (whiskeringLeft C₃ C₄ D).obj B).map τ

Tactic:
dsimp
    refine (Adjunction.homEquiv_naturality_left_symm ..).symm.trans
      (Eq.trans ?_ (Adjunction.homEquiv_naturality_right_symm ..))
    congr 1
    ext X
    have := R.lanUnit.naturality_app (T.obj X) τ
    simp [reassoc_of% this]

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

Goal state before:
pp: C₁ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Abelian C₁
inst✝⁶ : HasDerivedCategory C₁
C₂ : Type u₂
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Abelian C₂
inst✝³ : HasDerivedCategory C₂
F : C₁ ⥤ C₂
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
X : C₁
⊢ F.mapDerivedCategoryFactors.inv.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X) ≫
      (F.mapDerivedCategorySingleFunctor 0).hom.app X =
    DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).hom.app X)

Tactic:
simp [Functor.mapDerivedCategorySingleFunctor, Functor.mapCochainComplexSingleFunctor,
    CochainComplex.singleFunctor, CochainComplex.singleFunctors,
    DerivedCategory.singleFunctorIsoCompQ]

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

Goal state before:
pp: C₁ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Abelian C₁
inst✝⁶ : HasDerivedCategory C₁
C₂ : Type u₂
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Abelian C₂
inst✝³ : HasDerivedCategory C₂
F : C₁ ⥤ C₂
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
X : C₁
⊢ (F.mapDerivedCategorySingleFunctor 0).inv.app X ≫
      F.mapDerivedCategoryFactors.hom.app ((HomologicalComplex.single C₁ (ComplexShape.up ℤ) 0).obj X) =
    DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).inv.app X)

Tactic:
simp [Functor.mapDerivedCategorySingleFunctor, Functor.mapCochainComplexSingleFunctor,
    CochainComplex.singleFunctor, CochainComplex.singleFunctors,
    DerivedCategory.singleFunctorIsoCompQ]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective

Goal state before:
pp: case succ
C : Type u
inst✝¹² : Category.{v, u} C
inst✝¹¹ : Abelian C
D : Type u'
inst✝¹⁰ : Category.{v', u'} D
inst✝⁹ : Abelian D
F : C ⥤ D
inst✝⁸ : F.Additive
inst✝⁷ : PreservesFiniteLimits F
inst✝⁶ : PreservesFiniteColimits F
inst✝⁵ : F.Full
inst✝⁴ : F.Faithful
inst✝³ : HasExt C
inst✝² : HasExt D
inst✝¹ : EnoughProjectives C
inst✝ : F.PreservesProjectiveObjects
Y : C
n : ℕ
hn : ∀ (X : C), Function.Bijective ⇑(F.mapExtAddHom X Y n)
X : C
P : ProjectivePresentation X := Classical.arbitrary (ProjectivePresentation X)
S : ShortComplex C := { X₁ := Limits.kernel P.f, X₂ := P.p, X₃ := X, f := kernel.ι P.f, g := P.f, zero := ⋯ }
this : Projective (S.map F).X₂
⊢ Function.Bijective ⇑(F.mapExtAddHom X Y (n + 1))

Tactic:
have hS : S.ShortExact := { exact := ShortComplex.exact_kernel P.f }

Goal state after:
case succ
C : Type u
inst✝¹² : Category.{v, u} C
inst✝¹¹ : Abelian C
D : Type u'
inst✝¹⁰ : Category.{v', u'} D
inst✝⁹ : Abelian D
F : C ⥤ D
inst✝⁸ : F.Additive
inst✝⁷ : PreservesFiniteLimits F
inst✝⁶ : PreservesFiniteColimits F
inst✝⁵ : F.Full
inst✝⁴ : F.Faithful
inst✝³ : HasExt C
inst✝² : HasExt D
inst✝¹ : EnoughProjectives C
inst✝ : F.PreservesProjectiveObjects
Y : C
n : ℕ
hn : ∀ (X : C), Function.Bijective ⇑(F.mapExtAddHom X Y n)
X : C
P : ProjectivePresentation X := Classical.arbitrary (ProjectivePresentation X)
S : ShortComplex C := { X₁ := Limits.kernel P.f, X₂ := P.p, X₃ := X, f := kernel.ι P.f, g := P.f, zero := ⋯ }
this : Projective (S.map F).X₂
hS : S.ShortExact
⊢ Function.Bijective ⇑(F.mapExtAddHom X Y (n + 1))
Module: Mathlib.Algebra.Homology.HomotopyCategory.KProjective

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K : CochainComplex C ℤ
hK : (HomotopyCategory.subcategoryAcyclic C).leftOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
L : CochainComplex C ℤ
f : K ⟶ L
hL : HomologicalComplex.Acyclic L
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map 0

Tactic:
rw [← HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic] at hL

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K : CochainComplex C ℤ
hK : (HomotopyCategory.subcategoryAcyclic C).leftOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
L : CochainComplex C ℤ
f : K ⟶ L
hL : HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map f = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map 0
Module: Mathlib.Algebra.Homology.Embedding.StupidTrunc

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
inst✝² : HasZeroObject C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝¹ : e.IsRelIff
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst✝ : K.IsStrictlySupported e'
i' : ι'
hi' : ∀ (i : ι''), e'.f i ≠ i'
hi'' : ¬∃ i, e.f i = i'
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
simpa using hi''

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
i j i' j' n : ℕ
x✝⁴ : i ≤ j
x✝³ : i' ≤ j'
x✝² : i ≤ i'
x✝¹ : j ≤ j'
x✝ : j' ≤ n
S : ComposableArrows C n
⊢ ((functorArrows C i j n ⋯ ⋯).obj S).map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ S.map' j j' x✝¹ x✝ =
    S.map' i i' x✝² ⋯ ≫ ((functorArrows C i' j' n ⋯ ⋯).obj S).map' 0 1 homMk₁._proof_4 homMk₁._proof_5

Tactic:
by simp [← Functor.map_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Reduced

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
inst✝² : Preadditive C
inst✝¹ : Preadditive A
inst✝ : ι.Additive
X : A
⊢ (𝟙 (Λ.F.obj X) - Λ.F.map 0) ≫ (𝟙 (Λ.F.obj X) - Λ.F.map 0) = 𝟙 (Λ.F.obj X) - Λ.F.map 0

Tactic:
by simp [← Functor.map_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Reduced

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
inst✝² : Preadditive C
inst✝¹ : Preadditive A
inst✝ : ι.Additive
X Y : A
f : X ⟶ Y
⊢ { X := Λ.F.obj X, p := 𝟙 (Λ.F.obj X) - Λ.F.map 0, idem := ⋯ }.p ≫
      (Λ.F.map f - Λ.F.map 0) ≫ { X := Λ.F.obj Y, p := 𝟙 (Λ.F.obj Y) - Λ.F.map 0, idem := ⋯ }.p =
    Λ.F.map f - Λ.F.map 0

Tactic:
by simp [← Functor.map_comp]

Goal state after: