Commit 2020-07-27 10:07 8c8d6a22

feat(topology/tactic): continuity faster and more powerful (#3545) Following up on the recent introduction of Reid's continuity tactic in #2879, I've made some tweaks that make it both faster and more capable.

1. we use apply_rules {md:=semireducible}, taking advantage of #3538. This makes examples like example : continuous (λ x : ℝ, exp ((max x (-x)) + sin (cos x))^2) := by continuity viable.
2. in apply_rules, if we pull in lemmas using an attribute, we reverse the list of lemmas (on the heuristic that older lemmas are more frequently applicable than newer lemmas)
3. in continuity, I removed the apply_assumption step in the tidy loop, since apply_rules is already calling assumption
4. also in the tidy loop, I moved intro1 above apply_rules. The example in the test file

example {κ ι : Type}
  (K : κ → Type) [∀ k, topological_space (K k)] (I : ι → Type) [∀ i, topological_space (I i)]
  (e : κ ≃ ι) (F : Π k, homeomorph (K k) (I (e k))) :
  continuous (λ (f : Π k, K k) (i : ι), F (e.symm i) (f (e.symm i))) :=
by show_term { continuity }

which previously timed out now runs happily even with -T50000.