feat: fun_prop lemmas for GL n R and SL n R

Author: j-loreaux

Mathlib/Analysis/Complex/UpperHalfPlane/ProperAction.lean

@@ -26,25 +26,30 @@ public section
 
 namespace UpperHalfPlane
 
+@[fun_prop]
+theorem num_continuous : Continuous ↿num := by unfold num; fun_prop
+
+@[fun_prop]
+theorem denom_continuous : Continuous ↿denom := by unfold denom; fun_prop
+
 lemma continuous_toSL2R : Continuous toSL2R := by
   refine continuous_induced_rng.mpr (continuous_matrix fun i j ↦ ?_)
   fin_cases i <;> fin_cases j
-  · exact Real.continuous_sqrt.comp continuous_im
-  · exact continuous_re.div₀ (by fun_prop) (fun τ : ℍ ↦ Real.sqrt_ne_zero'.mpr τ.im_pos)
-  · exact continuous_const
-  · simpa using .inv₀ (by fun_prop) (fun τ : ℍ ↦ Real.sqrt_ne_zero'.mpr τ.im_pos)
+  all_goals
+    simp only [Fin.zero_eta, Fin.isValue, Function.comp_apply, coe_toSL2R, one_div,
+      Matrix.of_apply, Matrix.cons_val', Matrix.cons_val_zero, Matrix.cons_val_fin_one, Fin.mk_one,
+      Matrix.cons_val_one]
+    fun_prop (disch := grind [im_pos])
 
 /-- The action of `SL(2, ℝ)` on `ℍ` is jointly continuous. -/
-instance instContinuousSMulSL2R : ContinuousSMul SL(2, ℝ) ℍ := by
-  constructor
-  suffices ∀ (g : SL(2, ℝ)) (τ : ℍ),
-      ContinuousAt (fun ⟨h, z⟩ ↦ (h 0 0 * (z : ℂ) + h 0 1) / (h 1 0 * z + h 1 1)) (g, τ) by
-    simpa [continuous_induced_rng, continuous_iff_continuousAt, Function.comp_def,
-      coe_specialLinearGroup_apply]
-  refine fun g τ ↦ .div ?_ ?_ (denom_ne_zero g τ) <;>
-  refine .add (.mul ?_ (by fun_prop)) ?_ <;>
-  · refine (Complex.continuous_ofReal.comp ?_).continuousAt
-    exact (continuous_subtype_val.matrix_elem _ _).comp continuous_fst
+instance instContinuousSMulSL2R : ContinuousSMul SL(2, ℝ) ℍ where
+  continuous_smul := by
+    suffices ∀ (g : SL(2, ℝ)) (τ : ℍ),
+        ContinuousAt (fun ⟨h, z⟩ ↦ (h 0 0 * (z : ℂ) + h 0 1) / (h 1 0 * z + h 1 1)) (g, τ) by
+      simpa [continuous_induced_rng, continuous_iff_continuousAt, Function.comp_def,
+        coe_specialLinearGroup_apply]
+    refine fun g τ ↦ ?_
+    fun_prop (disch := exact denom_ne_zero g τ)
 
 open Topology in
 lemma σ_eventuallyEq (g : GL (Fin 2) ℝ) : σ =ᶠ[𝓝 g] fun _ ↦ σ g := by
@@ -63,12 +68,8 @@ instance instContinuousSMulGL2R : ContinuousSMul (GL (Fin 2) ℝ) ℍ := by
   simp only [continuous_induced_rng, Function.comp_def, coe_smul, continuous_iff_continuousAt,
     Prod.forall]
   refine fun g τ ↦ .congr ?_ (f := fun x ↦ (σ g) (num x.1 x.2 / denom x.1 x.2))
-      (by filter_upwards [(σ_eventuallyEq g).prod_inl_nhds _] using by simp +contextual)
-  refine ContinuousAt.comp (by fun_prop) (.div₀ ?_ ?_ (denom_ne_zero _ _)) <;>
-  · refine .add (.mul ?_ (by fun_prop)) ?_ <;>
-    · refine (Complex.continuous_ofReal.comp ?_).continuousAt
-      refine Continuous.comp (g := fun g : GL (Fin 2) ℝ ↦ g _ _) ?_ continuous_fst
-      exact (continuous_id.matrix_elem _ _).comp Units.continuous_val
+    (by filter_upwards [(σ_eventuallyEq g).prod_inl_nhds _] using by simp +contextual)
+  fun_prop (disch := apply denom_ne_zero)
 
 section proper_orbit_map
 

Mathlib/Topology/Algebra/Group/Matrix.lean

@@ -31,6 +31,13 @@ variable [Fintype n] [DecidableEq n] [CommRing R] [TopologicalSpace R] [IsTopolo
 
 namespace Matrix.GeneralLinearGroup
 
+omit [IsTopologicalRing R] in
+@[fun_prop]
+theorem continuous_apply {α : Type*} [TopologicalSpace α]
+    (f : α → GL n R) (hf : Continuous f) (i : n) :
+    Continuous (fun x => f x i) :=
+  (by fun_prop : Continuous fun A : Matrix n n R ↦ A i).comp <| by fun_prop
+
 /-- The determinant is continuous as a map from the general linear group to the units. -/
 @[continuity, fun_prop] protected lemma continuous_det :
     Continuous (det : GL n R → Rˣ) := by
@@ -56,6 +63,13 @@ omit [IsTopologicalRing R] in
 instance : TopologicalSpace (SL n R) :=
   inferInstanceAs <| TopologicalSpace (Subtype _)
 
+omit [IsTopologicalRing R] in
+@[fun_prop]
+theorem Matrix.SpecialLinearGroup.continuous_apply {α : Type*} [TopologicalSpace α]
+    (f : α → SL n R) (hf : Continuous f) (i) :
+    Continuous (fun x => f x i) :=
+  (by fun_prop : Continuous fun A : Matrix n n R ↦ A i).comp <| by fun_prop
+
 /-- If `R` is a commutative ring with the discrete topology, then `SL(n, R)` has the discrete
 topology. -/
 instance [DiscreteTopology R] : DiscreteTopology (SL n R) :=