mathlib-initiative/mathlib-tactics huggingface dataset:
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
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ ((K.restriction e).sc j).iCycles ≫ (K.restrictionXIso e hj').hom ≫ (K.sc j').pOpcycles =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j' ≫ (K.sc j').homologyι

Tactic:
apply (K.restrictionCyclesIso_hom_iCycles_assoc e j k hk hj' hk' hk'' _).symm.trans

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
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.iCycles j' ≫ (K.sc j').pOpcycles =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j' ≫ (K.sc j').homologyι
Module: Mathlib.Algebra.Homology.Embedding.TruncLE

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 L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝³ : e.IsTruncLE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : ∀ (i' : ι'), M.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : ¬e.BoundaryLE i
⊢ ¬e.op.BoundaryGE i

Tactic:
by simpa

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

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 L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝³ : e.IsTruncLE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : ∀ (i' : ι'), M.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryLE i
⊢ e.op.BoundaryGE i

Tactic:
by simpa

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

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.IsTruncLE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hj : ¬e.BoundaryLE j
⊢ ¬e.op.BoundaryGE j

Tactic:
by simpa

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

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.IsTruncLE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hj : ¬e.BoundaryLE j
⊢ ((K.truncLE' e).d i j).op = ((K.truncLE'XIso e hi' ⋯).hom ≫ K.d i' j' ≫ (K.truncLE'XIso e hj' hj).inv).op

Tactic:
simpa using! K.op.truncGE'_d_eq e.op hij hj' hi' (by simpa)

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

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.IsTruncLE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hj : e.BoundaryLE j
⊢ e.op.BoundaryGE j

Tactic:
by simpa

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

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 L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁴ : e.IsTruncLE
inst✝³ : ∀ (i' : ι'), K.HasHomology i'
inst✝² : ∀ (i' : ι'), L.HasHomology i'
inst✝¹ : ∀ (i' : ι'), M.HasHomology i'
inst✝ : HasZeroObject C
i : ι
i' : ι'
hi' : e.f i = i'
hi : ¬e.BoundaryLE i
⊢ ¬e.op.BoundaryGE i

Tactic:
by simpa

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

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 L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁴ : e.IsTruncLE
inst✝³ : ∀ (i' : ι'), K.HasHomology i'
inst✝² : ∀ (i' : ι'), L.HasHomology i'
inst✝¹ : ∀ (i' : ι'), M.HasHomology i'
inst✝ : HasZeroObject C
i : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryLE i
⊢ e.op.BoundaryGE i

Tactic:
by simpa

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

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 L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ e.op.BoundaryGE i

Tactic:
by simpa

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

Goal state before:
pp: case mpr
ι : 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 : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
inst✝¹ : ∀ (j : ι), K.HasHomology j
inst✝ : ∀ (j : ι), L.HasHomology j
h : ∀ (i : ι), QuasiIsoAt (extendMap φ e) (e.f i)
j' : ι'
⊢ QuasiIsoAt (extendMap φ e) j'

Tactic:
by_cases hj' : ∃ j, e.f j = j'

Goal state after:
case pos
ι : 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 : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
inst✝¹ : ∀ (j : ι), K.HasHomology j
inst✝ : ∀ (j : ι), L.HasHomology j
h : ∀ (i : ι), QuasiIsoAt (extendMap φ e) (e.f i)
j' : ι'
hj' : ∃ j, e.f j = j'
⊢ QuasiIsoAt (extendMap φ e) j'

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
inst✝² : HasZeroObject C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
inst✝¹ : ∀ (j : ι), K.HasHomology j
inst✝ : ∀ (j : ι), L.HasHomology j
h : ∀ (i : ι), QuasiIsoAt (extendMap φ e) (e.f i)
j' : ι'
hj' : ¬∃ j, e.f j = j'
⊢ QuasiIsoAt (extendMap φ e) j'
Module: Mathlib.Algebra.Homology.Embedding.TruncLE

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 L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ ¬e.op.BoundaryGE i

Tactic:
by simpa

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

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.IsTruncLE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
⊢ ¬e.op.BoundaryGE i

Tactic:
by simpa

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

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.IsTruncLE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryLE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncLE' e).HasHomology j
this : (K.op.restriction e.op).HasHomology j
⊢ ¬e.op.BoundaryGE j

Tactic:
by simpa

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

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'
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : HasZeroObject C
hK : K.Acyclic
e : c.Embedding c'
inst✝ : e.IsTruncLE
⊢ (K.truncLE e).Acyclic

Tactic:
acyclic_truncLE_iff_isSupportedOutside

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
K : HomologicalComplex C c'
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : HasZeroObject C
hK : K.Acyclic
e : c.Embedding c'
inst✝ : e.IsTruncLE
⊢ K.IsSupportedOutside e
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.IsLE n → ∀ (i : ℤ), n < i → ExactAt K i

pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ (∀ (i : ℤ), n < i → ExactAt K i) → K.IsLE n

Tactic:
· intro _ i hi
    exact K.exactAt_of_isLE n i hi

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ (∀ (i : ℤ), n < i → ExactAt K i) → K.IsLE n
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K L : CochainComplex C ℤ
e : K ≅ L
n : ℤ
inst✝ : K.IsLE n
⊢ L.IsLE n

Tactic:
apply isSupported_of_iso e

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K L : CochainComplex C ℤ
e : K ≅ L
n : ℤ
inst✝ : K.IsGE n
⊢ L.IsGE n

Tactic:
apply isSupported_of_iso e

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
X Y : CochainComplex C ℤ
f : Q.obj X ⟶ Q.obj Y
X' : HomologicalComplex C (ComplexShape.up ℤ)
s : X' ⟶ X
hs✝ : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s)
hs : IsIso (Qh.map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s))
g : X' ⟶ Y
hφ :
  f =
    { X' := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X',
          s := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s, hs := hs✝,
          f := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map g }.map
      Qh ⋯
⊢ ∃ X' s, ∃ (x : IsIso (Q.map s)), ∃ g, f = inv (Q.map s) ≫ Q.map g

Tactic:
exact ⟨X', s, hs, g, hφ⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ (singleObjCyclesSelfIso c j A).hom ≫ (singleObjOpcyclesSelfIso c j A).hom ≫ opcyclesMap ((single C c j).map f) j =
    (singleObjCyclesSelfIso c j A).hom ≫ f ≫ (singleObjOpcyclesSelfIso c j B).hom

Tactic:
singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ ((single C c j).obj A).iCycles j ≫ ((single C c j).obj A).pOpcycles j ≫ opcyclesMap ((single C c j).map f) j =
    (singleObjCyclesSelfIso c j A).hom ≫ f ≫ (singleObjOpcyclesSelfIso c j B).hom
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'
inst✝ : HasSmallLocalizedHom W X Y
⊢ HasSmallLocalizedHom W X' Y'

Tactic:
by
  rwa [← hasSmallLocalizedHom_iff_of_isos _ e e']

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K : CochainComplex C ℤ
n₀ n₁ : ℤ
inst✝² : Injective (K.X n₀)
inst✝¹ : Injective (K.X n₁)
inst✝ : K.IsStrictlyGE n₀
hK : ExactAt K n₀
h : n₀ + 1 = n₁
S : ShortComplex C :=
  { X₁ := K.X n₀, X₂ := K.X n₁, X₃ := opcycles K n₁, f := K.d n₀ n₁, g := pOpcycles K n₁, zero := ⋯ }
T : ShortComplex C := sc' K (n₀ - 1) n₀ n₁
⊢ (up ℤ).next n₀ = n₁

Tactic:
by simpa

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₁ 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)
⊢ Epi (homologyMap φ.τ₃ i)

