awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (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
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop :=
  fun (g : StructuredArrow (W.Q.obj X) W.Q) ↦
    P ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L) g)
hP₃ : P' (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₄ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P' (StructuredArrow.mk φ) → P' (StructuredArrow.mk (φ ≫ W.Q.map f))
⊢ P
    ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L)
      ((Equiv.symm (structuredArrowEquiv W W.Q L) : (a : StructuredArrow (L.obj X) L) → StructuredArrow (W.Q.obj X) W.Q)
        g))
have hP₅ : ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
  P' (StructuredArrow.mk φ) → P' (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
Tactic: apply induction_structuredArrow' W P'
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (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
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop :=
  fun (g : StructuredArrow (W.Q.obj X) W.Q) ↦
    P ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L) g)
⊢ P' (StructuredArrow.mk (𝟙 (W.Q.obj X)))
have h : (structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L)
    (StructuredArrow.mk (𝟙 (W.Q.obj X))) =
  StructuredArrow.mk (𝟙 (L.obj X))
Tactic: convert! hP₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (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
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop :=
  fun (g : StructuredArrow (W.Q.obj X) W.Q) ↦
    P ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L) g)
Y₁ Y₂ : C
f : Y₁ ⟶ Y₂
φ : W.Q.obj X ⟶ W.Q.obj Y₁
hφ : P' (StructuredArrow.mk φ)
⊢ P' (StructuredArrow.mk (φ ≫ W.Q.map f))
have h : Eq (α := StructuredArrow (L.obj X) L)
  ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L)
      (StructuredArrow.mk (φ ≫ W.Q.map f)) :
    StructuredArrow (L.obj X) L)
  (StructuredArrow.mk (Y := Y₂) ((homEquiv W W.Q L : (a : W.Q.obj X ⟶ W.Q.obj Y₁) → L.obj X ⟶ L.obj Y₁) φ ≫ L.map f) :
    StructuredArrow (L.obj X) L)
Tactic: convert! hP₁ f (homEquiv W W.Q L φ) hφ
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (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
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop :=
  fun (g : StructuredArrow (W.Q.obj X) W.Q) ↦
    P ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L) g)
Y₁ Y₂ : C
w : Y₁ ⟶ Y₂
hw : W w
φ : W.Q.obj X ⟶ W.Q.obj Y₂
hφ : P' (StructuredArrow.mk φ)
⊢ P' (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
have h : Eq (α := StructuredArrow (L.obj X) L)
  ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L)
      (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv)) :
    StructuredArrow (L.obj X) L)
  (StructuredArrow.mk (Y := Y₁)
      ((homEquiv W W.Q L : (a : W.Q.obj X ⟶ W.Q.obj Y₂) → L.obj X ⟶ L.obj Y₂) φ ≫ (isoOfHom L W w hw).inv) :
    StructuredArrow (L.obj X) L)
Tactic: convert! hP₂ w hw (homEquiv W W.Q L φ) hφ
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (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
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
Y : C
P : CostructuredArrow L (L.obj Y) → Prop
hP₀ : P (CostructuredArrow.mk (𝟙 (L.obj Y)))
hP₁ :
  ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk (L.map f ≫ φ))
hP₂ :
  ∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk ((isoOfHom L W w hw).inv ≫ φ))
g : CostructuredArrow L (L.obj Y)
g' : StructuredArrow (op (L.obj Y)) L.op := StructuredArrow.mk (Y := op g.left) g.hom.op
⊢ P g
have change : P (CostructuredArrow.mk g'.hom.unop)
Tactic: change P (CostructuredArrow.mk g'.hom.unop)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (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
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
Y : C
P : CostructuredArrow L (L.obj Y) → Prop
hP₀ : P (CostructuredArrow.mk (𝟙 (L.obj Y)))
hP₁ :
  ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk (L.map f ≫ φ))
hP₂ :
  ∀ ⦃X₁ X₂ : C⦄ (w : X₁ ⟶ X₂) (hw : W w) (φ : L.obj X₁ ⟶ L.obj Y),
    P (CostructuredArrow.mk φ) → P (CostructuredArrow.mk ((isoOfHom L W w hw).inv ≫ φ))
g : CostructuredArrow L (L.obj Y)
g' : StructuredArrow (op (L.obj Y)) L.op := StructuredArrow.mk (Y := op g.left) g.hom.op
⊢ P (CostructuredArrow.mk g'.hom.unop)
have induction : ∀ (x : StructuredArrow (op (L.obj Y)) L.op), P (CostructuredArrow.mk x.hom.unop)
Tactic: induction g' using induction_structuredArrow L.op W.op with
  | hP₀ => exact hP₀
  | hP₁ f φ hφ => exact hP₁ f.unop φ.unop hφ
  | hP₂ w hw φ hφ => simpa [isoOfHom_op_inv L W w hw] using hP₂ w.unop hw φ.unop 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 : ℤ), 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 ℤ
T₁ T₂ : Triangle.{v_2, u_2} D
e : T₂ ≅ T₁
h : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T₁
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T₂
have obtain : ∀ (T' : Triangle.{v_1, u_1} C) (e' : T₁ ≅ obj L.mapTriangle T')
  (hT' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T'),
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T₂
Tactic: obtain ⟨T', e', hT'⟩ := h
Cleared hypotheses: 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 : ℤ), 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 ℤ
inst_9 : L.EssSurj
inst_10 : HasZeroObject.{v_2, u_2} D
inst_11 : HasZeroMorphisms.{v_2, u_2} D
inst_12 : L.PreservesZeroMorphisms
X : D
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang (contractibleTriangle X)
have refine : Iso (C := Triangle.{v_2, u_2} D) (contractibleTriangle X)
  (obj (C := Triangle.{v_1, u_1} C) L.mapTriangle (contractibleTriangle (L.objPreimage X)))
Tactic: refine ⟨contractibleTriangle (L.objPreimage X), ?_, contractible_distinguished _⟩
-- 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 : ℤ), 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 ℤ
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : L.Additive
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
T : Triangle.{v_2, u_2} D
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T ↔
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T.rotate
have mp : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T →
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T.rotate
Tactic: constructor
-- 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 : ℤ), 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 ℤ
inst_9 : Preadditive.{v_2, u_2} D
inst_10 : L.Additive
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
T : Triangle.{v_2, u_2} D
mp :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T →
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T.rotate
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T ↔
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T.rotate
have mpr : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T.rotate →
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T
Tactic: constructor
-- 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 : ℤ), 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 ℤ
H :
  ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
      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₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
            ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle.{v_2, u_2} D
