awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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₁
this : ∀ (α : X ⟶ Y₂), α ≫ h = 0 → α = 0
α₁ α₂ : X ⟶ Y₂
hα : Eq.{v + 1} (α := X ⟶ Y₃) ((fun (f : X ⟶ Y₂) ↦ f ≫ h) α₁) ((fun (f : X ⟶ Y₂) ↦ f ≫ h) α₂)
⊢ α₁ = α₂

Tactic:
simpa [sub_eq_zero] using this (α₁ - α₂) (by simpa [sub_eq_zero])

Premises used: sub_eq_zero, HSub.hSub
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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₁ : ∀ (α : X ⟶ Y₂), α ≫ h = 0 → α = 0
⊢ Function.Injective (β := X ⟶ Y₃) fun (f : X ⟶ Y₂) ↦ f ≫ h

Tactic:
suffices ∀ (α : X ⟶ Y₂), α ≫ h = 0 → α = 0 from fun α₁ α₂ hα ↦ by
        simpa [sub_eq_zero] using this (α₁ - α₂) (by simpa [sub_eq_zero])
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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
h₁ :
  ∀ (β : X ⟶ (Triangle.mk f h g).obj₁) (hα : (β ≫ (Triangle.mk f h g).mor₁) ≫ h = 0), β ≫ (Triangle.mk f h g).mor₁ = 0
⊢ α = 0

Tactic:
obtain ⟨β, rfl⟩ := Triangle.coyoneda_exact₂ _ hT α hα

Premises used: CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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 ⟶ (Triangle.mk f h g).obj₁
hα : (β ≫ (Triangle.mk f h g).mor₁) ≫ h = 0
⊢ β ≫ (Triangle.mk f h g).mor₁ = 0

