C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
⊢ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
⊢ IsIdempotentComplete C
refine' ⟨_⟩
C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
⊢ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
intro X p hp
case intro.intro.intro.intro
C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ X.op
e : X.op ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
rcases IsIdempotentComplete.idempotents_split (op X) p.op (by rw [← op_comp, hp]) with
  ⟨Y, i, e, ⟨h₁, h₂⟩⟩
case intro.intro.intro.intro
C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ X.op
e : X.op ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ e.unop ≫ i.unop = 𝟙 Y.unop ∧ i.unop ≫ e.unop = p
case intro.intro.intro.intro
C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ X.op
e : X.op ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
use Y.unop, e.unop, i.unop
case intro.intro.intro.intro.left
C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ X.op
e : X.op ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ e.unop ≫ i.unop = 𝟙 Y.unop

case intro.intro.intro.intro.right
C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ X.op
e : X.op ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ i.unop ≫ e.unop = p
case intro.intro.intro.intro
C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ X.op
e : X.op ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ e.unop ≫ i.unop = 𝟙 Y.unop ∧ i.unop ≫ e.unop = p
constructor
no goals
C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ p.op ≫ p.op = p.op
rw [← op_comp, hp]
case intro.intro.intro.intro.left
C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ X.op
e : X.op ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ (𝟙 Y).unop = 𝟙 Y.unop
case intro.intro.intro.intro.left
C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ X.op
e : X.op ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ e.unop ≫ i.unop = 𝟙 Y.unop
simp only [← unop_comp, h₁]
no goals
case intro.intro.intro.intro.left
C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ X.op
e : X.op ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ (𝟙 Y).unop = 𝟙 Y.unop
rfl
case intro.intro.intro.intro.right
C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ X.op
e : X.op ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ p.op.unop = p
case intro.intro.intro.intro.right
C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ X.op
e : X.op ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ i.unop ≫ e.unop = p
simp only [← unop_comp, h₂]
no goals
case intro.intro.intro.intro.right
C : Type u_1
inst✝ : Category C
h : IsIdempotentComplete Cᵒᵖ
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : Cᵒᵖ
i : Y ⟶ X.op
e : X.op ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p.op
⊢ p.op.unop = p
rfl