awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this_1 : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) f g)
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (G.obj T.obj₁) ≫
        Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' :
  Eq (α := Z ⟶ (shiftFunctor D (A := ℤ) 1 ⋙ G).obj T.obj₁)
    (g ≫ NatTrans.app (Iso.inv (Functor.commShiftIso G 1)) T.obj₁)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h ≫
      G.map T.mor₃)
this :
  Mono.{v_1, u_1} (X := Z)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h :
      Z ⟶ G.obj T.obj₃)
Y : C
φ₁ φ₂ : Y ⟶ Z
hφ :
  Eq.{v_1 + 1} (α := Y ⟶ G.obj T.obj₃)
    ((fun (x : Y ⟶ Z) ↦
        (x ≫
            ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
                (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
              h :
          Y ⟶ G.obj T.obj₃))
      φ₁)
    ((fun (x : Y ⟶ Z) ↦
        (x ≫
            ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
                (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
              h :
          Y ⟶ G.obj T.obj₃))
      φ₂)
⊢ Eq (α := Y ⟶ G.obj T.obj₃)
    (φ₁ ≫
      ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h)
    (φ₂ ≫
      ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h)

Tactic:
exact hφ
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this_1 : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) f g)
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (G.obj T.obj₁) ≫
        Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' :
  Eq (α := Z ⟶ (shiftFunctor D (A := ℤ) 1 ⋙ G).obj T.obj₁)
    (g ≫ NatTrans.app (Iso.inv (Functor.commShiftIso G 1)) T.obj₁)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h ≫
      G.map T.mor₃)
this :
  Mono.{v_1, u_1} (X := Z)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h :
      Z ⟶ G.obj T.obj₃)
Y : C
φ : Y ⟶ G.obj T.obj₃
dsimp :
  Eq (α := Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₂))
    ((φ ≫ G.map T.mor₃ ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G 1)) T.obj₁) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (G.map T.mor₁))
    0
⊢ Eq (α := Y ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (Triangle.mk (G.map T.mor₁) f g).obj₂)
    ((φ ≫ G.map T.mor₃ ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G 1)) T.obj₁) ≫
      Functor.map (shiftFunctor C (A := ℤ) 1) (Triangle.mk (G.map T.mor₁) f g).mor₁)
    0

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this_1 : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) f g)
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (G.obj T.obj₁) ≫
        Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' :
  Eq (α := Z ⟶ (shiftFunctor D (A := ℤ) 1 ⋙ G).obj T.obj₁)
    (g ≫ NatTrans.app (Iso.inv (Functor.commShiftIso G 1)) T.obj₁)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h ≫
      G.map T.mor₃)
this :
  Mono.{v_1, u_1} (X := Z)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h :
      Z ⟶ G.obj T.obj₃)
Y : C
φ : Y ⟶ G.obj T.obj₃
ψ : Y ⟶ Z
hψ : φ ≫ G.map T.mor₃ ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G 1)) T.obj₁ = ψ ≫ g
⊢ ∃ (α : Y ⟶ G.obj T.obj₃),
    α =
      φ -
        ψ ≫
          ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
              (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
            h

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this_1 : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) f g)
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (G.obj T.obj₁) ≫
        Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' :
  Eq (α := Z ⟶ (shiftFunctor D (A := ℤ) 1 ⋙ G).obj T.obj₁)
    (g ≫ NatTrans.app (Iso.inv (Functor.commShiftIso G 1)) T.obj₁)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h ≫
      G.map T.mor₃)
this :
  Mono.{v_1, u_1} (X := Z)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h :
      Z ⟶ G.obj T.obj₃)
Y : C
φ : Y ⟶ G.obj T.obj₃
ψ : Y ⟶ Z
hψ : φ ≫ G.map T.mor₃ ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G 1)) T.obj₁ = ψ ≫ g
right :
  ∀ (α : Y ⟶ G.obj T.obj₃)
    (hα :
      α =
        φ -
          ψ ≫
            ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
                (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
              h),
    ∃ (a : Y ⟶ Z),
      (fun (x : Y ⟶ Z) ↦
            (x ≫
                ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
                    (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
                  h :
              Y ⟶ G.obj T.obj₃))
          a =
        φ
⊢ ∃ (a : Y ⟶ Z),
    (fun (x : Y ⟶ Z) ↦
          (x ≫
              ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
                  (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
                h :
            Y ⟶ G.obj T.obj₃))
        a =
      φ

Tactic:
obtain ⟨α, hα⟩ : ∃ α, α = φ - ψ ≫ adj.homEquiv _ _ h := ⟨_, rfl⟩

Premises used: CategoryTheory.Adjunction.homEquiv, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this_1 : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) f g)
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (G.obj T.obj₁) ≫
        Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' :
  Eq (α := Z ⟶ (shiftFunctor D (A := ℤ) 1 ⋙ G).obj T.obj₁)
    (g ≫ NatTrans.app (Iso.inv (Functor.commShiftIso G 1)) T.obj₁)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h ≫
      G.map T.mor₃)
this :
  Mono.{v_1, u_1} (X := Z)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h :
      Z ⟶ G.obj T.obj₃)
Y : C
φ : Y ⟶ G.obj T.obj₃
ψ : Y ⟶ Z
hψ : φ ≫ G.map T.mor₃ ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G 1)) T.obj₁ = ψ ≫ g
α : Y ⟶ G.obj T.obj₃
hα :
  α =
    φ -
      ψ ≫
        ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
            (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
          h
⊢ α ≫ G.map T.mor₃ = 0

Tactic:
have hα₀ : α ≫ G.map T.mor₃ = 0 := by
          rw [hα, sub_comp, ← cancel_mono ((Functor.commShiftIso G (1 : ℤ)).hom.app T.obj₁),
            assoc, sub_comp, assoc, assoc, hψ, zero_comp, sub_eq_zero,
            ← cancel_mono ((Functor.commShiftIso G (1 : ℤ)).inv.app T.obj₁), assoc,
            assoc, assoc, assoc, h₂', Iso.hom_inv_id_app, comp_id]
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this_1 : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) f g)
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (G.obj T.obj₁) ≫
        Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' :
  Eq (α := Z ⟶ (shiftFunctor D (A := ℤ) 1 ⋙ G).obj T.obj₁)
    (g ≫ NatTrans.app (Iso.inv (Functor.commShiftIso G 1)) T.obj₁)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h ≫
      G.map T.mor₃)
this :
  Mono.{v_1, u_1} (X := Z)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h :
      Z ⟶ G.obj T.obj₃)
Y : C
φ : Y ⟶ G.obj T.obj₃
ψ : Y ⟶ Z
hψ : φ ≫ G.map T.mor₃ ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G 1)) T.obj₁ = ψ ≫ g
α : Y ⟶ G.obj T.obj₃
hα :
  α =
    φ -
      ψ ≫
        ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
            (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
          h
hα₀ : α ≫ G.map T.mor₃ = 0
β : Y ⟶ Z
hβ :
  β ≫
      ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h =
    α
⊢ ∃ (a : Y ⟶ Z),
    (fun (x : Y ⟶ Z) ↦
          (x ≫
              ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
                  (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
                h :
            Y ⟶ G.obj T.obj₃))
        a =
      φ

Tactic:
⟨ψ + β, ?_⟩

Premises used: HAdd.hAdd, Exists.intro
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this_1 : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) f g)
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (G.obj T.obj₁) ≫
        Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' :
  Eq (α := Z ⟶ (shiftFunctor D (A := ℤ) 1 ⋙ G).obj T.obj₁)
    (g ≫ NatTrans.app (Iso.inv (Functor.commShiftIso G 1)) T.obj₁)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h ≫
      G.map T.mor₃)
this :
  Mono.{v_1, u_1} (X := Z)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h :
      Z ⟶ G.obj T.obj₃)
Y : C
φ : Y ⟶ G.obj T.obj₃
ψ : Y ⟶ Z
hψ : φ ≫ G.map T.mor₃ ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G 1)) T.obj₁ = ψ ≫ g
α : Y ⟶ G.obj T.obj₃
hα :
  α =
    φ -
      ψ ≫
        ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
            (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
          h
hα₀ : α ≫ G.map T.mor₃ = 0
β : Y ⟶ Z
hβ :
  β ≫
      ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h =
    α
refine :
  (fun (x : Y ⟶ Z) ↦
        (x ≫
            ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
                (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
              h :
          Y ⟶ G.obj T.obj₃))
      (ψ + β) =
    φ
⊢ ∃ (a : Y ⟶ Z),
    (fun (x : Y ⟶ Z) ↦
          (x ≫
              ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
                  (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
                h :
            Y ⟶ G.obj T.obj₃))
        a =
      φ

Tactic:
refine ⟨ψ + β, ?_⟩
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this_1 : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) f g)
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso F 1)) (G.obj T.obj₁) ≫
        Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' :
  Eq (α := Z ⟶ (shiftFunctor D (A := ℤ) 1 ⋙ G).obj T.obj₁)
    (g ≫ NatTrans.app (Iso.inv (Functor.commShiftIso G 1)) T.obj₁)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h ≫
      G.map T.mor₃)
this :
  Mono.{v_1, u_1} (X := Z)
    (((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
          (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
        h :
      Z ⟶ G.obj T.obj₃)
Y : C
φ : Y ⟶ G.obj T.obj₃
ψ : Y ⟶ Z
hψ : φ ≫ G.map T.mor₃ ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G 1)) T.obj₁ = ψ ≫ g
α : Y ⟶ G.obj T.obj₃
hα :
  α =
    φ -
      ψ ≫
        ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
            (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
          h
hα₀ : α ≫ G.map T.mor₃ = 0
right :
  ∃ (β : Y ⟶ Z),
    β ≫
        ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
            (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
          h =
      α
⊢ ∃ (a : Y ⟶ Z),
    (fun (x : Y ⟶ Z) ↦
          (x ≫
              ((adj.homEquiv Z T.obj₃ : Equiv.{v_2 + 1, v_1 + 1} (F.obj Z ⟶ T.obj₃) (Z ⟶ G.obj T.obj₃)) :
                  (a : F.obj Z ⟶ T.obj₃) → Z ⟶ G.obj T.obj₃)
                h :
            Y ⟶ G.obj T.obj₃))
        a =
      φ

Tactic:
suffices ∃ (β : Y ⟶ Z), β ≫ adj.homEquiv _ _ h = α by
          obtain ⟨β, hβ⟩ := this
          refine ⟨ψ + β, ?_⟩
          dsimp
          rw [add_comp, hβ, hα, add_sub_cancel]