awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : P ⟶ Q
X : J
inst_2 : IsIdempotentComplete.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} J C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Y : Functor.{v_1, v_2, u_1, u_2} J C :=
  { obj := fun (j : J) ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j' : J} (φ : j ⟶ j') ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯,
    map_comp := ⋯ }
i : Y ⟶ F := { app := fun (j : J) ↦ equalizer.ι (𝟙 (F.obj j)) (p.app j), naturality := ⋯ }
e : F ⟶ Y := { app := fun (j : J) ↦ equalizer.lift (p.app j) ⋯, naturality := ⋯ }
⊢ e ≫ i = p
have h : ∀ (j : J), (e ≫ i).app j = p.app j
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P_1 Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : P_1 ⟶ Q
X : J
P : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
j j' : J
φ : j ⟶ j'
⊢ { X := P.X.obj j, p := P.p.app j, idem := ⋯ : Karoubi.{v_2, u_2} C }.p ≫
      (P.p.app j ≫ P.X.map φ) ≫ { X := P.X.obj j', p := P.p.app j', idem := ⋯ : Karoubi.{v_2, u_2} C }.p =
    P.p.app j ≫ P.X.map φ
have simp : P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ
Tactic: simp only [NatTrans.naturality, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (hypothesis)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P_1 Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : P_1 ⟶ Q
X : J
P : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
j j' : J
φ : j ⟶ j'
⊢ P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ
have h : (P.p ≫ P.p).app j = P.p.app j
Tactic: have h := congr_app P.idem j
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (hypothesis)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P_1 Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : P_1 ⟶ Q
X : J
P : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
j j' : J
φ : j ⟶ j'
h : (P.p ≫ P.p).app j = P.p.app j
⊢ P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ
have h₁ : P.p.app j ≫ P.p.app j = P.p.app j
Tactic: rw [NatTrans.comp_app] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P_1 Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : P_1 ⟶ Q
X : J
P : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
j j' : J
φ : j ⟶ j'
h : P.p.app j ≫ P.p.app j = P.p.app j
⊢ P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ
have rw : P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ
Tactic: rw [reassoc_of% h, reassoc_of% h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P_1 Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : P_1 ⟶ Q
X : J
P : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
j j' : J
φ : j ⟶ j'
h : P.p.app j ≫ P.p.app j = P.p.app j
rw : P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ
⊢ P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ
have rw₁ : P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ
Tactic: rw [reassoc_of% h, reassoc_of% h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P_1 Q_1 : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f_1 : P_1 ⟶ Q_1
X : J
P Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : Functor.obj (karoubiFunctorCategoryEmbedding J C) P ⟶ Functor.obj (karoubiFunctorCategoryEmbedding J C) Q
j j' : J
φ : j ⟶ j'
⊢ P.X.map φ ≫ (f.app j').f = (f.app j).f ≫ Q.X.map φ
have rw : P.X.map φ ≫ (f.app j').f = (f.app j).f ≫ ((Functor.obj (karoubiFunctorCategoryEmbedding J C) Q).obj j).p ≫ Q.X.map φ
Tactic: rw [← Karoubi.comp_p_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (hypothesis)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P_1 Q_1 : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f_1 : P_1 ⟶ Q_1
X : J
P Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : Functor.obj (karoubiFunctorCategoryEmbedding J C) P ⟶ Functor.obj (karoubiFunctorCategoryEmbedding J C) Q
j j' : J
φ : j ⟶ j'
⊢ P.X.map φ ≫ (f.app j').f = (f.app j).f ≫ ((Functor.obj (karoubiFunctorCategoryEmbedding J C) Q).obj j).p ≫ Q.X.map φ
have h : ((Functor.obj (karoubiFunctorCategoryEmbedding J C) P).map φ ≫ f.app j').f =
  (f.app j ≫ (Functor.obj (karoubiFunctorCategoryEmbedding J C) Q).map φ).f
Tactic: have h := hom_ext_iff.mp (f.naturality φ)
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P_1 Q_1 : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f_1 : P_1 ⟶ Q_1
X : J
P Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : Functor.obj (karoubiFunctorCategoryEmbedding J C) P ⟶ Functor.obj (karoubiFunctorCategoryEmbedding J C) Q
j j' : J
φ : j ⟶ j'
h : (P.p.app j ≫ P.X.map φ) ≫ (f.app j').f = (f.app j).f ≫ Q.p.app j ≫ Q.X.map φ
⊢ P.X.map φ ≫ (f.app j').f = (f.app j).f ≫ ((Functor.obj (karoubiFunctorCategoryEmbedding J C) Q).obj j).p ≫ Q.X.map φ
have simp : P.X.map φ ≫ (f.app j').f = P.p.app j ≫ P.X.map φ ≫ (f.app j').f
Tactic: simp only [assoc, h.symm, karoubiFunctorCategoryEmbedding_obj,
              KaroubiFunctorCategoryEmbedding.obj_obj_p]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P_1 Q_1 : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f_1 : P_1 ⟶ Q_1
X : J
P Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : Functor.obj (karoubiFunctorCategoryEmbedding J C) P ⟶ Functor.obj (karoubiFunctorCategoryEmbedding J C) Q
j j' : J
φ : j ⟶ j'
h : (P.p.app j ≫ P.X.map φ) ≫ (f.app j').f = (f.app j).f ≫ Q.p.app j ≫ Q.X.map φ
⊢ P.X.map φ ≫ (f.app j').f = P.p.app j ≫ P.X.map φ ≫ (f.app j').f
have rw : P.X.map φ ≫ (f.app j').f = P.X.map φ ≫ P.p.app j' ≫ (f.app j').f
Tactic: rw [← P.p.naturality_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P_1 Q_1 : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f_1 : P_1 ⟶ Q_1
X : J
P Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : Functor.obj (karoubiFunctorCategoryEmbedding J C) P ⟶ Functor.obj (karoubiFunctorCategoryEmbedding J C) Q
⊢ P.p ≫ { app := fun (j : J) ↦ (f.app j).f, naturality := ⋯ : NatTrans P.X Q.X } ≫ Q.p =
    { app := fun (j : J) ↦ (f.app j).f, naturality := ⋯ }
have w : ∀ (j : J),
  (P.p ≫ { app := fun (j : J) ↦ (f.app j).f, naturality := sorry : NatTrans P.X Q.X } ≫ Q.p).app j =
    NatTrans.app { app := fun (j : J) ↦ (f.app j).f, naturality := sorry } j
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
P Q : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
f : P ⟶ Q
X : J
X_1 Y : Karoubi (Functor.{v_1, v_2, u_1, u_2} J C)
a₁ a₂ : X_1 ⟶ Y
h :
  Eq (α := Functor.obj (karoubiFunctorCategoryEmbedding J C) X_1 ⟶ Functor.obj (karoubiFunctorCategoryEmbedding J C) Y)
    (Functor.map (karoubiFunctorCategoryEmbedding J C) a₁) (Functor.map (karoubiFunctorCategoryEmbedding J C) a₂)
⊢ a₁ = a₂
have h₁ : ∀ (j : J), a₁.f.app j = a₂.f.app j
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
⊢ Eq (α := Functor.{v_1, v_2, u_1, u_2} J C ⥤ J ⥤ Karoubi.{v_2, u_2} C)
    (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C)
    (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C))
have h_map : autoParam
  (∀ (X Y : Functor.{v_1, v_2, u_1, u_2} J C) (f : X ⟶ Y),
    Eq (α :=
      Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X ⟶
        Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) Y)
      (Functor.map (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) f)
      (CategoryStruct.comp (Y :=
        Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X) (eqToHom sorry)
        (Functor.map (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) f ≫ eqToHom sorry)))
  Functor.ext._auto_1
Tactic: apply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
h_map :
  autoParam
    (∀ (X Y : Functor.{v_1, v_2, u_1, u_2} J C) (f : X ⟶ Y),
      Eq (α :=
        Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X ⟶
          Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) Y)
        (Functor.map (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) f)
        (CategoryStruct.comp (Y :=
          Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X) (eqToHom ⋯)
          (Functor.map (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) f ≫ eqToHom ⋯)))
    Functor.ext._auto_1
⊢ Eq (α := Functor.{v_1, v_2, u_1, u_2} J C ⥤ J ⥤ Karoubi.{v_2, u_2} C)
    (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C)
    (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C))
have h_obj : ∀ (X : Functor.{v_1, v_2, u_1, u_2} J C),
  Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X =
    Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X
Tactic: apply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
X Y : Functor.{v_1, v_2, u_1, u_2} J C
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X ⟶
      Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) Y)
    (Functor.map (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) f)
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X) (eqToHom ⋯)
      (Functor.map (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) f ≫ eqToHom ⋯))
have h_map : ∀ (j : J),
  Eq (α :=
    ((Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X).obj j).X ⟶
      ((Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) Y).obj j).X)
    (Hom.f
      (NatTrans.app (Functor.map (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) f)
        j))
    (Hom.f
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X) (eqToHom sorry)
          (Functor.map (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) f ≫ eqToHom sorry))
        j))
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
X : Functor.{v_1, v_2, u_1, u_2} J C
⊢ Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X =
    Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X
have h_obj : autoParam
  (∀ (X_1 Y : J) (f : X_1 ⟶ Y),
    (Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X).map f =
      eqToHom sorry ≫
        (Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X).map f ≫
          eqToHom sorry)
  Functor.ext._auto_1
Tactic: apply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
X : Functor.{v_1, v_2, u_1, u_2} J C
h_obj :
  autoParam
    (∀ (X_1 Y : J) (f : X_1 ⟶ Y),
      (Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X).map f =
        eqToHom ⋯ ≫
          (Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X).map f ≫
            eqToHom ⋯)
    Functor.ext._auto_1
⊢ Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X =
    Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X
have h_obj₁ : ∀ (X_1 : J),
  (Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X).obj X_1 =
    (Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X).obj X_1
Tactic: apply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.FunctorCategories (goal)
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
X : Functor.{v_1, v_2, u_1, u_2} J C
j j' : J
φ : j ⟶ j'
⊢ (Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X).map φ =
    eqToHom ⋯ ≫
      (Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X).map φ ≫ eqToHom ⋯
have h_obj : ((Functor.obj (toKaroubi (Functor.{v_1, v_2, u_1, u_2} J C) ⋙ karoubiFunctorCategoryEmbedding J C) X).map φ).f =
  (eqToHom sorry ≫
      (Functor.obj (Functor.obj (Functor.whiskeringRight J C (Karoubi.{v_2, u_2} C)) (toKaroubi C)) X).map φ ≫
        eqToHom sorry).f
Tactic: ext
-- 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
F G : Karoubi.{v_1, u_1} C ⥤ D
φ : F ⟶ G
P : Karoubi.{v_1, u_1} C
⊢ φ.app P = F.map P.decompId_i ≫ φ.app { X := P.X, p := 𝟙 P.X, idem := ⋯ } ≫ G.map P.decompId_p
have rw : φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P
Tactic: rw [← φ.naturality, ← assoc, ← F.map_comp]
-- 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
F G : Karoubi.{v_1, u_1} C ⥤ D
φ : F ⟶ G
P : Karoubi.{v_1, u_1} C
| φ.app P
have rw : F.map (𝟙 P) ≫ φ.app P
Tactic: rw [← id_comp (φ.app P), ← F.map_id]
-- 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
F G : Karoubi.{v_1, u_1} C ⥤ D
φ : F ⟶ G
P : Karoubi.{v_1, u_1} C
⊢ φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P
have conv_lhs : F.map (𝟙 P) ≫ φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P
Tactic: conv_lhs => rw [← id_comp (φ.app P), ← F.map_id]
-- 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
F G : Karoubi.{v_1, u_1} C ⥤ D
φ : F ⟶ G
P : Karoubi.{v_1, u_1} C
⊢ F.map (𝟙 P) ≫ φ.app P = F.map (P.decompId_i ≫ P.decompId_p) ≫ φ.app P
have e_a : 𝟙 P = P.decompId_i ≫ P.decompId_p
Tactic: congr
-- 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
P : Karoubi.{v_1, u_1} C
⊢ ((obj F).obj P).p ≫ ((F.map P.p).f ≫ Hom.f (φ.app P.X)) ≫ ((obj G).obj P).p = (F.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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
P : Karoubi.{v_1, u_1} C
h : F.map P.p ≫ φ.app P.X = φ.app P.X ≫ G.map P.p
⊢ ((obj F).obj P).p ≫ ((F.map P.p).f ≫ Hom.f (φ.app P.X)) ≫ ((obj G).obj P).p = (F.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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
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
⊢ ((obj F).obj P).p ≫ ((F.map P.p).f ≫ Hom.f (φ.app P.X)) ≫ ((obj G).obj P).p = (F.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, Karoubi.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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
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
⊢ ((obj F).obj P).p ≫ ((F.map P.p).f ≫ Hom.f (φ.app P.X)) ≫ ((obj G).obj P).p = (F.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, Karoubi.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 : C ⥤ Karoubi.{v_2, u_2} D
φ : F ⟶ G
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
⊢ ((obj F).obj P).p ≫ ((F.map P.p).f ≫ Hom.f (φ.app P.X)) ≫ ((obj G).obj P).p = (F.map P.p).f ≫ Hom.f (φ.app P.X)
have simp : (F.map P.p).f ≫ (F.map P.p).f ≫ (F.map P.p).f ≫ Hom.f (φ.app P.X) = (F.map P.p).f ≫ Hom.f (φ.app P.X)
Tactic: simp only [obj_obj_p, assoc, ← 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
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 ≫ (F.map P.p).f
have a : (F.map P.p).f
Tactic: rw [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
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 ≫ (F.map P.p).f ≫ Hom.f (φ.app P.X) = (F.map P.p).f ≫ Hom.f (φ.app P.X)
have slice_lhs : (F.map P.p).f ≫ (F.map P.p).f ≫ (F.map P.p).f ≫ Hom.f (φ.app P.X) = (F.map P.p).f ≫ Hom.f (φ.app P.X)
Tactic: slice_lhs 1 3 => rw [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
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
slice_lhs : (F.map P.p).f ≫ (F.map P.p).f ≫ (F.map P.p).f ≫ Hom.f (φ.app P.X) = (F.map P.p).f ≫ Hom.f (φ.app P.X)
⊢ (F.map P.p).f ≫ (F.map P.p).f ≫ (F.map P.p).f ≫ Hom.f (φ.app P.X) = (F.map P.p).f ≫ Hom.f (φ.app P.X)
have slice_lhs₁ : (F.map P.p).f ≫ Hom.f (φ.app P.X) = (F.map P.p).f ≫ Hom.f (φ.app P.X)
Tactic: slice_lhs 1 3 => rw [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
⊢ (obj F).map f ≫ { f := (F.map x_1.p).f ≫ Hom.f (φ.app x_1.X), comm := ⋯ : ((obj F).obj x_1).Hom ((obj G).obj x_1) } =
    { f := (F.map x.p).f ≫ Hom.f (φ.app x.X), comm := ⋯ : ((obj F).obj x).Hom ((obj G).obj x) } ≫ (obj G).map f
have h : ((obj F).map f ≫
      { f := (F.map x_1.p).f ≫ Hom.f (φ.app x_1.X), comm := sorry : ((obj F).obj x_1).Hom ((obj G).obj x_1) }).f =
  Hom.f ({ f := (F.map x.p).f ≫ Hom.f (φ.app x.X), comm := sorry : ((obj F).obj x).Hom ((obj G).obj x) } ≫ (obj G).map f)
Tactic: ext
-- 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
⊢ ((obj F).map f ≫
        { f := (F.map x_1.p).f ≫ Hom.f (φ.app x_1.X), comm := ⋯ : ((obj F).obj x_1).Hom ((obj G).obj x_1) }).f =
    Hom.f ({ f := (F.map x.p).f ≫ Hom.f (φ.app x.X), comm := ⋯ : ((obj F).obj x).Hom ((obj G).obj x) } ≫ (obj G).map 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 ≫ Hom.f (φ.app x.X)) ≫ (G.map f.f).f
Tactic: dsimp [obj]
-- 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
⊢ (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 ≫ φ.app x_1.X = φ.app x.X ≫ 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 : 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
⊢ (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 ≫ x_1.p) = F.map f.f
Tactic: have h' := F.congr_map (comp_p f)