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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ (δ n m z).v p q hpq = Cochain.v 0 p q hpq

Tactic:
dsimp only [δ]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ (Cochain.mk fun p q hpq ↦ z.v p (p + n) ⋯ ≫ G.d (p + n) q + m.negOnePow • F.d p (p + m - n) ≫ z.v (p + m - n) q ⋯).v p
      q hpq =
    Cochain.v 0 p q hpq
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (nullHomotopicMap hom).f k₁ = C.d k₁ k₀ ≫ hom k₀ k₁

Tactic:
by
  dsimp only [nullHomotopicMap]
  rw [dNext_eq hom r₁₀, prevD, AddMonoidHom.mk'_apply, D.shape, comp_zero, add_zero]
  exact hk₁ _

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ 0 + m.negOnePow • 0 ≫ z.v (p + m - n) q ⋯ = 0

pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ ¬(ComplexShape.up ℤ).Rel (p + n) q

pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ ¬(ComplexShape.up ℤ).Rel p (p + m - n)

Tactic:
zero_add,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ m.negOnePow • 0 ≫ z.v (p + m - n) q ⋯ = 0

case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ ¬(ComplexShape.up ℤ).Rel (p + n) q

case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : ¬n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ ¬(ComplexShape.up ℤ).Rel p (p + m - n)
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F₁ F₂ : Quotient r ⥤ D
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ F₁ = F₂

Tactic:
rw [lift_unique r (functor r ⋙ F₂) _ F₂ rfl]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F₁ F₂ : Quotient r ⥤ D
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ F₁ = lift r (functor r ⋙ F₂) ?m.62

C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F₁ F₂ : Quotient r ⥤ D
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ F₂).map f₁ = (functor r ⋙ F₂).map f₂
Module: Mathlib.CategoryTheory.Shift.Induced

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
this :
  (Induced.add F s i (m₁ + m₂) m₃).hom ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃) =
    eqToHom ⋯ ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom
X : D
⊢ (Induced.add F s i (m₁ + m₂) m₃).hom.app X ≫ (s m₃).map ((Induced.add F s i m₁ m₂).hom.app X) =
    eqToHom ⋯ ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom.app X ≫ (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj X)

Tactic:
simpa using NatTrans.congr_app this X

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
a b : ℤ
⊢ shiftFunctorAdd (CochainComplex C ℤ) a b = shiftFunctorAdd' C a b (a + b) ⋯

Tactic:
← CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
a b : ℤ
⊢ CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯ = shiftFunctorAdd' C a b (a + b) ⋯
Module: Mathlib.CategoryTheory.Shift.Induced

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
n : A
this : (Induced.add F s i 0 n).hom = eqToHom ⋯ ≫ whiskerRight (Induced.zero F s i).inv (s n)
X : D
⊢ (Induced.add F s i 0 n).hom.app X = eqToHom ⋯ ≫ (s n).map ((Induced.zero F s i).inv.app X)

Tactic:
simpa using NatTrans.congr_app this X

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

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
n : A
this : (Induced.add F s i n 0).hom = eqToHom ⋯ ≫ (s n).whiskerLeft (Induced.zero F s i).inv
X : D
⊢ (Induced.add F s i n 0).hom.app X = eqToHom ⋯ ≫ (Induced.zero F s i).inv.app ((s n).obj X)

Tactic:
simpa using NatTrans.congr_app this X

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ e.inv.hom₂ ≫ e.hom.hom₂ = 𝟙 B.obj₂

Tactic:
rw [← comp_hom₂, e.inv_hom_id, id_hom₂]

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

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₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : F₁.CommShift A
inst✝ : F₂.CommShift A
⊢ (Functor.commShiftIso F₁ 0).hom ≫ Functor.whiskerRight τ (shiftFunctor D 0) =
    (shiftFunctor C 0).whiskerLeft τ ≫ (Functor.commShiftIso F₂ 0).hom

Tactic:
ext X
    simp [Functor.commShiftIso_zero, ← NatTrans.naturality]

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