Tactic:
by_cases hi : ∃ j, c.Rel i j
  · obtain ⟨j, hij⟩ := hi
    apply epi_of_epi_of_epi_of_mono
      ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij))
    · exact (composableArrows₅_exact hS₁ i j hij).δ₀.δlast
    · exact (composableArrows₅_exact hS₂ i j hij).δ₀.δlast
    · exact h₁
    · exact h₂ j hij
    · exact h₃ j hij
  · have := hS₂.epi_g
    have eq := (homologyFunctor C _ i).congr_map φ.comm₂₃
    dsimp at eq
    simp only [homologyMap_comp] at eq
    have := epi_homologyMap_of_epi_of_not_rel S₂.g i (by simpa using hi)
    exact epi_of_epi_fac eq.symm

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

Tactic:
by simpa

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

Goal state before:
pp: C₁ : Type u₁
inst✝¹⁷ : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst✝¹⁶ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst✝¹⁵ : AddMonoid M
inst✝¹⁴ : HasShift C₁ M
inst✝¹³ : HasShift C₂ M
inst✝¹² : Φ.functor.CommShift M
X₁ Y₁ Z₁ : C₁
X₂ Y₂ Z₂ : C₂
inst✝¹¹ : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst✝¹⁰ : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst✝⁹ : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst✝⁸ : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor.obj X₁ ≅ X₂
eY : Φ.functor.obj Y₁ ≅ Y₂
eZ : Φ.functor.obj Z₁ ≅ Z₂
inst✝⁷ : W₁.IsCompatibleWithShift M
inst✝⁶ : W₂.IsCompatibleWithShift M
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂
inst✝² : HasSmallLocalizedShiftedHom W₁ M X₁ Z₁
inst✝¹ : HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁
inst✝ : HasSmallLocalizedShiftedHom W₂ M X₂ Z₂
a b c : M
f : SmallShiftedHom W₁ X₁ Y₁ a
g : SmallShiftedHom W₁ Y₁ Z₁ b
h : b + a = c
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
⊢ 0 + b + a = c

Tactic:
by simpa

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

Goal state before:
pp: C₁ : Type u₁
inst✝¹⁷ : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst✝¹⁶ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst✝¹⁵ : AddMonoid M
inst✝¹⁴ : HasShift C₁ M
inst✝¹³ : HasShift C₂ M
inst✝¹² : Φ.functor.CommShift M
X₁ Y₁ Z₁ : C₁
X₂ Y₂ Z₂ : C₂
inst✝¹¹ : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst✝¹⁰ : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst✝⁹ : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst✝⁸ : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor.obj X₁ ≅ X₂
eY : Φ.functor.obj Y₁ ≅ Y₂
eZ : Φ.functor.obj Z₁ ≅ Z₂
inst✝⁷ : W₁.IsCompatibleWithShift M
inst✝⁶ : W₂.IsCompatibleWithShift M
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂
inst✝² : HasSmallLocalizedShiftedHom W₁ M X₁ Z₁
inst✝¹ : HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁
inst✝ : HasSmallLocalizedShiftedHom W₂ M X₂ Z₂
a b c : M
f : SmallShiftedHom W₁ X₁ Y₁ a
g : SmallShiftedHom W₁ Y₁ Z₁ b
h : b + a = c
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
⊢ b + a + 0 = c

Tactic:
by simpa

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

Goal state before:
pp: C₁ : Type u₁
inst✝¹⁷ : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst✝¹⁶ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst✝¹⁵ : AddMonoid M
inst✝¹⁴ : HasShift C₁ M
inst✝¹³ : HasShift C₂ M
inst✝¹² : Φ.functor.CommShift M
X₁ Y₁ Z₁ : C₁
X₂ Y₂ Z₂ : C₂
inst✝¹¹ : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst✝¹⁰ : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst✝⁹ : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst✝⁸ : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor.obj X₁ ≅ X₂
eY : Φ.functor.obj Y₁ ≅ Y₂
eZ : Φ.functor.obj Z₁ ≅ Z₂
inst✝⁷ : W₁.IsCompatibleWithShift M
inst✝⁶ : W₂.IsCompatibleWithShift M
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂
inst✝² : HasSmallLocalizedShiftedHom W₁ M X₁ Z₁
inst✝¹ : HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁
inst✝ : HasSmallLocalizedShiftedHom W₂ M X₂ Z₂
a b c : M
f : SmallShiftedHom W₁ X₁ Y₁ a
g : SmallShiftedHom W₁ Y₁ Z₁ b
h : b + a = c
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
⊢ b + 0 + a = c

