awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
x x_1 : Karoubi.{v_1, u_1} C
f : x ⟶ x_1
h : F.map f.f ≫ φ.app x_1.X = φ.app x.X ≫ G.map f.f
h' : F.map (f.f ≫ x_1.p) = F.map f.f
⊢ (F.map f.f).f ≫ (F.map x_1.p).f ≫ Hom.f (φ.app x_1.X) = ((F.map x.p).f ≫ Hom.f (φ.app x.X)) ≫ (G.map f.f).f
have h'' : F.map (x.p ≫ f.f) = F.map f.f
Tactic: have h'' := F.congr_map (p_comp 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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
x x_1 : Karoubi.{v_1, u_1} C
f : x ⟶ x_1
h : F.map f.f ≫ φ.app x_1.X = φ.app x.X ≫ G.map f.f
h' : F.map (f.f ≫ x_1.p) = F.map f.f
h'' : F.map (x.p ≫ f.f) = F.map f.f
⊢ (F.map f.f).f ≫ (F.map x_1.p).f ≫ Hom.f (φ.app x_1.X) = ((F.map x.p).f ≫ Hom.f (φ.app x.X)) ≫ (G.map f.f).f
have h₁ : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = Hom.f (φ.app x.X) ≫ (G.map f.f).f
Tactic: simp only [hom_ext_iff, Functor.map_comp, comp_f] at h h' h'' ⊢
Cleared hypotheses: h, h', h''
-- 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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
x x_1 : Karoubi.{v_1, u_1} C
f : x ⟶ x_1
h : F.map f.f ≫ φ.app x_1.X = φ.app x.X ≫ G.map f.f
h' : F.map (f.f ≫ x_1.p) = F.map f.f
h'' : F.map (x.p ≫ f.f) = F.map f.f
h₁ : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = Hom.f (φ.app x.X) ≫ (G.map f.f).f
⊢ (F.map f.f).f ≫ (F.map x_1.p).f ≫ Hom.f (φ.app x_1.X) = ((F.map x.p).f ≫ Hom.f (φ.app x.X)) ≫ (G.map f.f).f
have h'₁ : (F.map f.f).f ≫ (F.map x_1.p).f = (F.map f.f).f
Tactic: simp only [hom_ext_iff, Functor.map_comp, comp_f] at h h' h'' ⊢
Cleared hypotheses: h, h', h''
-- 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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
x x_1 : Karoubi.{v_1, u_1} C
f : x ⟶ x_1
h : F.map f.f ≫ φ.app x_1.X = φ.app x.X ≫ G.map f.f
h' : F.map (f.f ≫ x_1.p) = F.map f.f
h'' : F.map (x.p ≫ f.f) = F.map f.f
h₁ : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = Hom.f (φ.app x.X) ≫ (G.map f.f).f
h'₁ : (F.map f.f).f ≫ (F.map x_1.p).f = (F.map f.f).f
⊢ (F.map f.f).f ≫ (F.map x_1.p).f ≫ Hom.f (φ.app x_1.X) = ((F.map x.p).f ≫ Hom.f (φ.app x.X)) ≫ (G.map f.f).f
have h''₁ : (F.map x.p).f ≫ (F.map f.f).f = (F.map f.f).f
Tactic: simp only [hom_ext_iff, Functor.map_comp, comp_f] at h h' h'' ⊢
Cleared hypotheses: h, h', h''
-- 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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
x x_1 : Karoubi.{v_1, u_1} C
f : x ⟶ x_1
h : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = Hom.f (φ.app x.X) ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x_1.p).f = (F.map f.f).f
h'' : (F.map x.p).f ≫ (F.map f.f).f = (F.map f.f).f
| Hom.f (φ.app x.X) ≫ (G.map f.f).f
have a : (F.map f.f).f ≫ Hom.f (φ.app x_1.X)
Tactic: rw [← h]
-- 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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
x x_1 : Karoubi.{v_1, u_1} C
f : x ⟶ x_1
h : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = Hom.f (φ.app x.X) ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x_1.p).f = (F.map f.f).f
h'' : (F.map x.p).f ≫ (F.map f.f).f = (F.map f.f).f
⊢ (F.map f.f).f ≫ (F.map x_1.p).f ≫ Hom.f (φ.app x_1.X) = ((F.map x.p).f ≫ Hom.f (φ.app x.X)) ≫ (G.map f.f).f
have h₁ : (F.map f.f).f ≫ (F.map x_1.p).f ≫ Hom.f (φ.app x_1.X) = (F.map x.p).f ≫ (F.map f.f).f ≫ Hom.f (φ.app x_1.X)
Tactic: slice_rhs 2 3 => rw [← h]
-- 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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
x x_1 : Karoubi.{v_1, u_1} C
f : x ⟶ x_1
h : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = Hom.f (φ.app x.X) ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x_1.p).f = (F.map f.f).f
h'' : (F.map x.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map f.f).f ≫ (F.map x_1.p).f
have a : (F.map f.f).f
Tactic: rw [h']
-- 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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
x x_1 : Karoubi.{v_1, u_1} C
f : x ⟶ x_1
h : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = Hom.f (φ.app x.X) ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x_1.p).f = (F.map f.f).f
h'' : (F.map x.p).f ≫ (F.map f.f).f = (F.map f.f).f
⊢ (F.map f.f).f ≫ (F.map x_1.p).f ≫ Hom.f (φ.app x_1.X) = (F.map x.p).f ≫ (F.map f.f).f ≫ Hom.f (φ.app x_1.X)
have h₁ : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = (F.map x.p).f ≫ (F.map f.f).f ≫ Hom.f (φ.app x_1.X)
Tactic: slice_lhs 1 2 => rw [h']
-- 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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
x x_1 : Karoubi.{v_1, u_1} C
f : x ⟶ x_1
h : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = Hom.f (φ.app x.X) ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x_1.p).f = (F.map f.f).f
h'' : (F.map x.p).f ≫ (F.map f.f).f = (F.map f.f).f
| (F.map x.p).f ≫ (F.map f.f).f
have a : (F.map f.f).f
Tactic: rw [h'']
-- 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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
x x_1 : Karoubi.{v_1, u_1} C
f : x ⟶ x_1
h : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = Hom.f (φ.app x.X) ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x_1.p).f = (F.map f.f).f
h'' : (F.map x.p).f ≫ (F.map f.f).f = (F.map f.f).f
⊢ (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = (F.map x.p).f ≫ (F.map f.f).f ≫ Hom.f (φ.app x_1.X)
have slice_rhs : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = (F.map x.p).f ≫ (F.map f.f).f ≫ Hom.f (φ.app x_1.X)
Tactic: slice_rhs 1 2 => rw [h'']
-- 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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
x x_1 : Karoubi.{v_1, u_1} C
f : x ⟶ x_1
h : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = Hom.f (φ.app x.X) ≫ (G.map f.f).f
h' : (F.map f.f).f ≫ (F.map x_1.p).f = (F.map f.f).f
h'' : (F.map x.p).f ≫ (F.map f.f).f = (F.map f.f).f
slice_rhs : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = (F.map x.p).f ≫ (F.map f.f).f ≫ Hom.f (φ.app x_1.X)
⊢ (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = (F.map x.p).f ≫ (F.map f.f).f ≫ Hom.f (φ.app x_1.X)
have h₁ : (F.map f.f).f ≫ Hom.f (φ.app x_1.X) = (F.map f.f).f ≫ Hom.f (φ.app x_1.X)
Tactic: slice_rhs 1 2 => rw [h'']
-- 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
⊢ FunctorExtension₁.map (𝟙 F) = 𝟙 (FunctorExtension₁.obj F)
have w : ∀ (P : Karoubi.{v_1, u_1} C), ((FunctorExtension₁.map (𝟙 F)).app P).f = (NatTrans.app (𝟙 (FunctorExtension₁.obj F)) P).f
Tactic: ext P
-- 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 H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
⊢ FunctorExtension₁.map (φ ≫ φ') = FunctorExtension₁.map φ ≫ FunctorExtension₁.map φ'
have w : ∀ (P : Karoubi.{v_1, u_1} C),
  ((FunctorExtension₁.map (φ ≫ φ')).app P).f = ((FunctorExtension₁.map φ ≫ FunctorExtension₁.map φ').app P).f
Tactic: ext P
-- 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 H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
⊢ ((FunctorExtension₁.map (φ ≫ φ')).app P).f = ((FunctorExtension₁.map φ ≫ FunctorExtension₁.map φ').app P).f
have w : (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ Hom.f (φ'.app P.X) =
  (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ (G.map P.p).f ≫ Hom.f (φ'.app P.X)
Tactic: simp only [comp_f, FunctorExtension₁.map_app_f, NatTrans.comp_app, assoc]
-- 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 H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
⊢ (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ Hom.f (φ'.app P.X) =
    (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ (G.map P.p).f ≫ Hom.f (φ'.app P.X)
have h : F.map P.p ≫ φ.app P.X = φ.app P.X ≫ G.map P.p
Tactic: have h := φ.naturality P.p
-- 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 H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
h : F.map P.p ≫ φ.app P.X = φ.app P.X ≫ G.map P.p
⊢ (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ Hom.f (φ'.app P.X) =
    (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ (G.map P.p).f ≫ Hom.f (φ'.app P.X)
have h' : F.map (P.p ≫ P.p) = F.map P.p
Tactic: have h' := F.congr_map P.idem
-- 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 H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
h : F.map P.p ≫ φ.app P.X = φ.app P.X ≫ G.map P.p
h' : F.map (P.p ≫ P.p) = F.map P.p
⊢ (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ Hom.f (φ'.app P.X) =
    (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ (G.map P.p).f ≫ Hom.f (φ'.app P.X)
have h₁ : (F.map P.p).f ≫ Hom.f (φ.app P.X) = Hom.f (φ.app P.X) ≫ (G.map P.p).f
Tactic: simp only [hom_ext_iff, comp_f, F.map_comp] at h h'
Cleared hypotheses: h, h'
-- 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 H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
h : F.map P.p ≫ φ.app P.X = φ.app P.X ≫ G.map P.p
h' : F.map (P.p ≫ P.p) = F.map P.p
h₁ : (F.map P.p).f ≫ Hom.f (φ.app P.X) = Hom.f (φ.app P.X) ≫ (G.map P.p).f
⊢ (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ Hom.f (φ'.app P.X) =
    (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ (G.map P.p).f ≫ Hom.f (φ'.app P.X)
have h'₁ : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
Tactic: simp only [hom_ext_iff, comp_f, F.map_comp] at h h'
Cleared hypotheses: h, h'
-- 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 H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
h : (F.map P.p).f ≫ Hom.f (φ.app P.X) = Hom.f (φ.app P.X) ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| Hom.f (φ.app P.X) ≫ (G.map P.p).f
have a : (F.map P.p).f ≫ Hom.f (φ.app P.X)
Tactic: rw [← h]
-- 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 H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
h : (F.map P.p).f ≫ Hom.f (φ.app P.X) = Hom.f (φ.app P.X) ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
⊢ (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ Hom.f (φ'.app P.X) =
    (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ (G.map P.p).f ≫ Hom.f (φ'.app P.X)
have w : (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ Hom.f (φ'.app P.X) =
  (F.map P.p).f ≫ ((F.map P.p).f ≫ Hom.f (φ.app P.X)) ≫ Hom.f (φ'.app P.X)
Tactic: slice_rhs 2 3 => rw [← h]
-- 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 H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
h : (F.map P.p).f ≫ Hom.f (φ.app P.X) = Hom.f (φ.app P.X) ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
| (F.map P.p).f ≫ (F.map P.p).f
have a : (F.map P.p).f
Tactic: rw [h']
-- 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 H : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
φ' : G ⟶ H
P : Karoubi.{v_1, u_1} C
h : (F.map P.p).f ≫ Hom.f (φ.app P.X) = Hom.f (φ.app P.X) ≫ (G.map P.p).f
h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f
⊢ (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ Hom.f (φ'.app P.X) =
    (F.map P.p).f ≫ ((F.map P.p).f ≫ Hom.f (φ.app P.X)) ≫ Hom.f (φ'.app P.X)
have w : (F.map P.p).f ≫ Hom.f (φ.app P.X) ≫ Hom.f (φ'.app P.X) = ((F.map P.p).f ≫ Hom.f (φ.app P.X)) ≫ Hom.f (φ'.app P.X)
Tactic: slice_rhs 1 2 => rw [h']
-- 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
G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
⊢ CategoryStruct.comp (Y := obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G)
      { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ }
      { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ } =
    𝟙
      (obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D)
        G)
have w : ∀ (P : Karoubi.{v_1, u_1} C),
  Hom.f
      (NatTrans.app
        (CategoryStruct.comp (Y := obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G)
          { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := sorry }, naturality := sorry }
          { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := sorry }, naturality := sorry })
        P) =
    (NatTrans.app
        (𝟙
          (obj
            (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D)
            G))
        P).f
Tactic: ext P
-- 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
G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
⊢ CategoryStruct.comp (Y :=
      obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D)
        G)
      { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ }
      { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ } =
    𝟙 (obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G)
have w : ∀ (P : Karoubi.{v_1, u_1} C),
  Hom.f
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          obj
            (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D)
            G)
          { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := sorry }, naturality := sorry }
          { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := sorry }, naturality := sorry })
        P) =
    (NatTrans.app (𝟙 (obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G)) P).f
Tactic: ext P
-- 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
X Y : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
φ : X ⟶ Y
P : Karoubi.{v_1, u_1} C
⊢ Eq (α :=
    ((obj (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D)
              X).obj
          P).X ⟶
      ((obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) Y).obj P).X)
    (Hom.f
      (NatTrans.app
        (map
            (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙ functorExtension₁ C D)
            φ ≫
          Iso.hom
            ((fun (G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D) ↦
                {
                  hom :=
                    { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := ⋯ },
                      naturality := ⋯ },
                  inv :=
                    { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := ⋯ },
                      naturality := ⋯ },
                  hom_inv_id := ⋯, inv_hom_id := ⋯ :
                  obj
                      (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙
                        functorExtension₁ C D)
                      G ≅
                    obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G })
              Y))
        P))
    (Hom.f
      (NatTrans.app
        (Iso.hom
            ((fun (G : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D) ↦
                {
                  hom :=
                    { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_p).f, comm := ⋯ },
                      naturality := ⋯ },
                  inv :=
                    { app := fun (P : Karoubi.{v_1, u_1} C) ↦ { f := (G.map P.decompId_i).f, comm := ⋯ },
                      naturality := ⋯ },
                  hom_inv_id := ⋯, inv_hom_id := ⋯ :
                  obj
                      (obj (whiskeringLeft C (Karoubi.{v_1, u_1} C) (Karoubi.{v_2, u_2} D)) (toKaroubi C) ⋙
                        functorExtension₁ C D)
                      G ≅
                    obj (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) G })
              X) ≫
          map (𝟭 (Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D)) φ)
        P))
have w : (Hom.f (X.map (map (toKaroubi C) P.p)) ≫ Hom.f (φ.app (obj (toKaroubi C) P.X))) ≫ (Y.map P.decompId_p).f =
  (X.map P.decompId_p).f ≫ (φ.app P).f
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
X Y : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
φ : X ⟶ Y
P : Karoubi.{v_1, u_1} C
⊢ (Hom.f (X.map (map (toKaroubi C) P.p)) ≫ Hom.f (φ.app (obj (toKaroubi C) P.X))) ≫ (Y.map P.decompId_p).f =
    (X.map P.decompId_p).f ≫ (φ.app P).f
have w : ((X.map (P.decompId_p ≫ P.decompId_i)).f ≫ Hom.f (φ.app (obj (toKaroubi C) P.X))) ≫ (Y.map P.decompId_p).f =
  (X.map P.decompId_p).f ≫ (X.map P.decompId_i ≫ φ.app { X := P.X, p := 𝟙 P.X, idem := sorry } ≫ Y.map P.decompId_p).f
Tactic: rw [natTrans_eq φ P, P.decomp_p]
-- 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
X Y : Karoubi.{v_1, u_1} C ⥤ Karoubi.{v_2, u_2} D
φ : X ⟶ Y
P : Karoubi.{v_1, u_1} C
⊢ ((X.map (P.decompId_p ≫ P.decompId_i)).f ≫ Hom.f (φ.app (obj (toKaroubi C) P.X))) ≫ (Y.map P.decompId_p).f =
    (X.map P.decompId_p).f ≫ (X.map P.decompId_i ≫ φ.app { X := P.X, p := 𝟙 P.X, idem := ⋯ } ≫ Y.map P.decompId_p).f
have w : (X.map P.decompId_p).f ≫ (X.map P.decompId_i).f ≫ Hom.f (φ.app (obj (toKaroubi C) P.X)) ≫ (Y.map P.decompId_p).f =
  (X.map P.decompId_p).f ≫
    (X.map P.decompId_i).f ≫ Hom.f (φ.app { X := P.X, p := 𝟙 P.X, idem := sorry }) ≫ (Y.map P.decompId_p).f
Tactic: simp only [Functor.map_comp, comp_f, assoc]
-- 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
⊢ map (functorExtension₁ C D)
        (NatTrans.app (Iso.hom (Iso.symm (functorExtension₁CompWhiskeringLeftToKaroubiIso C D))) F) ≫
      NatTrans.app (Iso.hom (KaroubiUniversal₁.counitIso C D)) (obj (functorExtension₁ C D) F) =
    𝟙 (obj (functorExtension₁ C D) F)
have w : ∀ (P : Karoubi.{v_1, u_1} C),
  Hom.f
      (NatTrans.app
        (map (functorExtension₁ C D)
            (NatTrans.app (Iso.hom (Iso.symm (functorExtension₁CompWhiskeringLeftToKaroubiIso C D))) F) ≫
          NatTrans.app (Iso.hom (KaroubiUniversal₁.counitIso C D)) (obj (functorExtension₁ C D) F))
        P) =
    (NatTrans.app (𝟙 (obj (functorExtension₁ C D) F)) P).f
Tactic: ext P
-- 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
⊢ Hom.f
      (NatTrans.app
        (map (functorExtension₁ C D)
            (NatTrans.app (Iso.hom (Iso.symm (functorExtension₁CompWhiskeringLeftToKaroubiIso C D))) F) ≫
          NatTrans.app (Iso.hom (KaroubiUniversal₁.counitIso C D)) (obj (functorExtension₁ C D) F))
        P) =
    (NatTrans.app (𝟙 (obj (functorExtension₁ C D) F)) P).f
have w : ((F.map P.p).f ≫ (F.obj P.X).p) ≫ (F.map P.p).f = (F.map P.p).f
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 : C ⥤ Karoubi.{v_2, u_2} D
P : Karoubi.{v_1, u_1} C
⊢ ((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 = (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
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
⊢ ((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.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
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
⊢ ((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 ≫ P.p)).f = (F.map P.p).f
Tactic: rw [comp_p, ← comp_f, ← F.map_comp, P.idem]