awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
rw : (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
⊢ IsIdempotentComplete.{v_1, u_1} C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p

Tactic:
rw [isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent]

Premises used: CategoryTheory.Idempotents.isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
mp : (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
mpr : (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasEqualizer (𝟙 X) (𝟙 X - p)

Tactic:
haveI : HasEqualizer (𝟙 X) (𝟙 X - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) (𝟙 X - p)
⊢ HasKernel (𝟙 X - (𝟙 X - p))

Tactic:
hasKernel_of_hasEqualizer (𝟙 X) (𝟙 X - p)

Premises used: CategoryTheory.Preadditive.hasKernel_of_hasEqualizer, HSub.hSub, CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) (𝟙 X - p)
h₁ : p = 𝟙 X - (𝟙 X - p)
⊢ HasKernel p

Tactic:
convert! hasKernel_of_hasEqualizer (𝟙 X) (𝟙 X - p)

Premises used: CategoryTheory.Preadditive.hasKernel_of_hasEqualizer, HSub.hSub, CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) (𝟙 X - p)
h₁ h₂ : p = p
⊢ p = 𝟙 X - (𝟙 X - p)

Tactic:
rw [sub_sub_cancel]

Premises used: sub_sub_cancel
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasKernel (𝟙 X - p)

Tactic:
haveI : HasKernel (𝟙 _ - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasKernel (𝟙 X - p)
⊢ HasEqualizer (𝟙 X) p

Tactic:
apply Preadditive.hasEqualizer_of_hasKernel

Premises used: CategoryTheory.Preadditive.hasEqualizer_of_hasKernel
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_2, u_2} D
rw : ∀ (X : D) (p : X ⟶ X), p ≫ p = p → HasKernel p
⊢ IsIdempotentComplete.{v_2, u_2} D

Tactic:
rw [isIdempotentComplete_iff_idempotents_have_kernels]

Premises used: CategoryTheory.Idempotents.isIdempotentComplete_iff_idempotents_have_kernels
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
inst_2 : Abelian.{v_2, u_2} D
X : D
p : X ⟶ X
h : p ≫ p = p
⊢ HasKernel p

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
h : ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
rcases :
  ∀ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y) (h₁ : i ≫ e = 𝟙 Y) (h₂ : e ≫ i = p),
    ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
⊢ ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'

Tactic:
rcases h with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
h : (i ≫ φ.hom) ≫ φ.inv ≫ e = 𝟙 Y ∧ (φ.inv ≫ e) ≫ i ≫ φ.hom = p'
⊢ ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'

Tactic:
use Y, i ≫ φ.hom, φ.inv ≫ e

Premises used: CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ (i ≫ φ.hom) ≫ φ.inv ≫ e = 𝟙 Y ∧ (φ.inv ≫ e) ≫ i ≫ φ.hom = p'

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
mp :
  (∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p) →
    ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'
mpr :
  (∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p') →
    ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
⊢ (∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p) ↔
    ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p) →
    ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'

Tactic:
split_imp_of_iso φ p p' hpp'

Premises used: CategoryTheory.Idempotents.split_imp_of_iso
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p) →
    ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p'

Tactic:
exact split_imp_of_iso φ p p' hpp'

Premises used: CategoryTheory.Idempotents.split_imp_of_iso
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
mpr : p' ≫ φ.symm.hom = φ.symm.hom ≫ p
⊢ (∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p') →
    ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
apply split_imp_of_iso φ.symm p' p

Premises used: CategoryTheory.Idempotents.split_imp_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
mpr : p' ≫ φ.symm.hom = φ.symm.hom ≫ p ≫ φ.hom ≫ φ.inv
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ p

Tactic:
rw [← comp_id p, ← φ.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
a : φ.hom ≫ p'
| p ≫ φ.hom

Tactic:
rw [hpp']
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
mpr : p' ≫ φ.symm.hom = φ.symm.hom ≫ (φ.hom ≫ p') ≫ φ.inv
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ p ≫ φ.hom ≫ φ.inv

Tactic:
slice_rhs 2 3 => rw [hpp']
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ (φ.hom ≫ p') ≫ φ.inv

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
⊢ IsIdempotentComplete.{v_2, u_2} D

Tactic:
⟨?_⟩

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

Tactic:
refine ⟨?_⟩
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
a : 𝟙 X'
| φ.hom ≫ φ.inv

Tactic:
rw [φ.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
slice_rhs : p ≫ φ.hom = (𝟙 X' ≫ p) ≫ φ.hom
⊢ p ≫ φ.hom = φ.hom ≫ φ.inv ≫ p ≫ φ.hom

Tactic:
slice_rhs 1 2 => rw [φ.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
rw rw₁ : p ≫ φ.hom = p ≫ φ.hom
⊢ p ≫ φ.hom = (𝟙 X' ≫ p) ≫ φ.hom

Tactic:
rw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
rw :
  ∃ (Y' : D) (i' : Y' ⟶ (ε.inverse ⋙ ε.functor).obj X') (e' : (ε.inverse ⋙ ε.functor).obj X' ⟶ Y'),
    i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom
⊢ ∃ (Y : D) (i : Y ⟶ X') (e : X' ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
rw [split_iff_of_iso φ p (φ.inv ≫ p ≫ φ.hom)
      (by
        slice_rhs 1 2 => rw [φ.hom_inv_id]
        rw [id_comp])]

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Idempotents.split_iff_of_iso, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
rw : ε.inverse.map (p ≫ p) = ε.inverse.map p
rw₁ rw₂ : ε.inverse.map p = ε.inverse.map p
⊢ ε.inverse.map p ≫ ε.inverse.map p = ε.inverse.map p

Tactic:
rw [← ε.inverse.map_comp, hp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
rcases :
  ∀ (Y : C) (i : Y ⟶ ε.inverse.obj X') (e : ε.inverse.obj X' ⟶ Y) (h₁ : i ≫ e = 𝟙 Y) (h₂ : e ≫ i = ε.inverse.map p),
    ∃ (Y' : D) (i' : Y' ⟶ (ε.inverse ⋙ ε.functor).obj X') (e' : (ε.inverse ⋙ ε.functor).obj X' ⟶ Y'),
      i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom
⊢ ∃ (Y' : D) (i' : Y' ⟶ (ε.inverse ⋙ ε.functor).obj X') (e' : (ε.inverse ⋙ ε.functor).obj X' ⟶ Y'),
    i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom

Tactic:
rcases IsIdempotentComplete.idempotents_split (ε.inverse.obj X') (ε.inverse.map p)
      (by rw [← ε.inverse.map_comp, hp]) with
    ⟨Y, i, e, ⟨h₁, h₂⟩⟩

Premises used: CategoryTheory.Functor.map, CategoryTheory.Functor.obj, CategoryTheory.IsIdempotentComplete.idempotents_split, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
h₃ : ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y) ∧ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
⊢ ∃ (Y' : D) (i' : Y' ⟶ (ε.inverse ⋙ ε.functor).obj X') (e' : (ε.inverse ⋙ ε.functor).obj X' ⟶ Y'),
    i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom

Tactic:
use ε.functor.obj Y, ε.functor.map i, ε.functor.map e

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Functor.map, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
h₃ : ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y)
h₄ : ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y) ∧ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
h₃ : ε.functor.map (i ≫ e) = 𝟙 (ε.functor.obj Y)
h₄ : ε.functor.map (𝟙 Y) = 𝟙 (ε.functor.obj Y)
h₅ h₆ : Eq.{v_2 + 1} (α := ε.functor.obj Y ⟶ ε.functor.obj Y) (𝟙 (ε.functor.obj Y)) (𝟙 (ε.functor.obj Y))
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y)

Tactic:
rw [← ε.functor.map_comp, h₁, ε.functor.map_id]

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
h₃ : ε.counit.app X' ≫ p ≫ ε.counitInv.app X' = φ.inv ≫ p ≫ φ.hom
⊢ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom

Tactic:
simp only [← ε.functor.map_comp, h₂, Equivalence.fun_inv_map]

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Equivalence.fun_inv_map, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
h : IsIdempotentComplete.{v_1, u_1} C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.counit.app X' ≫ p ≫ ε.counitInv.app X' = φ.inv ≫ p ≫ φ.hom

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
mp : IsIdempotentComplete.{v_1, u_1} C → IsIdempotentComplete.{v_2, u_2} D
mpr : IsIdempotentComplete.{v_2, u_2} D → IsIdempotentComplete.{v_1, u_1} C
⊢ IsIdempotentComplete.{v_1, u_1} C ↔ IsIdempotentComplete.{v_2, u_2} D

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
⊢ IsIdempotentComplete.{v_1, u_1} C → IsIdempotentComplete.{v_2, u_2} D

Tactic:
Equivalence.isIdempotentComplete ε

Premises used: CategoryTheory.Idempotents.Equivalence.isIdempotentComplete
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
⊢ IsIdempotentComplete.{v_1, u_1} C → IsIdempotentComplete.{v_2, u_2} D

Tactic:
exact Equivalence.isIdempotentComplete ε

Premises used: CategoryTheory.Idempotents.Equivalence.isIdempotentComplete
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
⊢ IsIdempotentComplete.{v_2, u_2} D → IsIdempotentComplete.{v_1, u_1} C

Tactic:
Equivalence.isIdempotentComplete ε.symm

Premises used: CategoryTheory.Idempotents.Equivalence.isIdempotentComplete, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
ε : Equivalence.{v_1, v_2, u_1, u_2} C D
⊢ IsIdempotentComplete.{v_2, u_2} D → IsIdempotentComplete.{v_1, u_1} C

Tactic:
exact Equivalence.isIdempotentComplete ε.symm

Premises used: CategoryTheory.Idempotents.Equivalence.isIdempotentComplete, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
⊢ IsIdempotentComplete.{v_1, u_1} C

Tactic:
⟨?_⟩

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

Tactic:
refine ⟨?_⟩
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
rw : (p ≫ p).op = p.op
rw₁ rw₂ : p.op = p.op
⊢ p.op ≫ p.op = p.op

Tactic:
rw [← op_comp, hp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
rcases :
  ∀ (Y : Cᵒᵖ) (i : Y ⟶ op X) (e : op X ⟶ Y) (h₁ : i ≫ e = 𝟙 Y) (h₂ : e ≫ i = p.op),
    ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p
⊢ ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
rcases IsIdempotentComplete.idempotents_split (op X) p.op (by rw [← op_comp, hp]) with
    ⟨Y, i, e, ⟨h₁, h₂⟩⟩

Premises used: Quiver.Hom.op, Opposite.op, CategoryTheory.IsIdempotentComplete.idempotents_split
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
h₃ : e.unop ≫ i.unop = 𝟙 (unop Y) ∧ i.unop ≫ e.unop = p
⊢ ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
use Y.unop, e.unop, i.unop

Premises used: Quiver.Hom.unop, Opposite.unop
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
h₃ : e.unop ≫ i.unop = 𝟙 (unop Y)
h₄ : i.unop ≫ e.unop = p
⊢ e.unop ≫ i.unop = 𝟙 (unop Y) ∧ i.unop ≫ e.unop = p

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
h₃ : Eq.{v_1 + 1} (α := unop Y ⟶ unop Y) (Quiver.Hom.unop (𝟙 Y)) (𝟙 (unop Y))
⊢ e.unop ≫ i.unop = 𝟙 (unop Y)

Tactic:
simp only [← unop_comp, h₁]

Premises used: CategoryTheory.unop_comp
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ Eq.{v_1 + 1} (α := unop Y ⟶ unop Y) (Quiver.Hom.unop (𝟙 Y)) (𝟙 (unop Y))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
h₃ : p.op.unop = p
⊢ i.unop ≫ e.unop = p

Tactic:
simp only [← unop_comp, h₂]

Premises used: CategoryTheory.unop_comp
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ op X
e : op X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ p.op.unop = p

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
mp : IsIdempotentComplete.{v_1, u_1} Cᵒᵖ → IsIdempotentComplete.{v_1, u_1} C
mpr : IsIdempotentComplete.{v_1, u_1} C → IsIdempotentComplete.{v_1, u_1} Cᵒᵖ
⊢ IsIdempotentComplete.{v_1, u_1} Cᵒᵖ ↔ IsIdempotentComplete.{v_1, u_1} C

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ IsIdempotentComplete.{v_1, u_1} Cᵒᵖ → IsIdempotentComplete.{v_1, u_1} C

Tactic:
isIdempotentComplete_of_isIdempotentComplete_opposite

Premises used: CategoryTheory.Idempotents.isIdempotentComplete_of_isIdempotentComplete_opposite
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
⊢ IsIdempotentComplete.{v_1, u_1} Cᵒᵖ → IsIdempotentComplete.{v_1, u_1} C

Tactic:
exact isIdempotentComplete_of_isIdempotentComplete_opposite

Premises used: CategoryTheory.Idempotents.isIdempotentComplete_of_isIdempotentComplete_opposite
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} C
mpr : IsIdempotentComplete.{v_1, u_1} Cᵒᵖᵒᵖ
⊢ IsIdempotentComplete.{v_1, u_1} Cᵒᵖ

Tactic:
apply isIdempotentComplete_of_isIdempotentComplete_opposite

Premises used: CategoryTheory.Idempotents.isIdempotentComplete_of_isIdempotentComplete_opposite
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h mpr : IsIdempotentComplete.{v_1, u_1} C
⊢ IsIdempotentComplete.{v_1, u_1} Cᵒᵖᵒᵖ

Tactic:
rw [isIdempotentComplete_iff_of_equivalence (opOpEquivalence C)]

Premises used: CategoryTheory.Idempotents.isIdempotentComplete_iff_of_equivalence, CategoryTheory.opOpEquivalence
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} C
⊢ IsIdempotentComplete.{v_1, u_1} C

Tactic:
h
-- Module: Mathlib.CategoryTheory.Idempotents.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
h : IsIdempotentComplete.{v_1, u_1} C
⊢ IsIdempotentComplete.{v_1, u_1} C

Tactic:
exact h