-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem eq_of_one_to_two (f : ⦋1⦌ ⟶ ⦋2⦌) :
    (∃ i, f = (δ (n := 1) i)) ∨ ∃ a, f = SimplexCategory.const _ _ a

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 2
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a

Tactic:
refine .inl ⟨0, ?_⟩

Result:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 2
⊢ f = δ 0

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 1 = (Hom.toOrderHom (δ 0)) 1

Tactic:
exact e1

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 2
⊢ f = δ 1

Tactic:
ext i : 3

Result:
case a.h.h
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (δ 1)) i

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 0 = (Hom.toOrderHom (δ 0)) 0

Tactic:
exact e0

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 1 = (Hom.toOrderHom (δ 1)) 1

Tactic:
exact e1

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
⊢ 0 ≤ 1

Tactic:
decide

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a

Tactic:
match e0 : f.toOrderHom 0, e1 : f.toOrderHom 1 with
| 1, 2 =>
  refine .inl ⟨0, ?_⟩
  ext i : 3
  match i with
  | 0 => exact e0
  | 1 => exact e1
| 0, 2 =>
  refine .inl ⟨1, ?_⟩
  ext i : 3
  match i with
  | 0 => exact e0
  | 1 => exact e1
| 0, 1 =>
  refine .inl ⟨2, ?_⟩
  ext i : 3
  match i with
  | 0 => exact e0
  | 1 => exact e1
| 0, 0 | 1, 1 | 2, 2 =>
  refine .inr ⟨f.toOrderHom 0, ?_⟩
  ext i : 3
  match i with
  | 0 => rfl
  | 1 => exact e1.trans e0.symm
| 1, 0 | 2, 0 | 2, 1 =>
  rw [e0, e1] at this
  exact Not.elim (by decide) this

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 0 = (Hom.toOrderHom (δ 2)) 0

Tactic:
exact e0

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 2
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a

Tactic:
refine .inl ⟨1, ?_⟩

Result:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 2
⊢ f = δ 1

Proof state:
case a.h.h
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (δ 0)) i

Tactic:
match i with
| 0 => exact e0
| 1 => exact e1

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 2
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a

Tactic:
refine .inr ⟨f.toOrderHom 0, ?_⟩

Result:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 2
⊢ f = ⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0)

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 2
⊢ f = δ 0

Tactic:
ext i : 3

Result:
case a.h.h
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (δ 0)) i

Proof state:
case a.h.h
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (δ 2)) i

Tactic:
match i with
| 0 => exact e0
| 1 => exact e1

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 2
⊢ f = ⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0)

Tactic:
ext i : 3

Result:
case a.h.h
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0))) i

Proof state:
case a.h.h
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (δ 1)) i

Tactic:
match i with
| 0 => exact e0
| 1 => exact e1

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 1 = (Hom.toOrderHom (⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0))) 1

Tactic:
exact e1.trans e0.symm

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : 2 ≤ 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 1
⊢ ¬2 ≤ 1

Tactic:
decide

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 1 = (Hom.toOrderHom (δ 2)) 1

Tactic:
exact e1

Result:
no goals

Proof state:
case a.h.h
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0))) i

Tactic:
match i with
| 0 => rfl
| 1 => exact e1.trans e0.symm

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : 2 ≤ 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 1
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a

Tactic:
exact Not.elim (by decide) this

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 1
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a

Tactic:
rw [e0, e1] at this

Result:
f : ⦋1⦌ ⟶ ⦋2⦌
this : 2 ≤ 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 1
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
⊢ f = δ 2

Tactic:
ext i : 3

Result:
case a.h.h
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) i = (Hom.toOrderHom (δ 2)) i

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 0 = (Hom.toOrderHom (⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0))) 0

Tactic:
rfl

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 0 = (Hom.toOrderHom (δ 1)) 0

Tactic:
exact e0

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a

Tactic:
have : f.toOrderHom 0 ≤ f.toOrderHom 1 := f.toOrderHom.monotone (by decide : (0 : Fin 2) ≤ 1)

Result:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a