-- Mathlib/Order/Category/NonemptyFinLinOrd.lean
theorem epi_iff_surjective {A B : NonemptyFinLinOrd.{u}} (f : A ⟶ B) :
    Epi f ↔ Function.Surjective f

Proof state:
case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b => if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 0 } ≤ { down := 0 }

case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b => if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 0 } ≤ { down := 1 }

case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b => if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 1 } ≤ { down := 0 }

case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b => if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 1 } ≤ { down := 1 }

Tactic:
any_goals apply Fin.zero_le

Result:
case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b => if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : x₂ ≤ m
⊢ { down := 1 } ≤ { down := 0 }

case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b => if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ ≤ m
h₂ : ¬x₂ ≤ m
⊢ { down := 1 } ≤ { down := 1 }

Proof state:
case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b => if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
h₁ : (LinOrd.Hom.hom f) a < m
h₂ : ¬(LinOrd.Hom.hom f) a ≤ m
⊢ False

Tactic:
exact h₂ (le_of_lt h₁)

Result:
no goals

Proof state:
case e_a.e_a.hf.h.h
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b => if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
⊢ { toFun := fun b => if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ } ((LinOrd.Hom.hom f) a) =
    { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ } ((LinOrd.Hom.hom f) a)

Tactic:
change ite _ _ _ = ite _ _ _

Result:
case e_a.e_a.hf.h.h
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b => if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
⊢ (if (LinOrd.Hom.hom f) a < m then { down := 0 } else { down := 1 }) =
    if (LinOrd.Hom.hom f) a ≤ m then { down := 0 } else { down := 1 }

Proof state:
case e_a.e_a.hf.h.h
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b => if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
⊢ (LinOrd.Hom.hom (f ≫ p₁)) a = (LinOrd.Hom.hom (f ≫ p₂)) a

Tactic:
simp only [p₁, p₂, hom_comp, OrderHom.comp_coe, Function.comp_apply, hom_ofHom]

Result:
case e_a.e_a.hf.h.h
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b => if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
⊢ { toFun := fun b => if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ } ((LinOrd.Hom.hom f) a) =
    { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ } ((LinOrd.Hom.hom f) a)

Proof state:
case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : x₁ < m
h₂ : x₂ < m
⊢ { down := 0 } ≤ { down := 0 }

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

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

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

Tactic:
any_goals apply Fin.zero_le

Result:
case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ { down := 1 } ≤ { down := 0 }

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

Proof state:
case e_a.e_a
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b => if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
⊢ f ≫ p₁ = f ≫ p₂

Tactic:
ext a : 3

Result:
case e_a.e_a.hf.h.h
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b => if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b => if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : ↑A.toLinOrd
⊢ (LinOrd.Hom.hom (f ≫ p₁)) a = (LinOrd.Hom.hom (f ≫ p₂)) a