C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
⊢ ∀ (X : D) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
⊢ IsIdempotentComplete D
refine' ⟨_⟩
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
⊢ ∀ (X : D) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
intro X' p hp
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
let φ := ε.counitIso.symm.app X'
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
erw [split_iff_of_iso φ p (φ.inv ≫ p ≫ φ.hom)
    (by
      slice_rhs 1 2 => rw [φ.hom_inv_id]
      rw [id_comp])]
case intro.intro.intro.intro
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj 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
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom
rcases IsIdempotentComplete.idempotents_split (ε.inverse.obj X') (ε.inverse.map p)
    (by rw [← ε.inverse.map_comp, hp]) with
  ⟨Y, i, e, ⟨h₁, h₂⟩⟩
case intro.intro.intro.intro
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj 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
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y) ∧ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
case intro.intro.intro.intro
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj 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
⊢ ∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = φ.inv ≫ p ≫ φ.hom
use ε.functor.obj Y, ε.functor.map i, ε.functor.map e
case intro.intro.intro.intro.left
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj 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
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y)

case intro.intro.intro.intro.right
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj 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
⊢ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
case intro.intro.intro.intro
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj 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
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y) ∧ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
constructor
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ p ≫ φ.hom = (𝟙 ((𝟭 D).obj X') ≫ p) ≫ φ.hom
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ p ≫ φ.hom = φ.hom ≫ φ.inv ≫ p ≫ φ.hom
slice_rhs 1 2 => rw [φ.hom_inv_id]
no goals
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ p ≫ φ.hom = (𝟙 ((𝟭 D).obj X') ≫ p) ≫ φ.hom
rw [id_comp]
no goals
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ ε.inverse.map p ≫ ε.inverse.map p = ε.inverse.map p
rw [← ε.inverse.map_comp, hp]
no goals
case intro.intro.intro.intro.left
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj 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
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y)
rw [← ε.functor.map_comp, h₁, ε.functor.map_id]
case intro.intro.intro.intro.right
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj 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
⊢ (Equivalence.counit ε).app X' ≫ p ≫ (Equivalence.counitInv ε).app X' =
    (ε.counitIso.symm.app X').inv ≫ p ≫ (ε.counitIso.symm.app X').hom
case intro.intro.intro.intro.right
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj 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
⊢ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
simp only [← ε.functor.map_comp, h₂, Equivalence.fun_inv_map]
no goals
case intro.intro.intro.intro.right
C : Type u_4
inst✝¹ : Category C
D : Type u_1
inst✝ : Category D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : (𝟭 D).obj 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
⊢ (Equivalence.counit ε).app X' ≫ p ≫ (Equivalence.counitInv ε).app X' =
    (ε.counitIso.symm.app X').inv ≫ p ≫ (ε.counitIso.symm.app X').hom
rfl