case mp
C : Type u_1
inst✝ : Category C
⊢ IsIdempotentComplete C → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p

case mpr
C : Type u_1
inst✝ : Category C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → IsIdempotentComplete C
C : Type u_1
inst✝ : Category C
⊢ IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
constructor
case mp
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
⊢ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
case mp
C : Type u_1
inst✝ : Category C
⊢ IsIdempotentComplete C → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
intro
case mp
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasEqualizer (𝟙 X) p
case mp
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
⊢ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
intro X p hp
case mp.intro.intro.intro.intro
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ HasEqualizer (𝟙 X) p
case mp
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasEqualizer (𝟙 X) p
rcases IsIdempotentComplete.idempotents_split X p hp with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
no goals
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ i ≫ 𝟙 X = i ≫ p
rw [comp_id, ← h₂, ← assoc, h₁, id_comp]
case create
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ (s : Fork (𝟙 X) p) →
    { l //
      l ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s ∧
        ∀
          {m :
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
              ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj
                WalkingParallelPair.zero},
          m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s → m = l }
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ IsLimit (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p))
apply Fork.IsLimit.mk'
case create
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ { l //
    l ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj
              WalkingParallelPair.zero},
        m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s → m = l }
case create
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
⊢ (s : Fork (𝟙 X) p) →
    { l //
      l ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s ∧
        ∀
          {m :
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
              ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj
                WalkingParallelPair.zero},
          m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s → m = l }
intro s
case create
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ (Fork.ι s ≫ e) ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s ∧
    ∀
      {m :
        ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
          ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero},
      m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s → m = Fork.ι s ≫ e
case create
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ { l //
    l ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj
              WalkingParallelPair.zero},
        m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s → m = l }
refine' ⟨s.ι ≫ e, _⟩
case create.left
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ (Fork.ι s ≫ e) ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s

case create.right
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ ∀
    {m :
      ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
        ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero},
    m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s → m = Fork.ι s ≫ e
case create
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ (Fork.ι s ≫ e) ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s ∧
    ∀
      {m :
        ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
          ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero},
      m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s → m = Fork.ι s ≫ e
constructor
no goals
case create.left
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ (Fork.ι s ≫ e) ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s
erw [assoc, h₂, ← Limits.Fork.condition s, comp_id]
case create.right
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero
hm : m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s
⊢ m = Fork.ι s ≫ e
case create.right
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
⊢ ∀
    {m :
      ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
        ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero},
    m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s → m = Fork.ι s ≫ e
intro m hm
case create.right
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero
hm : m ≫ i = Fork.ι s
⊢ m = Fork.ι s ≫ e
case create.right
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero
hm : m ≫ Fork.ι (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)) = Fork.ι s
⊢ m = Fork.ι s ≫ e
rw [Fork.ι_ofι] at hm
case create.right
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero
hm : m ≫ i = Fork.ι s
⊢ m = (m ≫ i) ≫ e
case create.right
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero
hm : m ≫ i = Fork.ι s
⊢ m = Fork.ι s ≫ e
rw [← hm]
case create.right
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero
hm : m ≫ i = Fork.ι s
⊢ m = m ≫ 𝟙 Y
case create.right
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero
hm : m ≫ i = Fork.ι s
⊢ m = (m ≫ i) ≫ e
simp only [← hm, assoc, h₁]
no goals
case create.right
C : Type u_1
inst✝ : Category C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m :
  ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
    ((Functor.const WalkingParallelPair).obj (Fork.ofι i (_ : i ≫ 𝟙 X = i ≫ p)).pt).obj WalkingParallelPair.zero
hm : m ≫ i = Fork.ι s
⊢ m = m ≫ 𝟙 Y
exact (comp_id m).symm
case mpr
C : Type u_1
inst✝ : Category C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
⊢ IsIdempotentComplete C
case mpr
C : Type u_1
inst✝ : Category C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → IsIdempotentComplete C
intro h
case mpr
C : Type u_1
inst✝ : Category C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
⊢ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
case mpr
C : Type u_1
inst✝ : Category C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
⊢ IsIdempotentComplete C
refine' ⟨_⟩
case mpr
C : Type u_1
inst✝ : Category C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
case mpr
C : Type u_1
inst✝ : Category C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
⊢ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
intro X p hp
case mpr
C : Type u_1
inst✝ : Category 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) p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
case mpr
C : Type u_1
inst✝ : Category C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
haveI : HasEqualizer (𝟙 X) p := h X p hp
case mpr
C : Type u_1
inst✝ : Category 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) p
⊢ equalizer.ι (𝟙 X) p ≫ equalizer.lift p (_ : p ≫ 𝟙 X = p ≫ p) = 𝟙 (equalizer (𝟙 X) p)
case mpr
C : Type u_1
inst✝ : Category 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) p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
refine' ⟨equalizer (𝟙 X) p, equalizer.ι (𝟙 X) p,
  equalizer.lift p (show p ≫ 𝟙 X = p ≫ p by rw [hp, comp_id]), _, equalizer.lift_ι _ _⟩
case mpr.h
C : Type u_1
inst✝ : Category 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) p
⊢ (equalizer.ι (𝟙 X) p ≫ equalizer.lift p (_ : p ≫ 𝟙 X = p ≫ p)) ≫ equalizer.ι (𝟙 X) p =
    𝟙 (equalizer (𝟙 X) p) ≫ equalizer.ι (𝟙 X) p
case mpr
C : Type u_1
inst✝ : Category 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) p
⊢ equalizer.ι (𝟙 X) p ≫ equalizer.lift p (_ : p ≫ 𝟙 X = p ≫ p) = 𝟙 (equalizer (𝟙 X) p)
apply equalizer.hom_ext
case mpr.h
C : Type u_1
inst✝ : Category 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) p
⊢ equalizer.ι (𝟙 X) p ≫ p = equalizer.ι (𝟙 X) p
case mpr.h
C : Type u_1
inst✝ : Category 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) p
⊢ (equalizer.ι (𝟙 X) p ≫ equalizer.lift p (_ : p ≫ 𝟙 X = p ≫ p)) ≫ equalizer.ι (𝟙 X) p =
    𝟙 (equalizer (𝟙 X) p) ≫ equalizer.ι (𝟙 X) p
simp only [assoc, limit.lift_π, Eq.ndrec, id_eq, eq_mpr_eq_cast, Fork.ofι_pt,
  Fork.ofι_π_app, id_comp]
no goals
case mpr.h
C : Type u_1
inst✝ : Category 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) p
⊢ equalizer.ι (𝟙 X) p ≫ p = equalizer.ι (𝟙 X) p
rw [← equalizer.condition, comp_id]
no goals
C : Type u_1
inst✝ : Category 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) p
⊢ p ≫ 𝟙 X = p ≫ p
rw [hp, comp_id]