[GOAL]
α β : NonemptyFinLinOrdCat
e : ↑α ≃o ↑β
⊢ ↑e ≫ ↑(OrderIso.symm e) = 𝟙 α
[PROOFSTEP]
ext x
[GOAL]
case w
α β : NonemptyFinLinOrdCat
e : ↑α ≃o ↑β
x : (forget NonemptyFinLinOrdCat).obj α
⊢ ↑(↑e ≫ ↑(OrderIso.symm e)) x = ↑(𝟙 α) x
[PROOFSTEP]
exact e.symm_apply_apply x
[GOAL]
α β : NonemptyFinLinOrdCat
e : ↑α ≃o ↑β
⊢ ↑(OrderIso.symm e) ≫ ↑e = 𝟙 β
[PROOFSTEP]
ext x
[GOAL]
case w
α β : NonemptyFinLinOrdCat
e : ↑α ≃o ↑β
x : (forget NonemptyFinLinOrdCat).obj β
⊢ ↑(↑(OrderIso.symm e) ≫ ↑e) x = ↑(𝟙 β) x
[PROOFSTEP]
exact e.apply_symm_apply x
[GOAL]
A B : NonemptyFinLinOrdCat
x✝¹ x✝ : A ⟶ B
h :
  (fun f =>
        ↑(let_fun this := f;
          this))
      x✝¹ =
    (fun f =>
        ↑(let_fun this := f;
          this))
      x✝
⊢ x✝¹ = x✝
[PROOFSTEP]
ext x
[GOAL]
case w
A B : NonemptyFinLinOrdCat
x✝¹ x✝ : A ⟶ B
h :
  (fun f =>
        ↑(let_fun this := f;
          this))
      x✝¹ =
    (fun f =>
        ↑(let_fun this := f;
          this))
      x✝
x : (forget NonemptyFinLinOrdCat).obj A
⊢ ↑x✝¹ x = ↑x✝ x
[PROOFSTEP]
exact congr_fun h x
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Mono f ↔ Function.Injective ↑f
[PROOFSTEP]
refine' ⟨_, ConcreteCategory.mono_of_injective f⟩
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Mono f → Function.Injective ↑f
[PROOFSTEP]
intro
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
⊢ Function.Injective ↑f
[PROOFSTEP]
intro a₁ a₂ h
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
⊢ a₁ = a₂
[PROOFSTEP]
let X := NonemptyFinLinOrdCat.of (ULift (Fin 1))
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
⊢ a₁ = a₂
[PROOFSTEP]
let g₁ : X ⟶ A := ⟨fun _ => a₁, fun _ _ _ => by rfl⟩
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
x✝² x✝¹ : ↑X
x✝ : x✝² ≤ x✝¹
⊢ (fun x => a₁) x✝² ≤ (fun x => a₁) x✝¹
[PROOFSTEP]
rfl
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
⊢ a₁ = a₂
[PROOFSTEP]
let g₂ : X ⟶ A := ⟨fun _ => a₂, fun _ _ _ => by rfl⟩
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
x✝² x✝¹ : ↑X
x✝ : x✝² ≤ x✝¹
⊢ (fun x => a₂) x✝² ≤ (fun x => a₂) x✝¹
[PROOFSTEP]
rfl
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
⊢ a₁ = a₂
[PROOFSTEP]
change g₁ (ULift.up (0 : Fin 1)) = g₂ (ULift.up (0 : Fin 1))
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
⊢ ↑g₁ { down := 0 } = ↑g₂ { down := 0 }
[PROOFSTEP]
have eq : g₁ ≫ f = g₂ ≫ f := by
  ext
  exact h
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
⊢ g₁ ≫ f = g₂ ≫ f
[PROOFSTEP]
ext
[GOAL]
case w
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
x✝ : (forget NonemptyFinLinOrdCat).obj X
⊢ ↑(g₁ ≫ f) x✝ = ↑(g₂ ≫ f) x✝
[PROOFSTEP]
exact h
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
eq : g₁ ≫ f = g₂ ≫ f
⊢ ↑g₁ { down := 0 } = ↑g₂ { down := 0 }
[PROOFSTEP]
rw [cancel_mono] at eq 
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A
h : ↑f a₁ = ↑f a₂
X : NonemptyFinLinOrdCat := of (ULift (Fin 1))
g₁ : X ⟶ A := { toFun := fun x => a₁, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₁) x ≤ (fun x => a₁) x) }
g₂ : X ⟶ A := { toFun := fun x => a₂, monotone' := (_ : ∀ (x x_1 : ↑X), x ≤ x_1 → (fun x => a₂) x ≤ (fun x => a₂) x) }
eq : g₁ = g₂
⊢ ↑g₁ { down := 0 } = ↑g₂ { down := 0 }
[PROOFSTEP]
rw [eq]
[GOAL]
A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Epi f ↔ Function.Surjective ↑f
[PROOFSTEP]
constructor
[GOAL]
case mp
A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Epi f → Function.Surjective ↑f
[PROOFSTEP]
intro
[GOAL]
case mp
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
⊢ Function.Surjective ↑f
[PROOFSTEP]
dsimp only [Function.Surjective]
[GOAL]
case mp
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
⊢ ∀ (b : ↑B), ∃ a, ↑f a = b
[PROOFSTEP]
by_contra' hf'
[GOAL]
case mp
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
hf' : ∃ b, ∀ (a : ↑A), ↑f a ≠ b
⊢ False
[PROOFSTEP]
rcases hf' with ⟨m, hm⟩
[GOAL]
case mp.intro
A B : NonemptyFinLinOrdCat
f : A ⟶ B
a✝ : Epi f
m : ↑B
hm : ∀ (a : ↑A), ↑f a ≠ m
⊢ False
[PROOFSTEP]
let Y := NonemptyFinLinOrdCat.of (ULift (Fin 2))
[GOAL]
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
[PROOFSTEP]
let p₁ : B ⟶ Y :=
  ⟨fun b => if b < m then ULift.up 0 else ULift.up 1, fun x₁ x₂ h =>
    by
    simp only
    split_ifs with h₁ h₂ h₂
    any_goals apply Fin.zero_le
    · exfalso
      exact h₁ (lt_of_le_of_lt h h₂)
    · rfl⟩
[GOAL]
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₂
[PROOFSTEP]
simp only
[GOAL]
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 }
[PROOFSTEP]
split_ifs with h₁ h₂ h₂
[GOAL]
case pos
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 neg
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 pos
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 neg
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 }
[PROOFSTEP]
any_goals apply Fin.zero_le
[GOAL]
case pos
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 }
[PROOFSTEP]
apply Fin.zero_le
[GOAL]
case neg
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 }
[PROOFSTEP]
apply Fin.zero_le
[GOAL]
case pos
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 }
[PROOFSTEP]
apply Fin.zero_le
[GOAL]
case neg
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 }
[PROOFSTEP]
apply Fin.zero_le
[GOAL]
case pos
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 }
[PROOFSTEP]
exfalso
[GOAL]
case pos.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
[PROOFSTEP]
exact h₁ (lt_of_le_of_lt h h₂)
[GOAL]
case neg
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 }
[PROOFSTEP]
rfl
[GOAL]
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₂) }
⊢ False
[PROOFSTEP]
let p₂ : B ⟶ Y :=
  ⟨fun b => if b ≤ m then ULift.up 0 else ULift.up 1, fun x₁ x₂ h =>
    by
    simp only
    split_ifs with h₁ h₂ h₂
    any_goals apply Fin.zero_le
    · exfalso
      exact h₁ (h.trans h₂)
    · rfl⟩