Tactic:
by simpa

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
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
this : HasDerivedCategory C := HasDerivedCategory.standard 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
⊢ α.hom = β.hom

Tactic:
apply BinaryCofan.IsColimit.hom_ext
    (isBinaryBilimitOfPreserves (singleFunctor C 0)
      (BinaryBiproduct.isBilimit X₁ X₂)).isColimit

Goal state after:
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

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
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
n : ℕ
X₁ X₂ X₃ : Cᵒᵖ
f : X₁ ⟶ X₂
f' : X₂ ⟶ X₃
⊢ { app := fun Y ↦ AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α ↦ (Ext.mk₀ (f ≫ f').unop).comp α ⋯) ⋯),
      naturality := ⋯ } =
    { app := fun Y ↦ AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α ↦ (Ext.mk₀ f.unop).comp α ⋯) ⋯), naturality := ⋯ } ≫
      { app := fun Y ↦ AddCommGrpCat.ofHom (AddMonoidHom.mk' (fun α ↦ (Ext.mk₀ f'.unop).comp α ⋯) ⋯), naturality := ⋯ }

Tactic:
by
    ext Y α
    simp

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
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x : Ext c.pt Y n
⊢ ∑ x_1, (mk₀ (c.π x_1 ≫ c.ι x_1)).comp x ⋯ = x

Tactic:
← Ext.sum_comp,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x : Ext c.pt Y n
⊢ (∑ i, mk₀ (c.π i ≫ c.ι i)).comp x ⋯ = x
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:
by
  dsimp at h₀ h₁ h₃ h₄
  have : Mono (app' φ 2) := by
    apply mono_of_epi_of_mono_of_mono (δlastFunctor.map φ) (R₁.exact_iff_δlast.1 hR₁).1
      (R₂.exact_iff_δlast.1 hR₂).1 <;> dsimp <;> infer_instance
  have : Epi (app' φ 2) := by
    apply epi_of_epi_of_epi_of_mono (δ₀Functor.map φ) (R₁.exact_iff_δ₀.1 hR₁).2
      (R₂.exact_iff_δ₀.1 hR₂).2 <;> dsimp <;> infer_instance
  apply isIso_of_mono_of_epi

Goal state after:
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 Z : C
f : Y ⟶ X
n a : ℤ
x : Opposite.op ((shiftFunctor C a).obj Z) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ Quiver.Hom.op ((opEquiv' n a a' h).symm (x ≫ (shiftFunctor Cᵒᵖ n).map f.op)) = (f ≫ (opEquiv' n a a' h).symm x).op

Tactic:
by simp [opEquiv'_symm_apply, opEquiv_symm_apply]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasShift C ℤ
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
A : Cᵒᵖ
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ ((shortComplexOfDistTriangle T hT).map (preadditiveCoyoneda.obj A)).Exact

Tactic:
by
    rw [ShortComplex.ab_exact_iff]
    intro (x₂ : A.unop ⟶ T.obj₂) (hx₂ : x₂ ≫ T.mor₂ = 0)
    obtain ⟨x₁, hx₁⟩ := T.coyoneda_exact₂ hT x₂ hx₂
    exact ⟨x₁, hx₁.symm⟩

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
h : solution.IsPresentationCore
N✝ : Type w''
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : relations.Solution N✝
⊢ solution.postcomp (↑ULift.moduleEquiv ∘ₗ h.desc (s.postcomp ↑ULift.moduleEquiv.symm)) = s

Tactic:
simpa using! congr_postcomp
      (h.postcomp_desc (s.postcomp ULift.moduleEquiv.symm.toLinearMap))
        ULift.moduleEquiv.toLinearMap

Goal state after: