awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun (x_1 : PUnit.{(max u v) + 1}) ↦ ⊤
h₂ :
  ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x),
    Eq (α := G.obj x) ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ : G.obj x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) y₁ : G.obj x) →
      x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x),
    Eq (α := Sieve.{v, u} (Opposite.unop x))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app x) : (a : G.obj x) → Sieve (Opposite.unop x)) x₂ :
          Sieve.{v, u} (Opposite.unop x))
        (⊤ : Sieve.{v, u} (Opposite.unop x)) →
      ∃ (x₁ : F.obj x), (ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
⊢ Sieve.pullback f ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X) : (a : G.obj X) → Sieve (Opposite.unop X)) x) =
      ⊤ ↔
    ∃ (a : F.obj (Opposite.op Y)),
      Eq (α := G.obj (Opposite.op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x :
          G.obj (Opposite.op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
              (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
            a :
          G.obj (Opposite.op Y))
have this : Eq (α := Functor.obj (Functor.sieves C) (Opposite.op Y))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.sieves C) f.op) :
        (a : (Functor.sieves C).obj (Opposite.op (Opposite.unop X))) → (Functor.sieves C).obj (Opposite.op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X) :
          (a : (fun (X : Type (max u v)) ↦ X) (G.obj X)) → (fun (X : Type (max u v)) ↦ X) ((Functor.sieves C).obj X))
        x) :
    Functor.obj (Functor.sieves C) (Opposite.op Y))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾fun (S : Sieve.{v, u} (Opposite.unop (Opposite.op (Opposite.unop X)))) ↦ Sieve.pullback f.op.unop S) :
        (a : (Functor.sieves C).obj (Opposite.op (Opposite.unop X))) → (Functor.sieves C).obj (Opposite.op Y))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X) :
          (a : (fun (X : Type (max u v)) ↦ X) (G.obj X)) → (fun (X : Type (max u v)) ↦ X) ((Functor.sieves C).obj X))
        x) :
    Functor.obj (Functor.sieves C) (Opposite.op Y))
Tactic: have := ConcreteCategory.congr_hom (Functor.sieves_map C (f.op)) (χ'.app X x)
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun (x_1 : PUnit.{(max u v) + 1}) ↦ ⊤
h₂ :
  ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x),
    Eq (α := G.obj x) ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ : G.obj x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) y₁ : G.obj x) →
      x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x),
    Eq (α := Sieve.{v, u} (Opposite.unop x))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app x) : (a : G.obj x) → Sieve (Opposite.unop x)) x₂ :
          Sieve.{v, u} (Opposite.unop x))
        (⊤ : Sieve.{v, u} (Opposite.unop x)) →
      ∃ (x₁ : F.obj x), (ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
this :
  Eq (α := Functor.obj (Functor.sieves C) (Opposite.op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.sieves C) f.op) :
          (a : (Functor.sieves C).obj (Opposite.op (Opposite.unop X))) → (Functor.sieves C).obj (Opposite.op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X) :
            (a : (fun (X : Type (max u v)) ↦ X) (G.obj X)) → (fun (X : Type (max u v)) ↦ X) ((Functor.sieves C).obj X))
          x) :
      Functor.obj (Functor.sieves C) (Opposite.op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾fun (S : Sieve.{v, u} (Opposite.unop (Opposite.op (Opposite.unop X)))) ↦ Sieve.pullback f.op.unop S) :
          (a : (Functor.sieves C).obj (Opposite.op (Opposite.unop X))) → (Functor.sieves C).obj (Opposite.op Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X) :
            (a : (fun (X : Type (max u v)) ↦ X) (G.obj X)) → (fun (X : Type (max u v)) ↦ X) ((Functor.sieves C).obj X))
          x) :
      Functor.obj (Functor.sieves C) (Opposite.op Y))
a : F.obj (Opposite.op Y)
h :
  Eq (α := G.obj (Opposite.op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x :
      G.obj (Opposite.op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
          (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
        a :
      G.obj (Opposite.op Y))
⊢ Eq (α := Sieve.{v, u} Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app (Opposite.op Y)) : (a : G.obj (Opposite.op Y)) → Sieve Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x) :
      Sieve.{v, u} Y)
    (⊤ : Sieve.{v, u} Y)
have w : Eq (α := Sieve.{v, u} Y)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app (Opposite.op Y)) : (a : G.obj (Opposite.op Y)) → Sieve Y)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
          (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
        a) :
    Sieve.{v, u} Y)
  (⊤ : Sieve.{v, u} Y)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst_1 : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X) :
        (a : (fun (X : Type (max u v)) ↦ X) (G.obj X)) → (fun (X : Type (max u v)) ↦ X) ((Functor.sieves C).obj X))
      x)
    f
⊢ Sieve.arrows
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X) :
        (a : (fun (X : Type (max u v)) ↦ X) (G.obj X)) → (fun (X : Type (max u v)) ↦ X) ((Functor.sieves C).obj X))
      x)
    f
have simp : Sieve.arrows
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾fun (x : G.obj X) ↦
          {
            arrows := fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
              ∃ (a : F.obj (Opposite.op Y)),
                Eq (α := G.obj (Opposite.op Y))
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x :
                    G.obj (Opposite.op Y))
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                        (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
                      a :
                    G.obj (Opposite.op Y)),
            downward_closed := sorry : Sieve.{v, u} (Opposite.unop X) }) :
      (a : G.obj X) → (Functor.sieves C).obj X)
    x)
  f
Tactic: simp only [Presheaf.χ_app, Opposite.op_unop] at hf ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : GrothendieckTopology.{v, u} C
F G : Sheaf J_1 (Type (max u v))
J : GrothendieckTopology.{v, u} C
⊢ Presheaf.IsSheaf J (closedSieves J).toFunctor
have rw : Presieve.IsSheaf J (closedSieves J).toFunctor
Tactic: rw [CategoryTheory.isSheaf_iff_isSheaf_of_type]
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
X : Cᵒᵖ
⊢ (Subfunctor.range (Presheaf.χ m.hom)).obj X ≤ (closedSieves J).obj X
have simp : ∀ (y : G.obj (P := Presheaf.IsSheaf J).obj X),
  J.IsClosed (X := Opposite.unop X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Presheaf.χ m.hom).app X) : (a : G.obj.obj X) → Sieve (Opposite.unop X))
      y)
Tactic: simp only [sieves_obj, Subfunctor.range_obj, closedSieves_obj, Set.le_iff_subset,
      Set.range_subset_iff, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
⊢ IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) (χ m) (truth J)
have e : m ≫ χ m = (isTerminalTerminal J Types.isTerminalPUnit).from F ≫ truth J
Tactic: apply IsPullback.of_map (sheafToPresheaf J _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
e : m ≫ χ m = (isTerminalTerminal J Types.isTerminalPUnit).from F ≫ truth J
⊢ IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) (χ m) (truth J)
have H : IsPullback (P := obj (sheafToPresheaf J (Type (max u v))) F) (map (sheafToPresheaf J (Type (max u v))) m)
  (map (sheafToPresheaf J (Type (max u v))) ((isTerminalTerminal J Types.isTerminalPUnit).from F))
  (map (sheafToPresheaf J (Type (max u v))) (χ m)) (map (sheafToPresheaf J (Type (max u v))) (truth J))
Tactic: apply IsPullback.of_map (sheafToPresheaf J _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
⊢ m ≫ χ m = (isTerminalTerminal J Types.isTerminalPUnit).from F ≫ truth J
have e : (m ≫ χ m).hom = ((isTerminalTerminal J Types.isTerminalPUnit).from F ≫ truth J).hom
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
⊢ (m ≫ χ m).hom = ((isTerminalTerminal J Types.isTerminalPUnit).from F ≫ truth J).hom
have e : m.hom ≫ Presheaf.χ m.hom = ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom ≫ Presheaf.truth C
Tactic: simp only [Ω_obj, ObjectProperty.FullSubcategory.comp_hom, χ_hom, terminal_obj, truth_hom,
      ← cancel_mono (closedSieves J).ι, Category.assoc, Subfunctor.lift_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
⊢ IsPullback (P := obj (sheafToPresheaf J (Type (max u v))) F) (map (sheafToPresheaf J (Type (max u v))) m)
    (map (sheafToPresheaf J (Type (max u v))) ((isTerminalTerminal J Types.isTerminalPUnit).from F))
    (map (sheafToPresheaf J (Type (max u v))) (χ m)) (map (sheafToPresheaf J (Type (max u v))) (truth J))
have H : IsPullback m.hom ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom (Subfunctor.lift (Presheaf.χ m.hom) sorry)
  (Subfunctor.lift (Presheaf.truth C) sorry)
Tactic: simp only [ObjectProperty.ι_obj, terminal_obj, Ω_obj, ObjectProperty.ι_map, χ_hom, truth_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
⊢ IsPullback m.hom ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom (Subfunctor.lift (Presheaf.χ m.hom) ⋯)
    (Subfunctor.lift (Presheaf.truth C) ⋯)
have apply : IsPullback (m.hom ≫ 𝟙 (G.obj (P := Presheaf.IsSheaf J))) ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom
  (Presheaf.χ m.hom) (Subfunctor.lift (Presheaf.truth C) sorry ≫ (closedSieves J).ι)
Tactic: apply IsPullback.of_right _
      ((cancel_mono ((closedSieves J).ι)).mp (by simpa using Presheaf.comp_χ_eq _))
      (.of_horiz_isIso_mono ⟨_⟩ : IsPullback (𝟙 _) _ (Presheaf.χ m.hom) (closedSieves J).ι)
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
apply :
  IsPullback (m.hom ≫ 𝟙 (G.obj (P := Presheaf.IsSheaf J))) ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom
    (Presheaf.χ m.hom) (Subfunctor.lift (Presheaf.truth C) ⋯ ≫ (closedSieves J).ι)
⊢ IsPullback m.hom ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom (Subfunctor.lift (Presheaf.χ m.hom) ⋯)
    (Subfunctor.lift (Presheaf.truth C) ⋯)
have apply₁ : 𝟙 (G.obj (P := Presheaf.IsSheaf J)) ≫ Presheaf.χ m.hom = Subfunctor.lift (Presheaf.χ m.hom) sorry ≫ (closedSieves J).ι
Tactic: apply IsPullback.of_right _
      ((cancel_mono ((closedSieves J).ι)).mp (by simpa using Presheaf.comp_χ_eq _))
      (.of_horiz_isIso_mono ⟨_⟩ : IsPullback (𝟙 _) _ (Presheaf.χ m.hom) (closedSieves J).ι)
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
⊢ IsPullback (m.hom ≫ 𝟙 (G.obj (P := Presheaf.IsSheaf J))) ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom
    (Presheaf.χ m.hom) (Subfunctor.lift (Presheaf.truth C) ⋯ ≫ (closedSieves J).ι)
have simp : IsPullback m.hom ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom (Presheaf.χ m.hom)
  (Subfunctor.lift (Presheaf.truth C) sorry ≫ (closedSieves J).ι)
Tactic: simp only [Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
⊢ χ' = χ m
have h : χ'.hom = (χ m).hom
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
⊢ χ'.hom = (χ m).hom
have h : χ'.hom ≫ (closedSieves J).ι = Presheaf.χ m.hom
Tactic: rw [← cancel_mono (closedSieves J).ι, χ_hom, Subfunctor.lift_ι]
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
⊢ χ'.hom ≫ (closedSieves J).ι = Presheaf.χ m.hom
have h : IsPullback m.hom (IsTerminal.from (isTerminalConst Cᵒᵖ Types.isTerminalPUnit) (F.obj (P := Presheaf.IsSheaf J)))
  (χ'.hom ≫ (closedSieves J).ι) (Presheaf.truth C)
Tactic: apply Presheaf.χ_unique _
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
⊢ IsPullback m.hom (IsTerminal.from (isTerminalConst Cᵒᵖ Types.isTerminalPUnit) (F.obj (P := Presheaf.IsSheaf J)))
    (χ'.hom ≫ (closedSieves J).ι) (Presheaf.truth C)
have pb : IsPullback (𝟙 (G.obj (P := Presheaf.IsSheaf J))) χ'.hom (χ'.hom ≫ (closedSieves J).ι) (closedSieves J).ι
Tactic: have pb : IsPullback (𝟙 G.obj) χ'.hom (χ'.hom ≫ (closedSieves J).ι)
    (closedSieves J).ι := IsPullback.of_horiz_isIso_mono (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Topos.Sheaf (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
pb : IsPullback (𝟙 (G.obj (P := Presheaf.IsSheaf J))) χ'.hom (χ'.hom ≫ (closedSieves J).ι) (closedSieves J).ι
⊢ IsPullback m.hom (IsTerminal.from (isTerminalConst Cᵒᵖ Types.isTerminalPUnit) (F.obj (P := Presheaf.IsSheaf J)))
    (χ'.hom ≫ (closedSieves J).ι) (Presheaf.truth C)
have this : IsPullback m.hom (IsTerminal.from (isTerminalConst Cᵒᵖ Types.isTerminalPUnit) (F.obj (P := Presheaf.IsSheaf J))) χ'.hom
  (truth J).hom
Tactic: have : IsPullback m.hom ?_ χ'.hom <| (truth J).hom := by
    simpa using hχ'.map (sheafToPresheaf J _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Adjunction (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
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
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Functor.obj G.mapTriangle T)
have this : G.Additive
Tactic: have : G.Additive := adj.right_adjoint_additive
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Adjunction (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
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 : G.Additive
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Functor.obj G.mapTriangle T)
have obtain : ∀ (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)),
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Functor.obj G.mapTriangle T)
Tactic: obtain ⟨Z, f, g, mem⟩ := distinguished_cocone_triangle (G.map T.mor₁)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Adjunction (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
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 : 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)
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Functor.obj G.mapTriangle T)
have obtain : ∀ (h : Triangle.obj₃ (Functor.obj F.mapTriangle (Triangle.mk (G.map T.mor₁) f g)) ⟶ T.obj₃)
  (h₁ : Triangle.mor₂ (Functor.obj F.mapTriangle (Triangle.mk (G.map T.mor₁) f g)) ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂)
  (h₂ :
    Triangle.mor₃ (Functor.obj F.mapTriangle (Triangle.mk (G.map T.mor₁) f g)) ≫
        Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
      h ≫ T.mor₃),
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Functor.obj G.mapTriangle T)
Tactic: obtain ⟨h, ⟨h₁, h₂⟩⟩ := complete_distinguished_triangle_morphism _ _
      (F.map_distinguished _ mem) hT (adj.counit.app T.obj₁) (adj.counit.app T.obj₂) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Adjunction (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
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 : 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 : Triangle.obj₃ (Functor.obj F.mapTriangle (Triangle.mk (G.map T.mor₁) f g)) ⟶ T.obj₃
h₁ : Triangle.mor₂ (Functor.obj F.mapTriangle (Triangle.mk (G.map T.mor₁) f g)) ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  Triangle.mor₃ (Functor.obj F.mapTriangle (Triangle.mk (G.map T.mor₁) f g)) ≫
      Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Functor.obj G.mapTriangle T)
have dsimp : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
  (Triangle.mk (G.map T.mor₁) (G.map T.mor₂) (G.map T.mor₃ ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G 1)) T.obj₁))
Tactic: dsimp at h h₁ h₂ ⊢