awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
P Q : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
φ : P ⟶ Q
i : ι
⊢ φ.f.f i ≫ Q.p.f i = P.p.f i ≫ φ.f.f i

Tactic:
simp only [HomologicalComplex.comp_p_d, HomologicalComplex.p_comp_d]

Premises used: CategoryTheory.Idempotents.Karoubi.HomologicalComplex.comp_p_d, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comp_d
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
w :
  ∀ (x : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) (i : ι),
    Eq (α :=
      (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) x).X.X i ⟶
        (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) x).X.X i)
      (HomologicalComplex.Hom.f
        (Hom.f
          (NatTrans.app
            (CategoryStruct.comp (Y := functor ⋙ inverse)
              {
                app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
                  { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
                naturality := ⋯ }
              {
                app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
                  { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
                naturality := ⋯ })
            x))
        i)
      (HomologicalComplex.Hom.f (Hom.f (NatTrans.app (𝟙 (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)))) x)) i)
⊢ Eq (α :=
    Quiver.Hom (V :=
      Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c) ⥤ Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))
      (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))))
    (CategoryStruct.comp (Y := functor ⋙ inverse)
      {
        app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
          { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
        naturality := ⋯ }
      {
        app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
          { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
        naturality := ⋯ })
    (𝟙 (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
x : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
i : ι
w : x.p.f i ≫ x.p.f i = x.p.f i
⊢ Eq (α :=
    (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) x).X.X i ⟶
      (CategoryTheory.Functor.obj (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))) x).X.X i)
    (HomologicalComplex.Hom.f
      (Hom.f
        (NatTrans.app
          (CategoryStruct.comp (Y := functor ⋙ inverse)
            {
              app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
                { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
              naturality := ⋯ }
            {
              app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
                { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
              naturality := ⋯ })
          x))
      i)
    (HomologicalComplex.Hom.f (Hom.f (NatTrans.app (𝟙 (𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)))) x)) i)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
x : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
i : ι
⊢ x.p.f i ≫ x.p.f i = x.p.f i

Tactic:
simp only [HomologicalComplex.p_idem]

Premises used: CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
w :
  ∀ (x : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) (i : ι),
    Eq (α :=
      (CategoryTheory.Functor.obj (functor ⋙ inverse) x).X.X i ⟶
        (CategoryTheory.Functor.obj (functor ⋙ inverse) x).X.X i)
      (HomologicalComplex.Hom.f
        (Hom.f
          (NatTrans.app
            (CategoryStruct.comp (Y := 𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)))
              {
                app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
                  { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
                naturality := ⋯ }
              {
                app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
                  { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
                naturality := ⋯ })
            x))
        i)
      (HomologicalComplex.Hom.f (Hom.f (NatTrans.app (𝟙 (functor ⋙ inverse)) x)) i)
⊢ Eq (α :=
    Quiver.Hom (V :=
      Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c) ⥤ Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))
      (functor ⋙ inverse) (functor ⋙ inverse))
    (CategoryStruct.comp (Y := 𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)))
      {
        app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
          { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
        naturality := ⋯ }
      {
        app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
          { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
        naturality := ⋯ })
    (𝟙 (functor ⋙ inverse))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
x : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)
i : ι
w : x.p.f i ≫ x.p.f i = x.p.f i
⊢ Eq (α :=
    (CategoryTheory.Functor.obj (functor ⋙ inverse) x).X.X i ⟶ (CategoryTheory.Functor.obj (functor ⋙ inverse) x).X.X i)
    (HomologicalComplex.Hom.f
      (Hom.f
        (NatTrans.app
          (CategoryStruct.comp (Y := 𝟭 (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)))
            {
              app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
                { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
              naturality := ⋯ }
            {
              app := fun (P : Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c)) ↦
                { f := { f := fun (n : ι) ↦ P.p.f n, comm' := ⋯ }, comm := ⋯ },
              naturality := ⋯ })
          x))
      i)
    (HomologicalComplex.Hom.f (Hom.f (NatTrans.app (𝟙 (functor ⋙ inverse)) x)) i)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
α : Type u_3
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : IsIdempotentComplete.{v_1, u_1} C
rw : IsIdempotentComplete (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))
⊢ IsIdempotentComplete (HomologicalComplex.{v_1, u_1, u_2} C c)

Tactic:
rw [isIdempotentComplete_iff_of_equivalence
      ((toKaroubiEquivalence C).mapHomologicalComplex c),
    ← isIdempotentComplete_iff_of_equivalence (karoubiHomologicalComplexEquivalence C c)]

Premises used: CategoryTheory.Idempotents.isIdempotentComplete_iff_of_equivalence, CategoryTheory.Equivalence.mapHomologicalComplex, CategoryTheory.Idempotents.toKaroubiEquivalence, CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence
-- Module: Mathlib.CategoryTheory.Idempotents.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
α : Type u_3
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : IsIdempotentComplete.{v_1, u_1} C
⊢ IsIdempotentComplete (Karoubi (HomologicalComplex.{v_1, u_1, u_2} C c))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
h_X : P.X = Q.X
h_p : P.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p
mk :
  ∀ (X : C) (p : X ⟶ X) (idem : p ≫ p = p) (h_X : { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C }.X = Q.X)
    (h_p : { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C }.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p),
    { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C } = Q
⊢ P = Q

Tactic:
cases P
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
Q : Karoubi.{v_1, u_1} C
X : C
p : X ⟶ X
idem : p ≫ p = p
h_X : { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C }.X = Q.X
h_p : { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C }.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p
mk :
  ∀ (X_1 : C) (p_1 : X_1 ⟶ X_1) (idem_1 : p_1 ≫ p_1 = p_1)
    (h_X :
      { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C }.X =
        { X := X_1, p := p_1, idem := idem_1 : Karoubi.{v_1, u_1} C }.X)
    (h_p :
      { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C }.p ≫ eqToHom h_X =
        eqToHom h_X ≫ { X := X_1, p := p_1, idem := idem_1 : Karoubi.{v_1, u_1} C }.p),
    { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C } = { X := X_1, p := p_1, idem := idem_1 }
⊢ { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C } = Q

Tactic:
cases Q
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
p : X ⟶ X
idem : p ≫ p = p
X_1 : C
p_1 : X_1 ⟶ X_1
idem_1 : p_1 ≫ p_1 = p_1
h_X : X = X_1
h_p : p ≫ eqToHom h_X = eqToHom h_X ≫ p_1
mk :
  ∀ (p_2 : X ⟶ X) (idem_2 : p_2 ≫ p_2 = p_2) (h_p : p ≫ eqToHom ⋯ = eqToHom ⋯ ≫ p_2),
    { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C } = { X := X, p := p_2, idem := idem_2 }
⊢ { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C } = { X := X_1, p := p_1, idem := idem_1 }

Tactic:
subst h_X
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
p : X ⟶ X
idem : p ≫ p = p
p_1 : X ⟶ X
idem_1 : p_1 ≫ p_1 = p_1
h_p : p ≫ eqToHom ⋯ = eqToHom ⋯ ≫ p_1
⊢ { X := X, p := p, idem := idem : Karoubi.{v_1, u_1} C } = { X := X, p := p_1, idem := idem_1 }

Tactic:
simpa only [mk.injEq, heq_eq_eq, true_and, eqToHom_refl, comp_id, id_comp] using h_p

Premises used: heq_eq_eq, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Idempotents.Karoubi.mk.injEq, true_and, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
rw : Eq (α := P.X ⟶ Q.X) (P.p ≫ 0) 0
rw₁ rw₂ : Eq.{v_1 + 1} (α := P.X ⟶ Q.X) 0 0
⊢ P.p ≫ 0 ≫ Q.p = 0

