awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle.{v_1, u_1} C
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
⊢ ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
    φ.hom₁ = a ∧ φ.hom₂ = b
have obtain : ∀ (α : W.LeftFraction T₁.obj₁ T₂.obj₁) (hα : a = α.map (W := W) L sorry),
  ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
    φ.hom₁ = a ∧ φ.hom₂ = b
Tactic: obtain ⟨α, hα⟩ := exists_leftFraction L W a
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle.{v_1, u_1} C
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
⊢ ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
    φ.hom₁ = a ∧ φ.hom₂ = b
have obtain : ∀ (β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂)
  (hβ :
    (MorphismProperty.RightFraction.mk (W := W) (α.s (W := W)) sorry T₂.mor₁).f (W := W) ≫ β.s (W := W) =
      (MorphismProperty.RightFraction.mk (W := W) (α.s (W := W)) sorry T₂.mor₁).s (W := W) ≫ β.f (W := W)),
  ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
    φ.hom₁ = a ∧ φ.hom₂ = b
Tactic: obtain ⟨β, hβ⟩ := (MorphismProperty.RightFraction.mk α.s α.hs T₂.mor₁).exists_leftFraction
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle.{v_1, u_1} C
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ :
  (MorphismProperty.RightFraction.mk (W := W) (α.s (W := W)) ⋯ T₂.mor₁).f (W := W) ≫ β.s (W := W) =
    (MorphismProperty.RightFraction.mk (W := W) (α.s (W := W)) ⋯ T₂.mor₁).s (W := W) ≫ β.f (W := W)
⊢ ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
    φ.hom₁ = a ∧ φ.hom₂ = b
have obtain : ∀ (γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))) (hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L sorry),
  ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
    φ.hom₁ = a ∧ φ.hom₂ = b
Tactic: obtain ⟨γ, hγ⟩ := exists_leftFraction L W (b ≫ L.map β.s)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle.{v_1, u_1} C
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
⊢ L.map (α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W)) = L.map (T₁.mor₁ ≫ γ.f (W := W))
have rw : ∀ (hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)) (γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W)))
  (fac :
    L.map (T₁.mor₁ ≫ γ.f (W := W)) = α.map (W := W) L sorry ≫ L.map T₂.mor₁ ≫ L.map (β.s (W := W)) ≫ L.map (γ.s (W := W)))
  (hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L sorry),
  L.map (α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W)) = L.map (T₁.mor₁ ≫ γ.f (W := W))
Tactic: rw [← cancel_mono (L.map β.s), assoc, assoc, hγ, ← cancel_mono (L.map γ.s),
        assoc, assoc, assoc, hα, MorphismProperty.LeftFraction.map_comp_map_s,
        ← Functor.map_comp] at fac
Cleared hypotheses: fac, hβ, γ, hγ
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle.{v_1, u_1} C
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
⊢ ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
    φ.hom₁ = a ∧ φ.hom₂ = b
have obtain : ∀ (Z₂ : C) (σ : γ.Y' (W := W) ⟶ Z₂) (hσ : W σ)
  (fac : (α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W)) ≫ σ = (T₁.mor₁ ≫ γ.f (W := W)) ≫ σ),
  ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
    φ.hom₁ = a ∧ φ.hom₂ = b
Tactic: obtain ⟨Z₂, σ, hσ, fac⟩ := (MorphismProperty.map_eq_iff_postcomp L W
    (α.f ≫ β.f ≫ γ.s) (T₁.mor₁ ≫ γ.f)).1 (by
      rw [← cancel_mono (L.map β.s), assoc, assoc, hγ, ← cancel_mono (L.map γ.s),
        assoc, assoc, assoc, hα, MorphismProperty.LeftFraction.map_comp_map_s,
        ← Functor.map_comp] at fac
      rw [fac, ← Functor.map_comp_assoc, hβ, Functor.map_comp, Functor.map_comp,
        Functor.map_comp, assoc, MorphismProperty.LeftFraction.map_comp_map_s_assoc])
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle.{v_1, u_1} C
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac_1 : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
Z₂ : C
σ : γ.Y' (W := W) ⟶ Z₂
hσ : W σ
fac : (α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W)) ≫ σ = (T₁.mor₁ ≫ γ.f (W := W)) ≫ σ
⊢ ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
    φ.hom₁ = a ∧ φ.hom₂ = b
have fac₁ : α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = T₁.mor₁ ≫ γ.f (W := W) ≫ σ
Tactic: simp only [assoc] at fac
Cleared hypotheses: fac
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle.{v_1, u_1} C
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac_1 : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
Z₂ : C
σ : γ.Y' (W := W) ⟶ Z₂
hσ : W σ
fac : α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = T₁.mor₁ ≫ γ.f (W := W) ≫ σ
⊢ ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
    φ.hom₁ = a ∧ φ.hom₂ = b
