feat(topology/tactic): continuity tactic (#2879)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

docs/tutorial/category_theory/calculating_colimits_in_Top.lean

@@ -1,6 +1,7 @@
 import topology.category.Top.limits
 import category_theory.limits.shapes
 import topology.instances.real
+import topology.tactic
 
 /-! This file contains some demos of using the (co)limits API to do topology. -/
 
@@ -16,13 +17,11 @@ def pt : Top := Top.of unit
 section MappingCylinder
 -- Let's construct the mapping cylinder.
 def to_pt (X : Top) : X ⟶ pt :=
-{ to_fun := λ _, unit.star, continuous_to_fun := continuous_const }
+{ to_fun := λ _, unit.star, } -- We don't need to prove continuity: this is done automatically.
 def I₀ : pt ⟶ I :=
-{ to_fun := λ _, ⟨(0 : ℝ), by norm_num [set.left_mem_Icc]⟩,
-  continuous_to_fun := continuous_const }
+{ to_fun := λ _, ⟨(0 : ℝ), by norm_num [set.left_mem_Icc]⟩, }
 def I₁ : pt ⟶ I :=
-{ to_fun := λ _, ⟨(1 : ℝ), by norm_num [set.right_mem_Icc]⟩,
-  continuous_to_fun := continuous_const }
+{ to_fun := λ _, ⟨(1 : ℝ), by norm_num [set.right_mem_Icc]⟩, }
 
 def cylinder (X : Top) : Top := prod X I
 -- To define a map to the cylinder, we give a map to each factor.
@@ -71,7 +70,7 @@ end MappingCylinder
 section Gluing
 
 -- Here's two copies of the real line glued together at a point.
-def f : pt ⟶ R := { to_fun := λ _, (0 : ℝ), continuous_to_fun := continuous_const }
+def f : pt ⟶ R := { to_fun := λ _, (0 : ℝ), }
 
 /-- Two copies of the real line glued together at 0. -/
 def X : Top := pushout f f
@@ -95,7 +94,7 @@ We can define a point in this infinite product by specifying its coordinates.
 Let's define the point whose `n`-th coordinate is `n + 1` (as a real number).
 -/
 def q : pt ⟶ Y :=
-pi.lift (λ (n : ℕ), ⟨λ (_ : pt), (n + 1 : ℝ), continuous_const⟩)
+pi.lift (λ (n : ℕ), ⟨λ (_ : pt), (n + 1 : ℝ), by continuity⟩)
 
 -- "Looking under the hood", we see that `q` is a `subtype`, whose `val` is a function `unit → Y.α`.
 -- #check q.val -- q.val : pt.α → Y.α

src/analysis/analytic/basic.lean

@@ -192,7 +192,7 @@ def partial_sum (p : formal_multilinear_series 𝕜 E F) (n : ℕ) (x : E) : F :
 /-- The partial sums of a formal multilinear series are continuous. -/
 lemma partial_sum_continuous (p : formal_multilinear_series 𝕜 E F) (n : ℕ) :
   continuous (p.partial_sum n) :=
-continuous_finset_sum (finset.range n) $ λ k hk, (p k).cont.comp (continuous_pi (λ i, continuous_id))
+by continuity
 
 end formal_multilinear_series
 

src/analysis/normed_space/banach.lean

@@ -210,6 +210,7 @@ end
 namespace linear_equiv
 
 /-- If a bounded linear map is a bijection, then its inverse is also a bounded linear map. -/
+@[continuity]
 theorem continuous_symm (e : E ≃ₗ[𝕜] F) (h : continuous e) :
   continuous e.symm :=
 begin
@@ -227,7 +228,6 @@ def to_continuous_linear_equiv_of_continuous (e : E ≃ₗ[𝕜] F) (h : continu
 { continuous_to_fun := h,
   continuous_inv_fun := e.continuous_symm h,
   ..e }
-
 @[simp] lemma coe_fn_to_continuous_linear_equiv_of_continuous (e : E ≃ₗ[𝕜] F) (h : continuous e) :
   ⇑(e.to_continuous_linear_equiv_of_continuous h) = e := rfl
 

src/data/complex/exponential.lean

@@ -9,7 +9,7 @@ import data.complex.basic
 /-!
 # Exponential, trigonometric and hyperbolic trigonometric functions
 
-This file containss the definitions of the real and complex exponential, sine, cosine, tangent,
+This file contains the definitions of the real and complex exponential, sine, cosine, tangent,
 hyperbolic sine, hypebolic cosine, and hyperbolic tangent functions.
 
 -/
@@ -927,7 +927,7 @@ lemma exp_strict_mono : strict_mono exp :=
   exact (lt_mul_iff_one_lt_left (exp_pos _)).2
     (lt_of_lt_of_le (by linarith) (add_one_le_exp_of_nonneg (by linarith)))
 
-@[mono] lemma exp_monotone : ∀ {x y : ℝ}, x ≤ y → exp x ≤ exp y := exp_strict_mono.monotone 
+@[mono] lemma exp_monotone : ∀ {x y : ℝ}, x ≤ y → exp x ≤ exp y := exp_strict_mono.monotone
 
 lemma exp_lt_exp {x y : ℝ} : exp x < exp y ↔ x < y := exp_strict_mono.lt_iff_lt
 

src/geometry/manifold/smooth_manifold_with_corners.lean

@@ -130,8 +130,8 @@ structure model_with_corners (𝕜 : Type*) [nondiscrete_normed_field 𝕜]
   extends local_equiv H E :=
 (source_eq          : source = univ)
 (unique_diff'       : unique_diff_on 𝕜 (range to_fun))
-(continuous_to_fun  : continuous to_fun)
-(continuous_inv_fun : continuous inv_fun)
+(continuous_to_fun  : continuous to_fun . tactic.interactive.continuity')
+(continuous_inv_fun : continuous inv_fun . tactic.interactive.continuity')
 
 attribute [simp, mfld_simps] model_with_corners.source_eq
 

src/topology/algebra/group.lean

@@ -41,11 +41,13 @@ variables [topological_space α] [group α]
 lemma continuous_inv [topological_group α] : continuous (λx:α, x⁻¹) :=
 topological_group.continuous_inv
 
-@[to_additive]
+@[to_additive, continuity]
 lemma continuous.inv [topological_group α] [topological_space β] {f : β → α}
   (hf : continuous f) : continuous (λx, (f x)⁻¹) :=
 continuous_inv.comp hf
 
+attribute [continuity] continuous.neg
+
 @[to_additive]
 lemma continuous_on_inv [topological_group α] {s : set α} : continuous_on (λx:α, x⁻¹) s :=
 continuous_inv.continuous_on
@@ -250,7 +252,7 @@ end quotient_topological_group
 section topological_add_group
 variables [topological_space α] [add_group α]
 
-lemma continuous.sub [topological_add_group α] [topological_space β] {f : β → α} {g : β → α}
+@[continuity] lemma continuous.sub [topological_add_group α] [topological_space β] {f : β → α} {g : β → α}
   (hf : continuous f) (hg : continuous g) : continuous (λx, f x - g x) :=
 by simp [sub_eq_add_neg]; exact hf.add hg.neg
 

src/topology/algebra/module.lean

@@ -166,7 +166,7 @@ structure continuous_linear_map
   (M₂ : Type*) [topological_space M₂] [add_comm_monoid M₂]
   [semimodule R M] [semimodule R M₂]
   extends linear_map R M M₂ :=
-(cont : continuous to_fun)
+(cont : continuous to_fun . tactic.interactive.continuity')
 
 notation M ` →L[`:25 R `] ` M₂ := continuous_linear_map R M M₂
 
@@ -180,8 +180,8 @@ structure continuous_linear_equiv
   (M₂ : Type*) [topological_space M₂] [add_comm_monoid M₂]
   [semimodule R M] [semimodule R M₂]
   extends linear_equiv R M M₂ :=
-(continuous_to_fun  : continuous to_fun)
-(continuous_inv_fun : continuous inv_fun)
+(continuous_to_fun  : continuous to_fun . tactic.interactive.continuity')
+(continuous_inv_fun : continuous inv_fun . tactic.interactive.continuity')
 
 notation M ` ≃L[`:50 R `] ` M₂ := continuous_linear_equiv R M M₂
 
@@ -208,6 +208,7 @@ instance to_fun : has_coe_to_fun $ M →L[R] M₂ := ⟨λ _, M → M₂, λ f,
 @[simp] lemma coe_mk (f : M →ₗ[R] M₂) (h) : (mk f h : M →ₗ[R] M₂) = f := rfl
 @[simp] lemma coe_mk' (f : M →ₗ[R] M₂) (h) : (mk f h : M → M₂) = f := rfl
 
+@[continuity]
 protected lemma continuous (f : M →L[R] M₂) : continuous f := f.2
 
 theorem coe_injective : function.injective (coe : (M →L[R] M₂) → (M →ₗ[R] M₂)) :=
@@ -711,6 +712,10 @@ def to_homeomorph (e : M ≃L[R] M₂) : M ≃ₜ M₂ := { ..e }
 @[simp] lemma map_eq_zero_iff (e : M ≃L[R] M₂) {x : M} : e x = 0 ↔ x = 0 :=
 e.to_linear_equiv.map_eq_zero_iff
 
+attribute [continuity]
+  continuous_linear_equiv.continuous_to_fun continuous_linear_equiv.continuous_inv_fun
+
+@[continuity]
 protected lemma continuous (e : M ≃L[R] M₂) : continuous (e : M → M₂) :=
 e.continuous_to_fun
 
@@ -759,7 +764,6 @@ end
 { continuous_to_fun := e.continuous_inv_fun,
   continuous_inv_fun := e.continuous_to_fun,
   .. e.to_linear_equiv.symm }
-
 @[simp] lemma symm_to_linear_equiv (e : M ≃L[R] M₂) :
   e.symm.to_linear_equiv = e.to_linear_equiv.symm :=
 by { ext, refl }
@@ -769,7 +773,6 @@ by { ext, refl }
 { continuous_to_fun := e₂.continuous_to_fun.comp e₁.continuous_to_fun,
   continuous_inv_fun := e₁.continuous_inv_fun.comp e₂.continuous_inv_fun,
   .. e₁.to_linear_equiv.trans e₂.to_linear_equiv }
-
 @[simp] lemma trans_to_linear_equiv (e₁ : M ≃L[R] M₂) (e₂ : M₂ ≃L[R] M₃) :
   (e₁.trans e₂).to_linear_equiv = e₁.to_linear_equiv.trans e₂.to_linear_equiv :=
 by { ext, refl }
@@ -779,7 +782,6 @@ def prod (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) : (M × M₃) ≃L[R] (M
 { continuous_to_fun := e.continuous_to_fun.prod_map e'.continuous_to_fun,
   continuous_inv_fun := e.continuous_inv_fun.prod_map e'.continuous_inv_fun,
   .. e.to_linear_equiv.prod e'.to_linear_equiv }
-
 @[simp, norm_cast] lemma prod_apply (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (x) :
   e.prod e' x = (e x.1, e' x.2) := rfl
 
@@ -874,7 +876,6 @@ def skew_prod (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (f : M →L[R] M₄)
     (e'.continuous_inv_fun.comp $ continuous_snd.sub $ f.continuous.comp $
       e.continuous_inv_fun.comp continuous_fst),
 .. e.to_linear_equiv.skew_prod e'.to_linear_equiv ↑f  }
-
 @[simp] lemma skew_prod_apply (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (f : M →L[R] M₄) (x) :
   e.skew_prod e' f x = (e x.1, e' x.2 + f x.1) := rfl
 

src/topology/algebra/monoid.lean

@@ -38,12 +38,14 @@ variables [topological_space α] [has_mul α] [has_continuous_mul α]
 lemma continuous_mul : continuous (λp:α×α, p.1 * p.2) :=
 has_continuous_mul.continuous_mul
 
-@[to_additive]
+@[to_additive, continuity]
 lemma continuous.mul [topological_space β] {f : β → α} {g : β → α}
   (hf : continuous f) (hg : continuous g) :
   continuous (λx, f x * g x) :=
 continuous_mul.comp (hf.prod_mk hg)
 
+attribute [continuity] continuous.add
+
 @[to_additive]
 lemma continuous_mul_left (a : α) : continuous (λ b:α, a * b) :=
 continuous_const.mul continuous_id
@@ -111,10 +113,16 @@ continuous_iff_continuous_at.2 $ assume x, tendsto_list_prod l $ assume c hc,
   continuous_iff_continuous_at.1 (h c hc) x
 
 -- @[to_additive continuous_smul]
+@[continuity]
 lemma continuous_pow : ∀ n : ℕ, continuous (λ a : α, a ^ n)
 | 0 := by simpa using continuous_const
 | (k+1) := show continuous (λ (a : α), a * a ^ k), from continuous_id.mul (continuous_pow _)
 
+@[continuity]
+lemma continuous.pow {f : β → α} [topological_space β] (h : continuous f) (n : ℕ) :
+  continuous (λ b, (f b) ^ n) :=
+continuous.comp (continuous_pow n) h
+
 end has_continuous_mul
 
 section
@@ -139,14 +147,18 @@ lemma tendsto_finset_prod {f : γ → β → α} {x : filter β} {a : γ → α}
   (∀c∈s, tendsto (f c) x (𝓝 (a c))) → tendsto (λb, ∏ c in s, f c b) x (𝓝 (∏ c in s, a c)) :=
 tendsto_multiset_prod _
 
-@[to_additive]
+@[to_additive, continuity]
 lemma continuous_multiset_prod [topological_space β] {f : γ → β → α} (s : multiset γ) :
   (∀c∈s, continuous (f c)) → continuous (λa, (s.map (λc, f c a)).prod) :=
 by { rcases s with ⟨l⟩, simp, exact continuous_list_prod l }
 
-@[to_additive]
+attribute [continuity] continuous_multiset_sum
+
+@[to_additive, continuity]
 lemma continuous_finset_prod [topological_space β] {f : γ → β → α} (s : finset γ) :
   (∀c∈s, continuous (f c)) → continuous (λa, ∏ c in s, f c a) :=
 continuous_multiset_prod _
 
+attribute [continuity] continuous_finset_sum
+
 end

src/topology/algebra/multilinear.lean

@@ -67,6 +67,8 @@ variables [semiring R]
 instance : has_coe_to_fun (continuous_multilinear_map R M₁ M₂) :=
 ⟨_, λ f, f.to_multilinear_map.to_fun⟩
 
+attribute [continuity] cont
+
 @[simp] lemma coe_coe : (f.to_multilinear_map : (Π i, M₁ i) → M₂) = f := rfl
 
 @[ext] theorem ext {f f' : continuous_multilinear_map R M₁ M₂} (H : ∀ x, f x = f' x) : f = f' :=

src/topology/algebra/ordered.lean

@@ -339,11 +339,11 @@ lemma frontier_lt_subset_eq : frontier {b | f b < g b} ⊆ {b | f b = g b} :=
 by rw ← frontier_compl;
    convert frontier_le_subset_eq hg hf; simp [ext_iff, eq_comm]
 
-lemma continuous.max : continuous (λb, max (f b) (g b)) :=
+@[continuity] lemma continuous.max : continuous (λb, max (f b) (g b)) :=
 have ∀b∈frontier {b | f b ≤ g b}, g b = f b, from assume b hb, (frontier_le_subset_eq hf hg hb).symm,
 continuous_if this hg hf
 
-lemma continuous.min : continuous (λb, min (f b) (g b)) :=
+@[continuity] lemma continuous.min : continuous (λb, min (f b) (g b)) :=
 have ∀b∈frontier {b | f b ≤ g b}, f b = g b, from assume b hb, frontier_le_subset_eq hf hg hb,
 continuous_if this hf hg
 

src/topology/algebra/polynomial.lean

@@ -29,6 +29,7 @@ degree_pos_induction_on p h
         (by rw abv_neg abv; exact (hr z hz)))
         (le_trans (le_abs_self _) (abs_abv_sub_le_abv_sub _ _ _))⟩)
 
+@[continuity]
 lemma polynomial.continuous_eval {α} [comm_semiring α] [topological_space α]
   [topological_semiring α] (p : polynomial α) : continuous (λ x, p.eval x) :=
 begin

src/topology/compact_open.lean

@@ -15,7 +15,7 @@ open_locale topological_space
 namespace continuous_map
 
 section compact_open
-variables {α : Type} {β : Type*} {γ : Type*}
+variables {α : Type*} {β : Type*} {γ : Type*}
 variables [topological_space α] [topological_space β] [topological_space γ]
 
 def compact_open.gen (s : set α) (u : set β) : set C(α,β) := {f | f '' s ⊆ u}