-- Mathlib/CategoryTheory/Idempotents/Basic.lean
theorem isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent :
    IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, 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) p
⊢ equalizer.ι (𝟙 X) p ≫ equalizer.lift p ⋯ = 𝟙 (equalizer (𝟙 X) p)

Tactic:
ext

Result:
case mpr.h
C : Type u_1
inst✝ : Category.{u_2, 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) p
⊢ (equalizer.ι (𝟙 X) p ≫ equalizer.lift p ⋯) ≫ equalizer.ι (𝟙 X) p = 𝟙 (equalizer (𝟙 X) p) ≫ equalizer.ι (𝟙 X) p

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, 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) p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
refine ⟨equalizer (𝟙 X) p, equalizer.ι (𝟙 X) p,
  equalizer.lift p (show p ≫ 𝟙 X = p ≫ p by rw [hp, comp_id]), ?_, equalizer.lift_ι _ _⟩

Result:
case mpr
C : Type u_1
inst✝ : Category.{u_2, 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) p
⊢ equalizer.ι (𝟙 X) p ≫ equalizer.lift p ⋯ = 𝟙 (equalizer (𝟙 X) p)

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → IsIdempotentComplete C

Tactic:
intro h

Result:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
⊢ IsIdempotentComplete C

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasEqualizer (𝟙 X) p

Tactic:
rcases IsIdempotentComplete.idempotents_split X p hp with ⟨Y, i, e, ⟨h₁, h₂⟩⟩

Result:
case mp.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} 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

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
⊢ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p

Tactic:
intro X p hp

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
⊢ HasEqualizer (𝟙 X) p

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
⊢ IsIdempotentComplete C

Tactic:
refine ⟨?_⟩

Result:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} 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

Proof state:
case create
C : Type u_1
inst✝ : Category.{u_2, u_1} 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.ofι i ⋯).ι = s.ι ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj (Fork.ofι i ⋯).pt).obj WalkingParallelPair.zero},
        m ≫ (Fork.ofι i ⋯).ι = s.ι → m = l }

Tactic:
refine ⟨s.ι ≫ e, ?_⟩

Result:
case create
C : Type u_1
inst✝ : Category.{u_2, u_1} 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
⊢ (s.ι ≫ e) ≫ (Fork.ofι i ⋯).ι = s.ι ∧
    ∀
      {m :
        ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
          ((Functor.const WalkingParallelPair).obj (Fork.ofι i ⋯).pt).obj WalkingParallelPair.zero},
      m ≫ (Fork.ofι i ⋯).ι = s.ι → m = s.ι ≫ e

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} 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

Tactic:
haveI : HasEqualizer (𝟙 X) p := h X p hp

Result:
case mpr
C : Type u_1
inst✝ : Category.{u_2, 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) p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p

Proof state:
case create.right
C : Type u_1
inst✝ : Category.{u_2, u_1} 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 ⋯).pt).obj WalkingParallelPair.zero
hm : m ≫ (Fork.ofι i ⋯).ι = s.ι
⊢ m = s.ι ≫ e

Tactic:
rw [Fork.ι_ofι] at hm

Result:
case create.right
C : Type u_1
inst✝ : Category.{u_2, u_1} 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 ⋯).pt).obj WalkingParallelPair.zero
hm : m ≫ i = s.ι
⊢ m = s.ι ≫ e

Proof state:
case create
C : Type u_1
inst✝ : Category.{u_2, u_1} 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.ofι i ⋯).ι = s.ι ∧
        ∀
          {m :
            ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
              ((Functor.const WalkingParallelPair).obj (Fork.ofι i ⋯).pt).obj WalkingParallelPair.zero},
          m ≫ (Fork.ofι i ⋯).ι = s.ι → m = l }

Tactic:
intro s

Result:
case create
C : Type u_1
inst✝ : Category.{u_2, u_1} 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.ofι i ⋯).ι = s.ι ∧
      ∀
        {m :
          ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.zero ⟶
            ((Functor.const WalkingParallelPair).obj (Fork.ofι i ⋯).pt).obj WalkingParallelPair.zero},
        m ≫ (Fork.ofι i ⋯).ι = s.ι → m = l }

Proof state:
case create.right
C : Type u_1
inst✝ : Category.{u_2, u_1} 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 ⋯).pt).obj WalkingParallelPair.zero
hm : m ≫ i = s.ι
⊢ m = s.ι ≫ e

Tactic:
rw [← hm]

Result:
case create.right
C : Type u_1
inst✝ : Category.{u_2, u_1} 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 ⋯).pt).obj WalkingParallelPair.zero
hm : m ≫ i = s.ι
⊢ m = (m ≫ i) ≫ e

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} 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

Tactic:
rw [comp_id, ← h₂, ← assoc, h₁, id_comp]

Result:
no goals