awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (hypothesis)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : (g ≫ T.mor₁) ≫ φ.hom₂ = 0
⊢ g ≫ T.mor₁ = 0
have hf₁ : g ≫ T.mor₁ ≫ φ.hom₂ = 0
Tactic: rw [assoc] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
⊢ (g ≫ φ.hom₁) ≫ T'.invRotate.mor₂ = 0
have dsimp : (g ≫ φ.hom₁) ≫ T'.mor₁ = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
⊢ (g ≫ φ.hom₁) ≫ T'.mor₁ = 0
have rw : g ≫ φ.hom₁ ≫ T'.mor₁ = 0
Tactic: rw [assoc, ← φ.comm₁, hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
rw : g ≫ φ.hom₁ ≫ T'.mor₁ = 0
rw₁ : g ≫ T.mor₁ ≫ φ.hom₂ = 0
⊢ (g ≫ φ.hom₁) ≫ T'.mor₁ = 0
have rw₂ : Eq.{v + 1} (α := A ⟶ T'.obj₂) 0 0
Tactic: rw [assoc, ← φ.comm₁, hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
⊢ g ≫ T.mor₁ = 0
have obtain : ∀ (h : A ⟶ T'.invRotate.obj₁) (hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁), g ≫ T.mor₁ = 0
Tactic: obtain ⟨h, hh⟩ := Triangle.coyoneda_exact₂ T'.invRotate (inv_rot_of_distTriang _ hT')
      (g ≫ φ.hom₁) (by dsimp; rw [assoc, ← φ.comm₁, hf])
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
h : A ⟶ T'.invRotate.obj₁
hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
⊢ ∃ (k : A ⟶ T.invRotate.obj₁), k ≫ T.invRotate.mor₁ = g
have refine : (h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁ = g
Tactic: refine ⟨h ≫ inv (φ.hom₃⟦(-1 : ℤ)⟧'), ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (hypothesis)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
h : A ⟶ T'.invRotate.obj₁
hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
⊢ (h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁ = g
have eq : (Functor.obj (invRotate C) T).mor₁ ≫ TriangleMorphism.hom₂ (Functor.map (invRotate C) φ) =
  TriangleMorphism.hom₁ (Functor.map (invRotate C) φ) ≫ (Functor.obj (invRotate C) T').mor₁
Tactic: have eq := ((invRotate C).map φ).comm₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
h : A ⟶ T'.invRotate.obj₁
hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
eq : T.invRotate.mor₁ ≫ φ.hom₁ = Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃ ≫ T'.invRotate.mor₁
⊢ (h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁ = g
have rw : ((h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁) ≫ φ.hom₁ = g ≫ φ.hom₁
Tactic: rw [← cancel_mono φ.hom₁, assoc, assoc, eq, IsIso.inv_hom_id_assoc, hh]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
h : A ⟶ T'.invRotate.obj₁
hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
eq : T.invRotate.mor₁ ≫ φ.hom₁ = Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃ ≫ T'.invRotate.mor₁
rw : ((h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁) ≫ φ.hom₁ = g ≫ φ.hom₁
⊢ (h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁ = g
have rw₁ : (h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁ ≫ φ.hom₁ = g ≫ φ.hom₁
Tactic: rw [← cancel_mono φ.hom₁, assoc, assoc, eq, IsIso.inv_hom_id_assoc, hh]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
h : A ⟶ T'.invRotate.obj₁
hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
eq : T.invRotate.mor₁ ≫ φ.hom₁ = Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃ ≫ T'.invRotate.mor₁
rw : ((h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁) ≫ φ.hom₁ = g ≫ φ.hom₁
rw₁ : (h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁ ≫ φ.hom₁ = g ≫ φ.hom₁
⊢ (h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁ = g
have rw₂ : h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃) ≫ T.invRotate.mor₁ ≫ φ.hom₁ = g ≫ φ.hom₁
Tactic: rw [← cancel_mono φ.hom₁, assoc, assoc, eq, IsIso.inv_hom_id_assoc, hh]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
h : A ⟶ T'.invRotate.obj₁
hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
eq : T.invRotate.mor₁ ≫ φ.hom₁ = Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃ ≫ T'.invRotate.mor₁
rw : ((h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁) ≫ φ.hom₁ = g ≫ φ.hom₁
rw₁ : (h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁ ≫ φ.hom₁ = g ≫ φ.hom₁
rw₂ : h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃) ≫ T.invRotate.mor₁ ≫ φ.hom₁ = g ≫ φ.hom₁
⊢ (h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁ = g
have rw₃ : h ≫
    inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃) ≫
      Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃ ≫ T'.invRotate.mor₁ =
  g ≫ φ.hom₁
Tactic: rw [← cancel_mono φ.hom₁, assoc, assoc, eq, IsIso.inv_hom_id_assoc, hh]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
h : A ⟶ T'.invRotate.obj₁
hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
eq : T.invRotate.mor₁ ≫ φ.hom₁ = Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃ ≫ T'.invRotate.mor₁
rw : ((h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁) ≫ φ.hom₁ = g ≫ φ.hom₁
rw₁ : (h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁ ≫ φ.hom₁ = g ≫ φ.hom₁
rw₂ : h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃) ≫ T.invRotate.mor₁ ≫ φ.hom₁ = g ≫ φ.hom₁
rw₃ :
  h ≫
      inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃) ≫
        Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃ ≫ T'.invRotate.mor₁ =
    g ≫ φ.hom₁
⊢ (h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁ = g
have rw₄ : h ≫ T'.invRotate.mor₁ = g ≫ φ.hom₁
Tactic: rw [← cancel_mono φ.hom₁, assoc, assoc, eq, IsIso.inv_hom_id_assoc, hh]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
h : A ⟶ T'.invRotate.obj₁
hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
eq : T.invRotate.mor₁ ≫ φ.hom₁ = Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃ ≫ T'.invRotate.mor₁
rw : ((h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁) ≫ φ.hom₁ = g ≫ φ.hom₁
rw₁ : (h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁ ≫ φ.hom₁ = g ≫ φ.hom₁
rw₂ : h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃) ≫ T.invRotate.mor₁ ≫ φ.hom₁ = g ≫ φ.hom₁
rw₃ :
  h ≫
      inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃) ≫
        Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃ ≫ T'.invRotate.mor₁ =
    g ≫ φ.hom₁
rw₄ : h ≫ T'.invRotate.mor₁ = g ≫ φ.hom₁
⊢ (h ≫ inv (Functor.map (shiftFunctor C (A := ℤ) (-1)) φ.hom₃)) ≫ T.invRotate.mor₁ = g
have rw₅ : h ≫ T'.invRotate.mor₁ = h ≫ T'.invRotate.mor₁
Tactic: rw [← cancel_mono φ.hom₁, assoc, assoc, eq, IsIso.inv_hom_id_assoc, hh]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
h : A ⟶ T'.invRotate.obj₁
hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
⊢ g ≫ T.mor₁ = 0
have obtain : ∀ (k : A ⟶ T.invRotate.obj₁) (hf : (k ≫ T.invRotate.mor₁) ≫ T.mor₁ ≫ φ.hom₂ = 0)
  (hh : (k ≫ T.invRotate.mor₁) ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁), (k ≫ T.invRotate.mor₁) ≫ T.mor₁ = 0
Tactic: obtain ⟨k, rfl⟩ : ∃ (k : A ⟶ T.invRotate.obj₁), k ≫ T.invRotate.mor₁ = g := by
      refine ⟨h ≫ inv (φ.hom₃⟦(-1 : ℤ)⟧'), ?_⟩
      have eq := ((invRotate C).map φ).comm₁
      dsimp only [invRotate] at eq
      rw [← cancel_mono φ.hom₁, assoc, assoc, eq, IsIso.inv_hom_id_assoc, hh]
Cleared hypotheses: g, hf, hh
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
h : A ⟶ T'.invRotate.obj₁
k : A ⟶ T.invRotate.obj₁
hf : (k ≫ T.invRotate.mor₁) ≫ T.mor₁ ≫ φ.hom₂ = 0
hh : (k ≫ T.invRotate.mor₁) ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
⊢ (k ≫ T.invRotate.mor₁) ≫ T.mor₁ = 0
have erw : k ≫ T.invRotate.mor₁ ≫ T.mor₁ = 0
Tactic: erw [assoc, comp_distTriang_mor_zero₁₂ _ (inv_rot_of_distTriang _ hT), comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
h : A ⟶ T'.invRotate.obj₁
k : A ⟶ T.invRotate.obj₁
hf : (k ≫ T.invRotate.mor₁) ≫ T.mor₁ ≫ φ.hom₂ = 0
hh : (k ≫ T.invRotate.mor₁) ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
erw : k ≫ T.invRotate.mor₁ ≫ T.mor₁ = 0
⊢ (k ≫ T.invRotate.mor₁) ≫ T.mor₁ = 0
have erw₁ : Eq (α := A ⟶ T.obj₂) (k ≫ 0) 0
Tactic: erw [assoc, comp_distTriang_mor_zero₁₂ _ (inv_rot_of_distTriang _ hT), comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
h : A ⟶ T'.invRotate.obj₁
k : A ⟶ T.invRotate.obj₁
hf : (k ≫ T.invRotate.mor₁) ≫ T.mor₁ ≫ φ.hom₂ = 0
hh : (k ≫ T.invRotate.mor₁) ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
erw : k ≫ T.invRotate.mor₁ ≫ T.mor₁ = 0
erw₁ : Eq (α := A ⟶ T.obj₂) (k ≫ 0) 0
⊢ (k ≫ T.invRotate.mor₁) ≫ T.mor₁ = 0
have erw₂ : Eq.{v + 1} (α := A ⟶ T.obj₂) 0 0
Tactic: erw [assoc, comp_distTriang_mor_zero₁₂ _ (inv_rot_of_distTriang _ hT), comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (hypothesis)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
⊢ IsIso φ.hom₂
have this : Mono φ.hom₂
Tactic: have : Mono φ.hom₂ := by
    rw [mono_iff_cancel_zero]
    intro A f hf
    obtain ⟨g, rfl⟩ := Triangle.coyoneda_exact₂ _ hT f
      (by rw [← cancel_mono φ.hom₃, assoc, φ.comm₂, reassoc_of% hf, zero_comp, zero_comp])
    rw [assoc] at hf
    obtain ⟨h, hh⟩ := Triangle.coyoneda_exact₂ T'.invRotate (inv_rot_of_distTriang _ hT')
      (g ≫ φ.hom₁) (by dsimp; rw [assoc, ← φ.comm₁, hf])
    obtain ⟨k, rfl⟩ : ∃ (k : A ⟶ T.invRotate.obj₁), k ≫ T.invRotate.mor₁ = g := by
      refine ⟨h ≫ inv (φ.hom₃⟦(-1 : ℤ)⟧'), ?_⟩
      have eq := ((invRotate C).map φ).comm₁
      dsimp only [invRotate] at eq
      rw [← cancel_mono φ.hom₁, assoc, assoc, eq, IsIso.inv_hom_id_assoc, hh]
    erw [assoc, comp_distTriang_mor_zero₁₂ _ (inv_rot_of_distTriang _ hT), comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
⊢ IsIso φ.hom₂
have refine_1 : ∀ (A : C), Function.Injective (β := A ⟶ T'.obj₂) fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂
Tactic: refine isIso_of_yoneda_map_bijective _ (fun A => ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
refine_1 : ∀ (A : C), Function.Injective (β := A ⟶ T'.obj₂) fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂
⊢ IsIso φ.hom₂
have refine_2 : ∀ (A : C), Function.Surjective (β := A ⟶ T'.obj₂) fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂
Tactic: refine isIso_of_yoneda_map_bijective _ (fun A => ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
⊢ ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂
have refine_2 : ∀ (x₃ : A ⟶ T.obj₃) (hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂), ∃ (a : A ⟶ T.obj₂), (fun (x : A ⟶ T.obj₂) ↦ x ≫ φ.hom₂) a = y₂
Tactic: obtain ⟨x₃, hx₃⟩ : ∃ (x₃ : A ⟶ T.obj₃), x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂ :=
      ⟨y₂ ≫ T'.mor₂ ≫ inv φ.hom₃, by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{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)
hC : Pretriangulated.{v, u} C
T T' : Triangle.{v, u} C
φ : T ⟶ T'
hT : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T
hT' : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T'
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
⊢ x₃ ≫ T.mor₃ = 0
have rw : (x₃ ≫ T.mor₃) ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁ = 0 ≫ Functor.map (shiftFunctor C (A := ℤ) 1) φ.hom₁
Tactic: rw [← cancel_mono (φ.hom₁⟦(1 : ℤ)⟧'), assoc, zero_comp, φ.comm₃, reassoc_of% hx₃,
        comp_distTriang_mor_zero₂₃ _ hT', comp_zero]