equal
deleted
inserted
replaced
6149 have fh': "f holomorphic_on cball z ((r + dist w z) / 2)" |
6149 have fh': "f holomorphic_on cball z ((r + dist w z) / 2)" |
6150 apply (rule holomorphic_on_subset [OF holf]) |
6150 apply (rule holomorphic_on_subset [OF holf]) |
6151 apply (clarsimp simp del: divide_const_simps) |
6151 apply (clarsimp simp del: divide_const_simps) |
6152 apply (metis add.commute dist_commute le_less_trans mem_ball real_gt_half_sum w) |
6152 apply (metis add.commute dist_commute le_less_trans mem_ball real_gt_half_sum w) |
6153 done |
6153 done |
6154 \<comment>\<open>Replacing @{term r} and the original (weak) premises\<close> |
6154 \<comment> \<open>Replacing @{term r} and the original (weak) premises\<close> |
6155 obtain r where "0 < r" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r" |
6155 obtain r where "0 < r" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r" |
6156 apply (rule that [of "(r + dist w z) / 2"]) |
6156 apply (rule that [of "(r + dist w z) / 2"]) |
6157 apply (simp_all add: fh') |
6157 apply (simp_all add: fh') |
6158 apply (metis add_0_iff ball_eq_empty dist_nz dist_self empty_iff not_less pos_add_strict w) |
6158 apply (metis add_0_iff ball_eq_empty dist_nz dist_self empty_iff not_less pos_add_strict w) |
6159 apply (metis add_less_cancel_right dist_commute mem_ball mult_2_right w) |
6159 apply (metis add_less_cancel_right dist_commute mem_ball mult_2_right w) |