sin_sin.lean

import topology.basic analysis.complex.exponential
import tactic.core
open real set

open tactic

meta def refine_list_expr : list expr → tactic unit
| []     := fail "no matching rule"
| (h::t) := do (refine ``(%%h _ _)) <|> refine_list_expr t

meta def apply_rules_with_refine (hs : list pexpr) (n : nat) : tactic unit :=
do l ← build_list_expr_for_apply hs,
   iterate_at_most_on_subgoals n (assumption <|> refine_list_expr l <|> apply_list_expr l)

open interactive interactive.types 
meta def apply_rules_with_refine_interactive (hs : parse pexpr_list_or_texpr) (n : nat := 50) : tactic unit :=
apply_rules_with_refine hs n

-- * sin(sin(x)) and friends are continuous on ℝ

lemma continuous_sin' : continuous (λ x : ℝ, sin x) := 
by apply_rules [continuous.comp, continuous_sin] 3

#print continuous_sin' 

lemma continuous_sin_sin : continuous (λ x : ℝ, sin(sin x)) := 
by apply_rules_with_refine_interactive [continuous.comp, continuous_sin] 30

lemma continuous_sin_sin_sin : continuous (λ x : ℝ, sin (sin (sin x))) := 
begin
refine continuous.comp _ _,
refine continuous.comp _ _,
apply continuous_sin,
apply continuous_sin,
apply continuous_sin,
end

#print continuous_sin_sin_sin