awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
M : Type u_1
inst_2 : AddGroup M
inst_3 : HasShift.{v, u, u_1} C M
inst_4 : HasZeroMorphisms.{v, u} C
inst_5 : P.IsStableUnderShift M
n : M
X : C
hX : P.leftOrthogonal X
Y : C
f : Functor.obj.{v, v, u, u} (shiftFunctor C n) X ⟶ Y
hY : P Y
⊢ f = 0
have obtain : ∀ (g : X ⟶ Functor.obj.{v, v, u, u} (Equivalence.inverse (shiftEquiv C n)) Y),
  Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C n) X ⟶ Y)
    ((Equiv.symm (Adjunction.homEquiv (Equivalence.toAdjunction (shiftEquiv C n)) X Y) :
          (a : X ⟶ (shiftEquiv C n).inverse.obj Y) → (shiftEquiv C n).functor.obj X ⟶ Y)
        g :
      Functor.obj.{v, v, u, u} (Equivalence.functor (shiftEquiv C n)) X ⟶ Y)
    (0 : Functor.obj.{v, v, u, u} (shiftFunctor C n) X ⟶ Y)
Tactic: obtain ⟨g, rfl⟩ := ((shiftEquiv C n).toAdjunction.homEquiv _ _).symm.surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_5 _) T
h₁ : P.rightOrthogonal T.obj₁
h₃ : P.rightOrthogonal T.obj₃
X : C
f : X ⟶ T.obj₂
hX : P X
⊢ f = 0
have obtain : ∀ (g : X ⟶ T.obj₁), g ≫ T.mor₁ = 0
Tactic: obtain ⟨g, rfl⟩ := Pretriangulated.Triangle.coyoneda_exact₂ T hT f (h₃ _ hX)
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
T : Triangle.{v, u} C
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_5 _) T
h₁ : P.leftOrthogonal T.obj₁
h₃ : P.leftOrthogonal T.obj₃
Y : C
f : T.obj₂ ⟶ Y
hY : P Y
⊢ f = 0
have obtain : ∀ (g : T.obj₃ ⟶ Y), T.mor₂ ≫ g = 0
Tactic: obtain ⟨g, rfl⟩ := Pretriangulated.Triangle.yoneda_exact₂ T hT f (h₁ _ hY)
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
⊢ P.trW.isLocal = P.rightOrthogonal
have h : ∀ (Y : C), P.trW.isLocal Y ↔ P.rightOrthogonal Y
Tactic: ext Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
⊢ P.trW.isLocal Y ↔ P.rightOrthogonal Y
have h : ∀ (hY : P.trW.isLocal Y) (X : C) (f : X ⟶ Y) (hX : P X), f = 0
Tactic: refine ⟨fun hY X f hX ↦ ?_, fun hY X₁ X₂ f ⟨X₃, g, h, hT, hX₃⟩ ↦ ⟨?_, fun α ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
h : ∀ (hY : P.trW.isLocal Y) (X : C) (f : X ⟶ Y) (hX : P X), f = 0
⊢ P.trW.isLocal Y ↔ P.rightOrthogonal Y
have h₁ : ∀ (hY : P.rightOrthogonal Y) (X₁ X₂ : C) (f : X₁ ⟶ X₂),
  P.trW f →
    ∀ (X₃ : C) (g : X₂ ⟶ X₃) (h : X₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X₁)
      (hT :
        Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
          (Triangle.mk f g h))
      (hX₃ : P X₃), Function.Injective (β := X₁ ⟶ Y) fun (g : X₂ ⟶ Y) ↦ f ≫ g
Tactic: refine ⟨fun hY X f hX ↦ ?_, fun hY X₁ X₂ f ⟨X₃, g, h, hT, hX₃⟩ ↦ ⟨?_, fun α ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
h : ∀ (hY : P.trW.isLocal Y) (X : C) (f : X ⟶ Y) (hX : P X), f = 0
h₁ :
  ∀ (hY : P.rightOrthogonal Y) (X₁ X₂ : C) (f : X₁ ⟶ X₂),
    P.trW f →
      ∀ (X₃ : C) (g : X₂ ⟶ X₃) (h : X₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X₁)
        (hT :
          Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
            (Triangle.mk f g h))
        (hX₃ : P X₃), Function.Injective (β := X₁ ⟶ Y) fun (g : X₂ ⟶ Y) ↦ f ≫ g
⊢ P.trW.isLocal Y ↔ P.rightOrthogonal Y
have h₂ : ∀ (hY : P.rightOrthogonal Y) (X₁ X₂ : C) (f : X₁ ⟶ X₂),
  P.trW f →
    ∀ (X₃ : C) (g : X₂ ⟶ X₃) (h : X₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X₁)
      (hT :
        Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
          (Triangle.mk f g h))
      (hX₃ : P X₃) (α : X₁ ⟶ Y), ∃ (a : X₂ ⟶ Y), (fun (g : X₂ ⟶ Y) ↦ f ≫ g) a = α
Tactic: refine ⟨fun hY X f hX ↦ ?_, fun hY X₁ X₂ f ⟨X₃, g, h, hT, hX₃⟩ ↦ ⟨?_, fun α ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
h_1 : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
hX₃ : P X₃
⊢ Function.Injective (β := X₁ ⟶ Y) fun (g : X₂ ⟶ Y) ↦ f ≫ g
have h₁ : ∀ (α : X₂ ⟶ Y), f ≫ α = 0 → α = 0
Tactic: suffices ∀ (α : X₂ ⟶ Y), f ≫ α = 0 → α = 0 from fun α₁ α₂ hα ↦ by
      simpa [sub_eq_zero] using this (α₁ - α₂) (by simpa [sub_eq_zero] using hα)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
h_1 : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
hX₃ : P X₃
α : X₂ ⟶ Y
hα : f ≫ α = 0
⊢ α = 0
have h₁ : ∀ (β : (Triangle.mk f g h).obj₃ ⟶ Y) (hα : f ≫ (Triangle.mk f g h).mor₂ ≫ β = 0), (Triangle.mk f g h).mor₂ ≫ β = 0
Tactic: obtain ⟨β, rfl⟩ := Triangle.yoneda_exact₂ _ hT α hα
Cleared hypotheses: α, hα
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
h_1 : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f g h)
hX₃ : P X₃
α : X₁ ⟶ Y
⊢ ∃ (a : X₂ ⟶ Y), (fun (g : X₂ ⟶ Y) ↦ f ≫ g) a = α
have h₁ : ∀ (β : (Triangle.mk f g h).invRotate.obj₃ ⟶ Y),
  ∃ (a : X₂ ⟶ Y), (fun (g : X₂ ⟶ Y) ↦ f ≫ g) a = (Triangle.mk f g h).invRotate.mor₂ ≫ β
Tactic: obtain ⟨β, rfl⟩ := Triangle.yoneda_exact₂ _ (inv_rot_of_distTriang _ hT)
      α (hY _ (P.le_shift _ _ hX₃))
Cleared hypotheses: α
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
⊢ P.trW.isColocal = P.leftOrthogonal
have h : ∀ (X : C), P.trW.isColocal X ↔ P.leftOrthogonal X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
⊢ P.trW.isColocal X ↔ P.leftOrthogonal X
have h : ∀ (hX : P.trW.isColocal X) (Y : C) (f : X ⟶ Y) (hY : P Y), f = 0
Tactic: refine ⟨fun hX Y f hY ↦ ?_, fun hX Y₂ Y₃ h hh ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
h : ∀ (hX : P.trW.isColocal X) (Y : C) (f : X ⟶ Y) (hY : P Y), f = 0
⊢ P.trW.isColocal X ↔ P.leftOrthogonal X
have h₁ : ∀ (hX : P.leftOrthogonal X) (Y₂ Y₃ : C) (h : Y₂ ⟶ Y₃) (hh : P.trW h),
  Function.Bijective (β := X ⟶ Y₃) fun (f : X ⟶ Y₂) ↦ f ≫ h
Tactic: refine ⟨fun hX Y f hY ↦ ?_, fun hX Y₂ Y₃ h hh ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
hh : P.trW h
⊢ Function.Bijective (β := X ⟶ Y₃) fun (f : X ⟶ Y₂) ↦ f ≫ h
have hh₁ : ∃ (X : C) (f : X ⟶ Y₂) (h_1 : Y₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (_ :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f h h_1)),
  P X
Tactic: rw [trW_iff'] at hh
Cleared hypotheses: hh
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
hh :
  ∃ (X : C) (f : X ⟶ Y₂) (h_1 : Y₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) X) (_ :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f h h_1)),
    P X
⊢ Function.Bijective (β := X ⟶ Y₃) fun (f : X ⟶ Y₂) ↦ f ≫ h
have h₁ : ∀ (Y₁ : C) (f : Y₁ ⟶ Y₂) (g : Y₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y₁)
  (hT :
    Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
      (Triangle.mk f h g))
  (hY₁ : P Y₁), Function.Bijective (β := X ⟶ Y₃) fun (f : X ⟶ Y₂) ↦ f ≫ h