[GOAL]
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₂
[PROOFSTEP]
simp only
[GOAL]
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 }
[PROOFSTEP]
split_ifs with h₁ h₂ h₂
[GOAL]
case pos
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 neg
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 pos
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 neg
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 }
[PROOFSTEP]
any_goals apply Fin.zero_le
[GOAL]
case pos
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 }
[PROOFSTEP]
apply Fin.zero_le
[GOAL]
case neg
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 }
[PROOFSTEP]
apply Fin.zero_le
[GOAL]
case pos
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 }
[PROOFSTEP]
apply Fin.zero_le
[GOAL]
case neg
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 }
[PROOFSTEP]
apply Fin.zero_le
[GOAL]
case pos
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 }
[PROOFSTEP]
exfalso
[GOAL]
case pos.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
[PROOFSTEP]
exact h₁ (h.trans h₂)
[GOAL]
case neg
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 }
[PROOFSTEP]
rfl
[GOAL]
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₂) }
⊢ False
[PROOFSTEP]
have h : p₁ m = p₂ m := by
  congr
  rw [← cancel_epi f]
  ext a
  simp only [coe_of, comp_apply]
  change ite _ _ _ = ite _ _ _
  split_ifs with h₁ h₂ h₂
  any_goals rfl
  · exfalso
    exact h₂ (le_of_lt h₁)
  · exfalso
    exact hm a (eq_of_le_of_not_lt h₂ h₁)
[GOAL]
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
[PROOFSTEP]
congr
[GOAL]
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₂
[PROOFSTEP]
rw [← cancel_epi f]
[GOAL]
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₂
[PROOFSTEP]
ext a
[GOAL]
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
⊢ ↑(f ≫ p₁) a = ↑(f ≫ p₂) a
[PROOFSTEP]
simp only [coe_of, comp_apply]
[GOAL]
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
⊢ ↑{ 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 a) =
    ↑{ 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 a)
[PROOFSTEP]
change ite _ _ _ = ite _ _ _
[GOAL]
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 }
[PROOFSTEP]
split_ifs with h₁ h₂ h₂
[GOAL]
case pos
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 neg
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 pos
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 neg
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 }
[PROOFSTEP]
any_goals rfl
[GOAL]
case pos
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 }
[PROOFSTEP]
rfl
[GOAL]
case neg
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 }
[PROOFSTEP]
rfl
[GOAL]
case pos
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 }
[PROOFSTEP]
rfl
[GOAL]
case neg
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 }
[PROOFSTEP]
rfl
[GOAL]
case neg
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 }
[PROOFSTEP]
exfalso
[GOAL]
case neg.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
[PROOFSTEP]
exact h₂ (le_of_lt h₁)
[GOAL]
case pos
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 }
[PROOFSTEP]
exfalso
[GOAL]
case pos.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
[PROOFSTEP]
exact hm a (eq_of_le_of_not_lt h₂ h₁)
[GOAL]
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
[PROOFSTEP]
simp [FunLike.coe] at h 
[GOAL]
case mpr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
⊢ Function.Surjective ↑f → Epi f
[PROOFSTEP]
intro h
[GOAL]
case mpr
A B : NonemptyFinLinOrdCat
f : A ⟶ B
h : Function.Surjective ↑f
⊢ Epi f
[PROOFSTEP]
exact ConcreteCategory.epi_of_surjective f h
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
⊢ IsSplitEpi f
[PROOFSTEP]
have H : ∀ y : Y, Nonempty (f ⁻¹' { y }) := by
  rw [epi_iff_surjective] at hf 
  intro y
  exact Nonempty.intro ⟨(hf y).choose, (hf y).choose_spec⟩
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
⊢ ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
[PROOFSTEP]
rw [epi_iff_surjective] at hf 
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Function.Surjective ↑f
⊢ ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
[PROOFSTEP]
intro y
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Function.Surjective ↑f
y : ↑Y
⊢ Nonempty ↑(↑f ⁻¹' {y})
[PROOFSTEP]
exact Nonempty.intro ⟨(hf y).choose, (hf y).choose_spec⟩
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
⊢ IsSplitEpi f
[PROOFSTEP]
let φ : Y → X := fun y => (H y).some.1
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
⊢ IsSplitEpi f
[PROOFSTEP]
have hφ : ∀ y : Y, f (φ y) = y := fun y => (H y).some.2
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
⊢ IsSplitEpi f
[PROOFSTEP]
refine' IsSplitEpi.mk' ⟨⟨φ, _⟩, _⟩
[GOAL]
case refine'_1
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
⊢ Monotone φ
case refine'_2
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
⊢ { toFun := φ, monotone' := ?refine'_1 } ≫ f = 𝟙 Y
[PROOFSTEP]
swap
[GOAL]
case refine'_2
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
⊢ { toFun := φ, monotone' := ?refine'_1 } ≫ f = 𝟙 Y
[PROOFSTEP]
ext b
[GOAL]
case refine'_2.w
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
b : (forget NonemptyFinLinOrdCat).obj Y
⊢ ↑({ toFun := φ, monotone' := ?refine'_1 } ≫ f) b = ↑(𝟙 Y) b
[PROOFSTEP]
apply hφ
[GOAL]
case refine'_1
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
⊢ Monotone φ
[PROOFSTEP]
intro a b
[GOAL]
case refine'_1
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
a b : ↑Y
⊢ a ≤ b → φ a ≤ φ b
[PROOFSTEP]
contrapose
[GOAL]
case refine'_1
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
a b : ↑Y
⊢ ¬φ a ≤ φ b → ¬a ≤ b
[PROOFSTEP]
intro h
[GOAL]
case refine'_1
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
a b : ↑Y
h : ¬φ a ≤ φ b
⊢ ¬a ≤ b
[PROOFSTEP]
simp only [not_le] at h ⊢
[GOAL]
case refine'_1
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
a b : ↑Y
h : ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b}))) < ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {a})))
⊢ b < a
[PROOFSTEP]
suffices b ≤ a by
  apply lt_of_le_of_ne this
  rintro rfl
  exfalso
  simp at h 
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
a b : ↑Y
h : ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b}))) < ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {a})))
this : b ≤ a
⊢ b < a
[PROOFSTEP]
apply lt_of_le_of_ne this
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
a b : ↑Y
h : ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b}))) < ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {a})))
this : b ≤ a
⊢ b ≠ a
[PROOFSTEP]
rintro rfl
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
b : ↑Y
h : ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b}))) < ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b})))
this : b ≤ b
⊢ False
[PROOFSTEP]
exfalso
[GOAL]
case h
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
b : ↑Y
h : ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b}))) < ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b})))
this : b ≤ b
⊢ False
[PROOFSTEP]
simp at h 
[GOAL]
case refine'_1
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
a b : ↑Y
h : ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b}))) < ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {a})))
⊢ b ≤ a
[PROOFSTEP]
have H : f (φ b) ≤ f (φ a) := f.monotone (le_of_lt h)
[GOAL]
case refine'_1
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
hf : Epi f
H✝ : ∀ (y : ↑Y), Nonempty ↑(↑f ⁻¹' {y})
φ : ↑Y → ↑X := fun y => ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {y})))
hφ : ∀ (y : ↑Y), ↑f (φ y) = y
a b : ↑Y
h : ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {b}))) < ↑(Nonempty.some (_ : Nonempty ↑(↑f ⁻¹' {a})))
H : ↑f (φ b) ≤ ↑f (φ a)
⊢ b ≤ a
[PROOFSTEP]
simpa only [hφ] using H
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
letI : NonemptyFinLinOrd (Set.image f ⊤) := ⟨by infer_instance⟩
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
⊢ Nonempty ↑(↑f '' ⊤)
[PROOFSTEP]
infer_instance
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
let I := NonemptyFinLinOrdCat.of (Set.image f ⊤)
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
let e : X ⟶ I := ⟨fun x => ⟨f x, ⟨x, by tauto⟩⟩, fun x₁ x₂ h => f.monotone h⟩
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
x : ↑X
⊢ x ∈ ⊤ ∧ ↑f x = ↑f x
[PROOFSTEP]
tauto
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
let m : I ⟶ Y := ⟨fun y => y.1, by tauto⟩
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
⊢ Monotone fun y => ↑y
[PROOFSTEP]
tauto
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
m : I ⟶ Y := { toFun := fun y => ↑y, monotone' := (_ : ∀ ⦃a b : ↑I⦄, a ≤ b → a ≤ b) }
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
haveI : Epi e := by
  rw [epi_iff_surjective]
  rintro ⟨_, y, h, rfl⟩
  exact ⟨y, rfl⟩
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
m : I ⟶ Y := { toFun := fun y => ↑y, monotone' := (_ : ∀ ⦃a b : ↑I⦄, a ≤ b → a ≤ b) }
⊢ Epi e
[PROOFSTEP]
rw [epi_iff_surjective]
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
m : I ⟶ Y := { toFun := fun y => ↑y, monotone' := (_ : ∀ ⦃a b : ↑I⦄, a ≤ b → a ≤ b) }
⊢ Function.Surjective ↑e
[PROOFSTEP]
rintro ⟨_, y, h, rfl⟩
[GOAL]
case mk.intro.intro
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
m : I ⟶ Y := { toFun := fun y => ↑y, monotone' := (_ : ∀ ⦃a b : ↑I⦄, a ≤ b → a ≤ b) }
y : ↑X
h : y ∈ ⊤
⊢ ∃ a, ↑e a = { val := ↑f y, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f y) }
[PROOFSTEP]
exact ⟨y, rfl⟩
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this✝ : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
m : I ⟶ Y := { toFun := fun y => ↑y, monotone' := (_ : ∀ ⦃a b : ↑I⦄, a ≤ b → a ≤ b) }
this : Epi e
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
haveI : StrongEpi e := strongEpi_of_epi e
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this✝¹ : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
m : I ⟶ Y := { toFun := fun y => ↑y, monotone' := (_ : ∀ ⦃a b : ↑I⦄, a ≤ b → a ≤ b) }
this✝ : Epi e
this : StrongEpi e
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
haveI : Mono m := ConcreteCategory.mono_of_injective _ (fun x y h => Subtype.ext h)
[GOAL]
X Y : NonemptyFinLinOrdCat
f : X ⟶ Y
this✝² : NonemptyFinLinOrd ↑(↑f '' ⊤) := NonemptyFinLinOrd.mk
I : NonemptyFinLinOrdCat := of ↑(↑f '' ⊤)
e : X ⟶ I :=
  { toFun := fun x => { val := ↑f x, property := (_ : ∃ a, a ∈ ⊤ ∧ ↑f a = ↑f x) },
    monotone' := (_ : ∀ (x₁ x₂ : ↑X), x₁ ≤ x₂ → ↑f x₁ ≤ ↑f x₂) }
m : I ⟶ Y := { toFun := fun y => ↑y, monotone' := (_ : ∀ ⦃a b : ↑I⦄, a ≤ b → a ≤ b) }
this✝¹ : Epi e
this✝ : StrongEpi e
this : Mono m
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
exact ⟨⟨I, m, e, rfl⟩⟩
