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

Goal state before:
pp: case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y✝ Z : C
z₁ : W.LeftFraction X Y✝
z₂ : W.LeftFraction Y✝ Z
z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f
z₄ : W.LeftFraction z₃.Y' z₃'.Y'
fac : z₃'.s ≫ z₄.s = z₃.s ≫ z₄.f
eq : z₁.s ≫ z₃.f ≫ z₄.f = z₁.s ≫ z₃'.f ≫ z₄.s
Y : C
t : z₄.Y' ⟶ Y
ht : W t
fac' : z₃.f ≫ z₄.f ≫ t = z₃'.f ≫ z₄.s ≫ t
⊢ W ((z₁.comp₀ z₂ z₃).s ≫ z₄.f ≫ t)

Tactic:
simp only [comp₀, assoc, ← reassoc_of% fac]

Goal state after:
case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y✝ Z : C
z₁ : W.LeftFraction X Y✝
z₂ : W.LeftFraction Y✝ Z
z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f
z₄ : W.LeftFraction z₃.Y' z₃'.Y'
fac : z₃'.s ≫ z₄.s = z₃.s ≫ z₄.f
eq : z₁.s ≫ z₃.f ≫ z₄.f = z₁.s ≫ z₃'.f ≫ z₄.s
Y : C
t : z₄.Y' ⟶ Y
ht : W t
fac' : z₃.f ≫ z₄.f ≫ t = z₃'.f ≫ z₄.s ≫ t
⊢ W (z₂.s ≫ z₃'.s ≫ z₄.s ≫ t)
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₂
inst✝ : Φ.IsLocalizedFullyFaithful
⊢ Φ.op.IsLocalizedFullyFaithful

Tactic:
let G := Φ.localizedFunctor W₁.Q W₂.Q

Goal state after:
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₂
inst✝ : Φ.IsLocalizedFullyFaithful
G : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor W₁.Q W₂.Q
⊢ Φ.op.IsLocalizedFullyFaithful
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
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f
⊢ LeftFractionRel (z₁.comp₀ z₂ z₃) (z₁.comp₀ z₂ z₃')

Tactic:
obtain ⟨z₄, fac⟩ := exists_leftFraction (RightFraction.mk z₃.s z₃.hs z₃'.s)
  dsimp at fac
  have eq : z₁.s ≫ z₃.f ≫ z₄.f = z₁.s ≫ z₃'.f ≫ z₄.s := by
    rw [← reassoc_of% h₃, ← reassoc_of% h₃', fac]
  obtain ⟨Y, t, ht, fac'⟩ := HasLeftCalculusOfFractions.ext _ _ _ z₁.hs eq
  simp only [assoc] at fac'
  refine ⟨Y, z₄.f ≫ t, z₄.s ≫ t, ?_, ?_, ?_⟩
  · simp only [comp₀, assoc, reassoc_of% fac]
  · simp only [comp₀, assoc, fac']
  · simp only [comp₀, assoc, ← reassoc_of% fac]
    exact W.comp_mem _ _ z₂.hs (W.comp_mem _ _ z₃'.hs (W.comp_mem _ _ z₄.hs ht))

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
X Y : C
f : Hom W X Y
⊢ ∃ z, f = mk z

Tactic:
obtain ⟨z⟩ := f

Goal state after:
case mk
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
f : Hom W X Y
z : W.LeftFraction X Y
⊢ ∃ z_1, Quot.mk LeftFractionRel z = mk z_1
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) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
⊢ (P.strictLimitsClosureIter J κ.ord).strictLimitsClosureStep J = P.strictLimitsClosureIter J κ.ord

Tactic:
refine le_antisymm (fun X hX ↦ ?_) (le_strictLimitsClosureStep _ _)

Goal state after:
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) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
X : C
hX : (P.strictLimitsClosureIter J κ.ord).strictLimitsClosureStep J X
⊢ P.strictLimitsClosureIter J κ.ord X
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure

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

Tactic:
apply colimitsClosure_le
    rw [← op_monotone_iff, op_unop]
    apply le_limitsClosure

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : Hom W X Y
⊢ (Hom.mk (ofHom W (𝟙 X))).comp f = f

Tactic:
obtain ⟨z, rfl⟩ := Hom.mk_surjective f

Goal state after:
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
z : W.LeftFraction X Y
⊢ (Hom.mk (ofHom W (𝟙 X))).comp (Hom.mk z) = Hom.mk z
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : Hom W X Y
⊢ f.comp (Hom.mk (ofHom W (𝟙 Y))) = f

Tactic:
obtain ⟨z, rfl⟩ := Hom.mk_surjective f

Goal state after:
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
z : W.LeftFraction X Y
⊢ (Hom.mk z).comp (Hom.mk (ofHom W (𝟙 Y))) = Hom.mk z
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 ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
⊢ ∀ (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

Tactic:
intro T₁ T₂ hT₁ hT₂ a b fac

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 ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
⊢ ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case e_a
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
this : IsIso ((Q W).map f.s)
⊢ eqToHom ⋯ ≫ F₁.map (𝟙 Y) = eqToHom ⋯

Tactic:
F₁.map_id,

Goal state after:
case e_a
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
this : IsIso ((Q W).map f.s)
⊢ eqToHom ⋯ ≫ 𝟙 (F₁.obj Y) = eqToHom ⋯
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✝
W : MorphismProperty Cᵒᵖ
h : W.HasRightCalculusOfFractions
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : W.unop s
eq : s ≫ f₁ = s ≫ f₂
Y' : Cᵒᵖ
t : Y' ⟶ Opposite.op Y
ht : W t
fac : t ≫ f₁.op = t ≫ f₂.op
⊢ ∃ Y' t, ∃ (_ : W.unop t), f₁ ≫ t = f₂ ≫ t

Tactic:
exact ⟨Opposite.unop Y', t.unop, ht, Quiver.Hom.op_inj fac⟩

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:
hm₀,

Goal state after:
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 + 0 = a
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:
hm₀,

Goal state after:
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 + 0 = a
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
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
g : Y ⟶ Z
⊢ m₀ + a = a

Tactic:
hm₀,

Goal state after:
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
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
g : Y ⟶ Z
⊢ 0 + a = a
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
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
⊢ m₀ + a = a

Tactic:
hm₀,

Goal state after:
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
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
⊢ 0 + a = a
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : 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' : C
r : Y ⟶ Y'
t : Y' ⟶ (shiftFunctor C 1).obj (Triangle.mk s g h).obj₃
mem' : Triangle.mk q r t ∈ distinguishedTriangles
⊢ f₁ ≫ r = f₂ ≫ r

Tactic:
have eq := comp_distTriang_mor_zero₁₂ _ mem'

Goal state after:
case refine_2
C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : 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' : C
r : Y ⟶ Y'
t : Y' ⟶ (shiftFunctor C 1).obj (Triangle.mk s g h).obj₃
mem' : Triangle.mk q r t ∈ distinguishedTriangles
eq : (Triangle.mk q r t).mor₁ ≫ (Triangle.mk q r t).mor₂ = 0
⊢ f₁ ≫ r = f₂ ≫ r
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 Y : C
φ : P.trW.LeftFraction X Y
Z : C
f : φ.Y' ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj Y
H : Triangle.mk φ.s f g ∈ distinguishedTriangles
mem : P Z
⊢ ∃ ψ, ψ.s ≫ φ.f = ψ.f ≫ φ.s

Tactic:
obtain ⟨X', f', h', mem'⟩ := distinguished_cocone_triangle₁ (φ.f ≫ f)

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 Y : C
φ : P.trW.LeftFraction X Y
Z : C
f : φ.Y' ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj Y
H : Triangle.mk φ.s f g ∈ distinguishedTriangles
mem : P Z
X' : C
f' : X' ⟶ X
h' : Z ⟶ (shiftFunctor C 1).obj X'
mem' : Triangle.mk f' (φ.f ≫ f) h' ∈ distinguishedTriangles
⊢ ∃ ψ, ψ.s ≫ φ.f = ψ.f ≫ φ.s
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : ObjectProperty C
inst✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
Y Z✝ Z' : C
f₁ f₂ : Y ⟶ Z✝
s : Z✝ ⟶ Z'
hf₁ : f₁ ≫ s = f₂ ≫ s
Z : C
g : Z ⟶ Z✝
h : Z' ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g s h ∈ distinguishedTriangles
mem : P Z
hf₂ : (f₁ - f₂) ≫ s = 0
q : Y ⟶ (Triangle.mk g s h).obj₁
hq : f₁ - f₂ = q ≫ (Triangle.mk g s h).mor₁
Y' : C
r : Y' ⟶ Y
t : (Triangle.mk g s h).obj₁ ⟶ (shiftFunctor C 1).obj Y'
mem' : Triangle.mk r q t ∈ distinguishedTriangles
⊢ r ≫ f₁ = r ≫ f₂

Tactic:
have eq := comp_distTriang_mor_zero₁₂ _ mem'

Goal state after:
case refine_2
C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : ObjectProperty C
inst✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
Y Z✝ Z' : C
f₁ f₂ : Y ⟶ Z✝
s : Z✝ ⟶ Z'
hf₁ : f₁ ≫ s = f₂ ≫ s
Z : C
g : Z ⟶ Z✝
h : Z' ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g s h ∈ distinguishedTriangles
mem : P Z
hf₂ : (f₁ - f₂) ≫ s = 0
q : Y ⟶ (Triangle.mk g s h).obj₁
hq : f₁ - f₂ = q ≫ (Triangle.mk g s h).mor₁
Y' : C
r : Y' ⟶ Y
t : (Triangle.mk g s h).obj₁ ⟶ (shiftFunctor C 1).obj Y'
mem' : Triangle.mk r q t ∈ distinguishedTriangles
eq : (Triangle.mk r q t).mor₁ ≫ (Triangle.mk r q t).mor₂ = 0
⊢ r ≫ f₁ = r ≫ f₂
Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : HomotopyCategory C (ComplexShape.up ℤ)
f : X ⟶ Y
⊢ IsIso (Qh.map f) ↔ HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f

Tactic:
constructor
  · intro hf
    rw [HomotopyCategory.mem_quasiIso_iff]
    intro n
    rw [← NatIso.isIso_map_iff (homologyFunctorFactorsh C n) f]
    dsimp
    infer_instance
  · exact Localization.inverts Qh (HomotopyCategory.quasiIso _ _) _

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : Category.{v_2, u_4} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
K : HomologicalComplex C c'
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
e : c.Embedding c'
inst✝ : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ F.map (𝟙 (K.X i')) = 0

Tactic:
(K.isZero_X_of_isStrictlySupported e i' hi').eq_of_src (𝟙 _) 0,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : Category.{v_2, u_4} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
K : HomologicalComplex C c'
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
e : c.Embedding c'
inst✝ : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ F.map 0 = 0
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: case pos
ι : 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
hij : c.Rel i (c.next i)
⊢ (K.fromOpcycles i (c.next i)).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles (c.next i) i

Tactic:
exact (K.sc i).fromOpcycles_op_cyclesOpIso_inv

Goal state after:
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 : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
hj' : e.r j' = none
⊢ (K.extend e).d i' j' = 0

Tactic:
exact extend.d_none_eq_zero' _ _ _ hj'

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

Goal state before:
pp: case pos
ι : 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' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ∃ j, e.f j = j'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

Tactic:
obtain ⟨j, hj⟩ := hj

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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
j : ι
hj : e.f j = j'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case pos
ι : 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
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
hj : ∃ j, e.f j = j'
⊢ (mkHomToSingle ((((single C c i).obj X).extendXIso e h).hom ≫ (singleObjXSelf c i X).hom) ⋯ ≫
          mkHomFromSingle ((singleObjXSelf c i X).inv ≫ (((single C c i).obj X).extendXIso e h).inv) ⋯).f
      j' =
    (𝟙 (((single C c i).obj X).extend e)).f j'

Tactic:
obtain ⟨j, hj⟩ := hj

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✝³ : HasZeroObject C
inst✝² : HasZeroMorphisms C
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
j : ι
hj : e.f j = j'
⊢ (mkHomToSingle ((((single C c i).obj X).extendXIso e h).hom ≫ (singleObjXSelf c i X).hom) ⋯ ≫
          mkHomFromSingle ((singleObjXSelf c i X).inv ≫ (((single C c i).obj X).extendXIso e h).inv) ⋯).f
      j' =
    (𝟙 (((single C c i).obj X).extend e)).f j'
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

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.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
⊢ d K e i j ≫ d K e j k = 0

Tactic:
dsimp [d]
  by_cases hij : c.Rel i j
  · by_cases hjk : c.Rel j k
    · rw [dif_pos hij, dif_pos hjk, dif_neg (e.not_boundaryGE_next hij)]
      split_ifs <;> simp
    · rw [dif_neg hjk, comp_zero]
  · rw [dif_neg hij, zero_comp]

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 : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyLE p
⊢ K.IsStrictlyLE q

Tactic:
rw [isStrictlyLE_iff]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyLE p
⊢ ∀ (i : ℤ), q < i → IsZero (K.X i)
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 ℤ
φ : K ⟶ L
e : K ≅ L
inst✝ : HasZeroObject C
A : C
n : ℤ
⊢ IsStrictlyLE ((single C (up ℤ) n).obj A) n

Tactic:
rw [isStrictlyLE_iff]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝ : HasZeroObject C
A : C
n : ℤ
⊢ ∀ (i : ℤ), n < i → IsZero (((single C (up ℤ) n).obj A).X i)