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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : HasShift D ℤ
inst✝ : L.CommShift ℤ
H :
  ∀ (T₁' T₂' : Triangle C),
    T₁' ∈ distinguishedTriangles →
      T₂' ∈ distinguishedTriangles →
        ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
T₁' : Triangle C
e₁ : T₁ ≅ L.mapTriangle.obj T₁'
hT₁' : T₁' ∈ distinguishedTriangles
T₂' : Triangle C
e₂ : T₂ ≅ L.mapTriangle.obj T₂'
hT₂' : T₂' ∈ distinguishedTriangles
comm₁ : (L.mapTriangle.obj T₁').mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ (L.mapTriangle.obj T₂').mor₁
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ (L.mapTriangle.obj T₁').mor₂
comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ (L.mapTriangle.obj T₂').mor₂
comm₃ : (L.mapTriangle.obj T₁').mor₃ ≫ (shiftFunctor D 1).map e₁.inv.hom₁ = e₁.inv.hom₃ ≫ T₁.mor₃
comm₃' : T₂.mor₃ ≫ (shiftFunctor D 1).map e₂.hom.hom₁ = e₂.hom.hom₃ ≫ (L.mapTriangle.obj T₂').mor₃
⊢ ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor D 1).map a = c ≫ T₂.mor₃

Tactic:
dsimp at comm₁ comm₁' comm₂ comm₂' comm₃ comm₃'

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : HasShift D ℤ
inst✝ : L.CommShift ℤ
H :
  ∀ (T₁' T₂' : Triangle C),
    T₁' ∈ distinguishedTriangles →
      T₂' ∈ distinguishedTriangles →
        ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
T₁' : Triangle C
e₁ : T₁ ≅ L.mapTriangle.obj T₁'
hT₁' : T₁' ∈ distinguishedTriangles
T₂' : Triangle C
e₂ : T₂ ≅ L.mapTriangle.obj T₂'
hT₂' : T₂' ∈ distinguishedTriangles
comm₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂
comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂
comm₃ :
  (L.map T₁'.mor₃ ≫ (commShiftIso L 1).hom.app T₁'.obj₁) ≫ (shiftFunctor D 1).map e₁.inv.hom₁ = e₁.inv.hom₃ ≫ T₁.mor₃
comm₃' :
  T₂.mor₃ ≫ (shiftFunctor D 1).map e₂.hom.hom₁ = e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ (commShiftIso L 1).hom.app T₂'.obj₁
⊢ ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor D 1).map a = c ≫ T₂.mor₃
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure

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

Tactic:
op_monotone_iff

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
⊢ P ≤ P.colimitsClosure J
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝¹ : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
a : α
⊢ (P.strictLimitsClosureIter J κ.ord).strictLimitsOfShape (J a) ≤
    (P.strictLimitsClosureIter J κ.ord).strictLimitsOfShape (J a)

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ Hom.mk f = homMk { Y' := f.Y', f := f.f, s := f.s, hs := ⋯ }

Tactic:
rfl

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

Goal state before:
pp: case mp
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₂ : X ⟶ Y
Z : C
t₁ t₂ : Y ⟶ Z
hst : 𝟙 Y ≫ t₁ = 𝟙 Y ≫ t₂
hft : f₁ ≫ t₁ = f₂ ≫ t₂
ht : W (𝟙 Y ≫ t₁)
⊢ ∃ Z s, ∃ (_ : W s), f₁ ≫ s = f₂ ≫ s

