mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Predicate

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
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
⊢ (whiskeringLeftFunctor' L W E).Faithful

Tactic:
rw [whiskeringLeftFunctor'_eq]

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
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
⊢ (whiskeringLeftFunctor L W E ⋙ inducedFunctor ObjectProperty.FullSubcategory.obj).Faithful
Module: Mathlib.CategoryTheory.CatCommSq

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (B.counitIso.inv.app (R.obj (T.functor.obj X)) ≫
        B.functor.map
            (B.inverse.map (R.map (T.counitIso.inv.app (T.functor.obj X))) ≫
              B.inverse.map ((iso T.functor L R B.functor).hom.app (T.inverse.obj (T.functor.obj X))) ≫
                B.unitIso.inv.app (L.obj (T.inverse.obj (T.functor.obj X)))) ≫
          B.functor.map (L.map (T.unitIso.inv.app X))) ≫
      B.functor.map (L.map (T.unitIso.hom.app X)) =
    R.map (T.functor.map (T.unitIso.hom.app X)) ≫
      (iso T.functor L R B.functor).hom.app (T.inverse.obj (T.functor.obj X))

Tactic:
simp only [Functor.comp_obj, assoc, ← Functor.map_comp, Iso.inv_hom_id_app,
    Equivalence.counitInv_app_functor, Functor.map_id]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ B.counitIso.inv.app (R.obj (T.functor.obj X)) ≫
      B.functor.map
        (B.inverse.map (R.map (T.functor.map (T.unit.app X))) ≫
          B.inverse.map ((iso T.functor L R B.functor).hom.app (T.inverse.obj (T.functor.obj X))) ≫
            B.unitIso.inv.app (L.obj (T.inverse.obj (T.functor.obj X))) ≫ 𝟙 (L.obj (T.inverse.obj (T.functor.obj X)))) =
    R.map (T.functor.map (T.unitIso.hom.app X)) ≫
      (iso T.functor L R B.functor).hom.app (T.inverse.obj (T.functor.obj X))
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G✝ : C ⥤ D
hG : W.IsInvertedBy G✝
G : W.FunctorsInverting D
⊢ 𝟙 W.Q ◫ natTransExtension (eqToHom ⋯ ≫ (𝟙 G).hom ≫ eqToHom ⋯) = 𝟙 W.Q ◫ 𝟙 (lift G.obj ⋯)

Tactic:
by
        rw [natTransExtension_hcomp]
        ext X
        simp only [NatTrans.comp_app, eqToHom_app, eqToHom_refl, comp_id, id_comp,
          NatTrans.hcomp_id_app, NatTrans.id_app, Functor.map_id]
        rfl

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

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₂
inst✝ : Φ.functor.IsEquivalence
h : W₂ ≤ W₁.map Φ.functor
⊢ W₂ ≤ W₁.isoClosure.inverseImage Φ.functor.asEquivalence.symm.functor

Tactic:
W₁.isoClosure.inverseImage_equivalence_functor_eq_map_inverse

Goal state after:
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₂
inst✝ : Φ.functor.IsEquivalence
h : W₂ ≤ W₁.map Φ.functor
⊢ W₂ ≤ W₁.isoClosure.map Φ.functor.asEquivalence.functor
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁹ : Category.{v₁, u₁} C₁
inst✝⁸ : Category.{v₂, u₂} C₂
inst✝⁷ : Category.{v₃, u₃} C₃
inst✝⁶ : Category.{v₄, u₄} D₁
inst✝⁵ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝⁴ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝³ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝² : Φ.functor.IsEquivalence
inst✝¹ : Φ.IsInduced
inst✝ : W₂.RespectsIso
⊢ Φ.inv.functor.IsEquivalence

Tactic:
dsimp
  infer_instance

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{v}
h : HasCardinalLT X κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ HasCardinalLT Y κ

Tactic:
dsimp [HasCardinalLT] at h ⊢
  rw [← Cardinal.lift_lt.{_, u}, Cardinal.lift_lift, Cardinal.lift_lift]
  rw [← Cardinal.lift_lt.{_, u'}, Cardinal.lift_lift, Cardinal.lift_lift] at h
  exact lt_of_le_of_lt (Cardinal.mk_le_of_injective
    (Function.Injective.comp ULift.up_injective
      (Function.Injective.comp hf ULift.down_injective))) h

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case isMin
C : Type u
inst✝⁵ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁴ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝³ : LinearOrder β
inst✝² : OrderBot β
inst✝¹ : SuccOrder β
inst✝ : WellFoundedLT β
b : β
hb : IsMin b
⊢ P.strictLimitsClosureIter J b ≤ P.limitsClosure J

Tactic:
obtain rfl := hb.eq_bot
    simp

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

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
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
L : C ⥤ D
inst✝ : L.IsLocalization W
⊢ z₁.map L ⋯ ≫ z₂.map L ⋯ = (z₁.comp₀ z₂ z₃).map L ⋯

Tactic:
by
  have : IsIso (L.map (z₂.s ≫ z₃.s)) := by
    rw [L.map_comp]
    infer_instance
  dsimp [LeftFraction.comp₀]
  rw [← cancel_mono (L.map (z₂.s ≫ z₃.s)), map_comp_map_s,
    L.map_comp, assoc, map_comp_map_s_assoc, ← L.map_comp, h₃,
    L.map_comp, map_comp_map_s_assoc, L.map_comp]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
X Y Z : C
inst✝ : Preadditive C
a b c : M
α₁ α₂ : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h

Tactic:
by
  rw [comp, comp, comp, Preadditive.add_comp]

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

Goal state before:
pp: C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasZeroObject C
inst✝¹² : HasShift C ℤ
inst✝¹¹ : Preadditive C
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁹ : Pretriangulated C
D : Type u_2
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
inst✝¹ : HasShift E ℤ
P : ObjectProperty C
inst✝ : P.IsTriangulatedClosed₂
⊢ ∀ T ∈ distinguishedTriangles, P.isoClosure T.obj₁ → P.isoClosure T.obj₃ → P.isoClosure.isoClosure T.obj₂

Tactic:
by
    rintro T hT ⟨X₁, h₁, ⟨e₁⟩⟩ ⟨X₃, h₃, ⟨e₃⟩⟩
    exact ObjectProperty.le_isoClosure _ _
      (P.ext_of_isTriangulatedClosed₂'
        (Triangle.mk (e₁.inv ≫ T.mor₁) (T.mor₂ ≫ e₃.hom) (e₃.inv ≫ T.mor₃ ≫ e₁.hom⟦1⟧'))
      (isomorphic_distinguished _ hT _
        (Triangle.isoMk _ _ e₁.symm (Iso.refl _) e₃.symm (by simp) (by simp) (by
          dsimp
          simp only [assoc, ← Functor.map_comp, e₁.hom_inv_id,
            Functor.map_id, comp_id]))) h₁ h₃)

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

Goal state before:
pp: case succ
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
n : ℕ
H : P.retractClosure.extensionProductIter n ≤ (P.extensionProductIter n).retractClosure
⊢ P.retractClosure.extensionProductIter (n + 1) ≤ (P.extensionProductIter (n + 1)).retractClosure

Tactic:
grw [extensionProductIter_succ, extensionProductIter_succ, monotone_extensionProduct_right _ H,
      extensionProduct_retractClosure_retractClosure_le]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
⊢ ∀ (f g : Arrow (HomotopyCategory C c)) (x : f ≅ g), quasiIso C c f.hom → quasiIso C c g.hom

Tactic:
intro f g e hf i

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
f g : Arrow (HomotopyCategory C c)
e : f ≅ g
hf : quasiIso C c f.hom
i : ι
⊢ IsIso ((homologyFunctor C c i).map g.hom)
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝³ : Preadditive C
inst✝² : CategoryWithHomology C
inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝ : c.QFactorsThroughHomotopy C
K : HomologicalComplex C c
⊢ ∀ (y : HomologicalComplex C c) (f₁ f₂ : K ⟶ y), homotopic C c f₁ f₂ → Q.map f₁ = Q.map f₂

Tactic:
L

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝³ : Preadditive C
inst✝² : CategoryWithHomology C
inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝ : c.QFactorsThroughHomotopy C
K L : HomologicalComplex C c
⊢ ∀ (f₁ f₂ : K ⟶ L), homotopic C c f₁ f₂ → Q.map f₁ = Q.map f₂
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ i, c.Rel i j
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
E : Type u_3
inst✝ : Category.{v_2, u_3} E
F : HomologicalComplex C c ⥤ E
hF : (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy F
K : HomologicalComplex C c
⊢ ∀ (y : HomologicalComplex C c) (f₁ f₂ : K ⟶ y), homotopic C c f₁ f₂ → F.map f₁ = F.map f₂

Tactic:
L

Goal state after:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ i, c.Rel i j
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
E : Type u_3
inst✝ : Category.{v_2, u_3} E
F : HomologicalComplex C c ⥤ E
hF : (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy F
K L : HomologicalComplex C c
⊢ ∀ (f₁ f₂ : K ⟶ L), homotopic C c f₁ f₂ → F.map f₁ = F.map f₂
Module: Mathlib.Algebra.Homology.DerivedCategory.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
⊢ (singleFunctor C n).Additive

Tactic:
by
  dsimp [singleFunctor, singleFunctors]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K L : DerivedCategory C
f : K ⟶ L
⊢ IsIso f ↔ ∀ (n : ℤ), IsIso ((homologyFunctor C n).map f)

Tactic:
refine ⟨fun hf n ↦ inferInstance, fun hf ↦ ?_⟩
  refine ((MorphismProperty.isomorphisms (DerivedCategory C)).arrow_iso_iff
    (Qh.mapArrow.objObjPreimageIso (Arrow.mk f))).1 ?_
  let g := Qh.mapArrow.objPreimage (Arrow.mk f)
  change IsIso (Qh.map g.hom)
  rw [isIso_Qh_map_iff, HomotopyCategory.mem_quasiIso_iff]
  intro n
  have e : Arrow.mk ((homologyFunctor C n).map f) ≅
      Arrow.mk ((HomotopyCategory.homologyFunctor _ _ n).map g.hom) :=
    ((homologyFunctor C n).mapArrow.mapIso
      ((Qh.mapArrow.objObjPreimageIso (Arrow.mk f)).symm)) ≪≫
      ((Functor.mapArrowFunctor _ _).mapIso (homologyFunctorFactorsh C n)).app (Arrow.mk g.hom)
  exact ((MorphismProperty.isomorphisms C).arrow_iso_iff e).1 (hf n)

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.IsSupported

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
K : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
hn : ¬∃ i, e.f i = n
⊢ IsZero (K.X n)

Tactic:
exact K.isZero_X_of_isStrictlySupported e _ (by simpa using hn)

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Extend

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✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i : Option ι
j : ι
hj : i = some j
⊢ X K i = K.X j

Tactic:
by subst hj; rfl

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

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
⊢ ((opFunctor V c).obj (op K)).HasHomology i

Tactic:
dsimp
  infer_instance

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

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex Vᵒᵖ c
i : ι
inst✝ : K.HasHomology i
⊢ ((unopFunctor V c).obj (op K)).HasHomology i

Tactic:
dsimp
  infer_instance

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

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝⁴ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝³ : HasZeroMorphisms V
K L : HomologicalComplex V c
φ : K ⟶ L
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : QuasiIso φ
⊢ QuasiIso ((opFunctor V c).map φ.op)

Tactic:
rw [quasiIso_opFunctor_map_iff]

Goal state after:
ι : Type u_1
V : Type u_2
inst✝⁴ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝³ : HasZeroMorphisms V
K L : HomologicalComplex V c
φ : K ⟶ L
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : QuasiIso φ
⊢ QuasiIso φ
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsTruncGE
j k : ι
hjk : c.next j = k
k' : ι
hj : c.Rel j k'
hk' : e.f k' = c'.next (e.f j)
⊢ c'.next (e.f j) = e.f k

Tactic:
rw [← hk', ← c.next_eq' hj, hjk]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

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✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).LeftHomologyData
⊢ (isLimitKernelFork K e hj' hk hk' (KernelFork.ofι h.i ⋯) h.hi).lift (KernelFork.ofι ((K.extend e).d i' j') ⋯) ≫ h.π =
    0

Tactic:
rw [← lift_d_comp_eq_zero_iff K e hj' hi hi' hk hk' _ h.hi]

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✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).LeftHomologyData
⊢ h.hi.lift (KernelFork.ofι (K.d i j) ⋯) ≫ h.π = 0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

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✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
φ : W ⟶ cocone.pt
⊢ (K.extendXIso e hj').hom ≫
      Cofork.π cocone ≫
        (isColimitCokernelCofork K e hj' hi hi' cocone hcocone).desc (CokernelCofork.ofπ ((K.extend e).d j' k') ⋯) =
    (K.extend e).d j' k'

Tactic:
simpa using! (isColimitCokernelCofork K e hj' hi hi' cocone hcocone).fac _
      WalkingParallelPair.one

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: case inr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝³ : Category.{v_1, u_4} C
inst✝² : Abelian C
K : HomologicalComplex C c
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
inst✝¹ : e₁.IsTruncLE
inst✝ : e₂.IsTruncGE
ac : e₁.AreComplementary e₂
i₂ : ι₂
⊢ QuasiIsoAt (K.shortComplexTruncLEX₃ToTruncGE ac) (e₂.f i₂)

Tactic:
have := quasiIsoAt_shortComplexTruncLE_g K e₁ (e₂.f i₂) (fun _ => ac.disjoint _ _)
      rw [← quasiIsoAt_iff_comp_left (K.shortComplexTruncLE e₁).g
        (K.shortComplexTruncLEX₃ToTruncGE ac), g_shortComplexTruncLEX₃ToTruncGE]
      dsimp
      infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)).HasLeftCalculusOfFractions

Tactic:
by
  rw [HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (HomotopyCategory.quasiIso C (ComplexShape.up ℤ)).HasRightCalculusOfFractions

Tactic:
by
  rw [HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic]
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C✝ : Type u_1
inst✝⁵ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝⁴ : Category.{?u.7, u_2} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n✝ n i : ℤ
hi : i < n
h : (embeddingUpIntLE n).BoundaryLE (n - i).natAbs
⊢ False

Tactic:
boundaryLE_embeddingUpIntLE_iff,

Goal state after:
C✝ : Type u_1
inst✝⁵ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝⁴ : Category.{?u.7, u_2} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n✝ n i : ℤ
hi : i < n
h : (n - i).natAbs = 0
⊢ False
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ HasExt C

Tactic:
by
  let := HasDerivedCategory.standard
  exact hasExt_of_hasDerivedCategory _

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
n : ℕ
α : Ext Z T n
⊢ (mk₀ f).comp ((mk₀ g).comp α ⋯) ⋯ = (mk₀ (f ≫ g)).comp α ⋯

Tactic:
by
  rw [← mk₀_comp_mk₀, comp_assoc]
  lia

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasExt C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
e : Ext X Y n
⊢ homEquiv (chgUniv e) = homEquiv e

Tactic:
apply SmallShiftedHom.equiv_chgUniv

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ HasSmallLocalizedShiftedHom W ℤ (S.map (CochainComplex.singleFunctor C 0)).X₃
    (S.map (CochainComplex.singleFunctor C 0)).X₁

Tactic:
dsimp
  infer_instance

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

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctor C (a + b)).map (adj.unit.app X) =
    (shiftFunctorAdd C a b).hom.app X ≫
      (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫
        f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) ≫
          f₂.hom.app (F.obj ((shiftFunctor C a).obj X)) ≫
            (G ⋙ shiftFunctor C b).map (e₁.hom.app X) ≫
              (shiftFunctor C b).map (e₂.hom.app (F.obj X)) ≫ (shiftFunctorAdd C a b).inv.app (G.obj (F.obj X))

Tactic:
← cancel_mono ((shiftFunctorAdd C a b).hom.app _),

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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
f₁ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
f₂ : shiftFunctor D b ⋙ G ≅ G ⋙ shiftFunctor C b
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj f₁ f₂
X : C
this :
  (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫ f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) =
    adj.unit.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫ G.map (f₁.hom.app ((shiftFunctor C a).obj X))
⊢ (shiftFunctor C (a + b)).map (adj.unit.app X) ≫ (shiftFunctorAdd C a b).hom.app (G.obj (F.obj X)) =
    ((shiftFunctorAdd C a b).hom.app X ≫
        (shiftFunctor C b).map (adj.unit.app ((shiftFunctor C a).obj X)) ≫
          f₂.inv.app (F.obj ((shiftFunctor C a).obj X)) ≫
            f₂.hom.app (F.obj ((shiftFunctor C a).obj X)) ≫
              (G ⋙ shiftFunctor C b).map (e₁.hom.app X) ≫
                (shiftFunctor C b).map (e₂.hom.app (F.obj X)) ≫ (shiftFunctorAdd C a b).inv.app (G.obj (F.obj X))) ≫
      (shiftFunctorAdd C a b).hom.app (G.obj (F.obj X))
Module: Mathlib.CategoryTheory.Shift.ShiftedHomOpposite

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n : ℤ
x y : ShiftedHom (Opposite.op Y) (Opposite.op X) n
⊢ (opEquiv n).symm (x + y) = (opEquiv n).symm x + (opEquiv n).symm y

Tactic:
dsimp [opEquiv_symm_apply]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n : ℤ
x y : ShiftedHom (Opposite.op Y) (Opposite.op X) n
⊢ ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C n).map (Quiver.Hom.unop x + Quiver.Hom.unop y) =
    ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C n).map (Quiver.Hom.unop x) +
      ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
        (shiftFunctor C n).map (Quiver.Hom.unop y)
Module: Mathlib.CategoryTheory.Shift.Adjunction

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
E : C ≌ D
A : Type u_3
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift C A
inst✝⁸ : HasShift D A
inst✝⁷ : E.functor.CommShift A
inst✝⁶ : E.inverse.CommShift A
F : Type u_4
inst✝⁵ : Category.{v_3, u_4} F
inst✝⁴ : HasShift F A
E' : D ≌ F
inst✝³ : E.CommShift A
inst✝² : E'.functor.CommShift A
inst✝¹ : E'.inverse.CommShift A
inst✝ : E'.CommShift A
⊢ (E.trans E').functor.CommShift A

Tactic:
dsimp
  infer_instance

Goal state after: