Quelle  Cartan.thy

theory Cartan
imports "HOL-Complex_Analysis.Complex_Analysis"

begin

section‹First Cartan Theorem›

text‹Ported from HOL Light. See
 Gianni Ciolli, Graziano Gentili, Marco Maggesi.
 A Certified Proof of the Cartan Fixed Point Theorems.
 J Automated Reasoning (2011) 47:319--336 DOI 10.1007/s10817-010-9198-6›

lemma deriv_left_inverse:
  assumes "f holomorphic_on S" and "g holomorphic_on T"
      and "open S" and "open T"
      and "f ` S ⊆ T"
      and [simp]: "∧z. z ∈ S ==> g (f z) = z"
      and "w ∈ S"
    shows "deriv f w * deriv g (f w) = 1"
proof -
  have "deriv f w * deriv g (f w) = deriv g (f w) * deriv f w"
    by (simp add: algebra_simps)
  also have "… = deriv (g o f) w"
    using assms
    by (metis analytic_on_imp_differentiable_at analytic_on_open deriv_chain image_subset_iff)
  also have "… = deriv id w"
    apply (rule complex_derivative_transform_within_open [where s=S])
    apply (rule assms holomorphic_on_compose_gen holomorphic_intros)+
    apply simp
    done
  also have "… = 1"
    using higher_deriv_id [of 1] by simp
  finally show ?thesis .
qed

lemma Cauchy_higher_deriv_bound:
    assumes holf: "f holomorphic_on (ball z r)"
        and contf: "continuous_on (cball z r) f"
        and "0 < r" and "0 < n"
        and fin : "∧w. w ∈ ball z r ==> f w ∈ ball y B0"
      shows "norm ((deriv ^^ n) f z) ≤ (fact n) * B0 / r^n"
proof -
  have "0 < B0" using ‹0 < r› fin [of z]
    by (metis ball_eq_empty ex_in_conv fin not_less)
  have le_B0: "∧w. cmod (w - z) ≤ r ==> cmod (f w - y) ≤ B0"
    apply (rule continuous_on_closure_norm_le [of "ball z r" "λw. f w - y"])
    apply (auto simp: ‹0 < r›  dist_norm norm_minus_commute)
    apply (rule continuous_intros contf)+
    using fin apply (simp add: dist_commute dist_norm less_eq_real_def)
    done
  have "(deriv ^^ n) f z = (deriv ^^ n) (λw. f w) z - (deriv ^^ n) (λw. y) z"
    using ‹0 < n› by simp
  also have "… = (deriv ^^ n) (λw. f w - y) z"
    by (rule higher_deriv_diff [OF holf, symmetric]) (auto simp: ‹0 < r› holomorphic_on_const)
  finally have "(deriv ^^ n) f z = (deriv ^^ n) (λw. f w - y) z" .
  have contf': "continuous_on (cball z r) (λu. f u - y)"
    by (rule contf continuous_intros)+
  have holf': "(λu. (f u - y)) holomorphic_on (ball z r)"
    by (simp add: holf holomorphic_on_diff holomorphic_on_const)
  define a where "a = (2 * pi)/(fact n)"
  have "0 < a"  by (simp add: a_def)
  have "B0/r^(Suc n)*2 * pi * r = a*((fact n)*B0/r^n)"
    using ‹0 < r› by (simp add: a_def divide_simps)
  have der_dif: "(deriv ^^ n) (λw. f w - y) z = (deriv ^^ n) f z"
    using ‹0 < r› ‹0 < n›
    by (auto simp: higher_deriv_diff [OF holf holomorphic_on_const])
  have "norm ((2 * of_real pi * i)/(fact n) * (deriv ^^ n) (λw. f w - y) z)
        ≤ (B0/r^(Suc n)) * (2 * pi * r)"
    apply (rule has_contour_integral_bound_circlepath [of "(λu. (f u - y)/(u - z)^(Suc n))" _ z])
    using Cauchy_has_contour_integral_higher_derivative_circlepath [OF contf' holf']
    using ‹0 < B0› ‹0 < r›
    apply (auto simp: norm_divide norm_mult norm_power divide_simps le_B0)
    done
  then show ?thesis
    using ‹0 < r›
    by (auto simp: norm_divide norm_mult norm_power field_simps der_dif le_B0)
qed

lemma higher_deriv_comp_lemma:
    assumes s: "open s" and holf: "f holomorphic_on s"
        and "z ∈ s"
        and t: "open t" and holg: "g holomorphic_on t"
        and fst: "f ` s ⊆ t"
        and n: "i ≤ n"
        and dfz: "deriv f z = 1" and zero: "∧i. [1 < i; i ≤ n] ==> (deriv ^^ i) f z = 0"
      shows "(deriv ^^ i) (g o f) z = (deriv ^^ i) g (f z)"
using n holg
proof (induction i arbitrary: g)
  case 0 then show ?case by simp
next
  case (Suc i)
  have "g ∘ f holomorphic_on s" using "Suc.prems" holf
    using fst  by (simp add: holomorphic_on_compose_gen image_subset_iff)
  then have 1: "deriv (g ∘ f) holomorphic_on s"
    by (simp add: holomorphic_deriv s)
  have dg: "deriv g holomorphic_on t"
    using Suc.prems by (simp add: Suc.prems(2) holomorphic_deriv t)
  then have "deriv g holomorphic_on f ` s"
    using fst  by (simp add: holomorphic_on_subset image_subset_iff)
  then have dgf: "(deriv g o f) holomorphic_on s"
    by (simp add: holf holomorphic_on_compose)
  then have 2: "(λw. (deriv g o f) w * deriv f w) holomorphic_on s"
    by (blast intro: holomorphic_intros holomorphic_on_compose holf s)
  have "(deriv ^^ i) (deriv (g o f)) z = (deriv ^^ i) (λw. deriv g (f w) * deriv f w) z"
    apply (rule higher_deriv_transform_within_open [OF 1 2 [unfolded o_def] s ‹z ∈ s›])
    apply (rule deriv_chain)
    using holf Suc.prems fst apply (auto simp: holomorphic_on_imp_differentiable_at s t)
    done
  also have "… = (∑j=0..i. of_nat(i choose j) * (deriv ^^ j) (λw. deriv g (f w)) z * (deriv ^^ (i - j)) (deriv f) z)"
    apply (rule higher_deriv_mult [OF dgf [unfolded o_def] _ s ‹z ∈ s›])
    by (simp add: holf holomorphic_deriv s)
  also have "… = (∑j=i..i. of_nat(i choose j) * (deriv ^^ j) (λw. deriv g (f w)) z * (deriv ^^ Suc (i - j)) f z)"
  proof -
    have *: "(deriv ^^ j) (λw. deriv g (f w)) z = 0"  if "j < i" and nz: "(deriv ^^ (i - j)) (deriv f) z ≠ 0" for j
    proof -
      have "1 < Suc (i - j)" "Suc (i - j) ≤ n"
        using ‹j < i› ‹Suc i ≤ n› by auto
      then show ?thesis  by (metis comp_def funpow.simps(2) funpow_swap1 zero nz)
    qed
    then show ?thesis
      apply (simp only: funpow_Suc_right o_def)
      apply (rule comm_monoid_add_class.sum.mono_neutral_right, auto)
      done
  qed
  also have "… = (deriv ^^ i) (deriv g) (f z)"
    using Suc.IH [OF _ dg] Suc.prems by (simp add: dfz)
  finally show ?case
    by (simp only: funpow_Suc_right o_def)
qed


lemma higher_deriv_comp_iter_lemma:
    assumes s: "open s" and holf: "f holomorphic_on s"
        and fss: "f ` s ⊆ s"
        and "z ∈ s" and [simp]: "f z = z"
        and n: "i ≤ n"
        and dfz: "deriv f z = 1" and zero: "∧i. [1 < i; i ≤ n] ==> (deriv ^^ i) f z = 0"
      shows "(deriv ^^ i) (f^^m) z = (deriv ^^ i) f z"
