feat: port continuity tactic (#2145)

We implement the continuity tactic using aesop, this makes it more robust and reduces the code to trivial macros.

Mathlib.lean

@@ -944,6 +944,7 @@ import Mathlib.Tactic.ClearExcept
 import Mathlib.Tactic.Clear_
 import Mathlib.Tactic.Coe
 import Mathlib.Tactic.Constructor
+import Mathlib.Tactic.Continuity
 import Mathlib.Tactic.Contrapose
 import Mathlib.Tactic.Conv
 import Mathlib.Tactic.Convert

Mathlib/Mathport/Syntax.lean

@@ -22,6 +22,7 @@ import Mathlib.Tactic.Clear_
 import Mathlib.Tactic.Clear!
 import Mathlib.Tactic.ClearExcept
 import Mathlib.Tactic.Constructor
+import Mathlib.Tactic.Continuity
 import Mathlib.Tactic.Contrapose
 import Mathlib.Tactic.Conv
 import Mathlib.Tactic.Convert
@@ -284,11 +285,6 @@ syntax mono.side := &"left" <|> &"right" <|> &"both"
 /- S -/ syntax (name := mvBisim) "mv_bisim" (ppSpace (colGt term))? (" with " binderIdent+)? :
   tactic
 
-/- M -/ syntax (name := continuity) "continuity" (config)? : tactic
-/- M -/ syntax (name := continuity!) "continuity!" (config)? : tactic
-/- M -/ syntax (name := continuity?) "continuity?" (config)? : tactic
-/- M -/ syntax (name := continuity!?) "continuity!?" (config)? : tactic
-
 /- E -/ syntax (name := unitInterval) "unit_interval" : tactic
 
 /- N -/ syntax (name := measurability) "measurability" (config)? : tactic

Mathlib/Tactic/Continuity.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2023 Moritz Doll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Doll
+-/
+
+import Aesop
+
+/-!
+# Continuity
+
+We define the `continuity` tactic using `aesop`. -/
+
+declare_aesop_rule_sets [Continuous]
+
+attribute [aesop (rule_sets [Continuous]) unfold norm] Function.comp
+
+/--
+The `continuity` attribute used to tag continuity statements for the `continuity` tactic. -/
+macro "continuity" : attr =>
+  `(attr|aesop safe apply (rule_sets [$(Lean.mkIdent `Continuous):ident]))
+
+/--
+The tactic `continuity` solves goals of the form `Continuous f` by applying lemmas tagged with the
+`continuity` user attribute. -/
+macro "continuity" : tactic =>
+  `(tactic|aesop (rule_sets [$(Lean.mkIdent `Continuous):ident]))
+
+-- Todo: implement `continuity?`, `continuity!` and `continuity!?` and add configuration, original
+-- syntax was (same for the missing `continuity` variants):
+-- syntax (name := continuity) "continuity" (config)? : tactic

Mathlib/Topology/Algebra/ConstMulAction.lean

@@ -109,7 +109,7 @@ theorem ContinuousOn.const_smul (hg : ContinuousOn g s) (c : M) :
 #align continuous_on.const_smul ContinuousOn.const_smul
 #align continuous_on.const_vadd ContinuousOn.const_vadd
 
-@[to_additive] -- porting note: todo: restore `continuity`
+@[to_additive, continuity]
 theorem Continuous.const_smul (hg : Continuous g) (c : M) : Continuous fun x => c • g x :=
   (continuous_const_smul _).comp hg
 #align continuous.const_smul Continuous.const_smul

Mathlib/Topology/Algebra/Constructions.lean

@@ -37,13 +37,13 @@ instance [TopologicalSpace M] : TopologicalSpace Mᵐᵒᵖ :=
 
 variable [TopologicalSpace M]
 
-@[to_additive] -- porting note: todo: restore `continuity`
+@[to_additive, continuity]
 theorem continuous_unop : Continuous (unop : Mᵐᵒᵖ → M) :=
   continuous_induced_dom
 #align mul_opposite.continuous_unop MulOpposite.continuous_unop
 #align add_opposite.continuous_unop AddOpposite.continuous_unop
 
-@[to_additive] -- porting note: todo: restore `continuity`
+@[to_additive, continuity]
 theorem continuous_op : Continuous (op : M → Mᵐᵒᵖ) :=
   continuous_induced_rng.2 continuous_id
 #align mul_opposite.continuous_op MulOpposite.continuous_op

Mathlib/Topology/Algebra/Order/ProjIcc.lean

@@ -38,7 +38,7 @@ theorem Filter.Tendsto.IccExtend' (f : γ → Icc a b → β) {z : γ} {l : Filt
 
 variable [TopologicalSpace α] [OrderTopology α] [TopologicalSpace β]
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem continuous_projIcc : Continuous (projIcc a b h) :=
   (continuous_const.max <| continuous_const.min continuous_id).subtype_mk _
 #align continuous_proj_Icc continuous_projIcc
@@ -61,7 +61,7 @@ protected theorem Continuous.IccExtend {f : γ → Icc a b → β} {g : γ → 
 #align continuous.Icc_extend Continuous.IccExtend
 
 /-- A useful special case of `continuous.Icc_extend`. -/
--- porting note: todo: restore @[continuity]
+@[continuity]
 protected theorem Continuous.Icc_extend' {f : Icc a b → β} (hf : Continuous f) :
     Continuous (IccExtend h f) :=
   hf.comp continuous_projIcc

Mathlib/Topology/Algebra/Star.lean

@@ -57,7 +57,7 @@ theorem Filter.Tendsto.star {f : α → R} {l : Filter α} {y : R} (h : Tendsto
 
 variable [TopologicalSpace α] {f : α → R} {s : Set α} {x : α}
 
--- @[continuity] Porting note: restore attribute
+@[continuity]
 theorem Continuous.star (hf : Continuous f) : Continuous fun x => star (f x) :=
   continuous_star.comp hf
 #align continuous.star Continuous.star

Mathlib/Topology/Basic.lean

@@ -11,6 +11,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Jeremy Avigad
 import Mathlib.Order.Filter.Ultrafilter
 import Mathlib.Algebra.Support
 import Mathlib.Order.Filter.Lift
+import Mathlib.Tactic.Continuity
 
 /-!
 # Basic theory of topological spaces.
@@ -1640,15 +1641,25 @@ theorem preimage_interior_subset_interior_preimage {f : α → β} {s : Set β}
   interior_maximal (preimage_mono interior_subset) (isOpen_interior.preimage hf)
 #align preimage_interior_subset_interior_preimage preimage_interior_subset_interior_preimage
 
+@[continuity]
 theorem continuous_id : Continuous (id : α → α) :=
   continuous_def.2 fun _ => id
 #align continuous_id continuous_id
 
+-- This is needed due to reducibility issues with the `continuity` tactic.
+@[continuity]
+theorem continuous_id' : Continuous (fun (x : α) => x) := continuous_id
+
 theorem Continuous.comp {g : β → γ} {f : α → β} (hg : Continuous g) (hf : Continuous f) :
     Continuous (g ∘ f) :=
   continuous_def.2 fun _ h => (h.preimage hg).preimage hf
 #align continuous.comp Continuous.comp
 
+-- This is needed due to reducibility issues with the `continuity` tactic.
+@[continuity]
+theorem Continuous.comp' {g : β → γ} {f : α → β} (hg : Continuous g) (hf : Continuous f) :
+    Continuous (fun x => g (f x)) := hg.comp hf
+
 theorem Continuous.iterate {f : α → α} (h : Continuous f) (n : ℕ) : Continuous (f^[n]) :=
   Nat.recOn n continuous_id fun _ ihn => ihn.comp h
 #align continuous.iterate Continuous.iterate
@@ -1683,6 +1694,7 @@ theorem continuousAt_const {x : α} {b : β} : ContinuousAt (fun _ : α => b) x
   tendsto_const_nhds
 #align continuous_at_const continuousAt_const
 
+@[continuity]
 theorem continuous_const {b : β} : Continuous fun _ : α => b :=
   continuous_iff_continuousAt.mpr fun _ => continuousAt_const
 #align continuous_const continuous_const

Mathlib/Topology/Connected.lean

@@ -1467,7 +1467,7 @@ theorem quotientMap_coe : QuotientMap (mk : α → ConnectedComponents α) :=
   quotientMap_quot_mk
 #align connected_components.quotient_map_coe ConnectedComponents.quotientMap_coe
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem continuous_coe : Continuous (mk : α → ConnectedComponents α) :=
   quotientMap_coe.continuous
 #align connected_components.continuous_coe ConnectedComponents.continuous_coe
@@ -1495,7 +1495,7 @@ def Continuous.connectedComponentsLift (h : Continuous f) : ConnectedComponents
   Quotient.liftOn' x f h.image_eq_of_connectedComponent_eq
 #align continuous.connected_components_lift Continuous.connectedComponentsLift
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem Continuous.connectedComponentsLift_continuous (h : Continuous f) :
     Continuous h.connectedComponentsLift :=
   h.quotient_liftOn' <| by convert h.image_eq_of_connectedComponent_eq

Mathlib/Topology/Constructions.lean

@@ -323,7 +323,7 @@ variable [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] [Topo
     continuous_induced_rng.and continuous_induced_rng
 #align continuous_prod_mk continuous_prod_mk
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem continuous_fst : Continuous (@Prod.fst α β) :=
   (continuous_prod_mk.1 continuous_id).1
 #align continuous_fst continuous_fst
@@ -360,7 +360,7 @@ theorem ContinuousAt.fst'' {f : α → γ} {x : α × β} (hf : ContinuousAt f x
   hf.comp continuousAt_fst
 #align continuous_at.fst'' ContinuousAt.fst''
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem continuous_snd : Continuous (@Prod.snd α β) :=
   (continuous_prod_mk.1 continuous_id).2
 #align continuous_snd continuous_snd
@@ -397,18 +397,18 @@ theorem ContinuousAt.snd'' {f : β → γ} {x : α × β} (hf : ContinuousAt f x
   hf.comp continuousAt_snd
 #align continuous_at.snd'' ContinuousAt.snd''
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem Continuous.prod_mk {f : γ → α} {g : γ → β} (hf : Continuous f) (hg : Continuous g) :
     Continuous fun x => (f x, g x) :=
   continuous_prod_mk.2 ⟨hf, hg⟩
 #align continuous.prod_mk Continuous.prod_mk
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem Continuous.Prod.mk (a : α) : Continuous fun b : β => (a, b) :=
   continuous_const.prod_mk continuous_id
 #align continuous.prod.mk Continuous.Prod.mk
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem Continuous.Prod.mk_left (b : β) : Continuous fun a : α => (a, b) :=
   continuous_id.prod_mk continuous_const
 #align continuous.prod.mk_left Continuous.Prod.mk_left
@@ -430,6 +430,7 @@ theorem Continuous.comp₄ {g : α × β × γ × ζ → ε} (hg : Continuous g)
   hg.comp₃ he hf <| hk.prod_mk hl
 #align continuous.comp₄ Continuous.comp₄
 
+@[continuity]
 theorem Continuous.prod_map {f : γ → α} {g : δ → β} (hf : Continuous f) (hg : Continuous g) :
     Continuous fun x : γ × δ => (f x.1, g x.2) :=
   hf.fst'.prod_mk hg.snd'
@@ -848,26 +849,26 @@ theorem continuous_sum_elim {f : α → γ} {g : β → γ} :
   continuous_sum_dom
 #align continuous_sum_elim continuous_sum_elim
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem Continuous.sum_elim {f : α → γ} {g : β → γ} (hf : Continuous f) (hg : Continuous g) :
     Continuous (Sum.elim f g) :=
   continuous_sum_elim.2 ⟨hf, hg⟩
 #align continuous.sum_elim Continuous.sum_elim
 
--- porting note: todo: add @[continuity]
+@[continuity]
 theorem continuous_isLeft : Continuous (isLeft : α ⊕ β → Bool) :=
   continuous_sum_dom.2 ⟨continuous_const, continuous_const⟩
 
--- porting note: todo: add @[continuity]
+@[continuity]
 theorem continuous_isRight : Continuous (isRight : α ⊕ β → Bool) :=
   continuous_sum_dom.2 ⟨continuous_const, continuous_const⟩
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 -- porting note: the proof was `continuous_sup_rng_left continuous_coinduced_rng`
 theorem continuous_inl : Continuous (@inl α β) := ⟨fun _ => And.left⟩
 #align continuous_inl continuous_inl
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 -- porting note: the proof was `continuous_sup_rng_right continuous_coinduced_rng`
 theorem continuous_inr : Continuous (@inr α β) := ⟨fun _ => And.right⟩
 #align continuous_inr continuous_inr
@@ -946,7 +947,7 @@ theorem continuous_sum_map {f : α → β} {g : γ → δ} :
     embedding_inl.continuous_iff.symm.and embedding_inr.continuous_iff.symm
 #align continuous_sum_map continuous_sum_map
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem Continuous.sum_map {f : α → β} {g : γ → δ} (hf : Continuous f) (hg : Continuous g) :
     Continuous (Sum.map f g) :=
   continuous_sum_map.2 ⟨hf, hg⟩
@@ -991,7 +992,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
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem continuous_subtype_val : Continuous (@Subtype.val α p) :=
   continuous_induced_dom
 #align continuous_subtype_val continuous_subtype_val
@@ -1021,7 +1022,7 @@ nonrec theorem IsClosed.closedEmbedding_subtype_val {s : Set α} (hs : IsClosed
   closedEmbedding_subtype_val hs
 #align is_closed.closed_embedding_subtype_coe IsClosed.closedEmbedding_subtype_val
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem Continuous.subtype_mk {f : β → α} (h : Continuous f) (hp : ∀ x, p (f x)) :
     Continuous fun x => (⟨f x, hp x⟩ : Subtype p) :=
   continuous_induced_rng.2 h
@@ -1105,7 +1106,7 @@ theorem ContinuousAt.restrictPreimage {f : α → β} {s : Set β} {x : f ⁻¹'
   h.restrict _
 #align continuous_at.restrict_preimage ContinuousAt.restrictPreimage
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem Continuous.codRestrict {f : α → β} {s : Set β} (hf : Continuous f) (hs : ∀ a, f a ∈ s) :
     Continuous (s.codRestrict f hs) :=
   hf.subtype_mk hs
@@ -1144,12 +1145,12 @@ theorem quotientMap_quot_mk : QuotientMap (@Quot.mk α r) :=
   ⟨Quot.exists_rep, rfl⟩
 #align quotient_map_quot_mk quotientMap_quot_mk
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem continuous_quot_mk : Continuous (@Quot.mk α r) :=
   continuous_coinduced_rng
 #align continuous_quot_mk continuous_quot_mk
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem continuous_quot_lift {f : α → β} (hr : ∀ a b, r a b → f a = f b) (h : Continuous f) :
     Continuous (Quot.lift f hr : Quot r → β) :=
   continuous_coinduced_dom.2 h
@@ -1190,17 +1191,17 @@ theorem continuous_pi_iff : Continuous f ↔ ∀ i, Continuous fun a => f a i :=
   simp only [continuous_infᵢ_rng, continuous_induced_rng, comp]
 #align continuous_pi_iff continuous_pi_iff
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem continuous_pi (h : ∀ i, Continuous fun a => f a i) : Continuous f :=
   continuous_pi_iff.2 h
 #align continuous_pi continuous_pi
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem continuous_apply (i : ι) : Continuous fun p : ∀ i, π i => p i :=
   continuous_infᵢ_dom continuous_induced_dom
 #align continuous_apply continuous_apply
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem continuous_apply_apply {ρ : κ → ι → Type _} [∀ j i, TopologicalSpace (ρ j i)] (j : κ)
     (i : ι) : Continuous fun p : ∀ j, ∀ i, ρ j i => p j i :=
   (continuous_apply i).comp (continuous_apply j)
@@ -1246,7 +1247,7 @@ theorem Continuous.update [DecidableEq ι] (hf : Continuous f) (i : ι) {g : α
 #align continuous.update Continuous.update
 
 /-- `Function.update f i x` is continuous in `(f, x)`. -/
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem continuous_update [DecidableEq ι] (i : ι) :
     Continuous fun f : (∀ j, π j) × π i => update f.1 i f.2 :=
   continuous_fst.update i continuous_snd
@@ -1430,7 +1431,7 @@ section Sigma
 variable {ι κ : Type _} {σ : ι → Type _} {τ : κ → Type _} [∀ i, TopologicalSpace (σ i)]
   [∀ k, TopologicalSpace (τ k)] [TopologicalSpace α]
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem continuous_sigmaMk {i : ι} : Continuous (@Sigma.mk ι σ i) :=
   continuous_supᵢ_rng continuous_coinduced_rng
 #align continuous_sigma_mk continuous_sigmaMk
@@ -1517,7 +1518,7 @@ theorem continuous_sigma_iff {f : Sigma σ → α} :
 #align continuous_sigma_iff continuous_sigma_iff
 
 /-- A map out of a sum type is continuous if its restriction to each summand is. -/
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem continuous_sigma {f : Sigma σ → α} (hf : ∀ i, Continuous fun a => f ⟨i, a⟩) :
     Continuous f :=
   continuous_sigma_iff.2 hf
@@ -1529,7 +1530,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
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 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
@@ -1566,12 +1567,12 @@ end Sigma
 
 section ULift
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem continuous_uLift_down [TopologicalSpace α] : Continuous (ULift.down : ULift.{v, u} α → α) :=
   continuous_induced_dom
 #align continuous_ulift_down continuous_uLift_down
 
--- porting note: todo: restore @[continuity]
+@[continuity]
 theorem continuous_uLift_up [TopologicalSpace α] : Continuous (ULift.up : α → ULift.{v, u} α) :=
   continuous_induced_rng.2 continuous_id
 #align continuous_ulift_up continuous_uLift_up