Merge pull request #249 from teorth:golf

golf (using dot notation)

Author: teorth

analysis/Analysis/Appendix_A_3.lean

@@ -53,8 +53,8 @@ example {r:ℝ} (h: 0 < r) (h': r < 1) : Summable (fun n:ℕ ↦ n * r^n) := by
     use 1
     intro b hb
     simp [show b ≠ 0 by linarith, show r ≠ 0 by linarith]
-  suffices hconv: Filter.Tendsto (fun n:ℕ ↦ r * ((n+1) / n)) .atTop (nhds r)
-  . apply Filter.Tendsto.congr' _ hconv
+  suffices hconv: Filter.atTop.Tendsto (fun n:ℕ ↦ r * ((n+1) / n)) (nhds r)
+  . apply hconv.congr'
     simp [Filter.EventuallyEq, Filter.eventually_atTop]
     use 1
     intro b hb
@@ -63,18 +63,18 @@ example {r:ℝ} (h: 0 < r) (h': r < 1) : Summable (fun n:ℕ ↦ n * r^n) := by
     simp [abs_of_pos h, abs_of_pos hb1]
     field_simp
     ring_nf
-  suffices hconv : Filter.Tendsto (fun n:ℕ ↦ ((n+1:ℝ) / n)) .atTop (nhds 1)
-  . convert Filter.Tendsto.const_mul r hconv
+  suffices hconv : Filter.atTop.Tendsto (fun n:ℕ ↦ ((n+1:ℝ) / n)) (nhds 1)
+  . convert hconv.const_mul r
     simp
-  suffices hconv : Filter.Tendsto (fun n:ℕ ↦ 1 + 1/(n:ℝ)) .atTop (nhds 1)
-  . apply Filter.Tendsto.congr' _ hconv
+  suffices hconv : Filter.atTop.Tendsto (fun n:ℕ ↦ 1 + 1/(n:ℝ)) (nhds 1)
+  . apply hconv.congr'
     simp [Filter.EventuallyEq, Filter.eventually_atTop]
     use 1
     intro b hb
     have : (b:ℝ) > 0 := by norm_cast
     field_simp
-  suffices hconv : Filter.Tendsto (fun n:ℕ ↦ 1/(n:ℝ)) .atTop (nhds 0)
-  . convert Filter.Tendsto.const_add 1 hconv
+  suffices hconv : Filter.atTop.Tendsto (fun n:ℕ ↦ 1/(n:ℝ)) (nhds 0)
+  . convert hconv.const_add 1
     simp
   exact tendsto_one_div_atTop_nhds_zero_nat
 

analysis/Analysis/Appendix_B_2.lean

@@ -33,8 +33,7 @@ theorem NNRealDecimal.toNNReal_conv (d:NNRealDecimal) :
 theorem NNRealDecimal.surj (x:NNReal) : ∃ d:NNRealDecimal, x = d := by
   -- This proof is written to follow the structure of the original text.
   by_cases h : x = 0
-  . use mk 0 fun _ ↦ 0
-    simp [h, toNNReal]
+  . use mk 0 fun _ ↦ 0; simp [h, toNNReal]
   let s : ℕ → ℕ := fun n ↦ ⌊ x * 10^n ⌋₊
   have hs (n:ℕ) : s n ≤ x * 10^n := Nat.floor_le (by positivity)
   have hs' (n:ℕ) : x * 10^n < s n + 1 := Nat.lt_floor_add_one _
@@ -53,25 +52,22 @@ theorem NNRealDecimal.surj (x:NNReal) : ∃ d:NNRealDecimal, x = d := by
     have hd : d < 10 := by omega
     have : s (n+1) = 10 * s n + d := by omega
     use Digit.mk hd
-  set a : ℕ → Digit := fun n ↦ (hdigit n).choose
-  have ha (n:ℕ) : s (n+1) = 10 * s n + (a n : ℕ) := (hdigit n).choose_spec
+  choose a ha using hdigit
   set d := mk (s 0) a; use d
   have hsum (n:ℕ) : s n * (10:NNReal)^(-n:ℝ) = s 0 + ∑ i ∈ .range n, a i * (10:NNReal)^(-i-1:ℝ) := by
-    induction' n with n hn
-    . simp
+    induction' n with n hn; simp
     rw [ha n]; calc
       _ = s n * (10:NNReal)^(-n:ℝ) + a n * 10^(-n-1:ℝ) := by
         simp [add_mul]; congr 1 <;> ring_nf
         rw [mul_assoc, ←NNReal.rpow_add_one (by norm_num)]; congr; ring
       _ = s 0 + (∑ i ∈ .range n, a i * (10:NNReal)^(-i-1:ℝ) + a n * 10^(-n-1:ℝ)) := by
         rw [hn]; abel
-      _ = _ := by congr; exact (Finset.sum_range_succ _ _).symm
-  have := d.toNNReal_conv.tendsto_sum_tsum_nat
-  replace := this.const_add (s 0:NNReal)
-  convert_to Filter.Tendsto (fun n ↦ s n * (10:NNReal)^(-n:ℝ)) .atTop (nhds (d:NNReal)) at this
+      _ = _ := by congr; symm; apply Finset.sum_range_succ
+  have := (d.toNNReal_conv.tendsto_sum_tsum_nat).const_add (s 0:NNReal)
+  convert_to Filter.atTop.Tendsto (fun n ↦ s n * (10:NNReal)^(-n:ℝ)) (nhds (d:NNReal)) at this
   . ext n; rw [hsum n]
   apply tendsto_nhds_unique _ this
-  apply Filter.Tendsto.squeeze (g := fun n:ℕ ↦ x - (10:NNReal)^(-n:ℝ)) (h := fun n ↦ x)
+  apply Filter.Tendsto.squeeze (g := fun n:ℕ ↦ x - (10:NNReal)^(-n:ℝ)) (h := fun _ ↦ x)
   . convert Filter.Tendsto.const_sub (c := 0) x _
     . simp
     convert NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one
@@ -94,7 +90,7 @@ theorem NNRealDecimal.not_inj : (1:NNReal) = (mk 1 fun _ ↦ 0) ∧ (1:NNReal) =
   have := (mk 0 fun _ ↦ 9).toNNReal_conv.tendsto_sum_tsum_nat
   simp at this
   apply tendsto_nhds_unique _ this
-  convert_to Filter.Tendsto (fun n:ℕ ↦ 1 - (10:NNReal)^(-n:ℝ)) .atTop (nhds 1) using 2 with n
+  convert_to Filter.atTop.Tendsto (fun n:ℕ ↦ 1 - (10:NNReal)^(-n:ℝ)) (nhds 1) using 2 with n
   . induction' n with n hn
     . simp
     rw [Finset.sum_range_succ, hn, Nat.cast_add, Nat.cast_one, neg_add']
@@ -123,13 +119,8 @@ noncomputable instance RealDecimal.instCoeReal : Coe RealDecimal ℝ where
 
 theorem RealDecimal.surj (x:ℝ) : ∃ d:RealDecimal, x = d := by
   rcases le_or_gt 0 x with h | h
-  . obtain ⟨ d, hd ⟩ := NNRealDecimal.surj (x.toNNReal)
-    use pos d
-    simp [←hd, h]
-  . obtain ⟨ d, hd ⟩ := NNRealDecimal.surj ((-x).toNNReal)
-    use neg d
-    replace h : 0 ≤ -x := by linarith
-    simp [←hd, h]
+  . obtain ⟨ d, hd ⟩ := NNRealDecimal.surj (x.toNNReal); use pos d; simp [←hd, h]
+  . obtain ⟨ d, hd ⟩ := NNRealDecimal.surj ((-x).toNNReal); use neg d; simp [←hd, (show 0 ≤ -x by linarith)]
 
 /-- Exercise B.2.2 -/
 theorem RealDecimal.not_inj_one (d: RealDecimal) : (d:ℝ) = 1 ↔ (d = pos (NNRealDecimal.mk 1 fun _ ↦ 0) ∨ d = pos (NNRealDecimal.mk 0 fun _ ↦ 9)) := by

analysis/Analysis/Section_10_1.lean

@@ -28,25 +28,23 @@ variable (x₀ : ℝ)
 hypothesis that `x₀` is a limit point is not needed. -/
 theorem _root_.HasDerivWithinAt.iff (X: Set ℝ) (x₀ : ℝ) (f: ℝ → ℝ)
   (L:ℝ) :
-  HasDerivWithinAt f L X x₀ ↔ Filter.Tendsto (fun x ↦ (f x - f x₀) / (x - x₀))
-  (nhds x₀ ⊓ Filter.principal (X \ {x₀})) (nhds L) :=  by
+  HasDerivWithinAt f L X x₀ ↔ (nhds x₀ ⊓ .principal (X \ {x₀})).Tendsto (fun x ↦ (f x - f x₀) / (x - x₀))
+   (nhds L) :=  by
   rw [hasDerivWithinAt_iff_tendsto_slope, ←nhdsWithin.eq_1, iff_iff_eq, slope_fun_def_field]
 
 theorem _root_.DifferentiableWithinAt.iff (X: Set ℝ) (x₀ : ℝ) (f: ℝ → ℝ) :
   DifferentiableWithinAt ℝ f X x₀ ↔ ∃ L, HasDerivWithinAt f L X x₀ := by
   constructor
-  . intro h; use derivWithin f X x₀
-    exact DifferentiableWithinAt.hasDerivWithinAt h
-  intro ⟨ L, h ⟩
-  exact HasDerivWithinAt.differentiableWithinAt h
+  . intro h; use derivWithin f X x₀; exact h.hasDerivWithinAt
+  intro ⟨ L, h ⟩; exact h.differentiableWithinAt
 
 theorem _root_.DifferentiableWithinAt.of_hasDeriv {X: Set ℝ} {x₀ : ℝ} {f: ℝ → ℝ} {L:ℝ}
   (hL: HasDerivWithinAt f L X x₀) : DifferentiableWithinAt ℝ f X x₀ := by
   rw [DifferentiableWithinAt.iff]; use L
 
 
 theorem derivative_unique {X: Set ℝ} {x₀ : ℝ}
-  (hx₀: ClusterPt x₀ (Filter.principal (X \ {x₀}))) {f: ℝ → ℝ} {L L':ℝ}
+  (hx₀: ClusterPt x₀ (.principal (X \ {x₀}))) {f: ℝ → ℝ} {L L':ℝ}
   (hL: HasDerivWithinAt f L X x₀) (hL': HasDerivWithinAt f L' X x₀) :
   L = L' := by
     rw [_root_.HasDerivWithinAt.iff] at hL hL'
@@ -56,21 +54,21 @@ theorem derivative_unique {X: Set ℝ} {x₀ : ℝ}
 #check DifferentiableWithinAt.hasDerivWithinAt
 
 theorem derivative_unique' (X: Set ℝ) {x₀ : ℝ}
-  (hx₀: ClusterPt x₀ (Filter.principal (X \ {x₀}))) {f: ℝ → ℝ} {L :ℝ}
+  (hx₀: ClusterPt x₀ (.principal (X \ {x₀}))) {f: ℝ → ℝ} {L :ℝ}
   (hL: HasDerivWithinAt f L X x₀)
   (hdiff : DifferentiableWithinAt ℝ f X x₀):
   L = derivWithin f X x₀ := by
   solve_by_elim [derivative_unique, DifferentiableWithinAt.hasDerivWithinAt]
 
 
 /-- Example 10.1.3 -/
-example (x₀:ℝ) : HasDerivWithinAt (fun x ↦ x^2) (2 * x₀) (Set.univ) x₀ := by
+example (x₀:ℝ) : HasDerivWithinAt (fun x ↦ x^2) (2 * x₀) .univ x₀ := by
   sorry
 
-example (x₀:ℝ) : DifferentiableWithinAt ℝ (fun x ↦ x^2) (Set.univ) x₀ := by
+example (x₀:ℝ) : DifferentiableWithinAt ℝ (fun x ↦ x^2) .univ x₀ := by
   sorry
 
-example (x₀:ℝ) : derivWithin (fun x ↦ x^2) (Set.univ) x₀ = 2 * x₀ := by
+example (x₀:ℝ) : derivWithin (fun x ↦ x^2) .univ x₀ = 2 * x₀ := by
   sorry
 
 /-- Remark 10.1.4 -/
@@ -89,30 +87,28 @@ example : ∃ (X: Set ℝ) (x₀ :ℝ) (f g: ℝ → ℝ) (L:ℝ) (hfg: f x₀ =
 
 abbrev f_10_1_6 : ℝ → ℝ := abs
 
-example : Filter.Tendsto (fun x ↦ (f_10_1_6 x - f_10_1_6 0) / (x - 0))
-  (nhds 0 ⊓ Filter.principal (Set.Ioi 0)) (nhds 1) := by
+example : (nhds 0 ⊓ .principal (.Ioi 0)).Tendsto (fun x ↦ (f_10_1_6 x - f_10_1_6 0) / (x - 0)) (nhds 1) := by
   sorry
 
-example : Filter.Tendsto (fun x ↦ (f_10_1_6 x - f_10_1_6 0) / (x - 0))
-  (nhds 0 ⊓ Filter.principal (Set.Iio 0)) (nhds (-1)) := by
+example : (nhds 0 ⊓ .principal (.Iio 0)).Tendsto (fun x ↦ (f_10_1_6 x - f_10_1_6 0) / (x - 0)) (nhds (-1)) := by
   sorry
 
-example : ¬ ∃ L, Filter.Tendsto (fun x ↦ (f_10_1_6 x - f_10_1_6 0) / (x - 0))
-  (nhds 0 ⊓ Filter.principal (Set.univ \ {0})) (nhds L) := by sorry
+example : ¬ ∃ L, (nhds 0 ⊓ .principal (.univ \ {0})).Tendsto (fun x ↦ (f_10_1_6 x - f_10_1_6 0) / (x - 0))
+   (nhds L) := by sorry
 
-example : ¬ DifferentiableWithinAt ℝ f_10_1_6 (Set.univ) 0 := by
+example : ¬ DifferentiableWithinAt ℝ f_10_1_6 (.univ) 0 := by
   sorry
 
-example : DifferentiableWithinAt ℝ f_10_1_6 (Set.Ioi 0) 0 := by
+example : DifferentiableWithinAt ℝ f_10_1_6 (.Ioi 0) 0 := by
   sorry
 
-example : derivWithin f_10_1_6 (Set.Ioi 0) 0 = 1 := by
+example : derivWithin f_10_1_6 (.Ioi 0) 0 = 1 := by
   sorry
 
-example : DifferentiableWithinAt ℝ f_10_1_6 (Set.Iio 0) 0 := by
+example : DifferentiableWithinAt ℝ f_10_1_6 (.Iio 0) 0 := by
   sorry
 
-example : derivWithin f_10_1_6 (Set.Iio 0) 0 = -1 := by
+example : derivWithin f_10_1_6 (.Iio 0) 0 = -1 := by
   sorry
 
 /-- Proposition 10.1.7 (Newton's approximation) / Exercise 10.1.2 -/
@@ -181,7 +177,7 @@ theorem _root_.HasDerivWithinAt.of_div {X: Set ℝ} {x₀ f'x₀ g'x₀: ℝ}
   HasDerivWithinAt (f / g) ((f'x₀ * (g x₀) - (f x₀) * g'x₀) / (g x₀)^2) X x₀ := by
   sorry
 
-example (x₀:ℝ) (hx₀: x₀ ≠ 1): HasDerivWithinAt (fun x ↦ (x-2)/(x-1)) (1 /(x₀-1)^2) (Set.univ \ {1}) x₀ := by
+example (x₀:ℝ) (hx₀: x₀ ≠ 1): HasDerivWithinAt (fun x ↦ (x-2)/(x-1)) (1 /(x₀-1)^2) (.univ \ {1}) x₀ := by
   sorry
 
 /-- Theorem 10.1.15 (Chain rule) / Exercise 10.1.7 -/
@@ -193,12 +189,12 @@ theorem _root_.HasDerivWithinAt.of_comp {X Y: Set ℝ} {x₀ y₀ f'x₀ g'y₀:
 
 /-- Exercise 10.1.5 -/
 theorem _root_.HasDerivWithinAt.of_pow (n:ℕ) (x₀:ℝ) : HasDerivWithinAt (fun x ↦ x^n)
-(n * x₀^((n:ℤ)-1)) (Set.univ) x₀ := by
+(n * x₀^((n:ℤ)-1)) .univ x₀ := by
   sorry
 
 /-- Exercise 10.1.6 -/
 theorem _root_.HasDerivWithinAt.of_zpow (n:ℤ) (x₀:ℝ) (hx₀: x₀ ≠ 0) :
-  HasDerivWithinAt (fun x ↦ x^n) (n * x₀^(n-1)) (Set.univ \ {0}) x₀ := by
+  HasDerivWithinAt (fun x ↦ x^n) (n * x₀^(n-1)) (.univ \ {0}) x₀ := by
   sorry
 
 

analysis/Analysis/Section_10_2.lean

@@ -23,7 +23,7 @@ namespace Chapter10
 /-- Definition 10.2.1 (Local maxima and minima).  Here we use Mathlib's `IsLocalMaxOn` type. -/
 theorem IsLocalMaxOn.iff (X:Set ℝ) (f:ℝ → ℝ) (x₀:ℝ) :
   IsLocalMaxOn f X x₀ ↔
-  ∃ δ > 0, IsMaxOn f (X ∩ Set.Ioo (x₀ - δ) (x₀ + δ)) x₀ := by
+  ∃ δ > 0, IsMaxOn f (X ∩ .Ioo (x₀ - δ) (x₀ + δ)) x₀ := by
   simp [isMaxOn_iff, IsLocalMaxOn, IsMaxFilter, nhdsWithin.eq_1, Filter.eventually_inf_principal,
         Metric.eventually_nhds_iff, Real.dist_eq, abs_sub_lt_iff ]
   peel with ε hε x
@@ -33,7 +33,7 @@ theorem IsLocalMaxOn.iff (X:Set ℝ) (f:ℝ → ℝ) (x₀:ℝ) :
 
 theorem IsLocalMinOn.iff (X:Set ℝ) (f:ℝ → ℝ) (x₀:ℝ) :
   IsLocalMinOn f X x₀ ↔
-  ∃ δ > 0, IsMinOn f (X ∩ Set.Ioo (x₀ - δ) (x₀ + δ)) x₀ := by
+  ∃ δ > 0, IsMinOn f (X ∩ .Ioo (x₀ - δ) (x₀ + δ)) x₀ := by
   simp [isMinOn_iff, IsLocalMinOn, IsMinFilter, nhdsWithin.eq_1, Filter.eventually_inf_principal,
         Metric.eventually_nhds_iff, Real.dist_eq, abs_sub_lt_iff ]
   peel with ε hε x
@@ -44,20 +44,20 @@ theorem IsLocalMinOn.iff (X:Set ℝ) (f:ℝ → ℝ) (x₀:ℝ) :
 /-- Example 10.2.3 -/
 abbrev f_10_2_3 : ℝ → ℝ := fun x ↦ x^2 - x^4
 
-example : ¬ IsMinOn f_10_2_3 Set.univ 0 := by sorry
+example : ¬ IsMinOn f_10_2_3 .univ 0 := by sorry
 
-example : IsMinOn f_10_2_3 (Set.Ioo (-1) 1) 0 := by sorry
+example : IsMinOn f_10_2_3 (.Ioo (-1) 1) 0 := by sorry
 
-example : IsLocalMaxOn f_10_2_3 Set.univ 0 := by sorry
+example : IsLocalMaxOn f_10_2_3 .univ 0 := by sorry
 
 /-- Example 10.2.4 -/
-example : ¬ ∃ x, IsMaxOn (· : ℝ → ℝ)  ((↑· : ℤ → ℝ) '' Set.univ) x := by sorry
+example : ¬ ∃ x, IsMaxOn (· : ℝ → ℝ)  ((↑· : ℤ → ℝ) '' .univ) x := by sorry
 
-example : ¬ ∃ x, IsMinOn (· : ℝ → ℝ)  ((↑· : ℤ → ℝ) '' Set.univ) x := by sorry
+example : ¬ ∃ x, IsMinOn (· : ℝ → ℝ)  ((↑· : ℤ → ℝ) '' .univ) x := by sorry
 
-example (n:ℤ) : IsMaxOn (· : ℝ → ℝ)  ((↑· : ℤ → ℝ) '' Set.univ) n := by sorry
+example (n:ℤ) : IsMaxOn (· : ℝ → ℝ)  ((↑· : ℤ → ℝ) '' .univ) n := by sorry
 
-example (n:ℤ) : IsMinOn (· : ℝ → ℝ)  ((↑· : ℤ → ℝ) '' Set.univ) n := by sorry
+example (n:ℤ) : IsMinOn (· : ℝ → ℝ)  ((↑· : ℤ → ℝ) '' .univ) n := by sorry
 
 /-- Remark 10.2.5 -/
 theorem IsLocalMaxOn.of_restrict {X Y:Set ℝ} (hXY: Y ⊆ X) (f:ℝ → ℝ) (x₀:ℝ)
@@ -70,59 +70,59 @@ theorem IsLocalMinOn.of_restrict {X Y:Set ℝ} (hXY: Y ⊆ X) (f:ℝ → ℝ) (x
 
 /-- Proposition 10.2.6 (Local extrema are stationary) / Exercise 10.2.1 -/
 theorem IsLocalMaxOn.deriv_eq_zero {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} {x₀:ℝ}
-  (hx₀: x₀ ∈ Set.Ioo a b) (h: IsLocalMaxOn f (Set.Ioo a b) x₀) {L:ℝ}
-  (hderiv: HasDerivWithinAt f L (Set.Ioo a b) x₀) : L = 0 := by
+  (hx₀: x₀ ∈ Set.Ioo a b) (h: IsLocalMaxOn f (.Ioo a b) x₀) {L:ℝ}
+  (hderiv: HasDerivWithinAt f L (.Ioo a b) x₀) : L = 0 := by
   sorry
 
 /-- Proposition 10.2.6 (Local extrema are stationary) / Exercise 10.2.1 -/
 theorem IsLocalMinOn.deriv_eq_zero {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} {x₀:ℝ}
-  (hx₀: x₀ ∈ Set.Ioo a b) (h: IsLocalMinOn f (Set.Ioo a b) x₀) {L:ℝ}
-  (hderiv: HasDerivWithinAt f L (Set.Ioo a b) x₀) : L = 0 := by
+  (hx₀: x₀ ∈ Set.Ioo a b) (h: IsLocalMinOn f (.Ioo a b) x₀) {L:ℝ}
+  (hderiv: HasDerivWithinAt f L (.Ioo a b) x₀) : L = 0 := by
   sorry
 
 theorem IsMaxOn.deriv_eq_zero_counter : ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ)
-  (x₀:ℝ) (hx₀: x₀ ∈ Set.Icc a b) (h: IsMaxOn f (Set.Icc a b) x₀) (L:ℝ)
-  (hderiv: HasDerivWithinAt f L (Set.Icc a b) x₀), L ≠ 0 := by
+  (x₀:ℝ) (hx₀: x₀ ∈ Set.Icc a b) (h: IsMaxOn f (.Icc a b) x₀) (L:ℝ)
+  (hderiv: HasDerivWithinAt f L (.Icc a b) x₀), L ≠ 0 := by
   sorry
 
 /-- Theorem 10.2.7 (Rolle's theorem) / Exercise 10.2.4 -/
 theorem _root_.HasDerivWithinAt.exist_zero {a b:ℝ} (hab: a < b) {g:ℝ → ℝ}
-  (hcont: ContinuousOn g (Set.Icc a b)) (hderiv: DifferentiableOn ℝ g (Set.Ioo a b))
-  (hgab: g a = g b) : ∃ x ∈ Set.Ioo a b, HasDerivWithinAt g 0 (Set.Ioo a b) x := by
+  (hcont: ContinuousOn g (.Icc a b)) (hderiv: DifferentiableOn ℝ g (.Ioo a b))
+  (hgab: g a = g b) : ∃ x ∈ Set.Ioo a b, HasDerivWithinAt g 0 (.Ioo a b) x := by
   sorry
 
 /-- Corollary 10.2.9 (Mean value theorem ) / Exercise 10.2.5 -/
 theorem _root_.HasDerivWithinAt.mean_value {a b:ℝ} (hab: a < b) {f:ℝ → ℝ}
-  (hcont: ContinuousOn f (Set.Icc a b)) (hderiv: DifferentiableOn ℝ f (Set.Ioo a b)) :
-  ∃ x ∈ Set.Ioo a b, HasDerivWithinAt f ((f b - f a) / (b - a)) (Set.Ioo a b) x := by
+  (hcont: ContinuousOn f (.Icc a b)) (hderiv: DifferentiableOn ℝ f (.Ioo a b)) :
+  ∃ x ∈ Set.Ioo a b, HasDerivWithinAt f ((f b - f a) / (b - a)) (.Ioo a b) x := by
   sorry
 
 /-- Exercise 10.2.2 -/
-example : ∃ f:ℝ → ℝ, ContinuousOn f (Set.Icc (-1) 1) ∧
-  IsMaxOn f (Set.Icc (-1) 1) 0 ∧ ¬ DifferentiableWithinAt ℝ f (Set.Icc (-1) 1) 0 := by
+example : ∃ f:ℝ → ℝ, ContinuousOn f (.Icc (-1) 1) ∧
+  IsMaxOn f (.Icc (-1) 1) 0 ∧ ¬ DifferentiableWithinAt ℝ f (.Icc (-1) 1) 0 := by
   sorry
 
 /-- Exercise 10.2.3 -/
-example : ∃ f:ℝ → ℝ, DifferentiableOn ℝ f (Set.Icc (-1) 1) ∧
-  HasDerivWithinAt f 0 (Set.Ioo (-1) 1) 0 ∧
-  ¬ IsLocalMaxOn f (Set.Icc (-1) 1) 0 ∧ ¬ IsLocalMinOn f (Set.Icc (-1) 1) 0 := by
+example : ∃ f:ℝ → ℝ, DifferentiableOn ℝ f (.Icc (-1) 1) ∧
+  HasDerivWithinAt f 0 (.Ioo (-1) 1) 0 ∧
+  ¬ IsLocalMaxOn f (.Icc (-1) 1) 0 ∧ ¬ IsLocalMinOn f (.Icc (-1) 1) 0 := by
   sorry
 
 /-- Exercise 10.2.6 -/
 theorem lipschitz_bound {M a b:ℝ} (hM: M > 0) (hab: a < b) {f:ℝ → ℝ}
-  (hcont: ContinuousOn f (Set.Icc a b))
-  (hderiv: DifferentiableOn ℝ f (Set.Ioo a b))
-  (hlip: ∀ x ∈ Set.Ioo a b, |derivWithin f (Set.Ioo a b) x| ≤ M)
+  (hcont: ContinuousOn f (.Icc a b))
+  (hderiv: DifferentiableOn ℝ f (.Ioo a b))
+  (hlip: ∀ x ∈ Set.Ioo a b, |derivWithin f (.Ioo a b) x| ≤ M)
   {x y:ℝ} (hx: x ∈ Set.Ioo a b) (hy: y ∈ Set.Ioo a b) :
   |f x - f y| ≤ M * |x - y| := by
   sorry
 
 /-- Exercise 10.2.7 -/
 theorem _root_.UniformContinuousOn.of_lipschitz {f:ℝ → ℝ}
-  (hcont: ContinuousOn f Set.univ)
-  (hderiv: DifferentiableOn ℝ f Set.univ)
-  (hlip: BddOn (deriv f) Set.univ) :
-  UniformContinuousOn f (Set.univ) := by
+  (hcont: ContinuousOn f .univ)
+  (hderiv: DifferentiableOn ℝ f .univ)
+  (hlip: BddOn (deriv f) .univ) :
+  UniformContinuousOn f (.univ) := by
   sorry
 
 

analysis/Analysis/Section_10_3.lean

@@ -17,25 +17,25 @@ Main constructions and results of this section:
 namespace Chapter10
 
 /-- Proposition 10.3.1 / Exercise 10.3.1 -/
-theorem derivative_of_monotone (X:Set ℝ) {x₀:ℝ} (hx₀: ClusterPt x₀ (Filter.principal (X \ {x₀})))
+theorem derivative_of_monotone (X:Set ℝ) {x₀:ℝ} (hx₀: ClusterPt x₀ (.principal (X \ {x₀})))
   {f:ℝ → ℝ} (hmono: Monotone f) (hderiv: DifferentiableWithinAt ℝ f X x₀) :
     derivWithin f X x₀ ≥ 0 := by
   sorry
 
-theorem derivative_of_antitone (X:Set ℝ) {x₀:ℝ} (hx₀: ClusterPt x₀ (Filter.principal (X \ {x₀})))
+theorem derivative_of_antitone (X:Set ℝ) {x₀:ℝ} (hx₀: ClusterPt x₀ (.principal (X \ {x₀})))
   {f:ℝ → ℝ} (hmono: Antitone f) (hderiv: DifferentiableWithinAt ℝ f X x₀) :
     derivWithin f X x₀ ≤ 0 := by
   sorry
 
 /-- Proposition 10.3.3 / Exercise 10.3.4 -/
 theorem strictMono_of_positive_derivative {a b:ℝ} (hab: a < b) {f:ℝ → ℝ}
-  (hderiv: DifferentiableOn ℝ f (Set.Icc a b)) (hpos: ∀ x ∈ Set.Ioo a b, derivWithin f (Set.Icc a b) x > 0) :
-    StrictMonoOn f (Set.Icc a b) := by
+  (hderiv: DifferentiableOn ℝ f (.Icc a b)) (hpos: ∀ x ∈ Set.Ioo a b, derivWithin f (.Icc a b) x > 0) :
+    StrictMonoOn f (.Icc a b) := by
   sorry
 
 theorem strictAnti_of_negative_derivative {a b:ℝ} (hab: a < b) {f:ℝ → ℝ}
-  (hderiv: DifferentiableOn ℝ f (Set.Icc a b)) (hneg: ∀ x ∈ Set.Ioo a b, derivWithin f (Set.Icc a b) x < 0) :
-    StrictAntiOn f (Set.Icc a b) := by
+  (hderiv: DifferentiableOn ℝ f (.Icc a b)) (hneg: ∀ x ∈ Set.Ioo a b, derivWithin f (.Icc a b) x < 0) :
+    StrictAntiOn f (.Icc a b) := by
   sorry
 
 /-- Example 10.3.2 -/