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

Goal state before:
pp: C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_5, u_5} D₁
inst✝⁴ : Category.{v_6, u_6} D₂
inst✝³ : Category.{v_7, u_7} D₃
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝² : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝¹ : L₂.IsLocalization W
L₃ : C ⥤ D₃
inst✝ : L₃.IsLocalization W
X Y : C
f : L₁.obj X ⟶ L₁.obj Y
⊢ (homEquiv W L₂ L₃) ((homEquiv W L₁ L₂) f) = (homEquiv W L₁ L₃) f

Tactic:
by

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
A : C
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
by

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✝¹ : Preadditive C
K : CochainComplex C ℤ
n : ℤ
inst✝ : K.IsStrictlyGE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : autoParam (i < n') isStrictlyGE_iff._auto_1
⊢ i + a < n

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_5, u_5} D₁
inst✝² : Category.{v_6, u_6} D₂
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝¹ : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝ : L₂.IsLocalization W
X Y Z : C
f : L₁.obj X ⟶ L₁.obj Y
g : L₁.obj Y ⟶ L₁.obj Z
⊢ (homEquiv W L₁ L₂) (f ≫ g) = (homEquiv W L₁ L₂) f ≫ (homEquiv W L₁ L₂) g

Tactic:
by

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✝¹ : Preadditive C
K : CochainComplex C ℤ
n : ℤ
inst✝ : K.IsStrictlyGE n
a n' : ℤ
h : a + n' = n
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsStrictlyGE n'

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_5, u_5} D₁
inst✝² : Category.{v_6, u_6} D₂
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝¹ : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝ : L₂.IsLocalization W
X Y : C
f : X ⟶ Y
⊢ (homEquiv W L₁ L₂) (L₁.map f) = L₂.map f

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_5, u_5} D₁
inst✝² : Category.{v_6, u_6} D₂
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝¹ : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝ : L₂.IsLocalization W
X : C
⊢ (homEquiv W L₁ L₂) (𝟙 (L₁.obj X)) = 𝟙 (L₂.obj X)

Tactic:
by

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 ℤ
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
⊢ IsIso (Q.map (CochainComplex.truncGEMap s a))

Tactic:
by

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✝² : Preadditive C
K : CochainComplex C ℤ
inst✝¹ : CategoryWithHomology C
n : ℤ
inst✝ : K.IsLE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : n' < i
⊢ n < a + i

Tactic:
by

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✝² : Preadditive C
K : CochainComplex C ℤ
inst✝¹ : CategoryWithHomology C
n : ℤ
inst✝ : K.IsLE n
a n' : ℤ
h : a + n' = n
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsLE n'

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
⊢ HasSmallLocalizedHom W X Y ↔ Small.{w, v₂} (L.obj X ⟶ L.obj Y)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
⊢ HasSmallLocalizedHom W X Y

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
inst✝¹ : L.IsLocalization W
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
⊢ Small.{w, v₂} (L.obj X ⟶ L.obj Y)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_5, u_5} D₁
inst✝² : Category.{v_6, u_6} D₂
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝¹ : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝ : L₂.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
⊢ (homEquiv W L₁ L₂) (isoOfHom L₁ W f hf).inv = (isoOfHom L₂ W f hf).inv

Tactic:
by

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:
by

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'
inst✝ : HasSmallLocalizedHom W X Y
⊢ HasSmallLocalizedHom W X' Y'

Tactic:
by

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 Y' : C
f : Y ⟶ Y'
hf : W f
⊢ HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X Y'

Tactic:
by

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

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✝² : Preadditive C
K : CochainComplex C ℤ
inst✝¹ : CategoryWithHomology C
n : ℤ
inst✝ : K.IsGE n
a n' : ℤ
h : a + n' = n
i : ℤ
hi : i < n'
⊢ a + i < n

Tactic:
by

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✝² : Preadditive C
K : CochainComplex C ℤ
inst✝¹ : CategoryWithHomology C
n : ℤ
inst✝ : K.IsGE n
a n' : ℤ
h : a + n' = n
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsGE n'

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
D' : Type u₃
inst✝³ : Category.{v₃, u₃} D'
L : C ⥤ D
inst✝² : L.IsLocalization W
L' : C ⥤ D'
inst✝¹ : L'.IsLocalization W
G : D ⥤ D'
e : L ⋙ G ≅ L'
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
⊢ (homEquiv W W.Q L')
      ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) ((homEquiv W L W.Q) f))) =
    e.inv.app X ≫ G.map f ≫ e.hom.app Y

