[STATEMENT]
lemma residue_lmul:
  assumes "open s" "z \<in> s" and f_holo: "f holomorphic_on s - {z}"
  shows "residue (\<lambda>z. c * (f z)) z= c * residue f z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
proof (cases "c=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. c = 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
 2. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
c = 0

goal (2 subgoals):
 1. c = 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
 2. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
c = 0

goal (1 subgoal):
 1. residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
using residue_const
[PROOF STATE]
proof (prove)
using this:
c = 0
residue (\<lambda>_. ?c) ?z = 0

goal (1 subgoal):
 1. residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
residue (\<lambda>z. c * f z) z = c * residue f z

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
c \<noteq> 0

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
define c' where "c' \<equiv> 2 * pi * \<i>"
[PROOF STATE]
proof (state)
this:
c' \<equiv> complex_of_real (2 * pi) * \<i>

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
define f' where "f' \<equiv> (\<lambda>z. c * (f z))"
[PROOF STATE]
proof (state)
this:
f' \<equiv> \<lambda>z. c * f z

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
obtain e where "e>0" and e_cball:"cball z e \<subseteq> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>e. \<lbrakk>0 < e; cball z e \<subseteq> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>open s\<close> \<open>z\<in>s\<close>
[PROOF STATE]
proof (prove)
using this:
open s
z \<in> s

goal (1 subgoal):
 1. (\<And>e. \<lbrakk>0 < e; cball z e \<subseteq> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using open_contains_cball_eq
[PROOF STATE]
proof (prove)
using this:
open s
z \<in> s
open ?S \<Longrightarrow> \<forall>x. (x \<in> ?S) = (\<exists>e>0. cball x e \<subseteq> ?S)

goal (1 subgoal):
 1. (\<And>e. \<lbrakk>0 < e; cball z e \<subseteq> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < e
cball z e \<subseteq> s

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
have "(f' has_contour_integral c' * residue f' z) (circlepath z e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f' has_contour_integral c' * residue f' z) (circlepath z e)
[PROOF STEP]
unfolding f'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>z. c * f z) has_contour_integral c' * residue (\<lambda>z. c * f z) z) (circlepath z e)
[PROOF STEP]
using f_holo
[PROOF STATE]
proof (prove)
using this:
f holomorphic_on s - {z}

goal (1 subgoal):
 1. ((\<lambda>z. c * f z) has_contour_integral c' * residue (\<lambda>z. c * f z) z) (circlepath z e)
[PROOF STEP]
apply (intro base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>e>0\<close> _ e_cball,folded c'_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f holomorphic_on s - {z} \<Longrightarrow> (\<lambda>z. c * f z) holomorphic_on s - {z}
[PROOF STEP]
by (auto intro:holomorphic_intros)
[PROOF STATE]
proof (state)
this:
(f' has_contour_integral c' * residue f' z) (circlepath z e)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(f' has_contour_integral c' * residue f' z) (circlepath z e)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
have "(f' has_contour_integral c * (c' * residue f z)) (circlepath z e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f' has_contour_integral c * (c' * residue f z)) (circlepath z e)
[PROOF STEP]
unfolding f'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>z. c * f z) has_contour_integral c * (c' * residue f z)) (circlepath z e)
[PROOF STEP]
using f_holo
[PROOF STATE]
proof (prove)
using this:
f holomorphic_on s - {z}

goal (1 subgoal):
 1. ((\<lambda>z. c * f z) has_contour_integral c * (c' * residue f z)) (circlepath z e)
[PROOF STEP]
by (auto intro: has_contour_integral_lmul
      base_residue[OF \<open>open s\<close> \<open>z\<in>s\<close> \<open>e>0\<close> _ e_cball,folded c'_def])
[PROOF STATE]
proof (state)
this:
(f' has_contour_integral c * (c' * residue f z)) (circlepath z e)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(f' has_contour_integral c' * residue f' z) (circlepath z e)
(f' has_contour_integral c * (c' * residue f z)) (circlepath z e)
[PROOF STEP]
have "c' * residue f' z  = c * (c' * residue f z)"
[PROOF STATE]
proof (prove)
using this:
(f' has_contour_integral c' * residue f' z) (circlepath z e)
(f' has_contour_integral c * (c' * residue f z)) (circlepath z e)

goal (1 subgoal):
 1. c' * residue f' z = c * (c' * residue f z)
[PROOF STEP]
using has_contour_integral_unique
[PROOF STATE]
proof (prove)
using this:
(f' has_contour_integral c' * residue f' z) (circlepath z e)
(f' has_contour_integral c * (c' * residue f z)) (circlepath z e)
\<lbrakk>(?f has_contour_integral ?i) ?g; (?f has_contour_integral ?j) ?g\<rbrakk> \<Longrightarrow> ?i = ?j

goal (1 subgoal):
 1. c' * residue f' z = c * (c' * residue f z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c' * residue f' z = c * (c' * residue f z)

goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
c' * residue f' z = c * (c' * residue f z)

goal (1 subgoal):
 1. residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
unfolding f'_def c'_def
[PROOF STATE]
proof (prove)
using this:
complex_of_real (2 * pi) * \<i> * residue (\<lambda>z. c * f z) z = c * (complex_of_real (2 * pi) * \<i> * residue f z)

goal (1 subgoal):
 1. residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
complex_of_real (2 * pi) * \<i> * residue (\<lambda>z. c * f z) z = c * (complex_of_real (2 * pi) * \<i> * residue f z)
c \<noteq> 0

goal (1 subgoal):
 1. residue (\<lambda>z. c * f z) z = c * residue f z
[PROOF STEP]
by (auto simp add:field_simps)
[PROOF STATE]
proof (state)
this:
residue (\<lambda>z. c * f z) z = c * residue f z

goal:
No subgoals!
[PROOF STEP]
qed