-- Mathlib/Topology/Order/IntermediateValue.lean
theorem ContinuousOn.strictMonoOn_of_injOn_Ioo {a b : α} {f : α → δ} (hab : a < b)
    (hf_c : ContinuousOn f (Ioo a b)) (hf_i : InjOn f (Ioo a b)) :
    StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)

Proof state:
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
this : Inhabited ↑(Ioo a b)
g : ↑(Ioo a b) → δ := (Ioo a b).restrict f
⊢ StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)

Tactic:
have : StrictMono g ∨ StrictAnti g :=
  Continuous.strictMono_of_inj hf_c.restrict hf_i.injective

Result:
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
this✝ : Inhabited ↑(Ioo a b)
g : ↑(Ioo a b) → δ := (Ioo a b).restrict f
this : StrictMono g ∨ StrictAnti g
⊢ StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)

Proof state:
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
this : Inhabited ↑(Ioo a b)
⊢ StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)

Tactic:
let g : Ioo a b → δ := Set.restrict (Ioo a b) f

Result:
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
this : Inhabited ↑(Ioo a b)
g : ↑(Ioo a b) → δ := (Ioo a b).restrict f
⊢ StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)

Proof state:
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
this✝ : Inhabited ↑(Ioo a b)
g : ↑(Ioo a b) → δ := (Ioo a b).restrict f
this : StrictMono g ∨ StrictAnti g
⊢ StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)

Tactic:
exact this.imp strictMono_restrict.mp strictAntiOn_iff_strictAnti.mpr

Result:
no goals

Proof state:
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
⊢ StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)

Tactic:
haveI : Inhabited (Ioo a b) := Classical.inhabited_of_nonempty (nonempty_Ioo_subtype hab)

Result:
α : Type u
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
this : Inhabited ↑(Ioo a b)
⊢ StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)