have obtain : ∀ (Y₃ : C) (g : Z₂ ⟶ Y₃) (h : Y₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (α.Y' (W := W)))
  (hT₃ :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
      (Triangle.mk (β.f (W := W) ≫ γ.s (W := W) ≫ σ) g h)),
  ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
    φ.hom₁ = a ∧ φ.hom₂ = b
Tactic: obtain ⟨Y₃, g, h, hT₃⟩ := Pretriangulated.distinguished_cocone_triangle (β.f ≫ γ.s ≫ σ)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle.{v_1, u_1} C
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac_1 : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
Z₂ : C
σ : γ.Y' (W := W) ⟶ Z₂
hσ : W σ
fac : α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = T₁.mor₁ ≫ γ.f (W := W) ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (α.Y' (W := W))
T₃ : Triangle.{v_1, u_1} C := Triangle.mk (β.f (W := W) ≫ γ.s (W := W) ≫ σ) g h
hT₃ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₃
⊢ ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
    φ.hom₁ = a ∧ φ.hom₂ = b
have hβγσ : W (β.s (W := W) ≫ γ.s (W := W) ≫ σ)
Tactic: have hβγσ : W (β.s ≫ γ.s ≫ σ) := W.comp_mem _ _ β.hs (W.comp_mem _ _ γ.hs hσ)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle.{v_1, u_1} C
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac_1 : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
Z₂ : C
σ : γ.Y' (W := W) ⟶ Z₂
hσ : W σ
fac : α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = T₁.mor₁ ≫ γ.f (W := W) ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (α.Y' (W := W))
T₃ : Triangle.{v_1, u_1} C := Triangle.mk (β.f (W := W) ≫ γ.s (W := W) ≫ σ) g h
hT₃ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₃
hβγσ : W (β.s (W := W) ≫ γ.s (W := W) ≫ σ)
⊢ T₂.mor₁ ≫ β.s (W := W) ≫ γ.s (W := W) ≫ σ = α.s (W := W) ≫ T₃.mor₁
have dsimp : T₂.mor₁ ≫ β.s (W := W) ≫ γ.s (W := W) ≫ σ = α.s (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ
Tactic: dsimp [T₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle.{v_1, u_1} C
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac_1 : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
Z₂ : C
σ : γ.Y' (W := W) ⟶ Z₂
hσ : W σ
fac : α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = T₁.mor₁ ≫ γ.f (W := W) ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (α.Y' (W := W))
T₃ : Triangle.{v_1, u_1} C := Triangle.mk (β.f (W := W) ≫ γ.s (W := W) ≫ σ) g h
hT₃ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₃
hβγσ : W (β.s (W := W) ≫ γ.s (W := W) ≫ σ)
⊢ T₂.mor₁ ≫ β.s (W := W) ≫ γ.s (W := W) ≫ σ = α.s (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ
have rw : α.s (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = α.s (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ
Tactic: rw [reassoc_of% hβ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle.{v_1, u_1} C
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac_1 : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
Z₂ : C
σ : γ.Y' (W := W) ⟶ Z₂
hσ : W σ
fac : α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = T₁.mor₁ ≫ γ.f (W := W) ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (α.Y' (W := W))
T₃ : Triangle.{v_1, u_1} C := Triangle.mk (β.f (W := W) ≫ γ.s (W := W) ≫ σ) g h
hT₃ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₃
hβγσ : W (β.s (W := W) ≫ γ.s (W := W) ≫ σ)
⊢ ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
    φ.hom₁ = a ∧ φ.hom₂ = b
have obtain : ∀ (ψ₃ : T₂.obj₃ ⟶ T₃.obj₃) (hψ₃ : W ψ₃) (hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s (W := W) ≫ γ.s (W := W) ≫ σ) ≫ T₃.mor₂)
  (hψ₂ : T₂.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (α.s (W := W)) = ψ₃ ≫ T₃.mor₃),
  ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁) (Functor.obj L.mapTriangle T₂)),
    φ.hom₁ = a ∧ φ.hom₂ = b
Tactic: obtain ⟨ψ₃, hψ₃, hψ₁, hψ₂⟩ := MorphismProperty.compatible_with_triangulation
    T₂ T₃ hT₂ hT₃ α.s (β.s ≫ γ.s ≫ σ) α.hs hβγσ (by dsimp [T₃]; rw [reassoc_of% hβ])
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle.{v_1, u_1} C
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac_1 : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
Z₂ : C
σ : γ.Y' (W := W) ⟶ Z₂
hσ : W σ
fac : α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = T₁.mor₁ ≫ γ.f (W := W) ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (α.Y' (W := W))
T₃ : Triangle.{v_1, u_1} C := Triangle.mk (β.f (W := W) ≫ γ.s (W := W) ≫ σ) g h
hT₃ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₃
hβγσ : W (β.s (W := W) ≫ γ.s (W := W) ≫ σ)
ψ₃ : T₂.obj₃ ⟶ T₃.obj₃
hψ₃ : W ψ₃
hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s (W := W) ≫ γ.s (W := W) ≫ σ) ≫ T₃.mor₂
hψ₂ : T₂.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (α.s (W := W)) = ψ₃ ≫ T₃.mor₃
⊢ T₂.mor₁ ≫ β.s (W := W) ≫ γ.s (W := W) ≫ σ = α.s (W := W) ≫ T₃.mor₁
have dsimp : T₂.mor₁ ≫ β.s (W := W) ≫ γ.s (W := W) ≫ σ = α.s (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ
Tactic: dsimp [T₃]