Tactic:
simp [hX β hY₁]
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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₁ :
  ∀ (β : 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₁
⊢ ∃ (a : X ⟶ Y₂), (fun (f : X ⟶ Y₂) ↦ f ≫ h) a = α

Tactic:
obtain ⟨β, rfl⟩ := Triangle.coyoneda_exact₂ _ (rot_of_distTriang _ hT)
        α (hX _ (P.le_shift _ _ hY₁))

Premises used: CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂, CategoryTheory.Pretriangulated.rot_of_distTriang, rfl, CategoryTheory.ObjectProperty.le_shift
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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 ⟶ (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:
⟨β, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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 ⟶ (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:
exact ⟨β, rfl⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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
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
⊢ Function.Bijective (α := X ⟶ Y) L.map

Tactic:
rw [← isLocal_trW] at hY

Premises used: CategoryTheory.ObjectProperty.isLocal_trW
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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

Tactic:
⟨fun f₁ f₂ hf ↦ ?_, fun g ↦ ?_⟩

Premises used: And.intro, Function.Bijective
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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₂
refine_2 : ∀ (g : L.obj X ⟶ L.obj Y), ∃ (a : X ⟶ Y), L.map a = g
⊢ Function.Bijective (α := X ⟶ Y) L.map

Tactic:
refine ⟨fun f₁ f₂ hf ↦ ?_, fun g ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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₂
⊢ ∃ (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

Premises used: CategoryTheory.ObjectProperty.trW, CategoryTheory.MorphismProperty.map_eq_iff_precomp
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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₂
refine_1 : ∀ (Z : C) (s : Z ⟶ X) (hs : P.trW s) (eq : s ≫ f₁ = s ≫ f₂), f₁ = f₂
⊢ f₁ = f₂

Tactic:
obtain ⟨Z, s, hs, eq⟩ := hf
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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
Z : C
s : Z ⟶ X
hs : P.trW s
eq : s ≫ f₁ = s ≫ f₂
⊢ f₁ = f₂

Tactic:
(hY _ hs).1 eq

Premises used: And.left
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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
Z : C
s : Z ⟶ X
hs : P.trW s
eq : s ≫ f₁ = s ≫ f₂
⊢ f₁ = f₂

Tactic:
exact (hY _ hs).1 eq

Premises used: And.left
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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
refine_2 : ∀ (φ : P.trW.RightFraction X Y) (hφ : g = φ.map (W := P.trW) L ⋯), ∃ (a : X ⟶ Y), L.map a = g
⊢ ∃ (a : X ⟶ Y), L.map a = g

Tactic:
obtain ⟨φ, hφ⟩ := Localization.exists_rightFraction L P.trW g

Premises used: CategoryTheory.Localization.exists_rightFraction, CategoryTheory.ObjectProperty.trW
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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 ⋯
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
⊢ ∃ (a : X ⟶ Y), L.map a = g

Tactic:
obtain ⟨α, hα⟩ := (hY _ φ.hs).2 φ.f

Premises used: CategoryTheory.MorphismProperty.RightFraction.f, And.right, CategoryTheory.MorphismProperty.RightFraction.hs
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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

Tactic:
⟨α, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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)
refine_2 : L.map α = g
⊢ ∃ (a : X ⟶ Y), L.map a = g

Tactic:
refine ⟨α, ?_⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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)
refine_2 : L.map α = φ.map (W := P.trW) L ⋯
refine_2₁ : L.map (φ.s (W := P.trW)) ≫ L.map α = L.map (φ.s (W := P.trW)) ≫ φ.map (W := P.trW) L ⋯
refine_2₂ : L.map (φ.s (W := P.trW)) ≫ L.map α = L.map (φ.f (W := P.trW))
refine_2₃ : L.map (φ.s (W := P.trW)) ≫ L.map α = L.map ((fun (g : X ⟶ Y) ↦ φ.s (W := P.trW) ≫ g) α)
refine_2₄ refine_2₅ : L.map (φ.s (W := P.trW)) ≫ L.map α = L.map (φ.s (W := P.trW)) ≫ L.map α
⊢ L.map α = g

Tactic:
rw [hφ, ← cancel_epi (L.map φ.s), MorphismProperty.RightFraction.map_s_comp_map,
      ← hα, Functor.map_comp]

Premises used: CategoryTheory.MorphismProperty.RightFraction.map_s_comp_map, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi, CategoryTheory.MorphismProperty.RightFraction.s
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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
X : C
hX : P.leftOrthogonal X
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
Y : C
rw :
  ∀ (hX : P.trW.isColocal X) (L : Functor.{v, v', u, u'} C D) [L.IsLocalization P.trW] (Y : C),
    Function.Bijective (α := X ⟶ Y) L.map
⊢ Function.Bijective (α := X ⟶ Y) L.map

Tactic:
rw [← isColocal_trW] at hX

Premises used: CategoryTheory.ObjectProperty.isColocal_trW
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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
X : C
hX : P.trW.isColocal X
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
Y : C
⊢ Function.Bijective (α := X ⟶ Y) L.map

Tactic:
⟨fun f₁ f₂ hf ↦ ?_, fun g ↦ ?_⟩

Premises used: And.intro, Function.Bijective
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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
X : C
hX : P.trW.isColocal X
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
Y : C
refine_1 : ∀ (f₁ f₂ : X ⟶ Y) (hf : L.map f₁ = L.map f₂), f₁ = f₂
refine_2 : ∀ (g : L.obj X ⟶ L.obj Y), ∃ (a : X ⟶ Y), L.map a = g
⊢ Function.Bijective (α := X ⟶ Y) L.map

Tactic:
refine ⟨fun f₁ f₂ hf ↦ ?_, fun g ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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
X : C
hX : P.trW.isColocal X
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
Y : C
f₁ f₂ : X ⟶ Y
hf : L.map f₁ = L.map f₂
⊢ ∃ (Z : C) (s : Y ⟶ Z) (_ : P.trW s), f₁ ≫ s = f₂ ≫ s

Tactic:
rw [MorphismProperty.map_eq_iff_postcomp L P.trW] at hf

Premises used: CategoryTheory.MorphismProperty.map_eq_iff_postcomp, CategoryTheory.ObjectProperty.trW
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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
X : C
hX : P.trW.isColocal X
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
Y : C
f₁ f₂ : X ⟶ Y
hf : ∃ (Z : C) (s : Y ⟶ Z) (_ : P.trW s), f₁ ≫ s = f₂ ≫ s
refine_1 : ∀ (Z : C) (s : Y ⟶ Z) (hs : P.trW s) (eq : f₁ ≫ s = f₂ ≫ s), f₁ = f₂
⊢ f₁ = f₂

Tactic:
obtain ⟨Z, s, hs, eq⟩ := hf
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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
X : C
hX : P.trW.isColocal X
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
Y : C
f₁ f₂ : X ⟶ Y
Z : C
s : Y ⟶ Z
hs : P.trW s
eq : f₁ ≫ s = f₂ ≫ s
⊢ f₁ = f₂

Tactic:
(hX _ hs).1 eq

Premises used: And.left
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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
X : C
hX : P.trW.isColocal X
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
Y : C
f₁ f₂ : X ⟶ Y
Z : C
s : Y ⟶ Z
hs : P.trW s
eq : f₁ ≫ s = f₂ ≫ s
⊢ f₁ = f₂

Tactic:
exact (hX _ hs).1 eq

Premises used: And.left
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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
X : C
hX : P.trW.isColocal X
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
Y : C
g : L.obj X ⟶ L.obj Y
refine_2 : ∀ (φ : P.trW.LeftFraction X Y) (hφ : g = φ.map (W := P.trW) L ⋯), ∃ (a : X ⟶ Y), L.map a = g
⊢ ∃ (a : X ⟶ Y), L.map a = g

Tactic:
obtain ⟨φ, hφ⟩ := Localization.exists_leftFraction L P.trW g

Premises used: CategoryTheory.Localization.exists_leftFraction, CategoryTheory.ObjectProperty.trW
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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
X : C
hX : P.trW.isColocal X
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
Y : C
g : L.obj X ⟶ L.obj Y
φ : P.trW.LeftFraction X Y
hφ : g = φ.map (W := P.trW) L ⋯
refine_2 :
  ∀ (α : X ⟶ Y) (hα : (fun (f : X ⟶ Y) ↦ f ≫ φ.s (W := P.trW)) α = φ.f (W := P.trW)), ∃ (a : X ⟶ Y), L.map a = g
⊢ ∃ (a : X ⟶ Y), L.map a = g

Tactic:
obtain ⟨α, hα⟩ := (hX _ φ.hs).2 φ.f

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, And.right, CategoryTheory.MorphismProperty.LeftFraction.f
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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
X : C
hX : P.trW.isColocal X
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
Y : C
g : L.obj X ⟶ L.obj Y
φ : P.trW.LeftFraction X Y
hφ : g = φ.map (W := P.trW) L ⋯
α : X ⟶ Y
hα : (fun (f : X ⟶ Y) ↦ f ≫ φ.s (W := P.trW)) α = φ.f (W := P.trW)
⊢ ∃ (a : X ⟶ Y), L.map a = g

Tactic:
⟨α, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.Orthogonal
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
X : C
hX : P.trW.isColocal X
L : Functor.{v, v', u, u'} C D
inst_9 : L.IsLocalization P.trW
Y : C
g : L.obj X ⟶ L.obj Y
φ : P.trW.LeftFraction X Y
hφ : g = φ.map (W := P.trW) L ⋯
α : X ⟶ Y
hα : (fun (f : X ⟶ Y) ↦ f ≫ φ.s (W := P.trW)) α = φ.f (W := P.trW)
refine_2 : L.map α = g
⊢ ∃ (a : X ⟶ Y), L.map a = g

Tactic:
refine ⟨α, ?_⟩