-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem eq_of_one_to_one (f : ⦋1⦌ ⟶ ⦋1⦌) :
    (∃ a, f = const ⦋1⦌ _ a) ∨ f = 𝟙 _

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

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

Result:
no goals

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

Tactic:
rw [e0, e1] at this

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

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

Tactic:
decide

Result:
no goals

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

Tactic:
rfl

Result:
no goals

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

Tactic:
exact e1.trans e0.symm

Result:
no goals

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

Tactic:
exact Not.elim (by decide) this

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
⊢ (∃ a, f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌

Tactic:
right

Result:
case h
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
⊢ f = 𝟙 ⦋1⦌

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

Tactic:
exact e1

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 1
⊢ (∃ a, f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌

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

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

Proof state:
case h
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
⊢ f = 𝟙 ⦋1⦌

Tactic:
ext i : 3

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

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

Tactic:
exact e0

Result:
no goals

Proof state:
case h.a.h.h
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
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⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 1
⊢ f = ⦋1⦌.const ⦋1⦌ ((Hom.toOrderHom f) 0)

Tactic:
ext i : 3

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

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

Tactic:
decide

Result:
no goals

Proof state:
f : ⦋1⦌ ⟶ ⦋1⦌
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 0
⊢ (∃ a, f = ⦋1⦌.const ⦋1⦌ a) ∨ f = 𝟙 ⦋1⦌

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

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

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

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

Result:
no goals