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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
⊢ ∀ (a b : Cocycle K L n),
    a ≈ b →
      SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm a) =
        SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm b)

Tactic:
let := HasDerivedCategory.standard C
    intro y₁ y₂ h
    refine (SmallShiftedHom.equiv _ DerivedCategory.Q).injective ?_
    simp only [SmallShiftedHom.equiv_mk, ShiftedHom.map]
    rw [cancel_mono, DerivedCategory.Q_map_eq_of_homotopy]
    apply HomotopyCategory.homotopyOfEq
    rw [← toHom_mk, ← toHom_mk]
    congr 1
    exact Quotient.sound h

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
s : Cofork ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯)) 0
l : (CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt ⟶ s.pt
hl : Cofork.π (CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯) ≫ l = s.π
y : Cocycle K L m
⊢ (AddCommGrpCat.Hom.hom l) (CohomologyClass.mk y) =
    (AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (CohomologyClass.descAddMonoidHom (AddCommGrpCat.Hom.hom s.π) ⋯)))
      (CohomologyClass.mk y)

Tactic:
simpa using! ConcreteCategory.congr_hom hl y

Goal state after:
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 ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hL : HomologicalComplex.Acyclic L
m : ℤ
hm : m + 1 = n
β : Cochain L L (-1)
hβ : δ (-1) 0 β = ↑(Cocycle.ofHom (𝟙 L))
⊢ δ m n ((↑z).comp β ⋯) = ↑z

Tactic:
simp [δ_comp z.1 β _ _ 0 _ hm rfl (by simp), hβ]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithFibrations C
inst✝¹ : (fibrations C).IsStableUnderRetracts
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ (trivialFibrations C).IsStableUnderRetracts

Tactic:
by
  dsimp [trivialFibrations]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ : C
P✝ : Precylinder X✝
Y✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : Precylinder X
f g : X ⟶ Y
h : Q.LeftHomotopy f g
⊢ (Q.map P.ι).i₁ ≫ h.h.hom = g.hom

Tactic:
by
        dsimp
        simp only [← h.h₁, ObjectProperty.FullSubcategory.comp_hom]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Y✝ : C
P✝ : PrepathObject Y✝
X✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : PrepathObject Y
f g : X ⟶ Y
h : Q.RightHomotopy f g
⊢ h.h.hom ≫ (Q.map P.ι).p₁ = g.hom

Tactic:
by
        dsimp
        simp only [← h.h₁, ObjectProperty.FullSubcategory.comp_hom]

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

Goal state before:
pp: case mk
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : CategoryWithWeakEquivalences C
P : PathObject Y
inst✝¹ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝ : (weakEquivalences C).ContainsIdentities
f₀ f₁ : X ⟶ Y
h✝ : X ⟶ P.P
h₀✝ : h✝ ≫ P.p₀ = f₀
h₁✝ : h✝ ≫ P.p₁ = f₁
⊢ WeakEquivalence f₀ ↔ WeakEquivalence f₁

Tactic:
grind [weakEquivalence_postcomp_iff]

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

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
n : ℤ
⊢ (t.truncLE n).Additive

Tactic:
by
  dsimp only [truncLE]
  infer_instance

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

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
a b : ℤ
h : a + 1 = b
⊢ IsIso ((t.truncLE a).map f) ↔
    ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLEι a).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z b

Tactic:
subst h
  apply isIso_truncLT_map_iff

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

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : A.IsTriangulated
inst✝¹ : B.IsTriangulated
inst✝ : B.IsClosedUnderIsomorphisms
hA : ∀ ⦃X Y : Cᵒᵖ⦄ (s : X ⟶ Y), A.op X → B.op.trW s → ∃ Z s' b, A.op Z ∧ (A.op ⊓ B.op).trW s' ∧ s ≫ b = s'
X Y : C
s : X ⟶ Y
hY : A Y
hs : B.trW s
⊢ B.op.trW s.op

