Theorem: exercise6_5 (LeanCourse/Assignments/Assignment6.lean)

State before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
⊢ StrictMono f ∨ StrictAnti f
Tactic:
have h3f : ∀ {a b : ℝ} (hab : a ≤ b) (h2ab : f a < f b), StrictMonoOn f (Iic b)
State after:
case h3f
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
⊢ ∀ {a b : ℝ}, a ≤ b → f a < f b → StrictMonoOn f (Iic b)

α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
h3f : ∀ {a b : ℝ}, a ≤ b → f a < f b → StrictMonoOn f (Iic b)
⊢ StrictMono f ∨ StrictAnti f

State before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
h3f : ∀ {a b : ℝ}, a ≤ b → f a < f b → StrictMonoOn f (Iic b)
⊢ StrictMono f ∨ StrictAnti f
Tactic:
sorry
State after:
no goals

State before:
case h3f
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
⊢ ∀ {a b : ℝ}, a ≤ b → f a < f b → StrictMonoOn f (Iic b)
Tactic:
intro a b hab h2ab
State after:
case h3f
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
a b : ℝ
hab : a ≤ b
h2ab : f a < f b
⊢ StrictMonoOn f (Iic b)

State before:
case h3f
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
a b : ℝ
hab : a ≤ b
h2ab : f a < f b
⊢ StrictMonoOn f (Iic b)
Tactic:
have := exercise6_4 (OrderDual ℝ) hf h2f hab h2ab
State after:
case h3f
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
a b : ℝ
hab : a ≤ b
h2ab : f a < f b
this : StrictMonoOn f (Ici b)
⊢ StrictMonoOn f (Iic b)

State before:
case h3f
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
a b : ℝ
hab : a ≤ b
h2ab : f a < f b
this : StrictMonoOn f (Ici b)
⊢ StrictMonoOn f (Iic b)
Tactic:
convert this using 0
State after:
case a
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
a b : ℝ
hab : a ≤ b
h2ab : f a < f b
this : StrictMonoOn f (Ici b)
⊢ StrictMonoOn f (Iic b) ↔ StrictMonoOn f (Ici b)

State before:
case a
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : ℝ → ℝ
hf : Continuous f
h2f : Injective f
a b : ℝ
hab : a ≤ b
h2ab : f a < f b
this : StrictMonoOn f (Ici b)
⊢ StrictMonoOn f (Iic b) ↔ StrictMonoOn f (Ici b)
Tactic:
exact strict_mono_on_dual_iff.symm
State after:
no goals