Tactic:
rw [Equiv.symm_apply_apply, homEquiv_trans]

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
D' : Type u₃
inst✝³ : Category.{v₃, u₃} D'
L : C ⥤ D
inst✝² : L.IsLocalization W
L' : C ⥤ D'
inst✝¹ : L'.IsLocalization W
G : D ⥤ D'
e : L ⋙ G ≅ L'
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
⊢ (homEquiv W L L') f = e.inv.app X ≫ G.map f ≫ e.hom.app Y
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
D' : Type u₃
inst✝³ : Category.{v₃, u₃} D'
L : C ⥤ D
inst✝² : L.IsLocalization W
L' : C ⥤ D'
inst✝¹ : L'.IsLocalization W
G : D ⥤ D'
e : L ⋙ G ≅ L'
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
⊢ (equiv W L') ((equiv W L).symm f) = e.inv.app X ≫ G.map f ≫ e.hom.app Y

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
inst✝¹ : L.IsLocalization W
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
f : X ⟶ Y
⊢ (equiv W L) (mk W f) = L.map f

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
inst✝¹ : L.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
inst✝ : HasSmallLocalizedHom W X Y
⊢ (equiv W L) (mkInv f hf) = (isoOfHom L W f hf).inv

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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 ℤ
a b : ℤ
inst✝² : X.IsStrictlyGE a
inst✝¹ : X.IsStrictlyLE b
inst✝ : Y.IsStrictlyGE a
f : Q.obj X ⟶ Q.obj Y
⊢ ∃ X',
    ∃ (_ : X'.IsStrictlyGE a) (_ : X'.IsStrictlyLE b), ∃ s, ∃ (x : IsIso (Q.map s)), ∃ g, f = inv (Q.map s) ≫ Q.map g

Tactic:
by

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

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

Tactic:
by

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 ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
⊢ IsIso (Q.map (CochainComplex.truncLEMap s b))

Tactic:
by

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

Goal state before:
pp: C✝ : Type u_1
inst✝⁵ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝⁴ : Category.{?u.7, u_2} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n✝ n : ℤ
⊢ (embeddingUpIntGE n).f 0 = n

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝³ : L.IsLocalization W
X Y Z : C
inst✝² : HasSmallLocalizedHom W X Y
inst✝¹ : HasSmallLocalizedHom W Y Z
inst✝ : HasSmallLocalizedHom W X Z
α : SmallHom W X Y
β : SmallHom W Y Z
⊢ (equiv W L) (α.comp β) = (equiv W L) α ≫ (equiv W L) β

Tactic:
by

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 Z : C
inst✝² : HasSmallLocalizedHom W X Y
inst✝¹ : HasSmallLocalizedHom W Y Z
inst✝ : HasSmallLocalizedHom W X Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (equiv W W.Q) ((mk W f).comp (mk W g)) = (equiv W W.Q) (mk W (f ≫ g))

Tactic:
by

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 : C
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W Y Y
α : SmallHom W X Y
⊢ (equiv W W.Q) (α.comp (mk W (𝟙 Y))) = (equiv W W.Q) α

Tactic:
by

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

Goal state before:
pp: C✝ : Type u_1
inst✝⁵ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝⁴ : Category.{?u.7, u_2} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n✝ n : ℤ
⊢ (embeddingUpIntGE n).BoundaryGE 0

Tactic:
by

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 : C
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W X X
α : SmallHom W X Y
⊢ (equiv W W.Q) ((mk W (𝟙 X)).comp α) = (equiv W W.Q) α

Tactic:
by

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 Z T : C
inst✝⁵ : HasSmallLocalizedHom W X Y
inst✝⁴ : HasSmallLocalizedHom W X Z
inst✝³ : HasSmallLocalizedHom W X T
inst✝² : HasSmallLocalizedHom W Y Z
inst✝¹ : HasSmallLocalizedHom W Y T
inst✝ : HasSmallLocalizedHom W Z T
α : SmallHom W X Y
β : SmallHom W Y Z
γ : SmallHom W Z T
⊢ (α.comp β).comp γ = α.comp (β.comp γ)

Tactic:
by

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 : C
inst✝² : HasSmallLocalizedHom W X Y
inst✝¹ : HasSmallLocalizedHom W Y X
inst✝ : HasSmallLocalizedHom W Y Y
f : Y ⟶ X
hf : W f
⊢ (equiv W W.Q) ((mk W f).comp (mkInv f hf)) = (equiv W W.Q) (mk W (𝟙 Y))

Tactic:
by

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

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

Tactic:
by

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 : C
inst✝² : HasSmallLocalizedHom W X X
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W Y X
f : Y ⟶ X
hf : W f
⊢ (equiv W W.Q) ((mkInv f hf).comp (mk W f)) = (equiv W W.Q) (mk W (𝟙 X))

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝² : L.IsLocalization W
X Y : C
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W X Y
e : SmallHom W X Y
⊢ (equiv W L) (chgUniv e) = (equiv W L) e

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : CochainComplex C ℤ
inst✝ : ∀ (i : ℤ), HasHomology K i
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ Acyclic (K.truncGE n₁) ↔ K.IsLE n₀

Tactic:
by

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

Goal state before:
pp: C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : CochainComplex C ℤ
inst✝ : ∀ (i : ℤ), HasHomology K i
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ Acyclic (K.truncLE n₀) ↔ K.IsGE n₁

Tactic:
by

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 : ℤ
⊢ (K.shortComplexTruncLE n).ShortExact

Tactic:
by

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₁ : ℤ
h : n₀ + 1 = n₁
⊢ (K.shortComplexTruncLE n₀).g ≫ K.shortComplexTruncLEX₃ToTruncGE n₀ n₁ h = K.πTruncGE n₁

Tactic:
by

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₁
⊢ K.d n₀ n₁ ≫ pOpcycles K n₁ = 0

Tactic:
by

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 ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
⊢ ∃ Y', ∃ (_ : Y'.IsStrictlyGE a) (_ : Y'.IsStrictlyLE b), ∃ g s, ∃ (x : IsIso (Q.map s)), f = Q.map g ≫ inv (Q.map s)

Tactic:
by

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 ℤ).prev n₀ = n₀ - 1

Tactic:
by

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

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 ℤ
a b : ℤ
h : a < b
inst✝¹ : X.IsStrictlyLE a
inst✝ : Y.IsStrictlyGE b
this : ∀ (f : Q.obj X ⟶ Q.obj Y), f = 0
⊢ ∀ (a b : Q.obj X ⟶ Q.obj Y), a = b

Tactic:
by

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₁
⊢ T.Exact

Tactic:
by

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 := ⋯ }
⊢ Mono S.f

Tactic:
by

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 := ⋯ }
this : Mono S.f
⊢ (up ℤ).prev n₁ = n₀

Tactic:
by

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₁
⊢ Injective (opcycles K n₁)

Tactic:
by

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 ℤ
a b : ℤ
h : a < b
inst✝¹ : X.IsStrictlyLE a
inst✝ : Y.IsStrictlyGE b
X' : CochainComplex C ℤ
w✝¹ : X'.IsStrictlyLE a
s : X' ⟶ X
w✝ : IsIso (Q.map s)
g : X' ⟶ Y
i : ℤ
hi : ¬a < i
⊢ i < b

Tactic:
by

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 ℤ
a b : ℤ
h : a < b
inst✝¹ : X.IsStrictlyLE a
inst✝ : Y.IsStrictlyGE b
X' : CochainComplex C ℤ
w✝¹ : X'.IsStrictlyLE a
s : X' ⟶ X
w✝ : IsIso (Q.map s)
g : X' ⟶ Y
⊢ g = 0

Tactic:
by

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 ℤ
a b : ℤ
h : a < b
inst✝¹ : X.IsStrictlyLE a
inst✝ : Y.IsStrictlyGE b
⊢ Subsingleton (Q.obj X ⟶ Q.obj Y)

Tactic:
by

Goal state after: