chore: replace continuity by fun_prop, easy cases (#13880)

Inspired by #12661: let's start with some easy instances, so we can focus on the difficult ones.

In particular, this PR does not depend on any in-progress bugfixes, not tries to change a default value `by continuity` to `by fun_prop`.

I am not at all confident about the tagging of lemmas with fun_prop: I remember this being subtle, but can't find any documentation on this. @lecopivo Can you advise on these lemmas (or simply link to the right documentation if I just overlooked it)?

Author: grunweg

Mathlib/Topology/CompactOpen.lean

@@ -374,7 +374,7 @@ section Curry
     If `a × β` is locally compact, this is continuous. If `α` and `β` are both locally
     compact, then this is a homeomorphism, see `Homeomorph.curry`. -/
 def curry (f : C(X × Y, Z)) : C(X, C(Y, Z)) where
-  toFun a := ⟨Function.curry f a, f.continuous.comp <| by continuity⟩
+  toFun a := ⟨Function.curry f a, f.continuous.comp <| by fun_prop⟩
   continuous_toFun := (continuous_comp f).comp continuous_coev
 #align continuous_map.curry ContinuousMap.curry
 

Mathlib/Topology/Connected/PathConnected.lean

@@ -88,7 +88,7 @@ instance Path.funLike : FunLike (Path x y) I X where
 -- Porting note (#10754): added this instance so that we can use `FunLike.coe` for `CoeFun`
 -- this also fixed very strange `simp` timeout issues
 instance Path.continuousMapClass : ContinuousMapClass (Path x y) I X where
-  map_continuous := fun γ => show Continuous γ.toContinuousMap by continuity
+  map_continuous γ := show Continuous γ.toContinuousMap by fun_prop
 
 -- Porting note: not necessary in light of the instance above
 /-
@@ -246,7 +246,7 @@ theorem _root_.Continuous.path_extend {γ : Y → Path x y} {f : Y → ℝ} (hγ
 #align continuous.path_extend Continuous.path_extend
 
 /-- A useful special case of `Continuous.path_extend`. -/
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_extend : Continuous γ.extend :=
   γ.continuous.Icc_extend'
 #align path.continuous_extend Path.continuous_extend
@@ -326,7 +326,7 @@ def trans (γ : Path x y) (γ' : Path y z) : Path x z where
     refine
       (Continuous.if_le ?_ ?_ continuous_id continuous_const (by norm_num)).comp
         continuous_subtype_val <;>
-    continuity
+    fun_prop
   source' := by norm_num
   target' := by norm_num
 #align path.trans Path.trans
@@ -472,7 +472,7 @@ theorem cast_coe (γ : Path x y) {x' y'} (hx : x' = x) (hy : y' = y) : (γ.cast
   rfl
 #align path.cast_coe Path.cast_coe
 
-@[continuity]
+@[continuity, fun_prop]
 theorem symm_continuous_family {ι : Type*} [TopologicalSpace ι]
     {a b : ι → X} (γ : ∀ t : ι, Path (a t) (b t)) (h : Continuous ↿γ) :
     Continuous ↿fun t => (γ t).symm :=
@@ -666,7 +666,7 @@ theorem truncate_continuous_family {a b : X} (γ : Path a b) :
 @[continuity]
 theorem truncate_const_continuous_family {a b : X} (γ : Path a b)
     (t : ℝ) : Continuous ↿(γ.truncate t) := by
-  have key : Continuous (fun x => (t, x) : ℝ × I → ℝ × ℝ × I) := by continuity
+  have key : Continuous (fun x => (t, x) : ℝ × I → ℝ × ℝ × I) := by fun_prop
   exact γ.truncate_continuous_family.comp key
 #align path.truncate_const_continuous_family Path.truncate_const_continuous_family
 
@@ -709,7 +709,7 @@ path defined by `γ ∘ f`.
 def reparam (γ : Path x y) (f : I → I) (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) :
     Path x y where
   toFun := γ ∘ f
-  continuous_toFun := by continuity
+  continuous_toFun := by fun_prop
   source' := by simp [hf₀]
   target' := by simp [hf₁]
 #align path.reparam Path.reparam
@@ -834,7 +834,7 @@ theorem JoinedIn.somePath_mem (h : JoinedIn F x y) (t : I) : h.somePath t ∈ F
 theorem JoinedIn.joined_subtype (h : JoinedIn F x y) :
     Joined (⟨x, h.source_mem⟩ : F) (⟨y, h.target_mem⟩ : F) :=
   ⟨{  toFun := fun t => ⟨h.somePath t, h.somePath_mem t⟩
-      continuous_toFun := by continuity
+      continuous_toFun := by fun_prop
       source' := by simp
       target' := by simp }⟩
 #align joined_in.joined_subtype JoinedIn.joined_subtype
@@ -1202,7 +1202,7 @@ instance Quotient.instPathConnectedSpace {s : Setoid X} [PathConnectedSpace X] :
 /-- This is a special case of `NormedSpace.instPathConnectedSpace` (and
 `TopologicalAddGroup.pathConnectedSpace`). It exists only to simplify dependencies. -/
 instance Real.instPathConnectedSpace : PathConnectedSpace ℝ where
-  joined x y := ⟨⟨⟨fun (t : I) ↦ (1 - t) * x + t * y, by continuity⟩, by simp, by simp⟩⟩
+  joined x y := ⟨⟨⟨fun (t : I) ↦ (1 - t) * x + t * y, by fun_prop⟩, by simp, by simp⟩⟩
   nonempty := inferInstance
 
 theorem pathConnectedSpace_iff_eq : PathConnectedSpace X ↔ ∃ x : X, pathComponent x = univ := by

Mathlib/Topology/Constructions.lean

@@ -950,26 +950,26 @@ theorem continuous_sum_elim {f : X → Z} {g : Y → Z} :
   continuous_sum_dom
 #align continuous_sum_elim continuous_sum_elim
 
-@[continuity]
+@[continuity, fun_prop]
 theorem Continuous.sum_elim {f : X → Z} {g : Y → Z} (hf : Continuous f) (hg : Continuous g) :
     Continuous (Sum.elim f g) :=
   continuous_sum_elim.2 ⟨hf, hg⟩
 #align continuous.sum_elim Continuous.sum_elim
 
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_isLeft : Continuous (isLeft : X ⊕ Y → Bool) :=
   continuous_sum_dom.2 ⟨continuous_const, continuous_const⟩
 
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_isRight : Continuous (isRight : X ⊕ Y → Bool) :=
   continuous_sum_dom.2 ⟨continuous_const, continuous_const⟩
 
-@[continuity]
+@[continuity, fun_prop]
 -- Porting note: the proof was `continuous_sup_rng_left continuous_coinduced_rng`
 theorem continuous_inl : Continuous (@inl X Y) := ⟨fun _ => And.left⟩
 #align continuous_inl continuous_inl
 
-@[continuity]
+@[continuity, fun_prop]
 -- Porting note: the proof was `continuous_sup_rng_right continuous_coinduced_rng`
 theorem continuous_inr : Continuous (@inr X Y) := ⟨fun _ => And.right⟩
 #align continuous_inr continuous_inr
@@ -1048,7 +1048,7 @@ theorem continuous_sum_map {f : X → Y} {g : Z → W} :
     embedding_inl.continuous_iff.symm.and embedding_inr.continuous_iff.symm
 #align continuous_sum_map continuous_sum_map
 
-@[continuity]
+@[continuity, fun_prop]
 theorem Continuous.sum_map {f : X → Y} {g : Z → W} (hf : Continuous f) (hg : Continuous g) :
     Continuous (Sum.map f g) :=
   continuous_sum_map.2 ⟨hf, hg⟩
@@ -1093,7 +1093,7 @@ theorem closedEmbedding_subtype_val (h : IsClosed { a | p a }) :
   ⟨embedding_subtype_val, by rwa [Subtype.range_coe_subtype]⟩
 #align closed_embedding_subtype_coe closedEmbedding_subtype_val
 
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_subtype_val : Continuous (@Subtype.val X p) :=
   continuous_induced_dom
 #align continuous_subtype_val continuous_subtype_val
@@ -1123,7 +1123,7 @@ nonrec theorem IsClosed.closedEmbedding_subtype_val {s : Set X} (hs : IsClosed s
   closedEmbedding_subtype_val hs
 #align is_closed.closed_embedding_subtype_coe IsClosed.closedEmbedding_subtype_val
 
-@[continuity]
+@[continuity, fun_prop]
 theorem Continuous.subtype_mk {f : Y → X} (h : Continuous f) (hp : ∀ x, p (f x)) :
     Continuous fun x => (⟨f x, hp x⟩ : Subtype p) :=
   continuous_induced_rng.2 h
@@ -1190,18 +1190,18 @@ theorem ContinuousAt.restrictPreimage {f : X → Y} {s : Set Y} {x : f ⁻¹' s}
   h.restrict _
 #align continuous_at.restrict_preimage ContinuousAt.restrictPreimage
 
-@[continuity]
+@[continuity, fun_prop]
 theorem Continuous.codRestrict {f : X → Y} {s : Set Y} (hf : Continuous f) (hs : ∀ a, f a ∈ s) :
     Continuous (s.codRestrict f hs) :=
   hf.subtype_mk hs
 #align continuous.cod_restrict Continuous.codRestrict
 
-@[continuity]
+@[continuity, fun_prop]
 theorem Continuous.restrict {f : X → Y} {s : Set X} {t : Set Y} (h1 : MapsTo f s t)
     (h2 : Continuous f) : Continuous (h1.restrict f s t) :=
   (h2.comp continuous_subtype_val).codRestrict _
 
-@[continuity]
+@[continuity, fun_prop]
 theorem Continuous.restrictPreimage {f : X → Y} {s : Set Y} (h : Continuous f) :
     Continuous (s.restrictPreimage f) :=
   h.restrict _
@@ -1246,12 +1246,12 @@ theorem quotientMap_quot_mk : QuotientMap (@Quot.mk X r) :=
   ⟨Quot.exists_rep, rfl⟩
 #align quotient_map_quot_mk quotientMap_quot_mk
 
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_quot_mk : Continuous (@Quot.mk X r) :=
   continuous_coinduced_rng
 #align continuous_quot_mk continuous_quot_mk
 
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_quot_lift {f : X → Y} (hr : ∀ a b, r a b → f a = f b) (h : Continuous f) :
     Continuous (Quot.lift f hr : Quot r → Y) :=
   continuous_coinduced_dom.2 h
@@ -1276,7 +1276,8 @@ theorem Continuous.quotient_liftOn' {f : X → Y} (h : Continuous f)
   h.quotient_lift hs
 #align continuous.quotient_lift_on' Continuous.quotient_liftOn'
 
-@[continuity] theorem Continuous.quotient_map' {t : Setoid Y} {f : X → Y} (hf : Continuous f)
+@[continuity, fun_prop]
+theorem Continuous.quotient_map' {t : Setoid Y} {f : X → Y} (hf : Continuous f)
     (H : (s.r ⇒ t.r) f f) : Continuous (Quotient.map' f H) :=
   (continuous_quotient_mk'.comp hf).quotient_lift _
 #align continuous.quotient_map' Continuous.quotient_map'
@@ -1395,7 +1396,7 @@ theorem Continuous.update [DecidableEq ι] (hf : Continuous f) (i : ι) {g : X 
 #align continuous.update Continuous.update
 
 /-- `Function.update f i x` is continuous in `(f, x)`. -/
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_update [DecidableEq ι] (i : ι) :
     Continuous fun f : (∀ j, π j) × π i => update f.1 i f.2 :=
   continuous_fst.update i continuous_snd
@@ -1587,7 +1588,7 @@ section Sigma
 variable {ι κ : Type*} {σ : ι → Type*} {τ : κ → Type*} [∀ i, TopologicalSpace (σ i)]
   [∀ k, TopologicalSpace (τ k)] [TopologicalSpace X]
 
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_sigmaMk {i : ι} : Continuous (@Sigma.mk ι σ i) :=
   continuous_iSup_rng continuous_coinduced_rng
 #align continuous_sigma_mk continuous_sigmaMk
@@ -1674,7 +1675,7 @@ theorem continuous_sigma_iff {f : Sigma σ → X} :
 #align continuous_sigma_iff continuous_sigma_iff
 
 /-- A map out of a sum type is continuous if its restriction to each summand is. -/
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_sigma {f : Sigma σ → X} (hf : ∀ i, Continuous fun a => f ⟨i, a⟩) :
     Continuous f :=
   continuous_sigma_iff.2 hf
@@ -1702,7 +1703,7 @@ theorem continuous_sigma_map {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁
   continuous_sigma_iff.trans <| by simp only [Sigma.map, embedding_sigmaMk.continuous_iff, comp]
 #align continuous_sigma_map continuous_sigma_map
 
-@[continuity]
+@[continuity, fun_prop]
 theorem Continuous.sigma_map {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁ i)} (hf : ∀ i, Continuous (f₂ i)) :
     Continuous (Sigma.map f₁ f₂) :=
   continuous_sigma_map.2 hf

Mathlib/Topology/ContinuousFunction/Polynomial.lean

@@ -54,8 +54,7 @@ with domain restricted to some subset of the semiring of coefficients.
 -/
 @[simps]
 def toContinuousMapOn (p : R[X]) (X : Set R) : C(X, R) :=
-  -- Porting note: Old proof was `⟨fun x : X => p.toContinuousMap x, by continuity⟩`
-  ⟨fun x : X => p.toContinuousMap x, Continuous.comp (by continuity) (by continuity)⟩
+  ⟨fun x : X => p.toContinuousMap x, by fun_prop⟩
 #align polynomial.to_continuous_map_on Polynomial.toContinuousMapOn
 
 open ContinuousMap in

Mathlib/Topology/Gluing.lean

@@ -389,7 +389,7 @@ def MkCore.t' (h : MkCore.{u}) (i j k : h.J) :
   -- Porting note: was `continuity`, see https://github.com/leanprover-community/mathlib4/issues/5030
   have : Continuous (h.t i j) := map_continuous (self := ContinuousMap.toContinuousMapClass) _
   set_option tactic.skipAssignedInstances false in
-  exact ((Continuous.subtype_mk (by continuity) _).prod_mk (by continuity)).subtype_mk _
+  exact ((Continuous.subtype_mk (by fun_prop) _).prod_mk (by fun_prop)).subtype_mk _
 
 set_option linter.uppercaseLean3 false in
 #align Top.glue_data.mk_core.t' TopCat.GlueData.MkCore.t'

Mathlib/Topology/Homotopy/HSpaces.lean

@@ -174,7 +174,7 @@ def qRight (p : I × I) : I :=
 
 theorem continuous_qRight : Continuous qRight :=
   continuous_projIcc.comp <|
-    Continuous.div (by continuity) (by continuity) fun x => (add_pos zero_lt_one).ne'
+    Continuous.div (by fun_prop) (by fun_prop) fun x ↦ (add_pos zero_lt_one).ne'
 #align unit_interval.continuous_Q_right unitInterval.continuous_qRight
 
 theorem qRight_zero_left (θ : I) : qRight (0, θ) = 0 :=

Mathlib/Topology/Homotopy/HomotopyGroup.lean

@@ -220,7 +220,7 @@ theorem continuous_toLoop (i : N) : Continuous (@toLoop N X _ x _ i) :=
 /-- Generalized loop from a loop by uncurrying $I → (I^{N\setminus\{j\}} → X)$ into $I^N → X$. -/
 @[simps]
 def fromLoop (i : N) (p : Ω (Ω^ { j // j ≠ i } X x) const) : Ω^ N X x :=
-  ⟨(ContinuousMap.comp ⟨Subtype.val, by continuity⟩ p.toContinuousMap).uncurry.comp
+  ⟨(ContinuousMap.comp ⟨Subtype.val, by fun_prop⟩ p.toContinuousMap).uncurry.comp
     (Cube.splitAt i).toContinuousMap,
     by
     rintro y ⟨j, Hj⟩

Mathlib/Topology/MetricSpace/Algebra.lean

@@ -152,7 +152,7 @@ instance (priority := 100) BoundedSMul.continuousSMul : ContinuousSMul α β whe
     rw [Metric.continuous_iff]
     rintro ⟨a, b⟩ ε ε0
     obtain ⟨δ, δ0, hδε⟩ : ∃ δ > 0, δ * (δ + dist b 0) + dist a 0 * δ < ε := by
-      have : Continuous fun δ ↦ δ * (δ + dist b 0) + dist a 0 * δ := by continuity
+      have : Continuous fun δ ↦ δ * (δ + dist b 0) + dist a 0 * δ := by fun_prop
       refine ((this.tendsto' _ _ ?_).eventually (gt_mem_nhds ε0)).exists_gt
       simp
     refine ⟨δ, δ0, fun (a', b') hab' => ?_⟩

Mathlib/Topology/MetricSpace/Completion.lean

@@ -191,7 +191,7 @@ open UniformSpace Completion NNReal
 theorem LipschitzWith.completion_extension [MetricSpace β] [CompleteSpace β] {f : α → β}
     {K : ℝ≥0} (h : LipschitzWith K f) : LipschitzWith K (Completion.extension f) :=
   LipschitzWith.of_dist_le_mul fun x y => induction_on₂ x y
-    (isClosed_le (by continuity) (by continuity)) <| by
+    (isClosed_le (by fun_prop) (by fun_prop)) <| by
       simpa only [extension_coe h.uniformContinuous, Completion.dist_eq] using h.dist_le_mul
 
 theorem LipschitzWith.completion_map [PseudoMetricSpace β] {f : α → β} {K : ℝ≥0}
@@ -201,7 +201,7 @@ theorem LipschitzWith.completion_map [PseudoMetricSpace β] {f : α → β} {K :
 theorem Isometry.completion_extension [MetricSpace β] [CompleteSpace β] {f : α → β}
     (h : Isometry f) : Isometry (Completion.extension f) :=
   Isometry.of_dist_eq fun x y => induction_on₂ x y
-    (isClosed_eq (by continuity) (by continuity)) fun _ _ ↦ by
+    (isClosed_eq (by fun_prop) (by fun_prop)) fun _ _ ↦ by
       simp only [extension_coe h.uniformContinuous, Completion.dist_eq, h.dist_eq]
 
 theorem Isometry.completion_map [PseudoMetricSpace β] {f : α → β}

Mathlib/Topology/Order.lean

@@ -293,7 +293,7 @@ theorem isOpen_discrete (s : Set α) : IsOpen s := (@DiscreteTopology.eq_bot α
 theorem denseRange_discrete {ι : Type*} {f : ι → α} : DenseRange f ↔ Surjective f := by
   rw [DenseRange, dense_discrete, range_iff_surjective]
 
-@[nontriviality, continuity]
+@[nontriviality, continuity, fun_prop]
 theorem continuous_of_discreteTopology [TopologicalSpace β] {f : α → β} : Continuous f :=
   continuous_def.2 fun _ _ => isOpen_discrete _
 #align continuous_of_discrete_topology continuous_of_discreteTopology
@@ -690,7 +690,7 @@ lemma continuous_generateFrom_iff {t : TopologicalSpace α} {b : Set (Set β)} :
 alias ⟨_, continuous_generateFrom⟩ := continuous_generateFrom_iff
 #align continuous_generated_from continuous_generateFrom
 
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_induced_dom {t : TopologicalSpace β} : Continuous[induced f t, t] f :=
   continuous_iff_le_induced.2 le_rfl
 #align continuous_induced_dom continuous_induced_dom
@@ -794,12 +794,12 @@ theorem continuous_iInf_rng {t₁ : TopologicalSpace α} {t₂ : ι → Topologi
   simp only [continuous_iff_coinduced_le, le_iInf_iff]
 #align continuous_infi_rng continuous_iInf_rng
 
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_bot {t : TopologicalSpace β} : Continuous[⊥, t] f :=
   continuous_iff_le_induced.2 bot_le
 #align continuous_bot continuous_bot
 
-@[continuity]
+@[continuity, fun_prop]
 theorem continuous_top {t : TopologicalSpace α} : Continuous[t, ⊤] f :=
   continuous_iff_coinduced_le.2 le_top
 #align continuous_top continuous_top