-- Mathlib/Topology/Order/IntermediateValue.lean
theorem Continuous.strictMono_of_inj {f : α → δ}
    (hf_c : Continuous f) (hf_i : Injective f) : StrictMono f ∨ StrictAnti f

Proof state:
case pos
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
hn : Nonempty α
a : α := Classical.choice hn
⊢ StrictMono f ∨ StrictAnti f

Tactic:
by_cases h : ∃ b : α, a ≠ b

Result:
case pos
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
hn : Nonempty α
a : α := Classical.choice hn
h : ∃ b, a ≠ b
⊢ StrictMono f ∨ StrictAnti f

case neg
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
hn : Nonempty α
a : α := Classical.choice hn
h : ¬∃ b, a ≠ b
⊢ StrictMono f ∨ StrictAnti f

Proof state:
case neg
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
hn : Nonempty α
a : α := Classical.choice hn
h : ∀ (b : α), a = b
⊢ StrictMono f ∨ StrictAnti f

Tactic:
haveI : Subsingleton α := ⟨fun c d => Trans.trans (h c).symm (h d)⟩

Result:
case neg
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
hn : Nonempty α
a : α := Classical.choice hn
h : ∀ (b : α), a = b
this : Subsingleton α
⊢ StrictMono f ∨ StrictAnti f

Proof state:
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
⊢ StrictMono f ∨ StrictAnti f

Tactic:
by_cases hn : Nonempty α

Result:
case pos
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
hn : Nonempty α
⊢ StrictMono f ∨ StrictAnti f

case neg
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
hn : ¬Nonempty α
⊢ StrictMono f ∨ StrictAnti f

Proof state:
case pos
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
hn : Nonempty α
a : α := Classical.choice hn
h : ∃ b, a ≠ b
⊢ StrictMono f ∨ StrictAnti f

Tactic:
choose b hb using h

Result:
case pos
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
hn : Nonempty α
a : α := Classical.choice hn
b : α
hb : a ≠ b
⊢ StrictMono f ∨ StrictAnti f

Proof state:
case neg
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
hn : Nonempty α
a : α := Classical.choice hn
b : α
hb : a ≠ b
hab : b ≤ a
this : b < a
⊢ StrictMono f ∨ StrictAnti f

Tactic:
exact H this

Result:
no goals

Proof state:
case neg
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
hn : Nonempty α
a : α := Classical.choice hn
b : α
hb : a ≠ b
hab : ¬a < b
⊢ StrictMono f ∨ StrictAnti f

Tactic:
push_neg at hab

Result:
case neg
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
hn : Nonempty α
a : α := Classical.choice hn
b : α
hb : a ≠ b
hab : b ≤ a
⊢ StrictMono f ∨ StrictAnti f

Proof state:
case neg
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
hn : Nonempty α
a : α := Classical.choice hn
h : ∀ (b : α), a = b
this : Subsingleton α
⊢ StrictMono f ∨ StrictAnti f

Tactic:
exact Or.inl <| Subsingleton.strictMono f

Result:
no goals

Proof state:
case pos
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
hn : Nonempty α
a : α := Classical.choice hn
b : α
hb : a ≠ b
⊢ StrictMono f ∨ StrictAnti f

Tactic:
by_cases hab : a < b

Result:
case pos
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
hn : Nonempty α
a : α := Classical.choice hn
b : α
hb : a ≠ b
hab : a < b
⊢ StrictMono f ∨ StrictAnti f

case neg
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
hn : Nonempty α
a : α := Classical.choice hn
b : α
hb : a ≠ b
hab : ¬a < b
⊢ StrictMono f ∨ StrictAnti f