awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Biproducts (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
⊢ Eq (α := P.complement ⟶ P ⊞ P.complement) ((P.complement.decompId_i ≫ P.decompId_p) ≫ biprod.inl) 0
have h₁ : P.complement.decompId_i ≫ P.decompId_p = 0
Tactic: refine (?_ =≫ _).trans zero_comp
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Biproducts (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
⊢ P.complement.decompId_i ≫ P.decompId_p = 0
have h₁ : (P.complement.decompId_i ≫ P.decompId_p).f = Hom.f 0
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Idempotents.Biproducts (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
P : Karoubi.{v, u_1} C
⊢ CategoryStruct.comp (Y := P ⊞ P.complement) (biprod.lift P.decompId_p P.complement.decompId_p)
      (biprod.desc P.decompId_i P.complement.decompId_i) =
    𝟙 (Functor.obj (toKaroubi C) P.X)
have h : (CategoryStruct.comp (Y := P ⊞ P.complement) (biprod.lift P.decompId_p P.complement.decompId_p)
      (biprod.desc P.decompId_i P.complement.decompId_i)).f =
  Hom.f (𝟙 (Functor.obj (toKaroubi C) P.X))
Tactic: 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
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
⊢ IsIdempotentComplete (Functor.{v_1, v_2, u_1, u_2} J C)
have refine : ∀ (F : Functor.{v_1, v_2, u_1, u_2} J C) (p : F ⟶ F) (hp : p ≫ p = p),
  ∃ (Y : Functor.{v_1, v_2, u_1, u_2} J C) (i : Y ⟶ F) (e : F ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
Tactic: refine ⟨fun F p hp => ?_⟩
-- 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 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
⊢ ∃ (Y : Functor.{v_1, v_2, u_1, u_2} J C) (i : Y ⟶ F) (e : F ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
have hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
Tactic: have hC := (isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent C).mp inferInstance
-- 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 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
⊢ ∃ (Y : Functor.{v_1, v_2, u_1, u_2} J C) (i : Y ⟶ F) (e : F ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
have this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
Tactic: haveI : ∀ j : J, HasEqualizer (𝟙 _) (p.app j) := fun j => hC _ _ (congr_app hp 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
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)
j j' : J
φ : j ⟶ j'
⊢ Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j')
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ 𝟙 (F.obj j'))
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j')
have rw : Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
  ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j')
Tactic: rw [comp_id, assoc, p.naturality φ, ← assoc, ← Limits.equalizer.condition, comp_id]
-- 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)
j j' : J
φ : j ⟶ j'
rw :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j')
⊢ Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j')
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ 𝟙 (F.obj j'))
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j')
have rw₁ : Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
  (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ ≫ p.app j')
Tactic: rw [comp_id, assoc, p.naturality φ, ← assoc, ← Limits.equalizer.condition, comp_id]
-- 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)
j j' : J
φ : j ⟶ j'
rw :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j')
rw₁ :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ ≫ p.app j')
⊢ Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j')
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ 𝟙 (F.obj j'))
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j')
have rw₂ : Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
  (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ p.app j ≫ F.map φ)
Tactic: rw [comp_id, assoc, p.naturality φ, ← assoc, ← Limits.equalizer.condition, comp_id]
-- 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)
j j' : J
φ : j ⟶ j'
rw :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j')
rw₁ :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ ≫ p.app j')
rw₂ :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ p.app j ≫ F.map φ)
⊢ Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j')
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ 𝟙 (F.obj j'))
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j')
have rw₃ : Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
  ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ p.app j) ≫ F.map φ)
Tactic: rw [comp_id, assoc, p.naturality φ, ← assoc, ← Limits.equalizer.condition, comp_id]
-- 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)
j j' : J
φ : j ⟶ j'
rw :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j')
rw₁ :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ ≫ p.app j')
rw₂ :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ p.app j ≫ F.map φ)
rw₃ :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ p.app j) ≫ F.map φ)
⊢ Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j')
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ 𝟙 (F.obj j'))
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j')
have rw₄ : Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
  ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ 𝟙 (F.obj j)) ≫ F.map φ)
Tactic: rw [comp_id, assoc, p.naturality φ, ← assoc, ← Limits.equalizer.condition, comp_id]
-- 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)
j j' : J
φ : j ⟶ j'
rw :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j')
rw₁ :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ ≫ p.app j')
rw₂ :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ p.app j ≫ F.map φ)
rw₃ :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ p.app j) ≫ F.map φ)
rw₄ :
  Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ 𝟙 (F.obj j)) ≫ F.map φ)
