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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
⊢ ∀ (i j : ℤ),
    (ComplexShape.up ℤ).Rel i j →
      (mappingConeHomOfDegreewiseSplitXIso S σ i (i + { as := 1 }.as) ⋯).hom ≫
          ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj S.X₂).d i j =
        (mappingCone (homOfDegreewiseSplit S σ)).d i j ≫
          (mappingConeHomOfDegreewiseSplitXIso S σ j (j + { as := 1 }.as) ⋯).hom

Tactic:
by
    rintro p _ rfl
    have r_f := (σ (p + 1 + 1)).r_f
    have s_g := (σ (p + 1)).s_g
    dsimp at r_f s_g ⊢
    simp only [mappingConeHomOfDegreewiseSplitXIso, mappingCone.ext_from_iff _ _ _ rfl,
      mappingCone.inl_v_d_assoc _ (p + 1) _ (p + 1 + 1) (by linarith) (by lia),
      cocycleOfDegreewiseSplit, r_f, Int.reduceNeg, Cochain.ofHom_v, sub_comp, assoc,
      Hom.comm, comp_sub, mappingCone.inl_v_fst_v_assoc, mappingCone.inl_v_snd_v_assoc,
      shiftFunctor_obj_X', zero_comp, sub_zero, homOfDegreewiseSplit_f,
      mappingCone.inr_f_fst_v_assoc, comp_zero, zero_sub, mappingCone.inr_f_snd_v_assoc,
      neg_neg, mappingCone.inr_f_d_assoc, shiftFunctor_obj_d',
      Int.negOnePow_one, neg_comp, sub_neg_eq_add, zero_add, and_true,
      Units.neg_smul, one_smul, comp_neg, ShortComplex.map_X₂, eval_obj, Cocycle.mk_coe,
      Cochain.mk_v]
    simp only [← S.g.comm_assoc, reassoc_of% s_g, comp_id]
    abel

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✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ S.X₁.liftCycles x₁ k hk ⋯ ≫ HomologicalComplex.cyclesMap S.f j = (x₂ ≫ S.X₂.pOpcycles i) ≫ S.X₂.opcyclesToCycles i j

Tactic:
← cancel_mono (S.X₂.iCycles j),

Goal state after:
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ (S.X₁.liftCycles x₁ k hk ⋯ ≫ HomologicalComplex.cyclesMap S.f j) ≫ S.X₂.iCycles j =
    ((x₂ ≫ S.X₂.pOpcycles i) ≫ S.X₂.opcyclesToCycles i j) ≫ S.X₂.iCycles j
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows

Goal state before:
pp: case succ
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.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows D n
Z : D
f : Z ⟶ Y.left
Y' : ComposableArrows C n
e : (L.mapComposableArrows n).obj Y' ≅ Y
⊢ (L.mapComposableArrows (n + 1)).essImage (Y.precomp f)

Tactic:
obtain ⟨f', hf'⟩ := exists_rightFraction L W
        ((L.objObjPreimageIso Z).hom ≫ f ≫ (e.app 0).inv)

Goal state after:
case succ
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.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows D n
Z : D
f : Z ⟶ Y.left
Y' : ComposableArrows C n
e : (L.mapComposableArrows n).obj Y' ≅ Y
f' : W.RightFraction (L.objPreimage Z) (Y'.obj 0)
hf' : (L.objObjPreimageIso Z).hom ≫ f ≫ (e.app 0).inv = f'.map L ⋯
⊢ (L.mapComposableArrows (n + 1)).essImage (Y.precomp f)
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
X Y : C
φ : W.LeftFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
this : IsIso (L.map φ.s) := hL φ.s φ.hs
⊢ φ.map L hL ≫ L.map φ.s = L.map φ.f

Tactic:
simp [map]

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
X Y : C
f : X ⟶ Y
L : C ⥤ D
hL : W.IsInvertedBy L
inst✝ : W.ContainsIdentities
⊢ (ofHom W f).map L hL = L.map f

Tactic:
simp [map]

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
X Y : C
s : Y ⟶ X
hs : W s
L : C ⥤ D
hL : W.IsInvertedBy L
this : IsIso (L.map s) := hL s hs
⊢ (ofInv s hs).map L hL ≫ L.map s = 𝟙 (L.obj X)

Tactic:
simp [map]

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
X Y : C
s : Y ⟶ X
hs : W s
L : C ⥤ D
hL : W.IsInvertedBy L
this : IsIso (L.map s) := hL s hs
⊢ L.map s ≫ (ofInv s hs).map L hL = 𝟙 (L.obj Y)

Tactic:
simp [map]

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
X Y : C
φ : W.RightFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
this : IsIso (L.map φ.s) := hL φ.s φ.hs
⊢ L.map φ.s ≫ φ.map L hL = L.map φ.f

Tactic:
simp [map]

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

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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
⊢ ∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯

Tactic:
have ⟨β, hβ⟩ := exists_leftFraction L W f''

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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' f'' : L.obj X ⟶ L.obj Y
α : W.LeftFraction₂ X Y
hα : f = α.fst.map L ⋯
hα' : f' = α.snd.map L ⋯
β : W.LeftFraction X Y
hβ : f'' = β.map L ⋯
⊢ ∃ φ, f = φ.fst.map L ⋯ ∧ f' = φ.snd.map L ⋯ ∧ f'' = φ.thd.map L ⋯
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
inst✝ : Small.{w, u} X
⊢ HasCardinalLT X (Order.succ (max (Cardinal.mk (Shrink.{w, u} X)) Cardinal.aleph0))

Tactic:
simp [hasCardinalLT_iff_of_equiv (equivShrink.{w} X),
        hasCardinalLT_iff_cardinal_mk_lt]

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

Goal state before:
pp: case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderBinaryProducts
X Y : C
B : BinaryFan X Y
hB : IsLimit B
hX : P X
hY : P Y
⊢ P ((Limits.pair X Y).obj { as := WalkingPair.left })

Tactic:
assumption

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

Goal state before:
pp: case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderBinaryProducts
X Y : C
B : BinaryFan X Y
hB : IsLimit B
hX : P X
hY : P Y
⊢ P ((Limits.pair X Y).obj { as := WalkingPair.right })

Tactic:
assumption

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

Goal state before:
pp: case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderBinaryCoproducts
X Y : C
B : BinaryCofan X Y
hB : IsColimit B
hX : P X
hY : P Y
⊢ P ((Limits.pair X Y).obj { as := WalkingPair.left })

Tactic:
assumption

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

Goal state before:
pp: case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝ : P.IsClosedUnderBinaryCoproducts
X Y : C
B : BinaryCofan X Y
hB : IsColimit B
hX : P X
hY : P Y
⊢ P ((Limits.pair X Y).obj { as := WalkingPair.right })

Tactic:
assumption

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 : C
a : M
f : ShiftedHom X Y a
⊢ f.map (𝟭 C) = f

Tactic:
simp [map]

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

Goal state before:
pp: case refine_1
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 Q R : ObjectProperty C
inst✝¹ : P.IsStableUnderShift ℤ
inst✝ : Q.IsStableUnderShift ℤ
a : ℤ
X Y Z : C
f : Y ⟶ X
g : X ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj Y
hT : Triangle.mk f g h ∈ distinguishedTriangles
hP : P Y
hQ : Q Z
⊢ P (Triangle.mk f g h).obj₁

Tactic:
assumption

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

Goal state before:
pp: case refine_2
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 Q R : ObjectProperty C
inst✝¹ : P.IsStableUnderShift ℤ
inst✝ : Q.IsStableUnderShift ℤ
a : ℤ
X Y Z : C
f : Y ⟶ X
g : X ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj Y
hT : Triangle.mk f g h ∈ distinguishedTriangles
hP : P Y
hQ : Q Z
⊢ Q (Triangle.mk f g h).obj₃

Tactic:
assumption

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

Goal state before:
pp: case zero
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 Q R : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
⊢ (P.extensionProductIter 0).IsStableUnderShift ℤ

Tactic:
assumption

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
X✝ Y✝ Z✝ : HomotopyCategory C c
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : quasiIso C c f
hg : quasiIso C c g
⊢ quasiIso C c (f ≫ g)

Tactic:
by
    rw [mem_quasiIso_iff] at hf hg ⊢
    simp only [Functor.map_comp]
    infer_instance

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

Goal state before:
pp: case inr
ι : 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' j' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
⊢ extend.d K (e.r i') (e.r j') = 0

Tactic:
obtain hj' | ⟨j, hj⟩ := (e.r j').eq_none_or_eq_some
      · rw [extend.d_none_eq_zero' K _ _ hj']
      · rw [extend.d_eq K hi hj, K.shape, zero_comp, comp_zero]
        obtain rfl := e.f_eq_of_r_eq_some hi
        obtain rfl := e.f_eq_of_r_eq_some hj
        intro hij
        exact h (e.rel hij)

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

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hj : ¬e.BoundaryGE j
hjk : ¬c.Rel j (c.next j)
⊢ ¬e.BoundaryGE (c.next j)

Tactic:
simpa only [c.next_eq_self j hjk] using hj

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

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