Goal state before:
pp: case mpr
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ Mono T.mor₂ → T.mor₁ = 0

Tactic:
· intro
    rw [← cancel_mono T.mor₂, comp_distTriang_mor_zero₁₂ _ hT, zero_comp]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
π : C ⥤ D
H : D ⥤ A
e : π ⋙ H ≅ F
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
G : Type u_5
inst✝³ : AddGroup G
inst✝² : HasShift C G
inst✝¹ : F.ShiftSequence M
inst✝ : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ (shiftFunctor C m).obj Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ m + 0 = 0 + m

Tactic:
zero_add,

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
π : C ⥤ D
H : D ⥤ A
e : π ⋙ H ≅ F
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
G : Type u_5
inst✝³ : AddGroup G
inst✝² : HasShift C G
inst✝¹ : F.ShiftSequence M
inst✝ : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ (shiftFunctor C m).obj Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ m + 0 = m
Module: Mathlib.CategoryTheory.Shift.ShiftSequence

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} A
F : C ⥤ A
G : Type u_5
inst✝² : AddGroup G
inst✝¹ : HasShift C G
inst✝ : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ (shiftFunctor C m).obj Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ m + 0 = 0 + m

Tactic:
zero_add,

Goal state after:
C : Type u_1
A : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} A
F : C ⥤ A
G : Type u_5
inst✝² : AddGroup G
inst✝¹ : HasShift C G
inst✝ : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ (shiftFunctor C m).obj Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ m + 0 = m
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₂
h : Φ.IsLocalizedFullyFaithful
inst✝ : CatCommSq Φ.functor L₁ L₂ G
⊢ Nonempty (Φ.localizedFunctor W₁.Q W₂.Q).FullyFaithful

Tactic:
exact h.nonempty_fullyFaithful

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
φ : W.RightFraction₂ X Y
inst✝ : W.HasLeftCalculusOfFractions
ψ₁ : W.LeftFraction X Y
hψ₁ : φ.fst.f ≫ ψ₁.s = φ.fst.s ≫ ψ₁.f
ψ₂ : W.LeftFraction X Y
hψ₂ : φ.snd.f ≫ ψ₂.s = φ.snd.s ≫ ψ₂.f
⊢ ∃ ψ, φ.f ≫ ψ.s = φ.s ≫ ψ.f ∧ φ.f' ≫ ψ.s = φ.s ≫ ψ.f'

Tactic:
obtain ⟨α, hα⟩ := (RightFraction.mk _ ψ₁.hs ψ₂.s).exists_leftFraction

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
φ : W.RightFraction₂ X Y
inst✝ : W.HasLeftCalculusOfFractions
ψ₁ : W.LeftFraction X Y
hψ₁ : φ.fst.f ≫ ψ₁.s = φ.fst.s ≫ ψ₁.f
ψ₂ : W.LeftFraction X Y
hψ₂ : φ.snd.f ≫ ψ₂.s = φ.snd.s ≫ ψ₂.f
α : W.LeftFraction ψ₁.Y' ψ₂.Y'
hα : { X' := Y, s := ψ₁.s, hs := ⋯, f := ψ₂.s }.f ≫ α.s = { X' := Y, s := ψ₁.s, hs := ⋯, f := ψ₂.s }.s ≫ α.f
⊢ ∃ ψ, φ.f ≫ ψ.s = φ.s ≫ ψ.f ∧ φ.f' ≫ ψ.s = φ.s ≫ ψ.f'
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
X' Y' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
f₁ f₂ : X' ⟶ Y'
⊢ f₁ + f₂ = add W eX eY f₁ f₂

Tactic:
apply add_eq_add

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
P : ObjectProperty C
inst✝ : P.IsTriangulatedClosed₂
X Z : C
c : Z ⟶ (shiftFunctor C 1).obj X
hX : P X
hZ : P Z
⊢ ∃ Y, ∃ (_ : P Y), ∃ a b, Triangle.mk a b c ∈ distinguishedTriangles

