case mp
A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Epi f → Function.Surjective ↑f

case mpr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Function.Surjective ↑f → Epi f
A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Epi f ↔ Function.Surjective ↑f
constructor
case mp
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
⊢ Function.Surjective ↑f
case mp
A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Epi f → Function.Surjective ↑f
intro
case mp
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
⊢ ∀ (b : ↑B), ∃ a, ↑f a = b
case mp
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
⊢ Function.Surjective ↑f
dsimp only [Function.Surjective]
case mp
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
hf' : ∃ b, ∀ (a : ↑A), ↑f a ≠ b
⊢ False
case mp
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
⊢ ∀ (b : ↑B), ∃ a, ↑f a = b
by_contra' hf'
case mp.intro
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
⊢ False
case mp
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
hf' : ∃ b, ∀ (a : ↑A), ↑f a ≠ b
⊢ False
rcases hf' with ⟨m, hm⟩
case mp.intro
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
⊢ False
case mp.intro
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
⊢ False
let Y := NonemptyFinLinOrdCat.of (ULift (Fin 2))
no goals
case mp.intro
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
h : ↑p₁ m = ↑p₂ m
⊢ False
simp [FunLike.coe] at h
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
⊢ (if x₁ < m then { down := 0 } else { down := 1 }) ≤ if x₂ < m then { down := 0 } else { down := 1 }
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
⊢ (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
    (fun b => if b < m then { down := 0 } else { down := 1 }) x₂
simp only
case inl.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : x₁ < m
h₂ : x₂ < m
⊢ { down := 0 } ≤ { down := 0 }

case inl.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 0 } ≤ { down := 1 }

case inr.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ { down := 1 } ≤ { down := 0 }

case inr.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 1 } ≤ { down := 1 }
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
⊢ (if x₁ < m then { down := 0 } else { down := 1 }) ≤ if x₂ < m then { down := 0 } else { down := 1 }
split_ifs with h₁ h₂ h₂
case inr.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ { down := 1 } ≤ { down := 0 }

case inr.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 1 } ≤ { down := 1 }
case inl.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : x₁ < m
h₂ : x₂ < m
⊢ { down := 0 } ≤ { down := 0 }

case inl.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 0 } ≤ { down := 1 }

case inr.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ { down := 1 } ≤ { down := 0 }

case inr.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 1 } ≤ { down := 1 }
any_goals apply Fin.zero_le
case inr.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 1 } ≤ { down := 1 }
case inr.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 1 } ≤ { down := 1 }
apply Fin.zero_le
case inr.inl.h
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ False
case inr.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ { down := 1 } ≤ { down := 0 }
exfalso
no goals
case inr.inl.h
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ False
exact h₁ (lt_of_le_of_lt h h₂)
no goals
case inr.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 1 } ≤ { down := 1 }
rfl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
⊢ (if x₁ ≤ m then { down := 0 } else { down := 1 }) ≤ if x₂ ≤ m then { down := 0 } else { down := 1 }
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
⊢ (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
    (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂
simp only
case inl.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 0 } ≤ { down := 0 }

case inl.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 0 } ≤ { down := 1 }

case inr.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 1 } ≤ { down := 0 }

case inr.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 1 } ≤ { down := 1 }
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
⊢ (if x₁ ≤ m then { down := 0 } else { down := 1 }) ≤ if x₂ ≤ m then { down := 0 } else { down := 1 }
split_ifs with h₁ h₂ h₂
case inr.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 1 } ≤ { down := 0 }

case inr.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 1 } ≤ { down := 1 }
case inl.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 0 } ≤ { down := 0 }

case inl.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 0 } ≤ { down := 1 }

case inr.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 1 } ≤ { down := 0 }

case inr.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 1 } ≤ { down := 1 }
any_goals apply Fin.zero_le
case inr.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 1 } ≤ { down := 1 }
case inr.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 1 } ≤ { down := 1 }
apply Fin.zero_le
case inr.inl.h
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ False
case inr.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 1 } ≤ { down := 0 }
exfalso
no goals
case inr.inl.h
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ False
exact h₁ (h.trans h₂)
no goals
case inr.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
x₁ x₂ : ↑B
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 1 } ≤ { down := 1 }
rfl
case e_a
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
⊢ p₁ = p₂
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
⊢ ↑p₁ m = ↑p₂ m
congr
case e_a
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
⊢ f ≫ p₁ = f ≫ p₂
case e_a
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
⊢ p₁ = p₂
rw [← cancel_epi f]
case e_a.w
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
⊢ (forget NonemptyFinLinOrdCat).map (f ≫ p₁) a = (forget NonemptyFinLinOrdCat).map (f ≫ p₂) a
case e_a
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
⊢ f ≫ p₁ = f ≫ p₂
ext a
case e_a.w
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
⊢ (forget NonemptyFinLinOrdCat).map
      { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
        monotone' :=
          (_ :
            ∀ (x₁ x₂ : ↑B),
              x₁ ≤ x₂ →
                (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
                  (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
      ((forget NonemptyFinLinOrdCat).map f a) =
    (forget NonemptyFinLinOrdCat).map
      { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
        monotone' :=
          (_ :
            ∀ (x₁ x₂ : ↑B),
              x₁ ≤ x₂ →
                (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
                  (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
      ((forget NonemptyFinLinOrdCat).map f a)
case e_a.w
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
⊢ (forget NonemptyFinLinOrdCat).map (f ≫ p₁) a = (forget NonemptyFinLinOrdCat).map (f ≫ p₂) a
simp only [coe_of, FunctorToTypes.map_comp_apply]
case e_a.w
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
⊢ (if ↑f a < m then { down := 0 } else { down := 1 }) = if ↑f a ≤ m then { down := 0 } else { down := 1 }
case e_a.w
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
⊢ (forget NonemptyFinLinOrdCat).map
      { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
        monotone' :=
          (_ :
            ∀ (x₁ x₂ : ↑B),
              x₁ ≤ x₂ →
                (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
                  (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
      ((forget NonemptyFinLinOrdCat).map f a) =
    (forget NonemptyFinLinOrdCat).map
      { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
        monotone' :=
          (_ :
            ∀ (x₁ x₂ : ↑B),
              x₁ ≤ x₂ →
                (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
                  (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
      ((forget NonemptyFinLinOrdCat).map f a)
simp only [forget_map_apply]
case e_a.w.inl.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ↑f a < m
h₂ : ↑f a ≤ m
⊢ { down := 0 } = { down := 0 }

case e_a.w.inl.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ↑f a < m
h₂ : ¬↑f a ≤ m
⊢ { down := 0 } = { down := 1 }

case e_a.w.inr.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ¬↑f a < m
h₂ : ↑f a ≤ m
⊢ { down := 1 } = { down := 0 }

case e_a.w.inr.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ¬↑f a < m
h₂ : ¬↑f a ≤ m
⊢ { down := 1 } = { down := 1 }
case e_a.w
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
⊢ (if ↑f a < m then { down := 0 } else { down := 1 }) = if ↑f a ≤ m then { down := 0 } else { down := 1 }
split_ifs with h₁ h₂ h₂
case e_a.w.inl.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ↑f a < m
h₂ : ¬↑f a ≤ m
⊢ { down := 0 } = { down := 1 }

case e_a.w.inr.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ¬↑f a < m
h₂ : ↑f a ≤ m
⊢ { down := 1 } = { down := 0 }
case e_a.w.inl.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ↑f a < m
h₂ : ↑f a ≤ m
⊢ { down := 0 } = { down := 0 }

case e_a.w.inl.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ↑f a < m
h₂ : ¬↑f a ≤ m
⊢ { down := 0 } = { down := 1 }

case e_a.w.inr.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ¬↑f a < m
h₂ : ↑f a ≤ m
⊢ { down := 1 } = { down := 0 }

case e_a.w.inr.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ¬↑f a < m
h₂ : ¬↑f a ≤ m
⊢ { down := 1 } = { down := 1 }
any_goals rfl
no goals
case e_a.w.inr.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ¬↑f a < m
h₂ : ¬↑f a ≤ m
⊢ { down := 1 } = { down := 1 }
rfl
case e_a.w.inl.inr.h
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ↑f a < m
h₂ : ¬↑f a ≤ m
⊢ False
case e_a.w.inl.inr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ↑f a < m
h₂ : ¬↑f a ≤ m
⊢ { down := 0 } = { down := 1 }
exfalso
no goals
case e_a.w.inl.inr.h
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ↑f a < m
h₂ : ¬↑f a ≤ m
⊢ False
exact h₂ (le_of_lt h₁)
case e_a.w.inr.inl.h
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ¬↑f a < m
h₂ : ↑f a ≤ m
⊢ False
case e_a.w.inr.inl
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ¬↑f a < m
h₂ : ↑f a ≤ m
⊢ { down := 1 } = { down := 0 }
exfalso
no goals
case e_a.w.inr.inl.h
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
Y : NonemptyFinLinOrdCat := of (ULift (Fin 2))
p₁ : B ⟶ Y :=
  { toFun := fun b => if b < m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b < m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b < m then { down := 0 } else { down := 1 }) x₂) }
p₂ : B ⟶ Y :=
  { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 },
    monotone' :=
      (_ :
        ∀ (x₁ x₂ : ↑B),
          x₁ ≤ x₂ →
            (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₁ ≤
              (fun b => if b ≤ m then { down := 0 } else { down := 1 }) x₂) }
a : (forget NonemptyFinLinOrdCat).obj A
h₁ : ¬↑f a < m
h₂ : ↑f a ≤ m
⊢ False
exact hm a (eq_of_le_of_not_lt h₂ h₁)
case mpr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
h : Function.Surjective ↑f
⊢ Epi f
case mpr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Function.Surjective ↑f → Epi f
intro h
no goals
case mpr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
h : Function.Surjective ↑f
⊢ Epi f
exact ConcreteCategory.epi_of_surjective f h