mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
hT₀ : T.mor₃ = 0
inr : T.obj₃ ⟶ T.obj₂
inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃
fst : T.obj₂ ⟶ T.obj₁
total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂
this : Mono T.mor₁
⊢ fst ≫ T.mor₁ = fst ≫ T.mor₁ + T.mor₂ ≫ inr - T.mor₂ ≫ inr

Tactic:
add_sub_cancel_right

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
hT₀ : T.mor₃ = 0
inr : T.obj₃ ⟶ T.obj₂
inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃
fst : T.obj₂ ⟶ T.obj₁
total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂
this : Mono T.mor₁
⊢ fst ≫ T.mor₁ = fst ≫ T.mor₁
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ Cochain.ofHom ((triangle φ).mor₃ ≫ (rotateHomotopyEquiv φ).hom) =
    δ (-1) 0 (-(snd φ).comp (inl (inr φ)) ⋯) + Cochain.ofHom (inr (inr φ))

Tactic:
by
        ext p
        dsimp [rotateHomotopyEquiv]
        -- the following list of lemmas has been obtained by doing
        -- simp? [ext_from_iff _ _ _ rfl, ext_to_iff _ _ _ rfl,
        --  (inl φ).leftShift_v 1 0 (neg_add_cancel 1) p p (add_zero p) (p + 1) (by lia),
        --  δ_zero_cochain_comp _ _ _ (neg_add_cancel 1),
        --  Cochain.comp_v _ _ (add_neg_cancel 1) p (p + 1) p rfl (by lia),
        --  (Cochain.ofHom φ).leftShift_v 1 1 (zero_add 1) p (p + 1) rfl (p + 1) (by lia)]⟩
        simp only [Int.reduceNeg, Cochain.ofHom_comp, ofHom_lift, Cocycle.coe_neg,
          Cocycle.leftShift_coe, Cocycle.ofHom_coe, Cochain.comp_zero_cochain_v,
          shiftFunctor_obj_X', Cochain.ofHom_v, δ_neg, δ_zero_cochain_comp _ _ _ (neg_add_cancel 1),
          δ_inl, Int.negOnePow_neg, Int.negOnePow_one, δ_snd, Cochain.neg_comp,
          Cochain.comp_assoc_of_second_is_zero_cochain, smul_neg, Units.neg_smul, one_smul, neg_neg,
          neg_add_rev, Cochain.add_v, Cochain.neg_v,
          Cochain.comp_v _ _ (add_neg_cancel 1) p (p + 1) p rfl (by lia),
          Cochain.zero_cochain_comp_v, ext_from_iff _ _ _ rfl, inl_v_triangle_mor₃_f_assoc,
          triangle_obj₁, shiftFunctor_obj_X, shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl,
          Iso.refl_inv, Preadditive.neg_comp, id_comp, Preadditive.comp_add, Preadditive.comp_neg,
          inl_v_fst_v_assoc, inl_v_snd_v_assoc, zero_comp, neg_zero, add_zero, ext_to_iff _ _ _ rfl,
          liftCochain_v_fst_v,
          (Cochain.ofHom φ).leftShift_v 1 1 (zero_add 1) p (p + 1) rfl (p + 1) (by lia), mul_one,
          sub_self, mul_zero, Int.zero_ediv, Iso.refl_hom, Preadditive.add_comp, assoc, inl_v_fst_v,
          comp_id, inr_f_fst_v, comp_zero, liftCochain_v_snd_v,
          (inl φ).leftShift_v 1 0 (neg_add_cancel 1) p p (add_zero p) (p + 1) (by lia),
          Int.negOnePow_zero, inl_v_snd_v, inr_f_snd_v, zero_add, and_self,
          inr_f_triangle_mor₃_f_assoc, inr_f_fst_v_assoc, inr_f_snd_v_assoc, neg_add_cancel]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
⊢ K.opcyclesToCycles i j ≫ K.iCycles j = K.fromOpcycles i j