Tactic:
simpa only [e.rel_iff] using hjk'

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

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.IsRelIff
j : ι
i' j' k' : ι'
hj' : e.f j = j'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
hi' : e.f (c.prev j) = i'
hk' : e.f (c.next j) = k'
⊢ ((K.restriction e).sc' (c.prev j) j (c.next j)).HasHomology

Tactic:
assumption

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

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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
hi' : e.f i = c'.prev j'
hk' : e.f k = c'.next j'
⊢ (K.sc' (c'.prev j') j' (c'.next j')).HasHomology

Tactic:
assumption

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyGE a
inst✝¹ : X.IsStrictlyLE b
inst✝ : Y.IsStrictlyGE a
f : Q.obj X ⟶ Q.obj Y
X' : CochainComplex C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
fac : f = inv (Q.map s) ≫ Q.map g
this : IsIso (Q.map (CochainComplex.truncGEMap s a))
⊢ Q.map g = Q.map g ≫ Q.map (Y.πTruncGE a) ≫ inv (Q.map (Y.πTruncGE a))

Tactic:
IsIso.hom_inv_id,

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyGE a
inst✝¹ : X.IsStrictlyLE b
inst✝ : Y.IsStrictlyGE a
f : Q.obj X ⟶ Q.obj Y
X' : CochainComplex C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
fac : f = inv (Q.map s) ≫ Q.map g
this : IsIso (Q.map (CochainComplex.truncGEMap s a))
⊢ Q.map g = Q.map g ≫ 𝟙 (Q.obj Y)
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos.hR₁
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₂ : Mono (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₁ j)
j : ι
hij : c.Rel i j
⊢ ((δlastFunctor ⋙ δlastFunctor).obj (composableArrows₅ hS₁ i j hij)).Exact

Tactic:
exact (composableArrows₅_exact hS₁ i j hij).δlast.δlast

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
this : (C : Type ?u.11) → [inst : Category.{?u.12, ?u.11} C] → [inst_1 : Abelian C] → HasDerivedCategory C :=
  HasDerivedCategory.standard
⊢ HasExt C

Tactic:
exact hasExt_of_hasDerivedCategory _

Goal state after:
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 : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : S.X₁.ExactAt i
h₃ : S.X₃.ExactAt i
⊢ S.X₂.ExactAt i

Tactic:
by
  rw [exactAt_iff_isZero_homology] at h₁ h₃ ⊢
  exact (hS.homology_exact₂ i).isZero_X₂ (h₁.eq_of_src _ _) (h₃.eq_of_tgt _ _)

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:
rw [← mk₀_comp_mk₀, comp_assoc]
  lia

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

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
this : HasDerivedCategory C := ⋯
h₁ : (singleFunctor C 0).map biprod.inl ≫ α.hom = (singleFunctor C 0).map biprod.inl ≫ β.hom
h₂ : (singleFunctor C 0).map biprod.inr ≫ α.hom = (singleFunctor C 0).map biprod.inr ≫ β.hom
⊢ BinaryCofan.inl ((singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ α.hom =
    BinaryCofan.inl ((singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ β.hom

Tactic:
assumption

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

Goal state before:
pp: case h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
this : HasDerivedCategory C := ⋯
h₁ : (singleFunctor C 0).map biprod.inl ≫ α.hom = (singleFunctor C 0).map biprod.inl ≫ β.hom
h₂ : (singleFunctor C 0).map biprod.inr ≫ α.hom = (singleFunctor C 0).map biprod.inr ≫ β.hom
⊢ BinaryCofan.inr ((singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ α.hom =
    BinaryCofan.inr ((singleFunctor C 0).mapBinaryBicone (BinaryBiproduct.bicone X₁ X₂)).toCocone ≫ β.hom

Tactic:
assumption

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
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
⊢ (α + β).hom = α.hom + β.hom

Tactic:
by
  let α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α (zero_add n)
  let β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β (zero_add n)
  have eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') (zero_add n) := by
    simp [α', β']
  have eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom) := by
    apply biprod_ext
    all_goals ext; simp [α', β', ← Functor.map_comp]
  simp only [eq₁, eq₂, comp_hom, Equiv.apply_symm_apply, ShiftedHom.comp_add]
  congr
  · dsimp [α']
    rw [comp_hom, mk₀_hom, mk₀_hom]
    dsimp
    rw [ShiftedHom.mk₀_comp_mk₀_assoc, ← Functor.map_comp,
      biprod.lift_fst, Functor.map_id, ShiftedHom.mk₀_id_comp]
  · dsimp [β']
    rw [comp_hom, mk₀_hom, mk₀_hom]
    dsimp
    rw [ShiftedHom.mk₀_comp_mk₀_assoc, ← Functor.map_comp,
      biprod.lift_snd, Functor.map_id, ShiftedHom.mk₀_id_comp]

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
n : ℕ
R₁ R₂ : ComposableArrows C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ : ℕ
h : k₀ + 3 ≤ n
h₁ : Mono (app' φ (k₀ + 1) ⋯)
h₃ : Mono (app' φ (k₀ + 3) ⋯)
h₀ : Epi (app' φ (k₀ + 0) ⋯)
⊢ Mono (app' φ (k₀ + 2) ⋯)

Tactic:
← natAddLEFunctor_app' h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n : ℕ
R₁ R₂ : ComposableArrows C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ : ℕ
h : k₀ + 3 ≤ n
h₁ : Mono (app' ((natAddLEFunctor h).map φ) 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃ : Mono (app' ((natAddLEFunctor h).map φ) 3 mono_of_epi_of_mono_of_mono'._proof_7)
h₀ : Epi (app' ((natAddLEFunctor h).map φ) 0 mono_of_epi_of_mono_of_mono'._proof_13)
⊢ Mono (app' ((natAddLEFunctor h).map φ) 2 mono_of_epi_of_mono_of_mono'._proof_4)
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n : ℕ
R₁ R₂ : ComposableArrows C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ : ℕ
h : k₀ + 3 ≤ n
h₂ : Epi (app' φ (k₀ + 2) ⋯)
h₃ : Mono (app' φ (k₀ + 3) ⋯)
h₀ : Epi (app' φ (k₀ + 0) ⋯)
⊢ Epi (app' φ (k₀ + 1) ⋯)

Tactic:
← natAddLEFunctor_app' h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n : ℕ
R₁ R₂ : ComposableArrows C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ : ℕ
h : k₀ + 3 ≤ n
h₂ : Epi (app' ((natAddLEFunctor h).map φ) 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃ : Mono (app' ((natAddLEFunctor h).map φ) 3 mono_of_epi_of_mono_of_mono'._proof_7)
h₀ : Epi (app' ((natAddLEFunctor h).map φ) 0 mono_of_epi_of_mono_of_mono'._proof_13)
⊢ Epi (app' ((natAddLEFunctor h).map φ) 1 mono_of_epi_of_mono_of_mono'._proof_11)
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n : ℕ
R₁ R₂ : ComposableArrows C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ : ℕ
h : k₀ + 4 ≤ n
h₁ : IsIso (app' φ (k₀ + 1) ⋯)
h₃ : IsIso (app' φ (k₀ + 3) ⋯)
h₄ : Mono (app' φ (k₀ + 4) ⋯)
h₀ : Epi (app' φ (k₀ + 0) ⋯)
⊢ IsIso (app' φ (k₀ + 2) ⋯)

Tactic:
← natAddLEFunctor_app' h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n : ℕ
R₁ R₂ : ComposableArrows C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ : ℕ
h : k₀ + 4 ≤ n
h₁ : IsIso (app' ((natAddLEFunctor h).map φ) 1 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4)
h₃ : IsIso (app' ((natAddLEFunctor h).map φ) 3 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6)
h₄ : Mono (app' ((natAddLEFunctor h).map φ) 4 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7)
h₀ : Epi (app' ((natAddLEFunctor h).map φ) 0 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2)
⊢ IsIso (app' ((natAddLEFunctor h).map φ) 2 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_9)
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₁ S₂ : ShortComplex (CochainComplex C ℤ)
f : S₁ ⟶ S₂
n : ℤ
⊢ (inl S₁.f).v (n + 1) n ⋯ ≫ (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂).f n =
    (inl S₁.f).v (n + 1) n ⋯ ≫ (descShortComplex S₁ ≫ f.τ₃).f n

Tactic:
simp [map]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
I : C
inst✝¹ : Injective I
K : CochainComplex C ℤ
i n : ℤ
hn : i < n
inst✝ : K.IsStrictlyGE n
L : CochainComplex C ℤ
w✝ : L.IsStrictlyGE i
g : K ⟶ L
ι : (CochainComplex.singleFunctor C i).obj I ⟶ L
h : IsIso (Q.map ι)
hπ : IsSplitMono ι
⊢ Q.map ι ≫ inv (Q.map ι) = Q.map ι ≫ Q.map (retraction ι)

Tactic:
IsIso.hom_inv_id,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
I : C
inst✝¹ : Injective I
K : CochainComplex C ℤ
i n : ℤ
hn : i < n
inst✝ : K.IsStrictlyGE n
L : CochainComplex C ℤ
w✝ : L.IsStrictlyGE i
g : K ⟶ L
ι : (CochainComplex.singleFunctor C i).obj I ⟶ L
h : IsIso (Q.map ι)
hπ : IsSplitMono ι
⊢ 𝟙 (Q.obj ((CochainComplex.singleFunctor C i).obj I)) = Q.map ι ≫ Q.map (retraction ι)
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝ : Ring A
relations : Relations A
r : relations.R
⊢ relations.map (Finsupp.single r 1) = relations.relation r

Tactic:
simp [map]

Goal state after: