awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : C ⥤ Karoubi.{v_2, u_2} D
P : Karoubi.{v_1, u_1} C
w : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
w₁ : (F.map P.p ≫ F.map P.p).f = (F.map P.p).f
w₂ : (F.map (P.p ≫ P.p)).f = (F.map P.p).f
⊢ ((F.map P.p).f ≫ (F.obj P.X).p) ≫ (F.map P.p).f = (F.map P.p).f
have w₃ : (F.map P.p).f = (F.map P.p).f
Tactic: rw [comp_p, ← comp_f, ← F.map_comp, P.idem]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : IsIdempotentComplete.{v_2, u_2} D
⊢ IsEquivalence (C := Karoubi.{v_1, u_1} C ⥤ D)
    (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C) ⋙
      obj (whiskeringRight C D (Karoubi.{v_2, u_2} D)) (toKaroubi D) ⋙
        obj (whiskeringRight C (Karoubi.{v_2, u_2} D) D) (Functor.inv (toKaroubi D)))
have change : IsEquivalence (C := Karoubi.{v_1, u_1} C ⥤ D) (Equivalence.inverse (karoubiUniversal C D))
Tactic: change (karoubiUniversal C D).inverse.IsEquivalence
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (hypothesis)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : IsIdempotentComplete.{v_2, u_2} D
⊢ IsEquivalence (C := Karoubi.{v_1, u_1} C ⥤ D) (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C))
have this : IsEquivalence (C := Karoubi.{v_1, u_1} C ⥤ D)
  (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C) ⋙
    obj (whiskeringRight C D (Karoubi.{v_2, u_2} D)) (toKaroubi D) ⋙
      obj (whiskeringRight C (Karoubi.{v_2, u_2} D) D) (Functor.inv (toKaroubi D)))
Tactic: have : ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C) ⋙
    (whiskeringRight C D (Karoubi D)).obj (toKaroubi D) ⋙
    (whiskeringRight C (Karoubi D) D).obj (Functor.inv (toKaroubi D))).IsEquivalence := by
    change (karoubiUniversal C D).inverse.IsEquivalence
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (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 : IsIdempotentComplete.{v_2, u_2} D
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi.{v_1, u_1} C
⊢ NatTrans.app (preimage (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ) P =
    F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p
have rw : F.map P.decompId_i ≫
    NatTrans.app (preimage (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ)
        { X := P.X, p := 𝟙 P.X, idem := sorry : Karoubi.{v_1, u_1} C } ≫
      G.map P.decompId_p =
  F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p
Tactic: rw [natTrans_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (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 : IsIdempotentComplete.{v_2, u_2} D
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi.{v_1, u_1} C
⊢ F.map P.decompId_i ≫
      NatTrans.app (preimage (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ)
          { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C } ≫
        G.map P.decompId_p =
    F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p
have e_a : Eq (α := F.obj { X := P.X, p := 𝟙 P.X, idem := sorry : Karoubi.{v_1, u_1} C } ⟶ G.obj { X := P.X, p := 𝟙 P.X, idem := sorry })
  (NatTrans.app (preimage (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ)
    { X := P.X, p := 𝟙 P.X, idem := sorry })
  (τ.app P.X)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (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 : IsIdempotentComplete.{v_2, u_2} D
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi.{v_1, u_1} C
⊢ Eq (α := F.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ : Karoubi.{v_1, u_1} C } ⟶ G.obj { X := P.X, p := 𝟙 P.X, idem := ⋯ })
    (NatTrans.app (preimage (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ)
      { X := P.X, p := 𝟙 P.X, idem := ⋯ })
    (τ.app P.X)
have e_a : Eq.{v_2 + 1} (α :=
  F.obj { X := P.X, p := 𝟙 P.X, idem := sorry : Karoubi.{v_1, u_1} C } ⟶ G.obj { X := P.X, p := 𝟙 P.X, idem := sorry })
  (NatTrans.app (preimage (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ)
    { X := P.X, p := 𝟙 P.X, idem := sorry })
  (NatTrans.app
    (map (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C))
      (preimage (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) τ))
    P.X)
Tactic: rw [← congr_app (((whiskeringLeft _ _ _).obj (toKaroubi _)).map_preimage τ) P.X]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (hypothesis)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
have h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.f
Tactic: have h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ (toKaroubi C).map f.f := by simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (hypothesis)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.f
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
have h₂ : (toKaroubi C ⋙ F).map f.f ≫ τ.app Y.X = τ.app X.X ≫ (toKaroubi C ⋙ G).map f.f
Tactic: have h₂ := τ.naturality f.f
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (hypothesis)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.f
h₂ : (toKaroubi C ⋙ F).map f.f ≫ τ.app Y.X = τ.app X.X ≫ (toKaroubi C ⋙ G).map f.f
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
have h₃ : X.decompId_p ≫ f = map (toKaroubi C) f.f ≫ Y.decompId_p
Tactic: have h₃ : X.decompId_p ≫ f = (toKaroubi C).map f.f ≫ Y.decompId_p := by simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.f
h₂ : F.map (map (toKaroubi C) f.f) ≫ τ.app Y.X = τ.app X.X ≫ G.map (map (toKaroubi C) f.f)
h₃ : X.decompId_p ≫ f = map (toKaroubi C) f.f ≫ Y.decompId_p
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
have rw : F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
  F.map X.decompId_i ≫ (τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
Tactic: rw [Category.assoc, Category.assoc, ← F.map_comp_assoc,
          h₁, F.map_comp_assoc, reassoc_of% h₂, ← G.map_comp, ← h₃, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.f
h₂ : F.map (map (toKaroubi C) f.f) ≫ τ.app Y.X = τ.app X.X ≫ G.map (map (toKaroubi C) f.f)
h₃ : X.decompId_p ≫ f = map (toKaroubi C) f.f ≫ Y.decompId_p
rw :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ (τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
have rw₁ : F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
Tactic: rw [Category.assoc, Category.assoc, ← F.map_comp_assoc,
          h₁, F.map_comp_assoc, reassoc_of% h₂, ← G.map_comp, ← h₃, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.f
h₂ : F.map (map (toKaroubi C) f.f) ≫ τ.app Y.X = τ.app X.X ≫ G.map (map (toKaroubi C) f.f)
h₃ : X.decompId_p ≫ f = map (toKaroubi C) f.f ≫ Y.decompId_p
rw :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ (τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
rw₁ :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
have rw₂ : F.map (f ≫ Y.decompId_i) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
Tactic: rw [Category.assoc, Category.assoc, ← F.map_comp_assoc,
          h₁, F.map_comp_assoc, reassoc_of% h₂, ← G.map_comp, ← h₃, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.f
h₂ : F.map (map (toKaroubi C) f.f) ≫ τ.app Y.X = τ.app X.X ≫ G.map (map (toKaroubi C) f.f)
h₃ : X.decompId_p ≫ f = map (toKaroubi C) f.f ≫ Y.decompId_p
rw :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ (τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
rw₁ :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₂ :
  F.map (f ≫ Y.decompId_i) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
have rw₃ : F.map (X.decompId_i ≫ map (toKaroubi C) f.f) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
Tactic: rw [Category.assoc, Category.assoc, ← F.map_comp_assoc,
          h₁, F.map_comp_assoc, reassoc_of% h₂, ← G.map_comp, ← h₃, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.f
h₂ : F.map (map (toKaroubi C) f.f) ≫ τ.app Y.X = τ.app X.X ≫ G.map (map (toKaroubi C) f.f)
h₃ : X.decompId_p ≫ f = map (toKaroubi C) f.f ≫ Y.decompId_p
rw :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ (τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
rw₁ :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₂ :
  F.map (f ≫ Y.decompId_i) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₃ :
  F.map (X.decompId_i ≫ map (toKaroubi C) f.f) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
have rw₄ : F.map X.decompId_i ≫ F.map (map (toKaroubi C) f.f) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
Tactic: rw [Category.assoc, Category.assoc, ← F.map_comp_assoc,
          h₁, F.map_comp_assoc, reassoc_of% h₂, ← G.map_comp, ← h₃, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.f
h₂ : F.map (map (toKaroubi C) f.f) ≫ τ.app Y.X = τ.app X.X ≫ G.map (map (toKaroubi C) f.f)
h₃ : X.decompId_p ≫ f = map (toKaroubi C) f.f ≫ Y.decompId_p
rw :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ (τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
rw₁ :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₂ :
  F.map (f ≫ Y.decompId_i) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₃ :
  F.map (X.decompId_i ≫ map (toKaroubi C) f.f) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₄ :
  F.map X.decompId_i ≫ F.map (map (toKaroubi C) f.f) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
have rw₅ : F.map X.decompId_i ≫ τ.app X.X ≫ G.map (map (toKaroubi C) f.f) ≫ G.map Y.decompId_p =
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
Tactic: rw [Category.assoc, Category.assoc, ← F.map_comp_assoc,
          h₁, F.map_comp_assoc, reassoc_of% h₂, ← G.map_comp, ← h₃, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.f
h₂ : F.map (map (toKaroubi C) f.f) ≫ τ.app Y.X = τ.app X.X ≫ G.map (map (toKaroubi C) f.f)
h₃ : X.decompId_p ≫ f = map (toKaroubi C) f.f ≫ Y.decompId_p
rw :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ (τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
rw₁ :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₂ :
  F.map (f ≫ Y.decompId_i) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₃ :
  F.map (X.decompId_i ≫ map (toKaroubi C) f.f) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₄ :
  F.map X.decompId_i ≫ F.map (map (toKaroubi C) f.f) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₅ :
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map (map (toKaroubi C) f.f) ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
have rw₆ : F.map X.decompId_i ≫ τ.app X.X ≫ G.map (map (toKaroubi C) f.f ≫ Y.decompId_p) =
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
Tactic: rw [Category.assoc, Category.assoc, ← F.map_comp_assoc,
          h₁, F.map_comp_assoc, reassoc_of% h₂, ← G.map_comp, ← h₃, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.f
h₂ : F.map (map (toKaroubi C) f.f) ≫ τ.app Y.X = τ.app X.X ≫ G.map (map (toKaroubi C) f.f)
h₃ : X.decompId_p ≫ f = map (toKaroubi C) f.f ≫ Y.decompId_p
rw :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ (τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
rw₁ :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₂ :
  F.map (f ≫ Y.decompId_i) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₃ :
  F.map (X.decompId_i ≫ map (toKaroubi C) f.f) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₄ :
  F.map X.decompId_i ≫ F.map (map (toKaroubi C) f.f) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₅ :
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map (map (toKaroubi C) f.f) ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₆ :
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map (map (toKaroubi C) f.f ≫ Y.decompId_p) =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
have rw₇ : F.map X.decompId_i ≫ τ.app X.X ≫ G.map (X.decompId_p ≫ f) =
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
Tactic: rw [Category.assoc, Category.assoc, ← F.map_comp_assoc,
          h₁, F.map_comp_assoc, reassoc_of% h₂, ← G.map_comp, ← h₃, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi.{v_1, u_1} C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ map (toKaroubi C) f.f
h₂ : F.map (map (toKaroubi C) f.f) ≫ τ.app Y.X = τ.app X.X ≫ G.map (map (toKaroubi C) f.f)
h₃ : X.decompId_p ≫ f = map (toKaroubi C) f.f ≫ Y.decompId_p
rw :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ (τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
rw₁ :
  F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₂ :
  F.map (f ≫ Y.decompId_i) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₃ :
  F.map (X.decompId_i ≫ map (toKaroubi C) f.f) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₄ :
  F.map X.decompId_i ≫ F.map (map (toKaroubi C) f.f) ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₅ :
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map (map (toKaroubi C) f.f) ≫ G.map Y.decompId_p =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₆ :
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map (map (toKaroubi C) f.f ≫ Y.decompId_p) =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
rw₇ :
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map (X.decompId_p ≫ f) =
    F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f
have rw₈ : F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f =
  F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p ≫ G.map f
Tactic: rw [Category.assoc, Category.assoc, ← F.map_comp_assoc,
          h₁, F.map_comp_assoc, reassoc_of% h₂, ← G.map_comp, ← h₃, G.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ :
  obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) F ⟶
    obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) G
⊢ map (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C))
      { app := fun (P : Karoubi.{v_1, u_1} C) ↦ F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p, naturality := ⋯ } =
    τ
have w : ∀ (X : C),
  NatTrans.app
      (map (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C))
        { app := fun (P : Karoubi.{v_1, u_1} C) ↦ F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p,
          naturality := sorry })
      X =
    τ.app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ :
  obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) F ⟶
    obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) G
X : C
⊢ NatTrans.app
      (map (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C))
        { app := fun (P : Karoubi.{v_1, u_1} C) ↦ F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p,
          naturality := ⋯ })
      X =
    τ.app X
have w : F.map (decompId_i (obj (toKaroubi C) X)) ≫ τ.app X ≫ G.map (decompId_p (obj (toKaroubi C) X)) = τ.app X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ :
  obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) F ⟶
    obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) G
X : C
⊢ F.map (decompId_i (obj (toKaroubi C) X)) ≫ τ.app X ≫ G.map (decompId_p (obj (toKaroubi C) X)) = τ.app X
have w : τ.app X ≫
    G.map
      (𝟙
        { X := Karoubi.X.{v_1, u_1} (obj (toKaroubi C) X), p := 𝟙 (Karoubi.X.{v_1, u_1} (obj (toKaroubi C) X)),
          idem := sorry : Karoubi.{v_1, u_1} C }) =
  τ.app X
Tactic: rw [Karoubi.decompId_i_toKaroubi, Karoubi.decompId_p_toKaroubi,
      Functor.map_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorExtension (goal)
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F G : Karoubi.{v_1, u_1} C ⥤ D
τ :
  obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) F ⟶
    obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) D) (toKaroubi C)) G
X : C
⊢ τ.app X ≫
      G.map
        (𝟙
          { X := Karoubi.X.{v_1, u_1} (obj (toKaroubi C) X), p := 𝟙 (Karoubi.X.{v_1, u_1} (obj (toKaroubi C) X)),
            idem := ⋯ : Karoubi.{v_1, u_1} C }) =
    τ.app X
have w : τ.app X ≫ G.map (𝟙 (obj (toKaroubi C) X)) = τ.app X
Tactic: change _ ≫ G.map (𝟙 _) = _