⊢ Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j')
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ 𝟙 (F.obj j'))
    ((equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j')
have rw₅ : Eq (α := equalizer (𝟙 (F.obj j)) (p.app j) ⟶ F.obj j') (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
  (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ)
Tactic: rw [comp_id, assoc, p.naturality φ, ← assoc, ← Limits.equalizer.condition, comp_id]
-- 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 := ⋯ }
x x_1 : J
x_2 : x ⟶ x_1
⊢ Y.map x_2 ≫ equalizer.ι (𝟙 (F.obj x_1)) (p.app x_1) = equalizer.ι (𝟙 (F.obj x)) (p.app x) ≫ F.map x_2
have rw : Eq (α := Y.obj x ⟶ F.obj x_1) (equalizer.ι (𝟙 (F.obj x)) (p.app x) ≫ F.map x_2)
  (equalizer.ι (𝟙 (F.obj x)) (p.app x) ≫ F.map x_2)
Tactic: rw [equalizer.lift_ι]
-- 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 := ⋯ }
⊢ ∃ (Y : Functor.{v_1, v_2, u_1, u_2} J C) (i : Y ⟶ F) (e : F ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
have h : i ≫ e = 𝟙 Y ∧ e ≫ i = p
Tactic: use Y, i, e
-- 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 := ⋯ }
⊢ i ≫ e = 𝟙 Y ∧ e ≫ i = p
have h : i ≫ e = 𝟙 Y
Tactic: constructor
-- 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 := ⋯ }
h : i ≫ e = 𝟙 Y
⊢ i ≫ e = 𝟙 Y ∧ e ≫ i = p
have h₁ : e ≫ i = p
Tactic: constructor
-- 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 := ⋯ }
⊢ i ≫ e = 𝟙 Y
have h : ∀ (j : J),
  (i ≫ e).app j ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = NatTrans.app (𝟙 Y) j ≫ equalizer.ι (𝟙 (F.obj 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 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 := ⋯ }
j : J
⊢ (i ≫ e).app j ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = NatTrans.app (𝟙 Y) j ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
have h : (i.app j ≫ e.app j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
Tactic: dsimp
-- 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 := ⋯ }
j : J
⊢ (i.app j ≫ e.app j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
have h : i.app j ≫ e.app j ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
Tactic: rw [assoc, equalizer.lift_ι, ← equalizer.condition, id_comp, comp_id]
-- 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 := ⋯ }
j : J
h : i.app j ≫ e.app j ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
⊢ (i.app j ≫ e.app j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
have h₁ : i.app j ≫ p.app j = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
Tactic: rw [assoc, equalizer.lift_ι, ← equalizer.condition, id_comp, comp_id]
-- 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 := ⋯ }
j : J
h : i.app j ≫ e.app j ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
h₁ : i.app j ≫ p.app j = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
⊢ (i.app j ≫ e.app j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
have h₂ : equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ 𝟙 (F.obj j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
Tactic: rw [assoc, equalizer.lift_ι, ← equalizer.condition, id_comp, comp_id]
-- 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 := ⋯ }
j : J
h : i.app j ≫ e.app j ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
h₁ : i.app j ≫ p.app j = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
h₂ : equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ 𝟙 (F.obj j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
⊢ (i.app j ≫ e.app j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
have h₃ : Eq (α := Y.obj j ⟶ F.obj j) (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ 𝟙 (F.obj j)) (equalizer.ι (𝟙 (F.obj j)) (p.app j))
Tactic: rw [assoc, equalizer.lift_ι, ← equalizer.condition, id_comp, comp_id]
-- 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 := ⋯ }
j : J
h : i.app j ≫ e.app j ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
h₁ : i.app j ≫ p.app j = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
h₂ : equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ 𝟙 (F.obj j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
h₃ :
  Eq (α := Y.obj j ⟶ F.obj j) (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ 𝟙 (F.obj j)) (equalizer.ι (𝟙 (F.obj j)) (p.app j))
⊢ (i.app j ≫ e.app j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j) = 𝟙 (Y.obj j) ≫ equalizer.ι (𝟙 (F.obj j)) (p.app j)
have h₄ : Eq (α := Y.obj j ⟶ F.obj j) (equalizer.ι (𝟙 (F.obj j)) (p.app j)) (equalizer.ι (𝟙 (F.obj j)) (p.app j))
Tactic: rw [assoc, equalizer.lift_ι, ← equalizer.condition, id_comp, comp_id]