Tactic:
grind

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : W.op.LeftFraction (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map L.op ⋯
⊢ φ.map L.op ⋯ = φ.unop.op.map L.op ⋯

Tactic:
rfl

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

Goal state before:
pp: case mp
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
Y Z✝ : C
f₁ f₂ : Y ⟶ Z✝
Z : C
t₁ t₂ : Z ⟶ Y
hst : t₁ ≫ 𝟙 Y = t₂ ≫ 𝟙 Y
hft : t₁ ≫ f₁ = t₂ ≫ f₂
ht : W (t₁ ≫ 𝟙 Y)
⊢ ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂

Tactic:
grind

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
E : Type u_3
inst✝⁴ : Category.{v_3, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
a : M
g : ShiftedHom Y Z a
⊢ a + m₀ = a

Tactic:
by rw [hm₀, add_zero]

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
E : Type u_3
inst✝⁴ : Category.{v_3, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
m₀ : M
hm₀ : m₀ = 0
a : M
f : ShiftedHom X Y a
⊢ a + m₀ = a

Tactic:
by rw [hm₀, add_zero]

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

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
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n : M
X Y : C
f : X ⟶ (shiftFunctor C n).obj Y
a a' : M
h : n + a = a'
⊢ (F.shift a).map (L.map f) ≫
      (e' a).hom.app ((shiftFunctor C n).obj Y) ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y =
    (L ⋙ F' a).map f ≫ (e' a).hom.app ((shiftFunctor C n).obj Y) ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y

Tactic:
rfl

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 Q : ObjectProperty C
X A B : C
f₁ : A ⟶ X
f₂ : X ⟶ B
f₃ : B ⟶ (shiftFunctor C 1).obj A
hT : Triangle.mk f₁ f₂ f₃ ∈ distinguishedTriangles
A' : C
hP : P A'
a₁ : A ⟶ A'
b₁ : A' ⟶ A
h₁ : a₁ ≫ b₁ = 𝟙 A
B' : C
hQ : Q B'
a₃ : B ⟶ B'
b₃ : B' ⟶ B
h₃ : a₃ ≫ b₃ = 𝟙 B
X' : C
g₁ : A' ⟶ X'
g₂ : X' ⟶ B'
hT' : Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁) ∈ distinguishedTriangles
⊢ f₃ ≫ (shiftFunctor C 1).map a₁ = a₃ ≫ b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁

Tactic:
grind

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 Q : ObjectProperty C
X A B : C
f₁ : A ⟶ X
f₂ : X ⟶ B
f₃ : B ⟶ (shiftFunctor C 1).obj A
hT : Triangle.mk f₁ f₂ f₃ ∈ distinguishedTriangles
A' : C
hP : P A'
a₁ : A ⟶ A'
b₁ : A' ⟶ A
h₁ : a₁ ≫ b₁ = 𝟙 A
B' : C
hQ : Q B'
a₃ : B ⟶ B'
b₃ : B' ⟶ B
h₃ : a₃ ≫ b₃ = 𝟙 B
X' : C
g₁ : A' ⟶ X'
g₂ : X' ⟶ B'
hT' : Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁) ∈ distinguishedTriangles
a₂ : X ⟶ X'
ha₁₂ : (Triangle.mk f₁ f₂ f₃).mor₁ ≫ a₂ = a₁ ≫ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁)).mor₁
ha₂₃ : (Triangle.mk f₁ f₂ f₃).mor₂ ≫ a₃ = a₂ ≫ (Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁)).mor₂
⊢ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁) ≫ (shiftFunctor C 1).map b₁ = b₃ ≫ f₃

Tactic:
grind

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 Q : ObjectProperty C
X A B : C
f₁ : A ⟶ X
f₂ : X ⟶ B
f₃ : B ⟶ (shiftFunctor C 1).obj A
hT : Triangle.mk f₁ f₂ f₃ ∈ distinguishedTriangles
A' : C
hP : P A'
a₁ : A ⟶ A'
b₁ : A' ⟶ A
h₁ : a₁ ≫ b₁ = 𝟙 A
B' : C
hQ : Q B'
a₃ : B ⟶ B'
b₃ : B' ⟶ B
h₃ : a₃ ≫ b₃ = 𝟙 B
X' : C
g₁ : A' ⟶ X'
g₂ : X' ⟶ B'
hT' : Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁) ∈ distinguishedTriangles
a₂ : X ⟶ X'
ha₁₂ : f₁ ≫ a₂ = a₁ ≫ g₁
ha₂₃ : f₂ ≫ a₃ = a₂ ≫ g₂
b₂ : X' ⟶ X
hb₁₂ : g₁ ≫ b₂ = b₁ ≫ f₁
hb₂₃ : g₂ ≫ b₃ = b₂ ≫ f₂
⊢ f₁ ≫ a₂ ≫ b₂ = 𝟙 A ≫ f₁

Tactic:
grind

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 Q : ObjectProperty C
X A B : C
f₁ : A ⟶ X
f₂ : X ⟶ B
f₃ : B ⟶ (shiftFunctor C 1).obj A
hT : Triangle.mk f₁ f₂ f₃ ∈ distinguishedTriangles
A' : C
hP : P A'
a₁ : A ⟶ A'
b₁ : A' ⟶ A
h₁ : a₁ ≫ b₁ = 𝟙 A
B' : C
hQ : Q B'
a₃ : B ⟶ B'
b₃ : B' ⟶ B
h₃ : a₃ ≫ b₃ = 𝟙 B
X' : C
g₁ : A' ⟶ X'
g₂ : X' ⟶ B'
hT' : Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁) ∈ distinguishedTriangles
a₂ : X ⟶ X'
ha₁₂ : f₁ ≫ a₂ = a₁ ≫ g₁
ha₂₃ : f₂ ≫ a₃ = a₂ ≫ g₂
b₂ : X' ⟶ X
hb₁₂ : g₁ ≫ b₂ = b₁ ≫ f₁
hb₂₃ : g₂ ≫ b₃ = b₂ ≫ f₂
⊢ f₂ ≫ 𝟙 B = (a₂ ≫ b₂) ≫ f₂

Tactic:
grind

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 Q : ObjectProperty C
X A B : C
f₁ : A ⟶ X
f₂ : X ⟶ B
f₃ : B ⟶ (shiftFunctor C 1).obj A
hT : Triangle.mk f₁ f₂ f₃ ∈ distinguishedTriangles
A' : C
hP : P A'
a₁ : A ⟶ A'
b₁ : A' ⟶ A
h₁ : a₁ ≫ b₁ = 𝟙 A
B' : C
hQ : Q B'
a₃ : B ⟶ B'
b₃ : B' ⟶ B
h₃ : a₃ ≫ b₃ = 𝟙 B
X' : C
g₁ : A' ⟶ X'
g₂ : X' ⟶ B'
hT' : Triangle.mk g₁ g₂ (b₃ ≫ f₃ ≫ (shiftFunctor C 1).map a₁) ∈ distinguishedTriangles
a₂ : X ⟶ X'
ha₁₂ : f₁ ≫ a₂ = a₁ ≫ g₁
ha₂₃ : f₂ ≫ a₃ = a₂ ≫ g₂
b₂ : X' ⟶ X
hb₁₂ : g₁ ≫ b₂ = b₁ ≫ f₁
hb₂₃ : g₂ ≫ b₃ = b₂ ≫ f₂
φ : Triangle.mk f₁ f₂ f₃ ⟶ Triangle.mk f₁ f₂ f₃ :=
  (Triangle.mk f₁ f₂ f₃).homMk (Triangle.mk f₁ f₂ f₃) (𝟙 A) (a₂ ≫ b₂) (𝟙 B) ⋯ ⋯ ⋯
this : IsIso (a₂ ≫ b₂)
⊢ a₂ ≫ b₂ ≫ inv (a₂ ≫ b₂) = 𝟙 X

Tactic:
grind

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

Tactic:
rfl

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
⊢ P.extensionProductIter (0 + 1) = (P.extensionProductIter 0).extensionProduct P

Tactic:
rfl

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
L₁ : C₁ ⥤ C₂
L₂ : C₂ ⥤ C₃
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝¹ : L₁.IsLocalization W₁
inst✝ : L₂.IsLocalization W₂
W₃ : MorphismProperty C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := { functor := E₂.functor, map := ⋯ }
⊢ W₂' ≤ W₂.map Φ.functor

Tactic:
rfl

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 M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ'
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso φ

Tactic:
rw [← quasiIso_iff_comp_right φ φ']

Goal state after:
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ'
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso (φ ≫ φ')
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.ContainsZero
n m : ℕ
⊢ P.extensionProductIter n ≤ P.extensionProductIter n

Tactic:
rfl

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 : HomologicalComplex C c
inst✝ : CategoryWithHomology C
f : K ⟶ L
⊢ quasiIso C c f ↔ QuasiIso f

Tactic:
rfl

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
X Y : C
f : X ⟶ Y
⊢ P.trW f ↔ ∃ Z g h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), P Z

Tactic:
rfl

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 : HomotopyCategory C c
f : X ⟶ Y
⊢ quasiIso C c f ↔ ∀ (n : ι), IsIso ((homologyFunctor C c n).map f)

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : (up ℤ).next i = j
hf : f ≫ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = 0
i' : ℤ
hi' : n + i = i'
j' : ℤ
hj' : (up ℤ).next i' = j'
⊢ (sc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i).liftCycles f ⋯ ≫
      (sc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i).homologyπ =
    ((shiftFunctor C n ⋙ shortComplexFunctor C (up ℤ) i).obj K).liftCycles f ⋯ ≫
      ((shiftFunctor C n ⋙ shortComplexFunctor C (up ℤ) i).obj K).homologyπ

Tactic:
rfl

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

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 : C ⥤ D
ι : Type u_3
c : ComplexShape ι
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
inst✝⁸ : CategoryWithHomology C
inst✝⁷ : CategoryWithHomology D
inst✝⁶ : (HomologicalComplex.quasiIso D c).HasLocalization
inst✝⁵ : F.Additive
inst✝⁴ : F.PreservesHomology
inst✝³ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝² : c.QFactorsThroughHomotopy C
inst✝¹ : c.QFactorsThroughHomotopy D
inst✝ : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)
K : HomologicalComplex C c
⊢ (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K =
    (F.mapHomologicalComplexUpToQuasiIso c).map
        (𝟙 (HomologicalComplexUpToQuasiIso.Qh.obj ((HomotopyCategory.quotient C c).obj K))) ≫
      (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫
        𝟙
            (HomologicalComplexUpToQuasiIso.Qh.obj
              ((F.mapHomotopyCategory c).obj ((HomotopyCategory.quotient C c).obj K))) ≫
          HomologicalComplexUpToQuasiIso.Qh.map
            (𝟙 ((F.mapHomotopyCategory c).obj ((HomotopyCategory.quotient C c).obj K)))

Tactic:
simp only [map_id, Category.comp_id, Category.id_comp]

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

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
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
a : A
X : C
⊢ ((F.functor a).isoWhiskerLeft (shiftFunctorZero D A)).hom.app X = (shiftFunctorZero D A).hom.app ((F.functor a).obj X)

Tactic:
rfl

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

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
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
a : A
X : C
⊢ ((F.functor a).isoWhiskerLeft (shiftFunctorZero D A)).inv.app X = (shiftFunctorZero D A).inv.app ((F.functor a).1 X)

Tactic:
rfl

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

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (DerivedCategory C)
⊢ (∃ X Y f, Nonempty (T ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))) → T ∈ distinguishedTriangles

Tactic:
· rintro ⟨X, Y, f, ⟨e⟩⟩
    refine isomorphic_distinguished _ (Qh.map_distinguished _ ?_) _
      (e ≪≫ (Functor.mapTriangleIso (quotientCompQhIso C)).symm.app _ ≪≫
      (Functor.mapTriangleCompIso (HomotopyCategory.quotient C _) Qh).app _)
    exact ⟨_, _, f, ⟨Iso.refl _⟩⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
X : C
⊢ 𝟙 (HomologicalComplexUpToQuasiIso.Q.obj (((CochainComplex.singleFunctors C).functor n).obj X)) =
    𝟙 (((singleFunctors C).functor n).obj X)

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
X : C
⊢ (quotientCompQhIso C).inv.app (((CochainComplex.singleFunctors C).functor n).obj X) =
    𝟙 (Q.obj (((CochainComplex.singleFunctors C).functor n).obj X))

Tactic:
rfl

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (imageSubobjectIso g.op).hom ≫ (imageUnopOp g.op).inv ≫ (factorThruImage g.op.unop).op =
    (imageSubobjectIso g.op).hom ≫ (imageOpOp g).inv ≫ (factorThruImage g).op

Tactic:
rfl

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

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
j : ι
⊢ X K (some j) = K.X j

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
j : Option ι
⊢ d K none j = 0

Tactic:
rfl

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

Goal state before:
pp: case none
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
⊢ d K none none = 0

Tactic:
rfl

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

Goal state before:
pp: case some
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
val✝ : ι
⊢ d K (some val✝) none = 0

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i✝ j✝ : Option ι
i j : ι
⊢ (XIso K ⋯).inv.op ≫ (K.d j i).op ≫ (XIso K ⋯).hom.op = (XIso K.op ⋯).hom ≫ K.op.d i j ≫ (XIso K.op ⋯).inv

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
a : ι
⊢ mapX φ (some a) = φ.f a

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
⊢ mapX φ none = 0

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
⊢ ((opFunctor V c).obj (op K)).HasHomology i

Tactic:
by
  dsimp
  infer_instance

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

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex Vᵒᵖ c
i : ι
inst✝ : K.HasHomology i
⊢ ((unopFunctor V c).obj (op K)).HasHomology i

Tactic:
by
  dsimp
  infer_instance

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

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝³ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝² : HasZeroMorphisms V
K L : HomologicalComplex Vᵒᵖ c
φ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ QuasiIsoAt ((opFunctor V c.symm).map ((unopFunctor V c).map φ.op).op) i ↔ QuasiIsoAt φ i

Tactic:
rfl

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst✝ : Preadditive V
F G : HomologicalComplex V c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
⊢ (prevD n) h.hom + (dNext n) h.hom + φ₂.f n =
    ((((dNext n) fun i j ↦ (h.hom j i).op) + (prevD n) fun i j ↦ (h.hom j i).op) + (φ₂.f n).op).unop

Tactic:
rfl

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
ι : Type u_2
c : ComplexShape ι
inst✝ : Preadditive V
F G : HomologicalComplex Vᵒᵖ c
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
n : ι
⊢ (prevD n) h.hom + (dNext n) h.hom + φ₂.f n =
    ((((dNext n) fun i j ↦ (h.hom j i).unop) + (prevD n) fun i j ↦ (h.hom j i).unop) + (φ₂.f n).unop).op

Tactic:
rfl

Goal state after: