awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
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₁
⊢ Iso (C := ShortComplex.{v_3, u_3} A)
    { X₁ := (F.shift n₁).obj T.invRotate.obj₁, X₂ := (F.shift n₁).obj T.invRotate.obj₂,
      X₃ := (F.shift n₁).obj T.invRotate.obj₃, f := (F.shift n₁).map T.invRotate.mor₁,
      g := (F.shift n₁).map T.invRotate.mor₂, zero := ⋯ }
    { X₁ := (F.shift n₀).obj T.obj₃, X₂ := (F.shift n₁).obj T.obj₁, X₃ := (F.shift n₁).obj T.obj₂,
      f := F.homologySequenceδ T n₀ n₁ h, g := (F.shift n₁).map T.mor₁, zero := ⋯ }
have refine : Iso.hom (-Iso.app (F.shiftIso (-1) n₁ n₀ sorry) T.obj₃) ≫
    ShortComplex.f
      { X₁ := (F.shift n₀).obj T.obj₃, X₂ := (F.shift n₁).obj T.obj₁, X₃ := (F.shift n₁).obj T.obj₂,
        f := F.homologySequenceδ T n₀ n₁ h, g := (F.shift n₁).map T.mor₁, zero := sorry } =
  ShortComplex.f
      { X₁ := (F.shift n₁).obj T.invRotate.obj₁, X₂ := (F.shift n₁).obj T.invRotate.obj₂,
        X₃ := (F.shift n₁).obj T.invRotate.obj₃, f := (F.shift n₁).map T.invRotate.mor₁,
        g := (F.shift n₁).map T.invRotate.mor₂, zero := sorry : ShortComplex.{v_3, u_3} A } ≫
    Iso.hom
      (Iso.refl
        (ShortComplex.X₂
          { X₁ := (F.shift n₁).obj T.invRotate.obj₁, X₂ := (F.shift n₁).obj T.invRotate.obj₂,
            X₃ := (F.shift n₁).obj T.invRotate.obj₃, f := (F.shift n₁).map T.invRotate.mor₁,
            g := (F.shift n₁).map T.invRotate.mor₂, zero := sorry : ShortComplex.{v_3, u_3} A }))
Tactic: refine ShortComplex.isoMk (-((F.shiftIso (-1) n₁ n₀ (by lia)).app _))
    (Iso.refl _) (Iso.refl _) ?_ (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
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₁
⊢ Iso.hom (-Iso.app (F.shiftIso (-1) n₁ n₀ ⋯) T.obj₃) ≫
      ShortComplex.f
        { X₁ := (F.shift n₀).obj T.obj₃, X₂ := (F.shift n₁).obj T.obj₁, X₃ := (F.shift n₁).obj T.obj₂,
          f := F.homologySequenceδ T n₀ n₁ h, g := (F.shift n₁).map T.mor₁, zero := ⋯ } =
    ShortComplex.f
        { X₁ := (F.shift n₁).obj T.invRotate.obj₁, X₂ := (F.shift n₁).obj T.invRotate.obj₂,
          X₃ := (F.shift n₁).obj T.invRotate.obj₃, f := (F.shift n₁).map T.invRotate.mor₁,
          g := (F.shift n₁).map T.invRotate.mor₂, zero := ⋯ : ShortComplex.{v_3, u_3} A } ≫
      Iso.hom
        (Iso.refl
          (ShortComplex.X₂
            { X₁ := (F.shift n₁).obj T.invRotate.obj₁, X₂ := (F.shift n₁).obj T.invRotate.obj₂,
              X₃ := (F.shift n₁).obj T.invRotate.obj₃, f := (F.shift n₁).map T.invRotate.mor₁,
              g := (F.shift n₁).map T.invRotate.mor₂, zero := ⋯ : ShortComplex.{v_3, u_3} A }))
have dsimp : Eq (α := (F.shift n₁).obj (obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) (-1)) T.obj₃) ⟶ (F.shift n₁).obj T.obj₁)
  ((-NatTrans.app (Iso.hom (F.shiftIso (-1) n₁ n₀ sorry)) T.obj₃) ≫ F.homologySequenceδ T n₀ n₁ h)
  ((F.shift n₁).map
      (-map (shiftFunctor C (A := ℤ) (-1)) T.mor₃ ≫ NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) sorry)) T.obj₁) ≫
    𝟙 ((F.shift n₁).obj T.obj₁))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
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
⊢ F.homologicalKernel.trW f ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
have 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)
Tactic: obtain ⟨Z, g, h, hT⟩ := distinguished_cocone_triangle f
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
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)
⊢ F.homologicalKernel.trW f ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
have apply : F.homologicalKernel (Triangle.mk f g h).obj₃ ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
Tactic: apply (F.homologicalKernel.trW_iff_of_distinguished _ hT).trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
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
⊢ F.homologicalKernel Z ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
have simp : (∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)) ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
Tactic: simp only [mem_homologicalKernel_iff, h₁, ← h₂, ← h₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
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
⊢ (∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)) ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
have mp : (∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)) → ∀ (n : ℤ), IsIso ((F.shift n).map f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
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)
⊢ (∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)) ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
have mpr : (∀ (n : ℤ), IsIso ((F.shift n).map f)) → ∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
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 : ℤ
⊢ IsIso ((F.shift n).map f)
have mp : ∀ (m : ℤ), IsIso ((F.shift (m + 1)).map f)
Tactic: obtain ⟨m, rfl⟩ : ∃ (m : ℤ), n = m + 1 := ⟨n - 1, by simp⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (hypothesis)
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 : ℤ
⊢ IsIso ((F.shift (m + 1)).map f)
have this : Epi ((F.shift (m + 1)).map f)
Tactic: have := (h (m + 1)).1
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (hypothesis)
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)
⊢ IsIso ((F.shift (m + 1)).map f)
have this₁ : Mono ((F.shift (m + 1)).map f)
Tactic: have := (h m).2
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
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) ∧ Mono ((F.shift (n + 1)).map f)
have mpr : Epi ((F.shift n).map f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (goal)
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)
⊢ Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)
have mpr₁ : Mono ((F.shift (n + 1)).map f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
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 : X ⟶ Z) (b : Z ⟶ Y), A.op Z ∧ B.op Z ∧ a ≫ b = f
have 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
Tactic: obtain ⟨Z, a, b, h₁, h₂, fac⟩ :=
      IsVerdierLeftLocalizing.fac f.unop hY hX
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
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 : X ⟶ Z) (b : Z ⟶ Y), A.unop Z ∧ B.unop Z ∧ a ≫ b = f
have 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
Tactic: obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierLeftLocalizing.fac f.op hY hX
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
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
⊢ ∃ (Z : Cᵒᵖ) (a : X ⟶ Z) (b : Z ⟶ Y), A.op Z ∧ B.op Z ∧ a ≫ b = f
have 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
Tactic: obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac f.unop hY hX
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
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 : IsVerdierRightLocalizing.{v_1, u_1} A B
X Y : C
f : X ⟶ Y
hX : A.unop X
hY : B.unop Y
⊢ ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A.unop Z ∧ B.unop Z ∧ a ≫ b = f
have 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
Tactic: obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac f.op hY hX
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
⊢ A.IsVerdierRightLocalizing B ↔
    ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
have refine_1 : A.IsVerdierRightLocalizing B →
  ∀ (X Y : C) (s : X ⟶ Y) (hX : A X) (hs : B.trW s),
    ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
Tactic: refine ⟨fun _ X Y s hX hs ↦ ?_, fun hA ↦ ⟨fun {X Y} f hX hY ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
refine_1 :
  A.IsVerdierRightLocalizing B →
    ∀ (X Y : C) (s : X ⟶ Y) (hX : A X) (hs : B.trW s),
      ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
⊢ A.IsVerdierRightLocalizing B ↔
    ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
have refine_2 : ∀ (hA : ∀ ⦃X Y : C⦄ (s : X ⟶ Y), A X → B.trW s → ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s')
  {X Y : C} (f : X ⟶ Y) (hX : B X) (hY : A Y), ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), A Z ∧ B Z ∧ a ≫ b = f
Tactic: refine ⟨fun _ X Y s hX hs ↦ ?_, fun hA ↦ ⟨fun {X Y} f hX hY ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
A B : ObjectProperty.{v_1, u_1} C
inst_1 : HasZeroObject.{v_1, u_1} C
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_5 : Pretriangulated.{v_1, u_1} C
inst_6 : A.IsTriangulated
inst_7 : B.IsTriangulated
inst_8 : B.IsClosedUnderIsomorphisms
h : A.IsVerdierRightLocalizing B
X Y : C
s : X ⟶ Y
hX : A X
hs : B.trW s
⊢ ∃ (Z : C) (s' : X ⟶ Z) (b : Y ⟶ Z), A Z ∧ (A ⊓ B).trW s' ∧ s ≫ b = s'
have hs₁ : ∃ (X_1 : C) (f : X_1 ⟶ X) (h : Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X_1) (_ :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C))
    (@Pretriangulated.distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) (Triangle.mk f s h)),
  B X_1
Tactic: rw [ObjectProperty.trW_iff'] at hs
Cleared hypotheses: hs