Tactic: obtain ⟨Y₁, f, g, hT, hY₁⟩ := hh
Cleared hypotheses: hh
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
Y₁ : C
f : Y₁ ⟶ Y₂
g : Y₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f h g)
hY₁ : P Y₁
⊢ Function.Bijective (β := X ⟶ Y₃) fun (f : X ⟶ Y₂) ↦ f ≫ h
have h₁ : Function.Injective (β := X ⟶ Y₃) fun (f : X ⟶ Y₂) ↦ f ≫ h
Tactic: refine ⟨?_, fun α ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
Y₁ : C
f : Y₁ ⟶ Y₂
g : Y₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f h g)
hY₁ : P Y₁
h₁ : Function.Injective (β := X ⟶ Y₃) fun (f : X ⟶ Y₂) ↦ f ≫ h
⊢ Function.Bijective (β := X ⟶ Y₃) fun (f : X ⟶ Y₂) ↦ f ≫ h
have h₂ : ∀ (α : X ⟶ Y₃), ∃ (a : X ⟶ Y₂), (fun (f : X ⟶ Y₂) ↦ f ≫ h) a = α
Tactic: refine ⟨?_, fun α ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
Y₁ : C
f : Y₁ ⟶ Y₂
g : Y₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f h g)
hY₁ : P Y₁
⊢ Function.Injective (β := X ⟶ Y₃) fun (f : X ⟶ Y₂) ↦ f ≫ h
have h₁ : ∀ (α : X ⟶ Y₂), α ≫ h = 0 → α = 0
Tactic: suffices ∀ (α : X ⟶ Y₂), α ≫ h = 0 → α = 0 from fun α₁ α₂ hα ↦ by
        simpa [sub_eq_zero] using this (α₁ - α₂) (by simpa [sub_eq_zero])
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
Y₁ : C
f : Y₁ ⟶ Y₂
g : Y₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f h g)
hY₁ : P Y₁
α : X ⟶ Y₂
hα : α ≫ h = 0
⊢ α = 0
have h₁ : ∀ (β : X ⟶ (Triangle.mk f h g).obj₁) (hα : (β ≫ (Triangle.mk f h g).mor₁) ≫ h = 0), β ≫ (Triangle.mk f h g).mor₁ = 0
Tactic: obtain ⟨β, rfl⟩ := Triangle.coyoneda_exact₂ _ hT α hα
Cleared hypotheses: α, hα
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_5 : Pretriangulated.{v, u} C
inst_6 : P.IsTriangulated
X : C
hX : P.leftOrthogonal X
Y₂ Y₃ : C
h : Y₂ ⟶ Y₃
Y₁ : C
f : Y₁ ⟶ Y₂
g : Y₃ ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) Y₁
hT :
  Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _)
    (Triangle.mk f h g)
hY₁ : P Y₁
α : X ⟶ Y₃
⊢ ∃ (a : X ⟶ Y₂), (fun (f : X ⟶ Y₂) ↦ f ≫ h) a = α
have h₁ : ∀ (β : X ⟶ (Triangle.mk f h g).rotate.obj₁),
  ∃ (a : X ⟶ Y₂), (fun (f : X ⟶ Y₂) ↦ f ≫ h) a = β ≫ (Triangle.mk f h g).rotate.mor₁
Tactic: obtain ⟨β, rfl⟩ := Triangle.coyoneda_exact₂ _ (rot_of_distTriang _ hT)
        α (hX _ (P.le_shift _ _ hY₁))
Cleared hypotheses: α
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
inst_7 : P.IsTriangulated
inst_8 : IsTriangulated.{v, u} C
Y : C
hY : P.rightOrthogonal Y
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
X : C
⊢ Function.Bijective (α := X ⟶ Y) L.map
have rw : ∀ (hY : P.trW.isLocal Y) (L : Functor.{v, v', u, u'} C D) [L.IsLocalization P.trW] (X : C),
  Function.Bijective (α := X ⟶ Y) L.map