Tactic:
dsimp only [opcyclesToCycles]
  simp

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
hij : c.Rel i j
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
⊢ Epi
    ((composableArrows₃ K i j).map' 2 3 instEpiMap'ComposableArrows₃OfNatNat._proof_2
      instEpiMap'ComposableArrows₃OfNatNat._proof_3)

Tactic:
dsimp [-Fin.reduceFinMk]
  infer_instance

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

Goal state before:
pp: case cons
V : Type u₁
inst✝ : Quiver V
a : Paths V
P : {b : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 a)
comp : ∀ {u v : V} (p : a ⟶ (of V).obj u) (q : u ⟶ v), P p → P (p ≫ (of V).map q)
b✝¹ b✝ c✝ : Paths V
a✝ : Quiver.Path a b✝
w : b✝ ⟶ c✝
h : P a✝
⊢ P (a✝.cons w)

Tactic:
| cons _ w h =>

Goal state after:
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
⊢ W.paths (p.comp q) ↔ W.paths p ∧ W.paths q

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨hp, hq⟩ ↦ ?_⟩

Goal state after:
case refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
h : W.paths (p.comp q)
⊢ W.paths p

case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
h : W.paths (p.comp q)
⊢ W.paths q

case refine_3
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
q : Path Y Z
x✝ : W.paths p ∧ W.paths q
hp : W.paths p
hq : W.paths q
⊢ W.paths (p.comp q)
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V W : Quiv
e : V ≅ W
X Y : ↑W
f : X ⟶ Y
⊢ e.hom.map (e.inv.map f) = Quiver.homOfEq f ⋯ ⋯

Tactic:
rw [← Prefunctor.comp_map]
  exact (Prefunctor.congr_hom e.inv_hom_id.symm f).symm

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a : A
X : C
⊢ (commShiftIso F' a).inv.app (L.obj X) =
    (shiftFunctor E a).map ((Lifting.iso L W F F').hom.app X) ≫
      (commShiftIso F a).inv.app X ≫
        (Lifting.iso L W F F').inv.app ((shiftFunctor C a).obj X) ≫ F'.map ((commShiftIso L a).hom.app X)

Tactic:
by
  apply commShiftOfLocalization.iso_inv_app

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

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✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : HasShift D ℤ
inst✝ : L.CommShift ℤ
T₁ T₂ : Triangle D
e : T₂ ≅ T₁
h : T₁ ∈ L.essImageDistTriang
⊢ T₂ ∈ L.essImageDistTriang

Tactic:
obtain ⟨T', e', hT'⟩ := h

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✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : HasShift D ℤ
inst✝ : L.CommShift ℤ
T₁ T₂ : Triangle D
e : T₂ ≅ T₁
T' : Triangle C
e' : T₁ ≅ L.mapTriangle.obj T'
hT' : T' ∈ distinguishedTriangles
⊢ T₂ ∈ L.essImageDistTriang
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type w
α : ι → Type w
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
hι : Cardinal.mk ι < κ
hα : ∀ (i : ι), Cardinal.mk (α i) < κ
⊢ Cardinal.mk ((i : ι) × α i) < κ

Tactic:
rw [Cardinal.mk_sigma]

Goal state after:
ι : Type w
α : ι → Type w
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
hι : Cardinal.mk ι < κ
hα : ∀ (i : ι), Cardinal.mk (α i) < κ
⊢ (Cardinal.sum fun i ↦ Cardinal.mk (α i)) < κ
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
⊢ P.isoClosure.colimitsClosure J = P.colimitsClosure J

Tactic:
refine le_antisymm (colimitsClosure_le ?_)
    (colimitsClosure_monotone _ P.le_isoClosure)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
⊢ P.isoClosure ≤ P.colimitsClosure J
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
⊢ ∀ {W_1 X Y Z : Localization W} (f : Hom W W_1 X) (g : Hom W X Y) (h : Hom W Y Z),
    (f.comp g).comp h = f.comp (g.comp h)

Tactic:
by
    rintro (X₁ X₂ X₃ X₄ : C) f₁ f₂ f₃
    obtain ⟨z₁, rfl⟩ := Hom.mk_surjective f₁
    obtain ⟨z₂, rfl⟩ := Hom.mk_surjective f₂
    obtain ⟨z₃, rfl⟩ := Hom.mk_surjective f₃
    rw [Hom.comp_eq z₁ z₂, Hom.comp_eq z₂ z₃]
    obtain ⟨z₁₂, fac₁₂⟩ := exists_leftFraction (RightFraction.mk z₁.s z₁.hs z₂.f)
    obtain ⟨z₂₃, fac₂₃⟩ := exists_leftFraction (RightFraction.mk z₂.s z₂.hs z₃.f)
    obtain ⟨z', fac⟩ := exists_leftFraction (RightFraction.mk z₁₂.s z₁₂.hs z₂₃.f)
    dsimp at fac₁₂ fac₂₃ fac
    rw [comp_eq z₁ z₂ z₁₂ fac₁₂, comp_eq z₂ z₃ z₂₃ fac₂₃, comp₀, comp₀,
      Hom.comp_eq, Hom.comp_eq,
      comp_eq _ z₃ (mk z'.f (z₂₃.s ≫ z'.s) (W.comp_mem _ _ z₂₃.hs z'.hs))
        (by dsimp; rw [assoc, reassoc_of% fac₂₃, fac]),
      comp_eq z₁ _ (mk (z₁₂.f ≫ z'.f) z'.s z'.hs)
        (by dsimp; rw [assoc, ← reassoc_of% fac₁₂, fac])]
    simp

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
h : LeftFractionRel f g
⊢ Hom.mk f = Hom.mk g

Tactic:
exact Quot.sound h

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

Goal state before:
pp: case mpr
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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction X Y
h : LeftFractionRel φ ψ
⊢ Localization.Hom.mk φ = Localization.Hom.mk ψ

Tactic:
exact Quot.sound h

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
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
a : M
g : ShiftedHom Y Z a
⊢ (mk₀ m₀ hm₀ f).comp g ⋯ = f ≫ g

Tactic:
by
  subst hm₀
  simp [comp, mk₀, shiftFunctorAdd'_add_zero_inv_app, shiftFunctorZero']

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
⊢ (quasiIso C c).RespectsIso

Tactic:
apply MorphismProperty.RespectsIso.of_respects_arrow_iso

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)) (x : f ≅ g), quasiIso C c f.hom → quasiIso C c g.hom
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.IsTriangulated
F : C ⥤ D
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : F.Full
T : Triangle D
hT : T ∈ distinguishedTriangles
X₁ : C
e₁ : F.obj X₁ ≅ T.obj₁
X₃ : C
e₃ : F.obj X₃ ≅ T.obj₃
h : X₃ ⟶ (shiftFunctor C 1).obj X₁
hh : F.map h = e₃.hom ≫ T.mor₃ ≫ (shiftFunctor D 1).map e₁.inv ≫ (Functor.commShiftIso F 1).inv.app X₁
X₂ : C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
H : Triangle.mk f g h ∈ distinguishedTriangles
⊢ (F.mapTriangle.obj (Triangle.mk f g h)).mor₃ ≫ (shiftFunctor D 1).map e₁.hom = e₃.hom ≫ T.mor₃

Tactic:
by simp [hh, ← Functor.map_comp]

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

Goal state before:
pp: p n : ℤ
⊢ (∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n) ↔ p < n

Tactic:
by
  constructor
  · intro h
    by_contra
    exact h (p - n).natAbs (by simp; lia)
  · intros
    dsimp
    lia

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
T : Triangle (CochainComplex C ℤ)
hT : DerivedCategory.Q.mapTriangle.obj T ∈ distinguishedTriangles
n : ℤ
⊢ { X₁ := homology T.obj₁ n, X₂ := homology T.obj₂ n, X₃ := homology T.obj₃ n, f := homologyMap T.mor₁ n,
      g := homologyMap T.mor₂ n, zero := ⋯ }.Exact

Tactic:
refine ShortComplex.exact_of_iso ?_ (DerivedCategory.HomologySequence.exact₂ _ hT n)
  exact ShortComplex.isoMk
    ((DerivedCategory.homologyFunctorFactors _ _).app _)
    ((DerivedCategory.homologyFunctorFactors _ _).app _)
    ((DerivedCategory.homologyFunctorFactors _ _).app _)

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'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
⊢ (Fork.ι cone ≫ (K.extendXIso e hj').inv) ≫ (K.extend e).d j' k' = 0

Tactic:
by rw [assoc, ← comp_d_eq_zero_iff K e hj' hk hk' cone.ι, cone.condition]

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 : 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'
h : (K.sc' i j k).RightHomologyData
hk'' : e.f k = k'
⊢ (K.extendXIso e hj').hom ≫ h.p ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' =
    (K.extendXIso e hj').hom ≫ h.p ≫ h.g' ≫ (K.extendXIso e hk'').inv

Tactic:
have := (rightHomologyData K e hj' hi hi' hk hk' h).p_g'

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 : 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'
h : (K.sc' i j k).RightHomologyData
hk'' : e.f k = k'
this :
  (rightHomologyData K e hj' hi hi' hk hk' h).p ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' =
    ((K.extend e).sc' i' j' k').g
⊢ (K.extendXIso e hj').hom ≫ h.p ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' =
    (K.extendXIso e hj').hom ≫ h.p ≫ h.g' ≫ (K.extendXIso e hk'').inv
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : (shortComplexFunctor C c' j').obj K ⟶ (shortComplexFunctor C c' j').obj (K.truncGE e) :=
  (shortComplexFunctor C c' j').map (K.πTruncGE e)
hi : ¬∃ i, e.f i = c'.prev j'
⊢ ∀ (i : ι), e.f i ≠ c'.prev j'

Tactic:
by simpa using hi

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

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ K.IsGE n → ∀ i < n, ExactAt K i

Tactic:
intro _ i hi
    exact K.exactAt_of_isGE n i hi

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y X' Y' : C
e : X ≅ X'
e' : Y ≅ Y'
⊢ HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X' Y'

Tactic:
simp only [hasSmallLocalizedHom_iff W W.Q]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y X' Y' : C
e : X ≅ X'
e' : Y ≅ Y'
⊢ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X' ⟶ W.Q.obj Y')
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y Y' : C
f : Y ⟶ Y'
hf : W f
⊢ HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X Y'

Tactic:
simp only [hasSmallLocalizedHom_iff W W.Q]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y Y' : C
f : Y ⟶ Y'
hf : W f
⊢ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y')
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X X' : C
f : X ⟶ X'
hf : W f
Y : C
⊢ HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X' Y

Tactic:
simp only [hasSmallLocalizedHom_iff W W.Q]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X X' : C
f : X ⟶ X'
hf : W f
Y : C
⊢ Small.{w, max u₁ v₁} (W.Q.obj X ⟶ W.Q.obj Y) ↔ Small.{w, max u₁ v₁} (W.Q.obj X' ⟶ W.Q.obj Y)
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
hi : ¬∃ j, c.Rel i j
this : Epi S₂.g
eq : homologyMap φ.τ₂ i ≫ homologyMap S₂.g i = homologyMap S₁.g i ≫ homologyMap φ.τ₃ i
⊢ ∀ (j : ι), ¬c.Rel i j

Tactic:
by simpa using hi

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 : C
a b : ℤ
inst✝ : HasDerivedCategory C
this :
  ∀ (a b : ℤ),
    Small.{w, w'}
      ((shiftFunctor (DerivedCategory C) a).obj ((singleFunctor C 0).obj X) ⟶
        (shiftFunctor (DerivedCategory C) b).obj ((singleFunctor C 0).obj Y))
⊢ Small.{w, w'} ((singleFunctor C a).obj X ⟶ (singleFunctor C b).obj Y)

Tactic:
exact small_of_injective
    (β := ((singleFunctor C 0).obj X)⟦-a⟧ ⟶ ((singleFunctor C 0).obj Y)⟦-b⟧)
    (f := fun φ ↦
      ((singleFunctors C).shiftIso (-a) a 0 (by simp)).hom.app X ≫ φ ≫
        ((singleFunctors C).shiftIso (-b) b 0 (by simp)).inv.app Y)
    (fun φ₁ φ₂ h ↦ by simpa using h)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (app' φ 0 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2)
h₁ : IsIso (app' φ 1 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4)
h₃ : IsIso (app' φ 3 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6)
h₄ : Mono (app' φ 4 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7)
⊢ IsIso (app' φ 2 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_9)

Tactic:
dsimp at h₀ h₁ h₃ h₄

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (φ.app 0)
h₁ : IsIso (φ.app 1)
h₃ : IsIso (φ.app 3)
h₄ : Mono (φ.app 4)
⊢ IsIso (app' φ 2 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_9)
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
⊢ 𝟙 ((𝟭 (PullbackShift C φ)).obj X) =
    (shiftFunctorZero C B).inv.app X ≫
      (pullbackShiftIso C φ 0 0 ⋯).inv.app X ≫ (pullbackShiftIso C φ 0 0 ⋯).hom.app X ≫ (shiftFunctorZero C B).hom.app X

Tactic:
Iso.inv_hom_id_app_assoc,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
⊢ 𝟙 ((𝟭 (PullbackShift C φ)).obj X) = (shiftFunctorZero C B).inv.app X ≫ (shiftFunctorZero C B).hom.app X
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: case h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast := ⋯
⊢ Epi (app' φ 0 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2)

pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast := ⋯
⊢ IsIso (app' φ 1 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4)

pp: case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast := ⋯
⊢ IsIso (app' φ 3 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6)

pp: case h₄
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast := ⋯
⊢ Mono (app' φ 4 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7)

Tactic:
all_goals dsimp [φ]; infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
f : S₁ ⟶ S₂
⊢ map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂ = descShortComplex S₁ ≫ f.τ₃

Tactic:
ext n
  apply ext_from _ (n + 1) n rfl
  · simp [map]
  · simp [map, ← HomologicalComplex.comp_f, f.comm₂₃]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
⊢ 𝟙 ((𝟭 (PullbackShift C φ)).obj X) =
    (shiftFunctorZero' C (φ 0) ⋯).inv.app X ≫
      (pullbackShiftIso C φ 0 (φ 0) ⋯).inv.app X ≫
        (pullbackShiftIso C φ 0 (φ 0) ⋯).hom.app X ≫ (shiftFunctorZero' C (φ 0) ⋯).hom.app X

Tactic:
Iso.inv_hom_id_app_assoc,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
⊢ 𝟙 ((𝟭 (PullbackShift C φ)).obj X) = (shiftFunctorZero' C (φ 0) ⋯).inv.app X ≫ (shiftFunctorZero' C (φ 0) ⋯).hom.app X