mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
hab : a ≤ b
⊢ Δ[n] _⦋1⦌

Tactic:
refine objMk ⟨![a, b], ?_⟩

Goal state after:
n : ℕ
a b : Fin (n + 1)
hab : a ≤ b
⊢ Monotone ![a, b]
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
S : ↑{S | #S = d + 1}
i : Fin (d + 1)
⊢ ↑(nonDegenerateEquiv'.symm S) i ∈ ↑S

Tactic:
by
  obtain ⟨f, rfl⟩ := nonDegenerateEquiv'.{u}.surjective S
  dsimp [nonDegenerateEquiv']
  simp only [Equiv.ofBijective_symm_apply_apply, Finset.mem_image, Finset.mem_univ, true_and]
  exact ⟨i, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : SimplexCategory
d : SimplexCategoryᵒᵖ
⊢ Finite ((stdSimplex.obj n).obj d)

Tactic:
objEquiv.finite_iff

Goal state after:
n : SimplexCategory
d : SimplexCategoryᵒᵖ
⊢ Finite (unop d ⟶ n)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case mpr
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ Mono (yonedaEquiv.symm x) → IsIso (toOfSimplex x)

Tactic:
intro h
    have := mono_of_mono_fac (toOfSimplex_ι x)
    apply isIso_of_mono_of_epi

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c
inst✝² : TotalComplexShape c₂ c₃ c₂₃
inst✝¹ : TotalComplexShape c₁ c₂₃ c
inst✝ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c
i₁ : I₁
i₂ : I₂
i₃ : I₃
⊢ c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₁ c₃ c₂₃ (i₂, i₃) =
    c₁₂.ε₁ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)

Tactic:
by
  apply Associative.ε₂_ε₁

Goal state after:
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
⊢ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h ≫ (K.totalShift₂Iso y).hom.f n =
    (a * y).negOnePow •
      (K.shiftFunctor₂XXIso a b y (b + y) ⋯).hom ≫
        K.ιTotal (up ℤ) a (b + y) (n + y) ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv

Tactic:
dsimp [totalShift₂Iso, totalShift₂XIso]

Goal state after:
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
⊢ (((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h ≫
      ((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) (n + y) ⋯) =
    (a * y).negOnePow • 𝟙 ((K.X a).X (b + y)) ≫ K.ιTotal (up ℤ) a (b + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))
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
⊢ (s.ι ≫ biprod.fst) ≫ f = (s.ι ≫ biprod.snd) ≫ g

Tactic:
rw [← sub_eq_zero, assoc, assoc, ← Preadditive.comp_sub]

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
⊢ s.ι ≫ (biprod.fst ≫ f - biprod.snd ≫ g) = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1))
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : ↑(X n)), (↑(φ n x)).EqUpTo (↑x) (p₀ + ↑n)
x₀ : ↑(X 0)
n₁ n₂ : ℕ
h : n₁ ≤ n₂
⊢ (↑(sequence φ x₀ n₁)).EqUpTo (↑(sequence φ x₀ n₂)) (p₀ + ↑n₁)

Tactic:
by
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h
  clear h
  induction k generalizing n₁ with
  | zero => intro _ _ _ _; simp
  | succ k hk =>
    intro p q hpq hp
    rw [hk n₁ p q hpq hp, ← hφ (n₁ + k) (sequence φ x₀ (n₁ + k)) p q hpq (by lia)]
    dsimp [sequence]

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

Goal state before:
pp: case pos.h
C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
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_6, u_4} 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✝¹² : G₂₃.PreservesZeroMorphisms
inst✝¹¹ : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹⁰ : F.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : 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 ι₂₃
c₄ : ComplexShape ι₄
inst✝⁷ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁶ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁵ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁴ : TotalComplexShape c₁ c₂₃ c₄
inst✝³ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝² : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝¹ : DecidableEq ι₂₃
inst✝ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
h₁ : c₁.Rel i₁ (c₁.next i₁)
h₂ : c₁.π c₂₃ c₄ (c₁.next i₁, c₂.π c₃ c₂₃ (i₂, i₃)) = j'
⊢ c₁.r c₂ c₃ c₁₂ c₄ (c₁.next i₁, i₂, i₃) = j'

Tactic:
rw [← h₂, ← ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄]
        rfl

Goal state after:
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
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
⊢ h.ofExtend.extend e = h

Tactic:
ext i' j'

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
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i' j' : ι'
⊢ (h.ofExtend.extend e).hom i' j' = h.hom i' j'
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
L : CochainComplex C ℤ
d : ℤ
inst✝¹ : L.IsStrictlyGE d
inst✝ : ∀ (n : ℤ), Injective (L.X n)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : ℕ → Set (Cochain K L (-1)) := fun n ↦ {α | (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) (↑n + d - 1)}
x₀ : ↑(X 0) := ⟨0, ⋯⟩
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1)) := fun n α ↦ ⟨↑α + Cochain.single ⋯.choose (-1), ⋯⟩
hφ : ∀ (k : ℕ) (x : ↑(X k)), (↑(φ k x)).EqUpTo (↑x) (d + ↑k)
n : ℤ
k₀ : ℕ := (n - d + 1).toNat
⊢ (Cochain.ofHom f).v n n ⋯ = (δ (-1) 0 (limitSequence φ hφ x₀)).v n n ⋯

Tactic:
rw [← (sequence φ x₀ k₀).2 n n (add_zero n) (by lia),
      δ_v (-1) 0 (neg_add_cancel 1) _ n n (by lia) (n - 1) (n + 1) rfl (by lia),
      δ_v (-1) 0 (neg_add_cancel 1) _ n n (by lia) (n - 1) (n + 1) rfl (by lia),
      limitSequence_eqUpTo φ hφ x₀ k₀ n (n - 1) (by lia) (by lia),
      limitSequence_eqUpTo φ hφ x₀ k₀ (n + 1) n (by lia) (by lia)]

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

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
hX : ∀ i < n, IsZero ((homologyFunctor C i).obj X)
⊢ X.IsGE n

Tactic:
have : (Q.objPreimage X).IsGE n := by
      rw [CochainComplex.isGE_iff]
      intro i hi
      rw [HomologicalComplex.exactAt_iff_isZero_homology]
      apply (hX i hi).of_iso
      exact (homologyFunctorFactors C i).symm.app _ ≪≫
        (homologyFunctor C i).mapIso (Q.objObjPreimageIso X)

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
hX : ∀ i < n, IsZero ((homologyFunctor C i).obj X)
this : (Q.objPreimage X).IsGE n
⊢ X.IsGE n
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 : DerivedCategory C
n i : ℤ
hi : i < n
hX : X.IsGE n
⊢ IsZero ((homologyFunctor C i).obj X)

Tactic:
rw [isGE_iff] at hX
  exact hX i hi

Goal state after:
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 : ℤ
⊢ ((singleFunctor C n).obj X).IsGE n

Tactic:
let e := (singleFunctorIsoCompQ C n).app X
  dsimp only [Functor.comp_obj] at e
  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)
⊢ (fibrations C).IsStableUnderBaseChange

Tactic:
rw [← trivialCofibrations_rlp]
  infer_instance

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)
⊢ (fibrations C).IsMultiplicative

Tactic:
rw [← trivialCofibrations_rlp]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : Cylinder X
h : P.LeftHomotopy f g
⊢ AreEqualizedByLocalization (weakEquivalences C) f g

Tactic:
let L := (weakEquivalences C).Q

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : Cylinder X
h : P.LeftHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
⊢ AreEqualizedByLocalization (weakEquivalences C) f g
Module: Mathlib.CategoryTheory.Localization.OfQuotient

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
inst✝¹ : L.EssSurj
inst✝ : L.Full
W : MorphismProperty C
hW : W.IsInvertedBy L
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.ι
⊢ L.IsLocalization W

Tactic:
← Functor.IsLocalization.op_iff

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
inst✝¹ : L.EssSurj
inst✝ : L.Full
W : MorphismProperty C
hW : W.IsInvertedBy L
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.ι
⊢ L.op.IsLocalization W.op
Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : PathObject Y
h : P.RightHomotopy f g
⊢ AreEqualizedByLocalization (weakEquivalences C) f g

Tactic:
let L := (weakEquivalences C).Q

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : PathObject Y
h : P.RightHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
⊢ AreEqualizedByLocalization (weakEquivalences C) f g
Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h✝¹ : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
P : PathObject Y
left✝ : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject Z
h✝ : Q.IsVeryGood
sq : CommSq (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
⊢ (h.h ≫ sq.lift) ≫ Q.p₁ = g ≫ p

Tactic:
by
        have := sq.fac_right =≫ prod.snd
        simp only [Category.assoc, prod.lift_snd, Q.p_snd] at this
        simp [this]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{?u.6, u_1} C
inst✝⁷ : Category.{?u.9, u_2} D
inst✝⁶ : Category.{?u.12, u_3} E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝² : G.CommShift A
inst✝¹ : G.Full
inst✝ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
a : A
X : C
⊢ (lift.shiftIso hΦ 0 a a ⋯).hom.app X = ((Φ a).isoWhiskerLeft (shiftFunctorZero D A)).hom.app X

Tactic:
apply G.map_injective

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{?u.6, u_1} C
inst✝⁷ : Category.{?u.9, u_2} D
inst✝⁶ : Category.{?u.12, u_3} E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝² : G.CommShift A
inst✝¹ : G.Full
inst✝ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
a : A
X : C
⊢ G.map ((lift.shiftIso hΦ 0 a a ⋯).hom.app X) = G.map (((Φ a).isoWhiskerLeft (shiftFunctorZero D A)).hom.app X)
Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{?u.6, u_1} C
inst✝⁷ : Category.{?u.9, u_2} D
inst✝⁶ : Category.{?u.12, u_3} E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝² : G.CommShift A
inst✝¹ : G.Full
inst✝ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (lift.shiftIso hΦ (m + n) a a'' ⋯).hom.app X =
    ((Φ a'').isoWhiskerLeft (shiftFunctorAdd D m n) ≪≫
            ((Φ a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
              isoWhiskerRight (lift.shiftIso hΦ m a' a'' ha'') (shiftFunctor D n) ≪≫
                lift.shiftIso hΦ n a a' ha').hom.app
      X

Tactic:
apply G.map_injective

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{?u.6, u_1} C
inst✝⁷ : Category.{?u.9, u_2} D
inst✝⁶ : Category.{?u.12, u_3} E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝² : G.CommShift A
inst✝¹ : G.Full
inst✝ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ G.map ((lift.shiftIso hΦ (m + n) a a'' ⋯).hom.app X) =
    G.map
      (((Φ a'').isoWhiskerLeft (shiftFunctorAdd D m n) ≪≫
              ((Φ a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
                isoWhiskerRight (lift.shiftIso hΦ m a' a'' ha'') (shiftFunctor D n) ≪≫
                  lift.shiftIso hΦ n a a' ha').hom.app
        X)
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D₁
inst✝¹ : Category.{v_4, u_4} D₂
A B : ObjectProperty Cᵒᵖ
inst✝ : A.IsVerdierRightLocalizing B
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hX : A.unop X✝
hY : B.unop Y✝
⊢ ∃ Z a b, A.unop Z ∧ B.unop Z ∧ a ≫ b = f

Tactic:
obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac f.op hY hX

Goal state after:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D₁
inst✝¹ : Category.{v_4, u_4} D₂
A B : ObjectProperty Cᵒᵖ
inst✝ : A.IsVerdierRightLocalizing B
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hX : A.unop X✝
hY : B.unop Y✝
Z : Cᵒᵖ
a : op Y✝ ⟶ Z
b : Z ⟶ op X✝
h₁ : A Z
h₂ : B Z
fac : a ≫ b = f.op
⊢ ∃ Z a b, A.unop Z ∧ B.unop Z ∧ a ≫ b = f
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
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
⊢ t.liftTruncLT m₁ (b - 1) b ⋯ ≫ (t.truncLTι b).app ((t.truncGE a).obj X) =
    (t.truncGELTToLTGE a b).app X ≫ (t.truncLTι b).app ((t.truncGE a).obj X)

Tactic:
by dsimp; exact t.from_truncGE_obj_ext (by simpa using H.comm₁)

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 ℤ
inst✝ : EnoughInjectives C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi : i ≤ n₀
⊢ QuasiIsoAt (π K L n₁) i

Tactic:
by
  obtain (hi | rfl) := hi.lt_or_eq
  · rw [quasiIsoAt_iff' _ (i - 1) i (i + 1) (by simp) (by simp)]
    let φ := (shortComplexFunctor' C _ (i - 1) i (i + 1)).map (π K L n₁)
    have : IsIso φ.τ₁ := isIso_π_f ..
    have : IsIso φ.τ₂ := isIso_π_f ..
    have : IsIso φ.τ₃ := isIso_π_f ..
    exact ShortComplex.quasiIso_of_epi_of_isIso_of_mono φ
  · rw [quasiIsoAt_iff_isIso_homologyMap]
    have : homologyMap (biprod.inl : _ ⟶ mid K L n₁) i = 0 :=
      (ShortComplex.isZero_homology_of_isZero_X₂ _
        (isZero_single_obj_X (.up ℤ) _ _ _ (by lia))).eq_of_src _ _
    refine ⟨homologyMap (σ K L n₁) i, ?_, ?_⟩
    · simp [← homologyMap_id, ← biprod.total, homologyMap_comp, this]
    · simp [← homologyMap_comp, homologyMap_id]

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 : ℤ
this✝¹ : IsIso ((S f n).homologyπ n)
this✝ : Mono (homologyπ ((cokernel f).truncGE n) n ≫ homologyMap (p f n) n)
this : IsIso (homologyπ ((cokernel f).truncGE n) n)
⊢ Mono (homologyMap (p f n) n)

Tactic:
← IsIso.inv_hom_id_assoc ((truncGE (cokernel f) n).homologyπ n) (homologyMap (p f n) n)

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 : ℤ
this✝¹ : IsIso ((S f n).homologyπ n)
this✝ : Mono (homologyπ ((cokernel f).truncGE n) n ≫ homologyMap (p f n) n)
this : IsIso (homologyπ ((cokernel f).truncGE n) n)
⊢ Mono (inv (homologyπ ((cokernel f).truncGE n) n) ≫ homologyπ ((cokernel f).truncGE n) n ≫ homologyMap (p f n) n)
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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
i : ℤ
hi : i < n
⊢ ExactAt (cokernel f) i

Tactic:
exactAt_iff_isZero_homology

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
i : ℤ
hi : i < n
⊢ IsZero (homology (cokernel f) i)
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences

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 D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁷ : W₂'.RespectsIso
inst✝⁶ : L.IsLocalizedEquivalence
inst✝⁵ : R.IsLocalizedEquivalence
inst✝⁴ : R.functor.EssSurj
inst✝³ : L.functor.EssSurj
inst✝² : R.functor.Full
inst✝¹ : R.IsInduced
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
inst✝ : TwoSquare.GuitartExact iso.inv
⊢ T.IsLeftDerivabilityStructure ↔ B.IsLeftDerivabilityStructure

Tactic:
by
  refine ⟨fun _ ↦ isLeftDerivabilityStructure_of_isLocalizedEquivalence iso, fun _ ↦ ?_⟩
  have : T.HasLeftResolutions := fun X₂ ↦ by
    let ρ : B.LeftResolution (R.functor.obj X₂) := Classical.arbitrary _
    exact ⟨{
      X₁ := L.functor.objPreimage ρ.X₁
      w :=
        R.functor.preimage (iso.hom.app _ ≫
          B.functor.map (L.functor.objObjPreimageIso ρ.X₁).hom ≫ ρ.w)
      hw := by
        simp only [← R.inverseImage_eq, Functor.comp_obj,
          MorphismProperty.inverseImage_iff, Functor.map_preimage]
        refine (W₂'.arrow_mk_iso_iff ?_).2 ρ.hw
        exact Arrow.isoMk (iso.app _ ≪≫ B.functor.mapIso (L.functor.objObjPreimageIso ρ.X₁))
          (Iso.refl _) }⟩
  let F := B.localizedFunctor W₁'.Q W₂'.Q
  let e' := CatCommSq.iso B.functor W₁'.Q W₂'.Q F
  let e : T.functor ⋙ R.functor ⋙ W₂'.Q ≅ (L.functor ⋙ W₁'.Q) ⋙ F :=
    (Functor.associator _ _ _).symm ≪≫ Functor.isoWhiskerRight iso _ ≪≫
      Functor.associator _ _ _ ≪≫
      Functor.isoWhiskerLeft _ e' ≪≫ (Functor.associator _ _ _).symm
  have he' : TwoSquare.GuitartExact e'.inv := inferInstance
  have : TwoSquare.hComp iso.inv e'.inv = e.inv := by ext; simp [e]
  rw [T.isLeftDerivabilityStructure_iff (L.functor ⋙ W₁'.Q)
    (R.functor ⋙ W₂'.Q) F e, ← this]
  infer_instance

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

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 D₁
W₂ : MorphismProperty C₂
W₂' : MorphismProperty D₂
T : LocalizerMorphism W₁ W₂
L : LocalizerMorphism W₁ W₁'
R : LocalizerMorphism W₂ W₂'
B : LocalizerMorphism W₁' W₂'
inst✝⁵ : W₁'.RespectsIso
inst✝⁴ : W₂'.RespectsIso
inst✝³ : L.IsInduced
inst✝² : L.functor.IsEquivalence
inst✝¹ : R.IsInduced
inst✝ : R.functor.IsEquivalence
iso : T.functor ⋙ R.functor ≅ L.functor ⋙ B.functor
x✝ : B.IsLeftDerivabilityStructure
e : B.functor ⋙ R.inv.functor ≅ L.inv.functor ⋙ T.functor :=
  (B.functor ⋙ R.inv.functor).leftUnitor.symm ≪≫
    isoWhiskerRight L.functor.asEquivalence.counitIso.symm (B.functor ⋙ R.inv.functor) ≪≫
      L.functor.asEquivalence.inverse.associator L.functor.asEquivalence.functor (B.functor ⋙ R.inv.functor) ≪≫
        L.functor.asEquivalence.inverse.isoWhiskerLeft
            (L.functor.asEquivalence.functor.associator B.functor R.inv.functor).symm ≪≫
          L.functor.asEquivalence.inverse.isoWhiskerLeft (isoWhiskerRight iso.symm R.inv.functor) ≪≫
            L.functor.asEquivalence.inverse.isoWhiskerLeft (T.functor.associator R.functor R.inv.functor) ≪≫
              L.functor.asEquivalence.inverse.isoWhiskerLeft
                  (T.functor.isoWhiskerLeft R.functor.asEquivalence.unitIso.symm) ≪≫
                (L.functor.asEquivalence.inverse.associator T.functor (𝟭 C₂)).symm ≪≫
                  (L.functor.asEquivalence.inverse ⋙ T.functor).rightUnitor
this✝ : W₁.RespectsIso
this : W₂.RespectsIso
⊢ T.IsLeftDerivabilityStructure

Tactic:
exact isLeftDerivabilityStructure_of_equivalences e

Goal state after: