[STATEMENT]
lemma tanh_real_at_top: "(tanh \<longlongrightarrow> (1::real)) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (tanh \<longlongrightarrow> 1) at_top
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (tanh \<longlongrightarrow> 1) at_top
[PROOF STEP]
have "((\<lambda>x::real. (1 - exp (- 2 * x)) / (1 + exp (- 2 * x))) \<longlongrightarrow> (1 - 0) / (1 + 0)) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. (1 - exp (- 2 * x)) / (1 + exp (- 2 * x))) \<longlongrightarrow> (1 - 0) / (1 + 0)) at_top
[PROOF STEP]
by (intro tendsto_intros filterlim_compose[OF exp_at_bot]
              filterlim_tendsto_neg_mult_at_bot[OF tendsto_const] filterlim_ident) auto
[PROOF STATE]
proof (state)
this:
((\<lambda>x. (1 - exp (- 2 * x)) / (1 + exp (- 2 * x))) \<longlongrightarrow> (1 - 0) / (1 + 0)) at_top

goal (1 subgoal):
 1. (tanh \<longlongrightarrow> 1) at_top
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>x. (1 - exp (- 2 * x)) / (1 + exp (- 2 * x))) \<longlongrightarrow> (1 - 0) / (1 + 0)) at_top

goal (1 subgoal):
 1. (tanh \<longlongrightarrow> 1) at_top
[PROOF STEP]
have "(\<lambda>x::real. (1 - exp (- 2 * x)) / (1 + exp (- 2 * x))) = tanh"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. (1 - exp (- 2 * x)) / (1 + exp (- 2 * x))) = tanh
[PROOF STEP]
by (rule ext) (simp add: tanh_real_altdef)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (1 - exp (- 2 * x)) / (1 + exp (- 2 * x))) = tanh

goal (1 subgoal):
 1. (tanh \<longlongrightarrow> 1) at_top
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(tanh \<longlongrightarrow> (1 - 0) / (1 + 0)) at_top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(tanh \<longlongrightarrow> (1 - 0) / (1 + 0)) at_top

goal (1 subgoal):
 1. (tanh \<longlongrightarrow> 1) at_top
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(tanh \<longlongrightarrow> 1) at_top

goal:
No subgoals!
[PROOF STEP]
qed