chore(Geometry/Manifold/Algebra): golf using custom elaborators (leanprover-community#36007)

Author: grunweg

Mathlib/Geometry/Manifold/Algebra/LieGroup.lean

@@ -6,6 +6,7 @@ Authors: Nicolò Cavalleri
 module
 
 public import Mathlib.Geometry.Manifold.Algebra.Monoid
+import Mathlib.Geometry.Manifold.Notation
 
 /-!
 # Lie groups
@@ -63,7 +64,7 @@ class LieAddGroup {𝕜 : Type*} [NontriviallyNormedField 𝕜] {H : Type*} [Top
     (n : WithTop ℕ∞) (G : Type*)
     [AddGroup G] [TopologicalSpace G] [ChartedSpace H G] : Prop extends ContMDiffAdd I n G where
   /-- Negation is smooth in an additive Lie group. -/
-  contMDiff_neg : ContMDiff I I n fun a : G => -a
+  contMDiff_neg : CMDiff n fun a : G ↦ -a
 
 -- See note [Design choices about smooth algebraic structures]
 /-- A (multiplicative) Lie group is a group and a `C^n` manifold at the same time in which
@@ -74,7 +75,7 @@ class LieGroup {𝕜 : Type*} [NontriviallyNormedField 𝕜] {H : Type*} [Topolo
     (n : WithTop ℕ∞) (G : Type*)
     [Group G] [TopologicalSpace G] [ChartedSpace H G] : Prop extends ContMDiffMul I n G where
   /-- Inversion is smooth in a Lie group. -/
-  contMDiff_inv : ContMDiff I I n fun a : G => a⁻¹
+  contMDiff_inv : CMDiff n fun a : G ↦ a⁻¹
 
 /-!
   ### Smoothness of inversion, negation, division and subtraction
@@ -122,7 +123,7 @@ variable (I n)
 
 /-- In a Lie group, inversion is `C^n`. -/
 @[to_additive /-- In an additive Lie group, inversion is a smooth map. -/]
-theorem contMDiff_inv : ContMDiff I I n fun x : G => x⁻¹ :=
+theorem contMDiff_inv : CMDiff n fun x : G ↦ x⁻¹ :=
   LieGroup.contMDiff_inv
 
 include I n in
@@ -137,41 +138,41 @@ end
 
 @[to_additive]
 theorem ContMDiffWithinAt.inv {f : M → G} {s : Set M} {x₀ : M}
-    (hf : ContMDiffWithinAt I' I n f s x₀) : ContMDiffWithinAt I' I n (fun x => (f x)⁻¹) s x₀ :=
+    (hf : CMDiffAt[s] n f x₀) : CMDiffAt[s] n (fun x ↦ (f x)⁻¹) x₀ :=
   (contMDiff_inv I n).contMDiffAt.contMDiffWithinAt.comp x₀ hf <| Set.mapsTo_univ _ _
 
 @[to_additive]
-theorem ContMDiffAt.inv {f : M → G} {x₀ : M} (hf : ContMDiffAt I' I n f x₀) :
-    ContMDiffAt I' I n (fun x => (f x)⁻¹) x₀ :=
+theorem ContMDiffAt.inv {f : M → G} {x₀ : M} (hf : CMDiffAt n f x₀) :
+    CMDiffAt n (fun x ↦ (f x)⁻¹) x₀ :=
   (contMDiff_inv I n).contMDiffAt.comp x₀ hf
 
 @[to_additive]
-theorem ContMDiffOn.inv {f : M → G} {s : Set M} (hf : ContMDiffOn I' I n f s) :
-    ContMDiffOn I' I n (fun x => (f x)⁻¹) s := fun x hx => (hf x hx).inv
+theorem ContMDiffOn.inv {f : M → G} {s : Set M} (hf : CMDiff[s] n f) :
+    CMDiff[s] n (fun x ↦ (f x)⁻¹) := fun x hx ↦ (hf x hx).inv
 
 @[to_additive]
-theorem ContMDiff.inv {f : M → G} (hf : ContMDiff I' I n f) : ContMDiff I' I n fun x => (f x)⁻¹ :=
-  fun x => (hf x).inv
+theorem ContMDiff.inv {f : M → G} (hf : CMDiff n f) : CMDiff n fun x ↦ (f x)⁻¹ :=
+  fun x ↦ (hf x).inv
 
 @[to_additive]
 theorem ContMDiffWithinAt.div {f g : M → G} {s : Set M} {x₀ : M}
-    (hf : ContMDiffWithinAt I' I n f s x₀) (hg : ContMDiffWithinAt I' I n g s x₀) :
-    ContMDiffWithinAt I' I n (fun x => f x / g x) s x₀ := by
+    (hf : CMDiffAt[s] n f x₀) (hg : CMDiffAt[s] n g x₀) :
+    CMDiffAt[s] n (fun x ↦ f x / g x) x₀ := by
   simp_rw [div_eq_mul_inv]; exact hf.mul hg.inv
 
 @[to_additive]
-theorem ContMDiffAt.div {f g : M → G} {x₀ : M} (hf : ContMDiffAt I' I n f x₀)
-    (hg : ContMDiffAt I' I n g x₀) : ContMDiffAt I' I n (fun x => f x / g x) x₀ := by
+theorem ContMDiffAt.div {f g : M → G} {x₀ : M} (hf : CMDiffAt n f x₀)
+    (hg : CMDiffAt n g x₀) : CMDiffAt n (fun x ↦ f x / g x) x₀ := by
   simp_rw [div_eq_mul_inv]; exact hf.mul hg.inv
 
 @[to_additive]
-theorem ContMDiffOn.div {f g : M → G} {s : Set M} (hf : ContMDiffOn I' I n f s)
-    (hg : ContMDiffOn I' I n g s) : ContMDiffOn I' I n (fun x => f x / g x) s := by
+theorem ContMDiffOn.div {f g : M → G} {s : Set M} (hf : CMDiff[s] n f)
+    (hg : CMDiff[s] n g) : CMDiff[s] n (fun x ↦ f x / g x) := by
   simp_rw [div_eq_mul_inv]; exact hf.mul hg.inv
 
 @[to_additive]
-theorem ContMDiff.div {f g : M → G} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) :
-    ContMDiff I' I n fun x => f x / g x := by simp_rw [div_eq_mul_inv]; exact hf.mul hg.inv
+theorem ContMDiff.div {f g : M → G} (hf : CMDiff n f) (hg : CMDiff n g) :
+    CMDiff n fun x ↦ f x / g x := by simp_rw [div_eq_mul_inv]; exact hf.mul hg.inv
 
 end PointwiseDivision
 
@@ -212,7 +213,7 @@ class ContMDiffInv₀ {𝕜 : Type*} [NontriviallyNormedField 𝕜] {H : Type*}
     (n : WithTop ℕ∞) (G : Type*)
     [Inv G] [Zero G] [TopologicalSpace G] [ChartedSpace H G] : Prop where
   /-- Inversion is `C^n` away from `0`. -/
-  contMDiffAt_inv₀ : ∀ ⦃x : G⦄, x ≠ 0 → ContMDiffAt I I n (fun y ↦ y⁻¹) x
+  contMDiffAt_inv₀ : ∀ ⦃x : G⦄, x ≠ 0 → CMDiffAt n (fun (y : G) ↦ y⁻¹) x
 
 instance {𝕜 : Type*} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} : ContMDiffInv₀ 𝓘(𝕜) n 𝕜 where
   contMDiffAt_inv₀ x hx := by
@@ -241,7 +242,7 @@ instance {a : WithTop ℕ∞} [ContMDiffInv₀ I ω G] : ContMDiffInv₀ I a G :
 instance [ContinuousInv₀ G] : ContMDiffInv₀ I 0 G := by
   have : T1Space G := I.t1Space G
   constructor
-  have A : ContMDiffOn I I 0 (fun (x : G) ↦ x⁻¹) {0}ᶜ := by
+  have A : CMDiff[{0}ᶜ] 0 (fun (x : G) ↦ x⁻¹) := by
     rw [contMDiffOn_zero_iff]
     exact continuousOn_inv₀
   intro x hx
@@ -267,25 +268,24 @@ theorem continuousInv₀_of_contMDiffInv₀ : ContinuousInv₀ G :=
 @[deprecated (since := "2025-09-01")] alias hasContinuousInv₀_of_hasContMDiffInv₀ :=
   continuousInv₀_of_contMDiffInv₀
 
-theorem contMDiffOn_inv₀ : ContMDiffOn I I n (Inv.inv : G → G) {0}ᶜ := fun _x hx =>
-  (contMDiffAt_inv₀ hx).contMDiffWithinAt
+theorem contMDiffOn_inv₀ : CMDiff[{0}ᶜ] n (Inv.inv : G → G) :=
+  fun _x hx ↦ (contMDiffAt_inv₀ hx).contMDiffWithinAt
 
 variable {s : Set M} {a : M}
 
-theorem ContMDiffWithinAt.inv₀ (hf : ContMDiffWithinAt I' I n f s a) (ha : f a ≠ 0) :
-    ContMDiffWithinAt I' I n (fun x => (f x)⁻¹) s a :=
+theorem ContMDiffWithinAt.inv₀ (hf : CMDiffAt[s] n f a) (ha : f a ≠ 0) :
+    CMDiffAt[s] n (fun x ↦ (f x)⁻¹) a :=
   (contMDiffAt_inv₀ ha).comp_contMDiffWithinAt a hf
 
-theorem ContMDiffAt.inv₀ (hf : ContMDiffAt I' I n f a) (ha : f a ≠ 0) :
-    ContMDiffAt I' I n (fun x ↦ (f x)⁻¹) a :=
+theorem ContMDiffAt.inv₀ (hf : CMDiffAt n f a) (ha : f a ≠ 0) : CMDiffAt n (fun x ↦ (f x)⁻¹) a :=
   (contMDiffAt_inv₀ ha).comp a hf
 
-theorem ContMDiff.inv₀ (hf : ContMDiff I' I n f) (h0 : ∀ x, f x ≠ 0) :
-    ContMDiff I' I n (fun x ↦ (f x)⁻¹) :=
+theorem ContMDiff.inv₀ (hf : CMDiff n f) (h0 : ∀ x, f x ≠ 0) :
+    CMDiff n (fun x ↦ (f x)⁻¹) :=
   fun x ↦ ContMDiffAt.inv₀ (hf x) (h0 x)
 
-theorem ContMDiffOn.inv₀ (hf : ContMDiffOn I' I n f s) (h0 : ∀ x ∈ s, f x ≠ 0) :
-    ContMDiffOn I' I n (fun x => (f x)⁻¹) s :=
+theorem ContMDiffOn.inv₀ (hf : CMDiff[s] n f) (h0 : ∀ x ∈ s, f x ≠ 0) :
+    CMDiff[s] n (fun x ↦ (f x)⁻¹) :=
   fun x hx ↦ ContMDiffWithinAt.inv₀ (hf x hx) (h0 x hx)
 
 end ContMDiffInv₀
@@ -308,19 +308,18 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
   {f g : M → G} {s : Set M} {a : M}
 
 theorem ContMDiffWithinAt.div₀
-    (hf : ContMDiffWithinAt I' I n f s a) (hg : ContMDiffWithinAt I' I n g s a) (h₀ : g a ≠ 0) :
-    ContMDiffWithinAt I' I n (f / g) s a := by
+    (hf : CMDiffAt[s] n f a) (hg : CMDiffAt[s] n g a) (h₀ : g a ≠ 0) : CMDiffAt[s] n (f / g) a := by
   simpa [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)
 
-theorem ContMDiffOn.div₀ (hf : ContMDiffOn I' I n f s) (hg : ContMDiffOn I' I n g s)
-    (h₀ : ∀ x ∈ s, g x ≠ 0) : ContMDiffOn I' I n (f / g) s := by
+theorem ContMDiffOn.div₀ (hf : CMDiff[s] n f) (hg : CMDiff[s] n g)
+    (h₀ : ∀ x ∈ s, g x ≠ 0) : CMDiff[s] n (f / g) := by
   simpa [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)
 
-theorem ContMDiffAt.div₀ (hf : ContMDiffAt I' I n f a) (hg : ContMDiffAt I' I n g a)
-    (h₀ : g a ≠ 0) : ContMDiffAt I' I n (f / g) a := by
+theorem ContMDiffAt.div₀ (hf : CMDiffAt n f a) (hg : CMDiffAt n g a)
+    (h₀ : g a ≠ 0) : CMDiffAt n (f / g) a := by
   simpa [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)
 
-theorem ContMDiff.div₀ (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) (h₀ : ∀ x, g x ≠ 0) :
-    ContMDiff I' I n (f / g) := by simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)
+theorem ContMDiff.div₀ (hf : CMDiff n f) (hg : CMDiff n g) (h₀ : ∀ x, g x ≠ 0) :
+    CMDiff n (f / g) := by simpa only [div_eq_mul_inv] using hf.mul (hg.inv₀ h₀)
 
 end Div