proof -
  have holfm: "(f^^m) holomorphic_on s" for m
    apply (induction m, simp add: holomorphic_on_ident)
    apply (simp only: funpow_Suc_right holomorphic_on_compose_gen [OF holf _ fss])
    done
  show ?thesis using n
  proof (induction m)
    case 0 with dfz show ?case
      by (auto simp: zero)
  next
    case (Suc m)
    have "(deriv ^^ i) (f ^^ m ∘ f) z = (deriv ^^ i) (f ^^ m) (f z)"
      using Suc.prems holfm ‹z ∈ s› dfz fss higher_deriv_comp_lemma holf s zero by blast
    also have "… = (deriv ^^ i) f z"
      by (simp add: Suc)
    finally show ?case
      by (simp only: funpow_Suc_right)
  qed
qed

lemma higher_deriv_iter_top_lemma:
    assumes s: "open s" and holf: "f holomorphic_on s"
        and fss: "f ` s ⊆ s"
        and "z ∈ s" and [simp]: "f z = z"
        and dfz [simp]: "deriv f z = 1"
        and n: "1 < n" "∧i. [1 < i; i < n] ==> (deriv ^^ i) f z = 0"
      shows "(deriv ^^ n) (f ^^ m) z = m * (deriv ^^ n) f z"
using n
proof (induction n arbitrary: m)
  case 0 then show ?case by simp
next
  case (Suc n)
  have [simp]: "(f^^m) z = z" for m
    by (induction m) auto
  have fms_sb: "(f^^m) ` s ⊆ s" for m
    apply (induction m)
    using fss
    apply force+
    done
  have holfm: "(f^^m) holomorphic_on s" for m
    apply (induction m, simp add: holomorphic_on_ident)
    apply (simp only: funpow_Suc_right holomorphic_on_compose_gen [OF holf _ fss])
    done
  then have holdfm: "deriv (f ^^ m) holomorphic_on s" for m
    by (simp add: holomorphic_deriv s)
  have holdffm: "(λz. deriv f ((f ^^ m) z)) holomorphic_on s" for m
    apply (rule holomorphic_on_compose_gen [where g="deriv f" and t=s, unfolded o_def])
    using s ‹z ∈ s› holfm holf fms_sb by (auto intro: holomorphic_intros)
  have f_cd_w: "∧w. w ∈ s ==> f field_differentiable at w"
    using holf holomorphic_on_imp_differentiable_at s by blast
  have f_cd_mw: "∧m w. w ∈ s ==> (f^^m) field_differentiable at w"
    using holfm holomorphic_on_imp_differentiable_at s by auto
  have der_fm [simp]: "deriv (f ^^ m) z = 1" for m
    apply (induction m, simp add: deriv_ident)
    apply (subst funpow_Suc_right)
    apply (subst deriv_chain)
    using ‹z ∈ s› holfm holomorphic_on_imp_differentiable_at s f_cd_w apply auto
    done
  note Suc(3) [simp]
  note n_Suc = Suc
  show ?case
  proof (induction m)
    case 0 with n_Suc show ?case
      by (metis Zero_not_Suc funpow_simps_right(1) higher_deriv_id lambda_zero nat_neq_iff of_nat_0)
  next
    case (Suc m)
    have deriv_nffm: "(deriv ^^ n) (deriv f o (f ^^ m)) z = (deriv ^^ n) (deriv f) ((f ^^ m) z)"
      apply (rule higher_deriv_comp_lemma [OF s holfm ‹z ∈ s› s _ fms_sb order_refl])
      using ‹z ∈ s› fss higher_deriv_comp_iter_lemma holf holf holomorphic_deriv s
        apply auto
      done
    have "deriv (f ^^ m ∘ f) holomorphic_on s"
      by (metis funpow_Suc_right holdfm)
    moreover have "(λw. deriv f ((f ^^ m) w) * deriv (f ^^ m) w) holomorphic_on s"
      by (rule holomorphic_on_mult [OF holdffm holdfm])
    ultimately have "(deriv ^^ n) (deriv (f ^^ m ∘ f)) z = (deriv ^^ n) (λw. deriv f ((f ^^ m) w) * deriv (f ^^ m) w) z"
      apply (rule higher_deriv_transform_within_open [OF _ _ s ‹z ∈ s›])
      by (metis comp_funpow deriv_chain f_cd_mw f_cd_w fms_sb funpow_swap1 image_subset_iff o_id)
    also have "… =
          (∑i=0..n. of_nat(n choose i) * (deriv ^^ i) (λw. deriv f ((f ^^ m) w)) z *
                     (deriv ^^ (n - i)) (deriv (f ^^ m)) z)"
      by (rule higher_deriv_mult [OF holdffm holdfm s ‹z ∈ s›])
    also have "… = (∑i ∈ {0,n}. of_nat(n choose i) * (deriv ^^ i) (λw. deriv f ((f ^^ m) w)) z *
                     (deriv ^^ (n - i)) (deriv (f ^^ m)) z)"
    proof -
      have *: "(deriv ^^ i) (λw. deriv f ((f ^^ m) w)) z = 0"  if "i ≤ n" "0 < i" "i ≠ n" and nz: "(deriv ^^ (n - i)) (deriv (f ^^ m)) z ≠ 0" for i
      proof -
        have less: "1 < Suc (n-i)" and le: "Suc (n-i) ≤ n"
          using that by auto
        have "(deriv ^^ (Suc (n - i))) (f ^^ m) z = (deriv ^^(Suc (n - i))) f z"
          apply (rule higher_deriv_comp_iter_lemma [OF s holf fss ‹z ∈ s› ‹f z = z› le dfz])
          by simp
        also have "… = 0"
          using n_Suc(3) less le le_imp_less_Suc by blast
        finally have "(deriv ^^ (Suc (n - i))) (f ^^ m) z = 0" .
        then show ?thesis by (simp add: funpow_swap1 nz)
      qed
      show ?thesis
        by (rule comm_monoid_add_class.sum.mono_neutral_right) (auto simp: *)
    qed
    also have "… = of_nat (Suc m) * (deriv ^^ n) (deriv f) z"
      apply (subst Groups_Big.comm_monoid_add_class.sum.insert)
      apply (simp_all add: deriv_nffm [unfolded o_def] of_nat_Suc [of 0] del: of_nat_Suc)
      using n_Suc(2) Suc
      apply (auto simp del: funpow.simps simp: algebra_simps funpow_simps_right)
      done
    finally have "(deriv ^^ n) (deriv (f ^^ m ∘ f)) z = of_nat (Suc m) * (deriv ^^ n) (deriv f) z" .
    then show ?case
      apply (simp only: funpow_Suc_right)
      apply (simp add: o_def del: of_nat_Suc)
      done
  qed
qed


text‹Should be proved for n-dimensional vectors of complex numbers›
theorem first_Cartan_dim_1:
    assumes holf: "f holomorphic_on s"
        and "open s" "connected s" "bounded s"
        and fss: "f ` s ⊆ s"
        and "z ∈ s" and [simp]: "f z = z"
        and dfz [simp]: "deriv f z = 1"
        and "w ∈ s"
      shows "f w = w"
proof -
  obtain c where "0 < c" and c: "s ⊆ ball z c"
    using ‹bounded s› bounded_subset_ballD by blast
  obtain r where "0 < r" and r: "cball z r ⊆ s"
    using ‹z ∈ s› open_contains_cball ‹open s› by blast
  then have bzr: "ball z r ⊆ s" using ball_subset_cball by blast
  have fms_sb: "(f^^m) ` s ⊆ s" for m
    apply (induction m)
    using fss apply force+
    done
  have holfm: "(f^^m) holomorphic_on s" for m
    apply (induction m, simp add: holomorphic_on_ident)
    apply (simp only: funpow_Suc_right holomorphic_on_compose_gen [OF holf _ fss])
    done
  have *: "(deriv ^^ n) f z = (deriv ^^ n) id z" for n
  proof -
    consider "n = 0" | "n = 1" | "1 < n" by arith
    then show ?thesis
    proof cases
      assume "n = 0" then show ?thesis by force
    next
      assume "n = 1" then show ?thesis by force
    next
      assume n1: "n > 1"
      then have "(deriv ^^ n) f z = 0"
      proof (induction n rule: less_induct)
        case (less n)
        have le: "real m * cmod ((deriv ^^ n) f z) ≤ fact n * c / r ^ n" if "m≠0" for m
        proof -
          have holfm': "(f ^^ m) holomorphic_on ball z r"
            using holfm bzr holomorphic_on_subset by blast
          then have contfm': "continuous_on (cball z r) (f ^^ m)"
            using ‹cball z r ⊆ s› holfm holomorphic_on_imp_continuous_on holomorphic_on_subset by blast
          have "real m * cmod ((deriv ^^ n) f z) = cmod (real m * (deriv ^^ n) f z)"
            by (simp add: norm_mult)
          also have "… = cmod ((deriv ^^ n) (f ^^ m) z)"
            apply (subst higher_deriv_iter_top_lemma [OF ‹open s› holf fss ‹z ∈ s› ‹f z = z› dfz])
            using less apply auto
            done
          also have "… ≤ fact n * c / r ^ n"
            apply (rule Cauchy_higher_deriv_bound [OF holfm' contfm' ‹0 < r›, where y=z])
            using less.prems apply linarith
            using fms_sb c r ball_subset_cball
            apply blast
            done
          finally show ?thesis .
        qed
        have "cmod ((deriv ^^ n) f z) = 0"
        proof (rule real_archimedian_rdiv_eq_0)
          show "∧m. 0 < m ==> real m * cmod ((deriv ^^ n) f z) ≤ fact n * c / r ^ n"
            using ‹0 < r› ‹0 < c› le by (simp add: divide_simps)
        qed auto
        then show ?case by simp
      qed
      with n1 show ?thesis by simp
    qed
  qed
  have "f w = id w"
    by (rule holomorphic_fun_eq_on_connected
                 [OF holf holomorphic_on_id ‹open s› ‹connected s› * ‹z ∈ s› ‹w ∈ s›])
  also have "… = w" by simp
  finally show ?thesis .
qed


text‹Second Cartan Theorem.›

lemma Cartan_is_linear:
  assumes holf: "f holomorphic_on s"
      and "open s" and "connected s"
      and "0 ∈ s"
      and ins: "∧u z. [norm u = 1; z ∈ s] ==> u * z ∈ s"
      and feq: "∧u z. [norm u = 1; z ∈ s] ==> f (u * z) = u * f z"
    shows "∃c. ∀z ∈ s. f z = c * z"
proof -
  have [simp]: "f 0 = 0"
    using feq [of "-1" 0] assms by simp
  have uneq: "u^n * (deriv ^^ n) f (u * z) = u * (deriv ^^ n) f z"
       if "norm u = 1" "z ∈ s" for n u z
  proof -
    have holfuw: "(λw. f (u * w)) holomorphic_on s"
      apply (rule holomorphic_on_compose_gen [OF _ holf, unfolded o_def])
      using that ins by (auto simp: holomorphic_on_linear)
    have hol_d_fuw: "(deriv ^^ n) (λw. u * f w) holomorphic_on s" for n
      by (rule holomorphic_higher_deriv holomorphic_intros holf assms)+
    have *: "(deriv ^^ n) (λw. u * f w) z = u * (deriv ^^ n) f z" if "z ∈ s" for z
    using that
    proof (induction n arbitrary: z)
      case 0 then show ?case by simp
    next
      case (Suc n)
      have "deriv ((deriv ^^ n) (λw. u * f w)) z = deriv (λw. u * (deriv ^^ n) f w) z"
        apply (rule complex_derivative_transform_within_open [OF hol_d_fuw])
        apply (auto intro!: holomorphic_higher_deriv holomorphic_intros assms Suc)
        done
      also have "… = u * deriv ((deriv ^^ n) f) z"
        apply (rule deriv_cmult)
        using Suc ‹open s› holf holomorphic_higher_deriv holomorphic_on_imp_differentiable_at by blast
      finally show ?case by simp
    qed
    have "(deriv ^^ n) (λw. f (u * w)) z = u ^ n * (deriv ^^ n) f (u * z)"
      apply (rule higher_deriv_compose_linear [OF holf ‹open s› ‹open s›])
      apply (simp add: that)
      apply (simp add: ins that)
      done
    moreover have "(deriv ^^ n) (λw. f (u * w)) z = u * (deriv ^^ n) f z"
      apply (subst higher_deriv_transform_within_open [OF holfuw, of "λw. u * f w"])
      apply (rule holomorphic_intros holf assms that)+
      apply blast
      using * ‹z ∈ s› apply blast
      done
    ultimately show ?thesis by metis
  qed
  have dnf0: "(deriv ^^ n) f 0 = 0" if len: "2 ≤ n" for n
  proof -
    have **: "z = 0" if "∧u::complex. norm u = 1 ==> u ^ n * z = u * z" for z
    proof -
      have "∃u::complex. norm u = 1 ∧ u ^ n ≠ u"
        using complex_not_root_unity [of "n-1"] len
        apply (simp add: algebra_simps le_diff_conv2, clarify)
        apply (rule_tac x=u in exI)
        apply (subst (asm) power_diff)
        apply auto
        done
      with that show ?thesis
        by auto
    qed
    show ?thesis
      apply (rule **)
      using uneq [OF _ ‹0 ∈ s›]
      by force
  qed
  show ?thesis
    apply (rule_tac x = "deriv f 0" in exI, clarify)
    apply (rule holomorphic_fun_eq_on_connected [OF holf _ ‹open s› ‹connected s› _ ‹0 ∈ s›])
    using dnf0 apply (auto simp: holomorphic_on_linear)
    done
qed

text‹Should be proved for n-dimensional vectors of complex numbers›
theorem second_Cartan_dim_1:
  assumes holf: "f holomorphic_on ball 0 r"
      and holg: "g holomorphic_on ball 0 r"
      and [simp]: "f 0 = 0" and [simp]: "g 0 = 0"
      and ballf: "∧z. z ∈ ball 0 r ==> f z ∈ ball 0 r"
      and ballg: "∧z. z ∈ ball 0 r ==> g z ∈ ball 0 r"
      and fg: "∧z. z ∈ ball 0 r ==> f (g z) = z"
      and gf: "∧z. z ∈ ball 0 r ==> g (f z) = z"
      and "0 < r"
    shows "∃t. ∀z ∈ ball 0 r. g z = exp(i * of_real t) * z"
proof -
  have c_le_1: "c ≤ 1"
    if "0 ≤ c" "∧x. 0 ≤ x ==> x < r ==> c * x < r" for c
  proof -
    have rst: "∧r s t::real. 0 = r ∨ s/r < t ∨ r < 0 ∨ ¬ s < r * t"
      by (metis (no_types) mult_less_cancel_left_disj nonzero_mult_div_cancel_left times_divide_eq_right)
    { assume "¬ r < c ∧ c * (c * (c * (c * r))) < 1"
     then have "1 ≤ c ==> (∃r. ¬ 1 < r ∧ ¬ r < c)"
          using ‹0 ≤ c› by (metis (full_types) less_eq_real_def mult.right_neutral mult_left_mono not_less)
      then have "¬ 1 < c ∨ ¬ 1 ≤ c"
        by linarith }
    moreover
    { have "¬ 0 ≤ r / c ==> ¬ 1 ≤ c"
          using ‹0 < r› by force
      then have "1 < c ==> ¬ 1 ≤ c"
        using rst ‹0 < r› that
        by (metis div_by_1 frac_less2 less_le_trans mult.commute not_le order_refl pos_divide_le_eq zero_less_one) }
    ultimately show ?thesis
      by (metis (no_types) linear not_less)
  qed
  have ugeq: "u * g z = g (u * z)" if nou: "norm u = 1" and z: "z ∈ ball 0 r" for u z
  proof -
    have [simp]: "u ≠ 0" using that by auto
    have hol1: "(λa. f (u * g a) / u) holomorphic_on ball 0 r"
      apply (rule holomorphic_intros)
      apply (rule holomorphic_on_compose_gen [OF _ holf, unfolded o_def])
      apply (rule holomorphic_intros holg)+
      using nou ballg
      apply (auto simp: dist_norm norm_mult holomorphic_on_const)
      done
    have cdf: "f field_differentiable at 0"
      using ‹0 < r› holf holomorphic_on_imp_differentiable_at by auto
    have cdg: "g field_differentiable at 0"
      using ‹0 < r› holg holomorphic_on_imp_differentiable_at by auto
    have cd_fug: "(λa. f (u * g a)) field_differentiable at 0"
      apply (rule field_differentiable_compose [where g=f and f = "λa. (u * g a)", unfolded o_def])
      apply (rule derivative_intros)+
      using cdf cdg
      apply auto
      done
    have "deriv g 0 = deriv g (f 0)"
      by simp
    then have "deriv f 0 * deriv g 0 = 1"
      by (metis open_ball ‹0 < r› ballf centre_in_ball deriv_left_inverse gf holf holg image_subsetI)
    then have equ: "deriv f 0 * deriv (λa. u * g a) 0 = u"
      by (simp add: cdg deriv_cmult)
    have der1: "deriv (λa. f (u * g a) / u) 0 = 1"
      apply (simp add: field_class.field_divide_inverse deriv_cmult_right [OF cd_fug])
      apply (subst deriv_chain [where g=f and f = "λa. (u * g a)", unfolded o_def])
      apply (rule derivative_intros cdf cdg | simp add: equ)+
      done
    have fugeq: "∧w. w ∈ ball 0 r ==> f (u * g w) / u = w"
      apply (rule first_Cartan_dim_1 [OF hol1, where z=0])
      apply (simp_all add: ‹0 < r›)
      apply (auto simp: der1)
      using nou ballf ballg
      apply (simp add: dist_norm norm_mult norm_divide)
      done
    have "f(u * g z) = u * z"
      by (metis ‹u ≠ 0› fugeq nonzero_mult_div_cancel_left z times_divide_eq_right)
    also have "… = f (g (u * z))"
      by (metis (no_types, lifting) fg mem_ball_0 mult_cancel_right2 norm_mult nou z)
    finally have "f(u * g z) = f (g (u * z))" .
    then have "g (f (u * g z)) = g (f (g (u * z)))"
      by simp
    then show ?thesis
      apply (subst (asm) gf)
      apply (simp add: dist_norm norm_mult nou)
      using ballg mem_ball_0 z apply blast
      apply (subst (asm) gf)
      apply (simp add: dist_norm norm_mult nou)
      apply (metis ballg mem_ball_0 mult.left_neutral norm_mult nou z, simp)
      done
  qed
  obtain c where c: "∧z. z ∈ ball 0 r ==> g z = c * z"
    apply (rule exE [OF Cartan_is_linear [OF holg]])
    apply (simp_all add: ‹0 < r› ugeq)
    apply (auto simp: dist_norm norm_mult)
    done
  have gr2: "g (f (r/2)) = c * f(r/2)"
    apply (rule c) using ‹0 < r› ballf mem_ball_0 by force
  then have "norm c > 0"
    using ‹0 < r›
    by simp (metis ‹f 0 = 0› c dist_commute fg mem_ball mult_zero_left perfect_choose_dist)
  then have [simp]: "c ≠ 0" by auto
  have xless: "x < r * cmod c" if "0 ≤ x" "x < r" for x
  proof -
    have "x = norm (g (f (of_real x)))"
    proof -
      have "r > cmod (of_real x)"
        by (simp add: that)
      then have "complex_of_real x ∈ ball 0 r"
        using mem_ball_0 by blast
      then show ?thesis
        using gf ‹0 ≤ x› by force
    qed
    moreover have "f (complex_of_real x) ∈ ball 0 r"
      using ballf that by auto
    ultimately show ?thesis
      by (metis ‹0 < cmod c› c mem_ball_0 mult.commute mult_less_cancel_left_pos norm_mult)
  qed
  have 11: "1 / norm c ≤ 1"
    using xless by (intro c_le_1) (auto simp: divide_simps)
  have "[0 ≤ x; x < r] ==> cmod c * x < r" for x
    using c [of x] ballg [of x] by (auto simp: norm_mult)
    then have "norm c ≤ 1"
    by (force intro: c_le_1)
  moreover have "1 ≤ norm c"
    using 11 by simp
  ultimately have "norm c = 1"  by (rule antisym)
  with complex_norm_eq_1_exp c show ?thesis
    by metis
qed

end