Tactic: rw [← isLocal_trW] at hY
Cleared hypotheses: hY, L, inst_9, X
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
inst_7 : P.IsTriangulated
inst_8 : IsTriangulated.{v, u} C
Y : C
hY : P.trW.isLocal Y
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
X : C
⊢ Function.Bijective (α := X ⟶ Y) L.map
have refine_1 : ∀ (f₁ f₂ : X ⟶ Y) (hf : L.map f₁ = L.map f₂), f₁ = f₂
Tactic: refine ⟨fun f₁ f₂ hf ↦ ?_, fun g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
inst_7 : P.IsTriangulated
inst_8 : IsTriangulated.{v, u} C
Y : C
hY : P.trW.isLocal Y
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
X : C
refine_1 : ∀ (f₁ f₂ : X ⟶ Y) (hf : L.map f₁ = L.map f₂), f₁ = f₂
⊢ Function.Bijective (α := X ⟶ Y) L.map
have refine_2 : ∀ (g : L.obj X ⟶ L.obj Y), ∃ (a : X ⟶ Y), L.map a = g
Tactic: refine ⟨fun f₁ f₂ hf ↦ ?_, fun g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
inst_7 : P.IsTriangulated
inst_8 : IsTriangulated.{v, u} C
Y : C
hY : P.trW.isLocal Y
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
X : C
f₁ f₂ : X ⟶ Y
hf : L.map f₁ = L.map f₂
⊢ f₁ = f₂
have hf₁ : ∃ (X_1 : C) (s : X_1 ⟶ X) (_ : P.trW s), s ≫ f₁ = s ≫ f₂
Tactic: rw [MorphismProperty.map_eq_iff_precomp L P.trW] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
inst_7 : P.IsTriangulated
inst_8 : IsTriangulated.{v, u} C
Y : C
hY : P.trW.isLocal Y
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
X : C
f₁ f₂ : X ⟶ Y
hf : ∃ (X_1 : C) (s : X_1 ⟶ X) (_ : P.trW s), s ≫ f₁ = s ≫ f₂
⊢ f₁ = f₂
have refine_1 : ∀ (Z : C) (s : Z ⟶ X) (hs : P.trW s) (eq : s ≫ f₁ = s ≫ f₂), f₁ = f₂
Tactic: obtain ⟨Z, s, hs, eq⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
inst_7 : P.IsTriangulated
inst_8 : IsTriangulated.{v, u} C
Y : C
hY : P.trW.isLocal Y
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
X : C
g : L.obj X ⟶ L.obj Y
⊢ ∃ (a : X ⟶ Y), L.map a = g
have refine_2 : ∀ (φ : P.trW.RightFraction X Y) (hφ : g = φ.map (W := P.trW) L sorry), ∃ (a : X ⟶ Y), L.map a = g
Tactic: obtain ⟨φ, hφ⟩ := Localization.exists_rightFraction L P.trW g
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
inst_7 : P.IsTriangulated
inst_8 : IsTriangulated.{v, u} C
Y : C
hY : P.trW.isLocal Y
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
X : C
g : L.obj X ⟶ L.obj Y
φ : P.trW.RightFraction X Y
hφ : g = φ.map (W := P.trW) L ⋯
⊢ ∃ (a : X ⟶ Y), L.map a = g
have refine_2 : ∀ (α : X ⟶ Y) (hα : (fun (g : X ⟶ Y) ↦ φ.s (W := P.trW) ≫ g) α = φ.f (W := P.trW)), ∃ (a : X ⟶ Y), L.map a = g
Tactic: obtain ⟨α, hα⟩ := (hY _ φ.hs).2 φ.f
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
inst_7 : P.IsTriangulated
inst_8 : IsTriangulated.{v, u} C
Y : C
hY : P.trW.isLocal Y
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
X : C
g : L.obj X ⟶ L.obj Y
φ : P.trW.RightFraction X Y
hφ : g = φ.map (W := P.trW) L ⋯
α : X ⟶ Y
hα : (fun (g : X ⟶ Y) ↦ φ.s (W := P.trW) ≫ g) α = φ.f (W := P.trW)
⊢ ∃ (a : X ⟶ Y), L.map a = g
have refine_2 : L.map α = g
Tactic: refine ⟨α, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Orthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
P : ObjectProperty.{v, u} C
inst_2 : HasZeroObject.{v, u} C
inst_3 : HasShift.{v, u, 0} C ℤ
inst_4 : Preadditive.{v, u} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
inst_6 : Pretriangulated.{v, u} C
inst_7 : P.IsTriangulated
inst_8 : IsTriangulated.{v, u} C
Y : C
hY : P.trW.isLocal Y
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
X : C
g : L.obj X ⟶ L.obj Y
φ : P.trW.RightFraction X Y
hφ : g = φ.map (W := P.trW) L ⋯
α : X ⟶ Y
hα : (fun (g : X ⟶ Y) ↦ φ.s (W := P.trW) ≫ g) α = φ.f (W := P.trW)
⊢ L.map α = g
have refine_2 : L.map α = φ.map (W := P.trW) L sorry
Tactic: rw [hφ, ← cancel_epi (L.map φ.s), MorphismProperty.RightFraction.map_s_comp_map,
      ← hα, Functor.map_comp]