Tactic:
rw [zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P.Hom Q
rw : P.p ≫ P.p ≫ f.f ≫ Q.p = P.p ≫ f.f ≫ Q.p
rw₁ : (P.p ≫ P.p) ≫ f.f ≫ Q.p = P.p ≫ f.f ≫ Q.p
rw₂ rw₃ : P.p ≫ f.f ≫ Q.p = P.p ≫ f.f ≫ Q.p
⊢ P.p ≫ f.f = f.f

Tactic:
rw [← f.comm, ← assoc, P.idem]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Idempotents.Karoubi.Hom.comm, CategoryTheory.Idempotents.Karoubi.idem
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P.Hom Q
rw : (P.p ≫ f.f ≫ Q.p) ≫ Q.p = P.p ≫ f.f ≫ Q.p
rw₁ : P.p ≫ (f.f ≫ Q.p) ≫ Q.p = P.p ≫ f.f ≫ Q.p
rw₂ : P.p ≫ f.f ≫ Q.p ≫ Q.p = P.p ≫ f.f ≫ Q.p
rw₃ rw₄ : P.p ≫ f.f ≫ Q.p = P.p ≫ f.f ≫ Q.p
⊢ f.f ≫ Q.p = f.f

Tactic:
rw [← f.comm, assoc, assoc, Q.idem]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Idempotents.Karoubi.Hom.comm, CategoryTheory.Idempotents.Karoubi.idem
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P.Hom Q
rw : f.f = f.f ≫ Q.p
rw₁ rw₂ : f.f = f.f
⊢ P.p ≫ f.f = f.f ≫ Q.p

Tactic:
rw [p_comp, comp_p]

Premises used: CategoryTheory.Idempotents.Karoubi.comp_p, CategoryTheory.Idempotents.Karoubi.p_comp
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q R : Karoubi.{v_1, u_1} C
g : Q.Hom R
f : P.Hom Q
⊢ P.p ≫ (f.f ≫ g.f) ≫ R.p = f.f ≫ g.f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
rw : P.p ≫ P.p = P.p
⊢ P.p ≫ P.p ≫ P.p = P.p

Tactic:
rw [P.idem]

Premises used: CategoryTheory.Idempotents.Karoubi.idem
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
rw rw₁ : P.p = P.p
⊢ P.p ≫ P.p = P.p

Tactic:
rw [P.idem]

Premises used: CategoryTheory.Idempotents.Karoubi.idem
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
repeat' repeat'₁ repeat'₂ : P.p ≫ P.p = P.p
⊢ P.p ≫ P.p ≫ P.p = P.p

Tactic:
repeat' rw [P.idem]

Premises used: CategoryTheory.Idempotents.Karoubi.idem
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g : P ⟶ Q
mp : f = g → f.f = g.f
mpr : f.f = g.f → f = g
⊢ f = g ↔ f.f = g.f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g : P ⟶ Q
h : f = g
mp mp₁ : g.f = g.f
⊢ f.f = g.f

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g : P ⟶ Q
⊢ f.f = g.f → f = g

Tactic:
apply Hom.ext

Premises used: CategoryTheory.Idempotents.Karoubi.Hom.ext
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g : P ⟶ Q
h : f.f = g.f
⊢ f = g

Tactic:
simpa [hom_ext_iff] using h

Premises used: CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q R : Karoubi.{v_1, u_1} C
f : P ⟶ Q
g : Q ⟶ R
⊢ (f ≫ g).f = f.f ≫ g.f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
⊢ Hom.f (𝟙 P) = P.p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
rw rw₁ : Eq.{v_1 + 1} (α := X ⟶ X) (𝟙 X) (𝟙 X)
⊢ Eq.{v_1 + 1} (α := X ⟶ X) (𝟙 X ≫ 𝟙 X) (𝟙 X)

Tactic:
rw [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
⊢ Karoubi.X.{v_1, u_1} { X := X, p := 𝟙 X, idem := ⋯ : Karoubi.{v_1, u_1} C } = X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α :=
    Karoubi.X.{v_1, u_1} { X := X, p := 𝟙 X, idem := ⋯ : Karoubi.{v_1, u_1} C } ⟶
      Karoubi.X.{v_1, u_1} { X := X, p := 𝟙 X, idem := ⋯ })
    (p { X := X, p := 𝟙 X, idem := ⋯ }) (𝟙 X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
h : P = Q
subst : Hom.f (eqToHom ⋯) = P.p ≫ eqToHom ⋯
⊢ Hom.f (eqToHom h) = P.p ≫ eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
⊢ Hom.f (eqToHom ⋯) = P.p ≫ eqToHom ⋯

Tactic:
simp only [eqToHom_refl, Karoubi.id_f, comp_id]

Premises used: CategoryTheory.Idempotents.Karoubi.id_f, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
⊢ Karoubi.p { X := X, p := 𝟙 X, idem := ⋯ : Karoubi.{v_1, u_1} C } ≫ f ≫ Karoubi.p { X := Y, p := 𝟙 Y, idem := ⋯ } = f

Tactic:
simp only [comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ Functor.Full (toKaroubi C)

Tactic:
(fullyFaithfulToKaroubi C).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.Idempotents.fullyFaithfulToKaroubi
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ Functor.Faithful (toKaroubi C)

Tactic:
(fullyFaithfulToKaroubi C).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CategoryTheory.Idempotents.fullyFaithfulToKaroubi
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g : P ⟶ Q
rw : P.p ≫ (f.f ≫ Q.p + g.f ≫ Q.p) = f.f + g.f
rw₁ : P.p ≫ f.f ≫ Q.p + P.p ≫ g.f ≫ Q.p = f.f + g.f
rw₂ : f.f + P.p ≫ g.f ≫ Q.p = f.f + g.f
rw₃ rw₄ : f.f + g.f = f.f + g.f
⊢ P.p ≫ (f.f + g.f) ≫ Q.p = f.f + g.f

Tactic:
rw [add_comp, comp_add, f.comm, g.comm]

Premises used: CategoryTheory.Idempotents.Karoubi.Hom.comm, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P ⟶ Q
⊢ P.p ≫ (-f.f) ≫ Q.p = -f.f

Tactic:
simpa only [neg_comp, comp_neg, neg_inj] using f.comm

Premises used: CategoryTheory.Preadditive.comp_neg, CategoryTheory.Idempotents.Karoubi.Hom.comm, neg_inj, CategoryTheory.Preadditive.neg_comp
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
⊢ P.p ≫ 0 ≫ Q.p = 0

Tactic:
simp only [comp_zero, zero_comp]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g h' : P ⟶ Q
h : (f + g + h').f = (f + (g + h')).f
⊢ f + g + h' = f + (g + h')

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g h' : P ⟶ Q
⊢ (f + g + h').f = (f + (g + h')).f

Tactic:
apply add_assoc

Premises used: add_assoc
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P ⟶ Q
h : (0 + f).f = f.f
⊢ 0 + f = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P ⟶ Q
⊢ (0 + f).f = f.f

Tactic:
apply zero_add

Premises used: zero_add
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P ⟶ Q
h : (f + 0).f = f.f
⊢ f + 0 = f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P ⟶ Q
⊢ (f + 0).f = f.f

Tactic:
apply add_zero

Premises used: add_zero
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P ⟶ Q
h : (-f + f).f = Karoubi.Hom.f 0
⊢ -f + f = 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P ⟶ Q
⊢ (-f + f).f = Karoubi.Hom.f 0

Tactic:
apply neg_add_cancel

Premises used: neg_add_cancel
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g : P ⟶ Q
h : (f + g).f = (g + f).f
⊢ f + g = g + f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f g : P ⟶ Q
⊢ (f + g).f = (g + f).f

Tactic:
apply add_comm

Premises used: add_comm
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
f : P ⟶ Q
⊢ f = 0 ↔ f.f = 0

Tactic:
hom_ext_iff

Premises used: CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
α : Type u_2
s : Finset α
f : α → (P ⟶ Q)
⊢ Eq.{v_1 + 1} (α := P.X ⟶ Q.X) (Hom.f (∑ x ∈ s, f x)) (∑ x ∈ s, (f x).f)

Tactic:
map_sum (inclusionHom P Q) f s

Premises used: CategoryTheory.Idempotents.Karoubi.inclusionHom, map_sum
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P Q : Karoubi.{v_1, u_1} C
⊢ AddCommGroup (P ⟶ Q)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ IsIdempotentComplete (Karoubi.{v_1, u_1} C)

Tactic:
⟨?_⟩

Premises used: CategoryTheory.IsIdempotentComplete.mk
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
refine :
  ∀ (X : Karoubi.{v_1, u_1} C) (p : X ⟶ X),
    p ≫ p = p → ∃ (Y : Karoubi.{v_1, u_1} C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
⊢ IsIdempotentComplete (Karoubi.{v_1, u_1} C)

Tactic:
refine ⟨?_⟩
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
p : P ⟶ P
hp : p ≫ p = p
⊢ p.f ≫ p.f = p.f

Tactic:
simp only [hom_ext_iff, comp_f] at hp

Premises used: CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Idempotents.Karoubi.hom_ext_iff
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
h :
  ∃ (i : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C } ⟶ P) (e : P ⟶ { X := P.X, p := p.f, idem := hp }),
    i ≫ e = 𝟙 { X := P.X, p := p.f, idem := hp } ∧ e ≫ i = p
⊢ ∃ (Y : Karoubi.{v_1, u_1} C) (i : Y ⟶ P) (e : P ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
use ⟨P.X, p.f, hp⟩
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
rw : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.p ≫ p.f = p.f
rw₁ rw₂ : p.f = p.f
⊢ { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.p ≫ p.f ≫ P.p = p.f

Tactic:
rw [comp_p p, hp]

Premises used: CategoryTheory.Idempotents.Karoubi.comp_p
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
h :
  ∃ (e : P ⟶ { X := P.X, p := p.f, idem := hp }),
    { f := p.f, comm := ⋯ : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.Hom P } ≫ e =
        𝟙 { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C } ∧
      e ≫ { f := p.f, comm := ⋯ : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.Hom P } = p
⊢ ∃ (i : { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C } ⟶ P) (e : P ⟶ { X := P.X, p := p.f, idem := hp }),
    i ≫ e = 𝟙 { X := P.X, p := p.f, idem := hp } ∧ e ≫ i = p

Tactic:
use ⟨p.f, by rw [comp_p p, hp]⟩
-- Module: Mathlib.CategoryTheory.Idempotents.Karoubi
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : Karoubi.{v_1, u_1} C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
rw : P.p ≫ p.f = p.f
rw₁ rw₂ : p.f = p.f
⊢ P.p ≫ p.f ≫ { X := P.X, p := p.f, idem := hp : Karoubi.{v_1, u_1} C }.p = p.f

Tactic:
rw [hp, p_comp p]

Premises used: CategoryTheory.Idempotents.Karoubi.p_comp