hT₁ : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T₂
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
have obtain : ∀ (T₁' : Triangle.{v_1, u_1} C) (e₁ : T₁ ≅ obj L.mapTriangle T₁')
  (hT₁' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁'),
  ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
Tactic: obtain ⟨T₁', e₁, hT₁'⟩ := hT₁
Cleared hypotheses: hT₁
-- 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 : ℤ), 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 ℤ
H :
  ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
      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₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
            ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle.{v_2, u_2} D
hT₂ : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T₂
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
T₁' : Triangle.{v_1, u_1} C
e₁ : T₁ ≅ obj L.mapTriangle T₁'
hT₁' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁'
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
have obtain : ∀ (T₂' : Triangle.{v_1, u_1} C) (e₂ : T₂ ≅ obj L.mapTriangle T₂')
  (hT₂' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂'),
  ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
Tactic: obtain ⟨T₂', e₂, hT₂'⟩ := hT₂
Cleared hypotheses: hT₂
-- 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 : ℤ), 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 ℤ
H :
  ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
      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₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
            ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle.{v_2, u_2} D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
T₁' : Triangle.{v_1, u_1} C
e₁ : T₁ ≅ obj L.mapTriangle T₁'
hT₁' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁'
T₂' : Triangle.{v_1, u_1} C
e₂ : T₂ ≅ obj L.mapTriangle T₂'
hT₂' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂'
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
have comm₁ : Triangle.mor₁ (obj L.mapTriangle T₁') ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
Tactic: have comm₁ := e₁.inv.comm₁
-- 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 : ℤ), 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 ℤ
H :
  ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
      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₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
            ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle.{v_2, u_2} D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
T₁' : Triangle.{v_1, u_1} C
e₁ : T₁ ≅ obj L.mapTriangle T₁'
hT₁' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁'
T₂' : Triangle.{v_1, u_1} C
e₂ : T₂ ≅ obj L.mapTriangle T₂'
hT₂' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂'
comm₁ : Triangle.mor₁ (obj L.mapTriangle T₁') ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
have comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ Triangle.mor₁ (obj L.mapTriangle T₂')
Tactic: have comm₁' := e₂.hom.comm₁
-- 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 : ℤ), 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 ℤ
H :
  ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
      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₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
            ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle.{v_2, u_2} D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
T₁' : Triangle.{v_1, u_1} C
e₁ : T₁ ≅ obj L.mapTriangle T₁'
hT₁' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁'
T₂' : Triangle.{v_1, u_1} C
e₂ : T₂ ≅ obj L.mapTriangle T₂'
hT₂' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂'
comm₁ : Triangle.mor₁ (obj L.mapTriangle T₁') ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ Triangle.mor₁ (obj L.mapTriangle T₂')
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
have comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ Triangle.mor₂ (obj L.mapTriangle T₁')
Tactic: have comm₂ := e₁.hom.comm₂
-- 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 : ℤ), 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 ℤ
H :
  ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
      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₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
            ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle.{v_2, u_2} D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
T₁' : Triangle.{v_1, u_1} C
e₁ : T₁ ≅ obj L.mapTriangle T₁'
hT₁' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁'
T₂' : Triangle.{v_1, u_1} C
e₂ : T₂ ≅ obj L.mapTriangle T₂'
hT₂' : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂'
comm₁ : Triangle.mor₁ (obj L.mapTriangle T₁') ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ Triangle.mor₁ (obj L.mapTriangle T₂')
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ Triangle.mor₂ (obj L.mapTriangle T₁')
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
have comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ Triangle.mor₂ (obj L.mapTriangle T₂')
Tactic: have comm₂' := e₂.hom.comm₂