Tactic:
obtain ⟨Y, a, b, h⟩ := distinguished_cocone_triangle₂ c

Goal state after:
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
inst✝ : P.IsTriangulatedClosed₂
X Z : C
c : Z ⟶ (shiftFunctor C 1).obj X
hX : P X
hZ : P Z
Y : C
a : X ⟶ Y
b : Y ⟶ Z
h : Triangle.mk a b c ∈ distinguishedTriangles
⊢ ∃ Y, ∃ (_ : P Y), ∃ a b, Triangle.mk a b c ∈ distinguishedTriangles
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z W : C
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
x✝ : IsIso g
⊢ MorphismProperty.isomorphisms C f

Tactic:
by
    refine ⟨h.i.right ≫ inv g ≫ h.r.left, ?_, ?_⟩
    · rw [← h.i_w_assoc, IsIso.hom_inv_id_assoc, h.retract_left]
    · rw [Category.assoc, Category.assoc, h.r_w, IsIso.inv_hom_id_assoc, h.retract_right]

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

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
c : ComplexShape ι
K L K' L' : HomologicalComplex C c
f : K ⟶ L
f' : K' ⟶ L'
h : RetractArrow f f'
i : ι
inst✝³ : K.HasHomology i
inst✝² : L.HasHomology i
inst✝¹ : K'.HasHomology i
inst✝ : L'.HasHomology i
hf' : QuasiIsoAt f' i
⊢ QuasiIsoAt f i

Tactic:
rw [quasiIsoAt_iff] at hf' ⊢

Goal state after:
ι : Type u_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
c : ComplexShape ι
K L K' L' : HomologicalComplex C c
f : K ⟶ L
f' : K' ⟶ L'
h : RetractArrow f f'
i : ι
inst✝³ : K.HasHomology i
inst✝² : L.HasHomology i
inst✝¹ : K'.HasHomology i
inst✝ : L'.HasHomology i
hf' : ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f')
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f) ↔ IsIso (homologyMap f i)

Tactic:
ShortComplex.quasiIso_iff

Goal state after:
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f)) ↔ IsIso (homologyMap f i)
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case a
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 Q : ObjectProperty C
⊢ (P.extensionProduct Q).retractClosure ≤ (P.retractClosure.extensionProduct Q.retractClosure).retractClosure

Tactic:
· apply monotone_retractClosure
    grw [monotone_extensionProduct_right _ (le_retractClosure Q),
      monotone_extensionProduct_left _ (le_retractClosure P)]

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
P : ObjectProperty C
inst✝ : IsTriangulated C
m m' : ℕ
h : m = m' + 1
⊢ P.extensionProductIter (0 + m) = (P.extensionProductIter 0).extensionProduct (P.extensionProductIter m')

Tactic:
zero_add,

Goal state after:
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
P : ObjectProperty C
inst✝ : IsTriangulated C
m m' : ℕ
h : m = m' + 1
⊢ P.extensionProductIter m = (P.extensionProductIter 0).extensionProduct (P.extensionProductIter m')
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
e : HomotopyEquiv K L
n : ι
inst✝¹ : K.HasHomology n
inst✝ : L.HasHomology n
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c n).map e.hom)

Tactic:
ShortComplex.quasiIso_iff

Goal state after:
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
e : HomotopyEquiv K L
n : ι
inst✝¹ : K.HasHomology n
inst✝ : L.HasHomology n
⊢ IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c n).map e.hom))
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 L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
this : DecidableRel c.Rel
⊢ F.map f = F.map g

Tactic:
exact h.map_eq_of_inverts_homotopyEquivalences hc F hF

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
⊢ NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯ =
    (single C (ComplexShape.up ℤ) a'').isoWhiskerLeft (shiftFunctorAdd (CochainComplex C ℤ) m n) ≪≫
      ((single C (ComplexShape.up ℤ) a'').associator (CategoryTheory.shiftFunctor (CochainComplex C ℤ) m)
            (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n)).symm ≪≫
        Functor.isoWhiskerRight (NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯)
            (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n) ≪≫
          NatIso.ofComponents (fun X ↦ Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯) ⋯

Tactic:
ext
    dsimp
    simp only [shiftFunctorAdd_eq, shiftFunctorAdd'_hom_app_f, XIsoOfEq,
      eqToIso.hom, eqToHom_trans, id_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✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
Z : C
g : X ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X'
H : Triangle.mk s g h ∈ distinguishedTriangles
mem : P Z
hf₁ : s ≫ f₁ = s ≫ f₂
hf₂ : s ≫ (f₁ - f₂) = 0
⊢ ∃ Y' t, ∃ (_ : P.trW t), f₁ ≫ t = f₂ ≫ t

Tactic:
obtain ⟨q, hq⟩ := Triangle.yoneda_exact₂ _ H _ hf₂

Goal state after:
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✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
Z : C
g : X ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X'
H : Triangle.mk s g h ∈ distinguishedTriangles
mem : P Z
hf₁ : s ≫ f₁ = s ≫ f₂
hf₂ : s ≫ (f₁ - f₂) = 0
q : (Triangle.mk s g h).obj₃ ⟶ Y
hq : f₁ - f₂ = (Triangle.mk s g h).mor₂ ≫ q
⊢ ∃ Y' t, ∃ (_ : P.trW t), f₁ ≫ t = f₂ ≫ t
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inl
ι : 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' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
hi' : e.r i' = none
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0

Tactic:
extend.d_none_eq_zero K _ _ hi',

Goal state after:
case inl
ι : 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' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
hi' : e.r i' = none
⊢ 0 ≫ extend.d K (e.r j') (e.r k') = 0
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

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 L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
⊢ 0 =
    ((shortComplexFunctor C c' j').obj K).fromOpcycles ≫
      (K.restrictionXIso e hk').inv ≫ (K.restrictionToTruncGE' e).f k ≫ ((K.truncGE' e).extendXIso e hk').inv

Tactic:
K.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv e hk' hj

Goal state after:
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 L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
⊢ 0 =
    ((shortComplexFunctor C c' j').obj K).fromOpcycles ≫
      (K.restrictionXIso e hk').inv ≫
        ((K.restrictionXIso e hk').hom ≫ K.pOpcycles (c'.next j') ≫ (K.truncGE'XIsoOpcycles e hk' hj).inv) ≫
          ((K.truncGE' e).extendXIso e hk').inv
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'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.cyclesIso.hom ≫
      (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.π =
    (K.extendCyclesIso e hj').hom ≫ (K.sc j).homologyData.left.cyclesIso.hom ≫ (K.sc j).homologyData.left.π

Tactic:
dsimp [extendCyclesIso]

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'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.cyclesIso.hom ≫ (K.sc j).homologyData.left.π =
    ((extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.cyclesIso.hom ≫
        (K.sc j).homologyData.left.cyclesIso.inv) ≫
      (K.sc j).homologyData.left.cyclesIso.hom ≫ (K.sc j).homologyData.left.π
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
⊢ Function.Bijective (fromSum e₁ e₂)

Tactic:
by
  constructor
  · rintro (i₁ | i₂) (j₁ | j₂) h
    · obtain rfl := e₁.injective_f h
      rfl
    · exact (ac.disjoint _ _ h).elim
    · exact (ac.disjoint _ _ h.symm).elim
    · obtain rfl := e₂.injective_f h
      rfl
  · intro n
    obtain ⟨i₁, rfl⟩ | ⟨i₂, rfl⟩ := ac.union n
    · exact ⟨Sum.inl i₁, rfl⟩
    · exact ⟨Sum.inr i₂, rfl⟩

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

Goal state before:
pp: case mpr
ι : 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✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex C c
⊢ K.IsSupported e₂ → K.IsSupportedOutside e₁

Tactic:
· intro _
    exact ⟨fun i₁ => K.exactAt_of_isSupported e₂ _
      (fun i₂ => (ac.disjoint i₁ i₂).symm)⟩

Goal state after: