awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.IsHomological
inst_9 : F.ShiftSequence ℤ
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ Epi ((F.shift n₀).map T.mor₂) ↔
    Eq (α := (F.shift n₀).obj T.obj₃ ⟶ (F.shift n₁).obj T.obj₁) (F.homologySequenceδ T n₀ n₁ h) 0

Tactic:
(F.homologySequence_exact₃ T hT n₀ n₁ h).epi_f_iff

Premises used: CategoryTheory.Functor.homologySequence_exact₃, CategoryTheory.Functor.shiftMap, CategoryTheory.Functor.homologySequenceδ, CategoryTheory.ShortComplex.Exact.epi_f_iff
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.IsHomological
inst_9 : F.ShiftSequence ℤ
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _) T
n₀ : ℤ
⊢ Mono ((F.shift n₀).map T.mor₂) ↔ (F.shift n₀).map T.mor₁ = 0

Tactic:
(F.homologySequence_exact₂ T hT n₀).mono_g_iff

Premises used: CategoryTheory.Functor.homologySequence_exact₂, CategoryTheory.ShortComplex.Exact.mono_g_iff
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.IsHomological
inst_9 : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
obtain :
  ∀ (Z : C) (g : Y ⟶ Z) (h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X)
    (hT :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _)
        (Triangle.mk f g h)),
    F.homologicalKernel.trW f ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
⊢ F.homologicalKernel.trW f ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)

Tactic:
obtain ⟨Z, g, h, hT⟩ := distinguished_cocone_triangle f

Premises used: CategoryTheory.Pretriangulated.distinguished_cocone_triangle
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.IsHomological
inst_9 : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _)
    (Triangle.mk f g h)
apply : F.homologicalKernel (Triangle.mk f g h).obj₃ ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
⊢ F.homologicalKernel.trW f ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)

Tactic:
apply (F.homologicalKernel.trW_iff_of_distinguished _ hT).trans

Premises used: CategoryTheory.Functor.homologicalKernel, CategoryTheory.ObjectProperty.trW_iff_of_distinguished, Iff.trans
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.IsHomological
inst_9 : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _)
    (Triangle.mk f g h)
h₁ :
  ∀ (n : ℤ),
    IsZero.{v_3, u_3} ((F.shift n).obj Z) ↔
      (F.shift n).map g = 0 ∧
        Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) 0
h₂ :
  ∀ (n : ℤ),
    Mono ((F.shift (n + 1)).map f) ↔
      Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
simp : (∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)) ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
⊢ F.homologicalKernel Z ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)

Tactic:
simp only [mem_homologicalKernel_iff, h₁, ← h₂, ← h₃]

Premises used: CategoryTheory.Functor.mem_homologicalKernel_iff
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.IsHomological
inst_9 : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _)
    (Triangle.mk f g h)
h₁ :
  ∀ (n : ℤ),
    IsZero.{v_3, u_3} ((F.shift n).obj Z) ↔
      (F.shift n).map g = 0 ∧
        Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) 0
h₂ :
  ∀ (n : ℤ),
    Mono ((F.shift (n + 1)).map f) ↔
      Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
mp : (∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)) → ∀ (n : ℤ), IsIso ((F.shift n).map f)
mpr : (∀ (n : ℤ), IsIso ((F.shift n).map f)) → ∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)
⊢ (∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)) ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.IsHomological
inst_9 : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h_1 : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _)
    (Triangle.mk f g h_1)
h₁ :
  ∀ (n : ℤ),
    IsZero.{v_3, u_3} ((F.shift n).obj Z) ↔
      (F.shift n).map g = 0 ∧
        Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h_1) n (n + 1) ⋯) 0
h₂ :
  ∀ (n : ℤ),
    Mono ((F.shift (n + 1)).map f) ↔
      Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h_1) n (n + 1) ⋯) 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
h : ∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)
n : ℤ
⊢ n = n - 1 + 1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.IsHomological
inst_9 : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h_1 : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _)
    (Triangle.mk f g h_1)
h₁ :
  ∀ (n : ℤ),
    IsZero.{v_3, u_3} ((F.shift n).obj Z) ↔
      (F.shift n).map g = 0 ∧
        Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h_1) n (n + 1) ⋯) 0
h₂ :
  ∀ (n : ℤ),
    Mono ((F.shift (n + 1)).map f) ↔
      Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h_1) n (n + 1) ⋯) 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
h : ∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)
n : ℤ
mp : ∀ (m : ℤ), IsIso ((F.shift (m + 1)).map f)
⊢ IsIso ((F.shift n).map f)

Tactic:
obtain ⟨m, rfl⟩ : ∃ (m : ℤ), n = m + 1 := ⟨n - 1, by simp⟩

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.IsHomological
inst_9 : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h_1 : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _)
    (Triangle.mk f g h_1)
h₁ :
  ∀ (n : ℤ),
    IsZero.{v_3, u_3} ((F.shift n).obj Z) ↔
      (F.shift n).map g = 0 ∧
        Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h_1) n (n + 1) ⋯) 0
h₂ :
  ∀ (n : ℤ),
    Mono ((F.shift (n + 1)).map f) ↔
      Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h_1) n (n + 1) ⋯) 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
h : ∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)
m : ℤ
⊢ Epi ((F.shift (m + 1)).map f)

Tactic:
have := (h (m + 1)).1
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.IsHomological
inst_9 : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h_1 : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _)
    (Triangle.mk f g h_1)
h₁ :
  ∀ (n : ℤ),
    IsZero.{v_3, u_3} ((F.shift n).obj Z) ↔
      (F.shift n).map g = 0 ∧
        Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h_1) n (n + 1) ⋯) 0
h₂ :
  ∀ (n : ℤ),
    Mono ((F.shift (n + 1)).map f) ↔
      Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h_1) n (n + 1) ⋯) 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
h : ∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)
m : ℤ
this : Epi ((F.shift (m + 1)).map f)
⊢ Mono ((F.shift (m + 1)).map f)

Tactic:
have := (h m).2
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.IsHomological
inst_9 : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h_1 : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _)
    (Triangle.mk f g h_1)
h₁ :
  ∀ (n : ℤ),
    IsZero.{v_3, u_3} ((F.shift n).obj Z) ↔
      (F.shift n).map g = 0 ∧
        Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h_1) n (n + 1) ⋯) 0
h₂ :
  ∀ (n : ℤ),
    Mono ((F.shift (n + 1)).map f) ↔
      Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h_1) n (n + 1) ⋯) 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
h : ∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)
m : ℤ
this_1 : Epi ((F.shift (m + 1)).map f)
this : Mono ((F.shift (m + 1)).map f)
⊢ IsIso ((F.shift (m + 1)).map f)

Tactic:
apply isIso_of_mono_of_epi

Premises used: CategoryTheory.isIso_of_mono_of_epi
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.IsHomological
inst_9 : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _)
    (Triangle.mk f g h)
h₁ :
  ∀ (n : ℤ),
    IsZero.{v_3, u_3} ((F.shift n).obj Z) ↔
      (F.shift n).map g = 0 ∧
        Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) 0
h₂ :
  ∀ (n : ℤ),
    Mono ((F.shift (n + 1)).map f) ↔
      Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
h_1 : ∀ (n : ℤ), IsIso ((F.shift n).map f)
n : ℤ
mpr : Epi ((F.shift n).map f)
mpr₁ : Mono ((F.shift (n + 1)).map f)
⊢ Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.IsHomological
inst_9 : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _)
    (Triangle.mk f g h)
h₁ :
  ∀ (n : ℤ),
    IsZero.{v_3, u_3} ((F.shift n).obj Z) ↔
      (F.shift n).map g = 0 ∧
        Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) 0
h₂ :
  ∀ (n : ℤ),
    Mono ((F.shift (n + 1)).map f) ↔
      Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
h_1 : ∀ (n : ℤ), IsIso ((F.shift n).map f)
n : ℤ
⊢ Epi ((F.shift n).map f)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.IsHomological
inst_9 : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _)
    (Triangle.mk f g h)
h₁ :
  ∀ (n : ℤ),
    IsZero.{v_3, u_3} ((F.shift n).obj Z) ↔
      (F.shift n).map g = 0 ∧
        Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) 0
h₂ :
  ∀ (n : ℤ),
    Mono ((F.shift (n + 1)).map f) ↔
      Eq (α := (F.shift n).obj Z ⟶ (F.shift (n + 1)).obj X) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
h_1 : ∀ (n : ℤ), IsIso ((F.shift n).map f)
n : ℤ
⊢ Mono ((F.shift (n + 1)).map f)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.IsHomological
inst_9 : F.ShiftSequence ℤ
T : Triangle.{v_1, u_1} C
hT : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _) T
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (F.homologySequenceComposableArrows₅ T n₀ n₁ h).Exact

Tactic:
exact_of_δ₀ (F.homologySequence_exact₂ T hT n₀).exact_toComposableArrows
    (exact_of_δ₀ (F.homologySequence_exact₃ T hT n₀ n₁ h).exact_toComposableArrows
      (exact_of_δ₀ (F.homologySequence_exact₁ T hT n₀ n₁ h).exact_toComposableArrows
        (F.homologySequence_exact₂ T hT n₁).exact_toComposableArrows))

Premises used: CategoryTheory.Functor.homologySequence_exact₂, CategoryTheory.Functor.homologySequence_exact₃, CategoryTheory.Functor.homologySequence_exact₁, CategoryTheory.ShortComplex.Exact.exact_toComposableArrows, CategoryTheory.ComposableArrows.exact_of_δ₀
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} C
inst_4 : A.IsVerdierLeftLocalizing B
X Y : Cᵒᵖ
f : X ⟶ Y
hX : B.op X
hY : A.op Y
obtain :
  ∀ (Z : C) (a : unop Y ⟶ Z) (b : Z ⟶ unop X) (h₁ : A Z) (h₂ : B Z) (fac : a ≫ b = f.unop),
    ∃ (Z : Cᵒᵖ) (a : X ⟶ Z) (b : Z ⟶ Y), A.op Z ∧ B.op Z ∧ a ≫ b = f
⊢ ∃ (Z : Cᵒᵖ) (a : X ⟶ Z) (b : Z ⟶ Y), A.op Z ∧ B.op Z ∧ a ≫ b = f

Tactic:
obtain ⟨Z, a, b, h₁, h₂, fac⟩ :=
      IsVerdierLeftLocalizing.fac f.unop hY hX

Premises used: CategoryTheory.ObjectProperty.IsVerdierLeftLocalizing.fac, Quiver.Hom.unop
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} C
inst_4 : A.IsVerdierLeftLocalizing B
X Y : Cᵒᵖ
f : X ⟶ Y
hX : B.op X
hY : A.op Y
Z : C
a : unop Y ⟶ Z
b : Z ⟶ unop X
h₁ : A Z
h₂ : B Z
fac : a ≫ b = f.unop
⊢ ∃ (Z : Cᵒᵖ) (a : X ⟶ Z) (b : Z ⟶ Y), A.op Z ∧ B.op Z ∧ a ≫ b = f

Tactic:
⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩

Premises used: Quiver.Hom.op, Quiver.Hom.unop_inj, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} C
inst_4 : A.IsVerdierLeftLocalizing B
X Y : Cᵒᵖ
f : X ⟶ Y
hX : B.op X
hY : A.op Y
Z : C
a : unop Y ⟶ Z
b : Z ⟶ unop X
h₁ : A Z
h₂ : B Z
fac : a ≫ b = f.unop
⊢ ∃ (Z : Cᵒᵖ) (a : X ⟶ Z) (b : Z ⟶ Y), A.op Z ∧ B.op Z ∧ a ≫ b = f

Tactic:
exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} Cᵒᵖ
inst_4 : IsVerdierLeftLocalizing.{v_1, u_1} A B
X Y : C
f : X ⟶ Y
hX : B.unop X
hY : A.unop Y
obtain :
  ∀ (Z : Cᵒᵖ) (a : op Y ⟶ Z) (b : Z ⟶ op X) (h₁ : A Z) (h₂ : B Z) (fac : a ≫ b = f.op),
    ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A.unop Z ∧ B.unop Z ∧ a ≫ b = f
⊢ ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A.unop Z ∧ B.unop Z ∧ a ≫ b = f

Tactic:
obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierLeftLocalizing.fac f.op hY hX

Premises used: Quiver.Hom.op, CategoryTheory.ObjectProperty.IsVerdierLeftLocalizing.fac
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} Cᵒᵖ
inst_4 : IsVerdierLeftLocalizing.{v_1, u_1} A B
X Y : C
f : X ⟶ Y
hX : B.unop X
hY : A.unop Y
Z : Cᵒᵖ
a : op Y ⟶ Z
b : Z ⟶ op X
h₁ : A Z
h₂ : B Z
fac : a ≫ b = f.op
⊢ ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A.unop Z ∧ B.unop Z ∧ a ≫ b = f

Tactic:
⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} Cᵒᵖ
inst_4 : IsVerdierLeftLocalizing.{v_1, u_1} A B
X Y : C
f : X ⟶ Y
hX : B.unop X
hY : A.unop Y
Z : Cᵒᵖ
a : op Y ⟶ Z
b : Z ⟶ op X
h₁ : A Z
h₂ : B Z
fac : a ≫ b = f.op
⊢ ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A.unop Z ∧ B.unop Z ∧ a ≫ b = f

Tactic:
exact ⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩
-- Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
Goal:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
A B : ObjectProperty.{v_1, u_1} C
inst_4 : A.IsVerdierRightLocalizing B
X Y : Cᵒᵖ
f : X ⟶ Y
hX : A.op X
hY : B.op Y
obtain :
  ∀ (Z : C) (a : unop Y ⟶ Z) (b : Z ⟶ unop X) (h₁ : A Z) (h₂ : B Z) (fac : a ≫ b = f.unop),
    ∃ (Z : Cᵒᵖ) (a : X ⟶ Z) (b : Z ⟶ Y), A.op Z ∧ B.op Z ∧ a ≫ b = f
⊢ ∃ (Z : Cᵒᵖ) (a : X ⟶ Z) (b : Z ⟶ Y), A.op Z ∧ B.op Z ∧ a ≫ b = f

Tactic:
obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac f.unop hY hX

Premises used: Quiver.Hom.unop, CategoryTheory.ObjectProperty.IsVerdierRightLocalizing.fac