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

State before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
⊢ ¬DifferentiableAt ℝ (fun x => |x|) 0
Tactic:
intro h
State after:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
⊢ False

State before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
⊢ False
Tactic:
have h1 : HasDerivWithinAt (fun x : ℝ ↦ |x|) 1 (Ici 0) 0
State after:
case h1
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
⊢ HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0

α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
⊢ False

State before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
⊢ False
Tactic:
have h2 : HasDerivWithinAt (fun x : ℝ ↦ |x|) (-1) (Iic 0) 0
State after:
case h2
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
⊢ HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0

α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
h2 : HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
⊢ False

State before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
h2 : HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
⊢ False
Tactic:
have h3 : UniqueDiffWithinAt ℝ (Ici (0 : ℝ)) 0 := by
  sorry
State after:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
h2 : HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
h3 : UniqueDiffWithinAt ℝ (Ici 0) 0
⊢ False

State before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
h2 : HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
h3 : UniqueDiffWithinAt ℝ (Ici 0) 0
⊢ False
Tactic:
have h4 : UniqueDiffWithinAt ℝ (Iic (0 : ℝ)) 0 := by
  sorry
State after:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
h2 : HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
h3 : UniqueDiffWithinAt ℝ (Ici 0) 0
h4 : UniqueDiffWithinAt ℝ (Iic 0) 0
⊢ False

State before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
h2 : HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
h3 : UniqueDiffWithinAt ℝ (Ici 0) 0
h4 : UniqueDiffWithinAt ℝ (Iic 0) 0
⊢ False
Tactic:
sorry
State after:
no goals

State before:
case h1
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
⊢ HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
Tactic:
sorry
State after:
no goals

State before:
case h2
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
⊢ HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
Tactic:
sorry
State after:
no goals

State before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
h2 : HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
⊢ UniqueDiffWithinAt ℝ (Ici 0) 0
Tactic:
sorry
State after:
no goals

State before:
α : Type u_1
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
h : DifferentiableAt ℝ (fun x => |x|) 0
h1 : HasDerivWithinAt (fun x => |x|) 1 (Ici 0) 0
h2 : HasDerivWithinAt (fun x => |x|) (-1) (Iic 0) 0
h3 : UniqueDiffWithinAt ℝ (Ici 0) 0
⊢ UniqueDiffWithinAt ℝ (Iic 0) 0
Tactic:
sorry
State after:
no goals