Tactic:
simpa [trW_op_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: case refine_1.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ biprod.inl ≫ (biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ = biprod.inl ≫ 0

Tactic:
simp [reassoc_of% w₁]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ biprod.inr ≫ (biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ = biprod.inr ≫ 0

Tactic:
simp [reassoc_of% σ₁.s_g, w₂]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ (biprod.inl ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂, zero := ⋯ }.f ≫
          (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
      biprod.snd =
    (biprod.inl ≫
        𝟙
          { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z, f := biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, g := g₁ ≫ g₂,
              zero := ⋯ }.X₁) ≫
      biprod.snd

Tactic:
simp [reassoc_of% w₁]

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5b

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K L : CochainComplex C ℤ
⊢ degreewiseEpiWithInjectiveKernel (p K L)

Tactic:
by
  intro n
  rw [epiWithInjectiveKernel_iff]
  refine ⟨(mappingCone (𝟙 (I K))).X n, inferInstance,
    (biprod.inl :_ ⟶ (mappingCone (𝟙 (I K))) ⊞ L).f n, ?_,
    (biprod.fst : (mappingCone (𝟙 (I K))) ⊞ L ⟶ _).f n,
    (biprod.inr :_ ⟶ (mappingCone (𝟙 (I K))) ⊞ L).f n, ?_, ?_, ?_⟩
  all_goals simp [← HomologicalComplex.comp_f, ← HomologicalComplex.add_f_apply]

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

Goal state before:
pp: case left
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsFibrant Z
f : X ⟶ Y
inst✝¹ : Cofibration f
inst✝ : WeakEquivalence f
⊢ Function.Injective fun g ↦ g.precomp f

Tactic:
intro f₀ f₁ h
    obtain ⟨f₀, rfl⟩ := f₀.mk_surjective
    obtain ⟨f₁, rfl⟩ := f₁.mk_surjective
    simp only [precomp_mk, mk_eq_mk_iff] at h
    obtain ⟨P, _, ⟨h⟩⟩ := h.exists_good_pathObject
    have sq : CommSq h.h f P.p (prod.lift f₀ f₁) := { }
    rw [mk_eq_mk_iff]
    exact ⟨P,
      ⟨{h := sq.lift
        h₀ := by
          have := sq.fac_right =≫ prod.fst
          rwa [Category.assoc, P.p_fst, prod.lift_fst] at this
        h₁ := by
          have := sq.fac_right =≫ prod.snd
          rwa [Category.assoc, P.p_snd, prod.lift_snd] at this }⟩⟩

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : HoCat C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences (HoCat C))
X : FibrantObject C
⊢ IsIso ((Functor.whiskerRight HoCat.ιCompResolutionNatTrans L).app X)

Tactic:
apply Localization.inverts L (weakEquivalences _)

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : HoCat C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences (HoCat C))
X : FibrantObject C
⊢ weakEquivalences (HoCat C) (HoCat.ιCompResolutionNatTrans.app X)
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
H : Type u_5
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₂
inst✝¹ : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
Φ : LocalizerMorphism W₁ W₂
inst✝ : Φ.HasRightResolutions
⊢ Φ.op.HasLeftResolutions

Tactic:
← hasRightResolutions_iff_op

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
H : Type u_5
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₂
inst✝¹ : Category.{v_5, u_5} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₁' : MorphismProperty D₁
W₂' : MorphismProperty D₂
Φ : LocalizerMorphism W₁ W₂
inst✝ : Φ.HasRightResolutions
⊢ Φ.HasRightResolutions
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences C)
X : C
⊢ IsIso ((HoCat.resolutionCompToLocalizationNatTrans L).app X)

Tactic:
apply Localization.inverts L (weakEquivalences _)

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences C)
X : C
⊢ weakEquivalences C (HoCat.iResolutionObj X)
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case refine_2
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
⊢ { X₁ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₂.homology i,
        X₂ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₃.homology i,
        X₃ := { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.X₁.homology (i + 1),
        f := homologyMap { X₁ := K, X₂ := L, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.g i,
        g := ⋯.δ i (i + 1) ⋯, zero := ⋯ }.g =
    0

Tactic:
· rw [← ((shortExact f).homology_exact₁ i (i + 1) (by simp)).mono_g_iff]
    by_cases hi' : i + 1 < n
    · have := hf (i + 1) (by lia)
      infer_instance
    · obtain rfl : n = i + 1 := by lia
      infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.StructuredArrowRightwards g
φ : f₁ ⟶ f₂
⊢ (w.structuredArrowDownwards X₂).map (StructuredArrow.homMk (StructuredArrow.Hom.right φ).left ⋯) ≫
      (CostructuredArrow.mk (StructuredArrow.homMk (StructuredArrow.right f₂).hom ⋯)).hom =
    (CostructuredArrow.mk (StructuredArrow.homMk (StructuredArrow.right f₁).hom ⋯)).hom

Tactic:
ext; exact CostructuredArrow.w φ.right

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

Goal state before:
pp: case mp
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₂
F : W₁.Localization ⥤ W₂.Localization := ⋯
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := ⋯
e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := ⋯
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
⊢ Φ.IsLeftDerivabilityStructure → Φ.op.IsRightDerivabilityStructure

pp: case mpr
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₂
F : W₁.Localization ⥤ W₂.Localization := ⋯
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := ⋯
e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := ⋯
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
⊢ Φ.op.IsRightDerivabilityStructure → Φ.IsLeftDerivabilityStructure

Tactic:
· rintro ⟨_, _⟩
    rwa [Φ.op.isRightDerivabilityStructure_iff _ _ _ e', eq]

Goal state after:
case mpr
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₂
F : W₁.Localization ⥤ W₂.Localization := ⋯
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ F := ⋯
e' : Φ.functor.op ⋙ W₂.Q.op ≅ W₁.Q.op ⋙ F.op := ⋯
eq : TwoSquare.GuitartExact e'.hom ↔ TwoSquare.GuitartExact e.inv
⊢ Φ.op.IsRightDerivabilityStructure → Φ.IsLeftDerivabilityStructure
Module: Mathlib.CategoryTheory.GuitartExact.KanExtension

Goal state before:
pp: case e_6
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₂
X : C₁
⊢ (T.whiskerLeft τ ≫
          T.whiskerLeft (R.lanUnit.app F₂) ≫
            (T.associator R (R.lan.obj F₂)).inv ≫
              whiskerRight w.natTrans (R.lan.obj F₂) ≫ (L.associator B (R.lan.obj F₂)).hom).app
      X =
    ((T.whiskerLeft (R.lanUnit.app F₁) ≫
            (T.associator R (R.lan.obj F₁)).inv ≫
              whiskerRight w.natTrans (R.lan.obj F₁) ≫ (L.associator B (R.lan.obj F₁)).hom) ≫
          ((whiskeringLeft C₁ C₃ D).obj L).map (B.whiskerLeft (R.lan.map τ))).app
      X

Tactic:
have := R.lanUnit.naturality_app (T.obj X) τ

Goal state after:
case e_6
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₂
X : C₁
this :
  ((𝟭 (C₂ ⥤ D)).map τ).app (T.obj X) ≫ (R.lanUnit.app F₂).app (T.obj X) =
    (R.lanUnit.app F₁).app (T.obj X) ≫ ((R.lan ⋙ (whiskeringLeft C₂ C₄ D).obj R).map τ).app (T.obj X)
⊢ (T.whiskerLeft τ ≫
          T.whiskerLeft (R.lanUnit.app F₂) ≫
            (T.associator R (R.lan.obj F₂)).inv ≫
              whiskerRight w.natTrans (R.lan.obj F₂) ≫ (L.associator B (R.lan.obj F₂)).hom).app
      X =
    ((T.whiskerLeft (R.lanUnit.app F₁) ≫
            (T.associator R (R.lan.obj F₁)).inv ≫
              whiskerRight w.natTrans (R.lan.obj F₁) ≫ (L.associator B (R.lan.obj F₁)).hom) ≫
          ((whiskeringLeft C₁ C₃ D).obj L).map (B.whiskerLeft (R.lan.map τ))).app
      X
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
⊢ T.IsRightDerivabilityStructure ↔ B.IsRightDerivabilityStructure

Tactic:
let e : T.op.functor ⋙ R.op.functor ≅ L.op.functor ⋙ B.op.functor := NatIso.op iso.symm
  simp only [isRightDerivabilityStructure_iff_op,
    isLeftDerivabilityStructure_iff_of_equivalences e]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
inst✝⁴ : HasExt C
K L : CochainComplex C ℤ
a b : ℤ
inst✝³ : K.IsGE a
inst✝² : K.IsLE a
inst✝¹ : L.IsGE b
inst✝ : L.IsLE b
this : (C : Type u) → [inst : Category.{v, u} C] → [inst_1 : Abelian C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
X : C
eX : Q.obj K ≅ (singleFunctor C a).obj X
Y : C
eY : Q.obj L ≅ (singleFunctor C b).obj Y
⊢ ∀ (a b : ℤ),
    Small.{w, max u v}
      ((shiftFunctor (DerivedCategory C) a).obj (Q.obj K) ⟶ (shiftFunctor (DerivedCategory C) b).obj (Q.obj L))

Tactic:
exact fun p q ↦ small_of_injective (f := fun φ ↦
    ((singleFunctors C).shiftIso p (a - p) a (by simp)).inv.app X ≫
      eX.inv⟦p⟧' ≫ φ ≫ eY.hom⟦q⟧' ≫
        ((singleFunctors C).shiftIso q (b - q) b (by simp)).hom.app Y)
    (fun φ₁ φ₂ h ↦ by simpa [cancel_epi, cancel_mono] using h)

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

Goal state before:
pp: 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
inst✝ : EnoughInjectives C
⊢ (localizerMorphism C).IsRightDerivabilityStructure

Tactic:
rw [LocalizerMorphism.isRightDerivabilityStructure_iff_of_equivalences
    (T := localizerMorphism C) (B := FibrantObject.localizerMorphism (Plus C))
    (R := .id _) (L := fibrantObjectLocalizerMorphism C) (Iso.refl _)]

Goal state after:
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
inst✝ : EnoughInjectives C
⊢ (FibrantObject.localizerMorphism (Plus C)).IsRightDerivabilityStructure
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

Goal state before:
pp: 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✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
⊢ F.mapDerivedCategory.map (triangleOfSESδ hS) =
    F.mapDerivedCategoryFactors.hom.app S.X₃ ≫
      triangleOfSESδ ⋯ ≫
        (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
          (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)

Tactic:
have := CochainComplex.mappingCone.quasiIso_descShortComplex hS

Goal state after:
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✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map (triangleOfSESδ hS) =
    F.mapDerivedCategoryFactors.hom.app S.X₃ ≫
      triangleOfSESδ ⋯ ≫
        (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
          (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
⊢ (F.map X.d ≫ η.app X.obj) ≫ (F ⋙ shiftFunctor D 1).map X.d ≫ (shiftFunctor D 1).map (η.app X.obj) = 0

Tactic:
slice_lhs 2 3 => rw [← η.naturality X.d]

Goal state after:
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
⊢ F.map X.d ≫
      ((shiftFunctor C 1 ⋙ F).map X.d ≫ η.app ((shiftFunctor C 1).obj X.obj)) ≫ (shiftFunctor D 1).map (η.app X.obj) =
    0
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : ¬k = i₀
hk₁ : k = i₁
⊢ (double f hi₀₁).X k = (double f hi₀₁).X i₁

Tactic:
hk₁

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : ¬k = i₀
hk₁ : k = i₁
⊢ (double f hi₀₁).X i₁ = (double f hi₀₁).X i₁
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : ¬k = i₀
hk₁ : k = i₁
⊢ K.X i₁ = K.X k

Tactic:
hk₁

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : ¬k = i₀
hk₁ : k = i₁
⊢ K.X i₁ = K.X i₁
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 : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
⊢ ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (φ.app P.X).f) ≫ ((obj G).obj P).p = (F.map P.p).f ≫ (φ.app P.X).f

Tactic:
by
        have h := φ.naturality P.p
        have h' := F.congr_map P.idem
        simp only [hom_ext_iff, Karoubi.comp_f, F.map_comp] at h h'
        simp only [obj_obj_p, assoc, ← h]
        slice_lhs 1 3 => rw [h', h']

Goal state after: