-- Module: Mathlib.Analysis.Complex.BranchLogRoot
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocPathConnectedSpace X
U : Set X
hUc : IsSimplyConnected U
hUo : IsOpen U
g : X → ℂ
hgc : ContinuousOn g U
hU₀ : 0 ∉ g '' U
have have₁ have₂ :
  ∀ (this : SimplyConnectedSpace.{u_1} (↑U : Type u_1)), ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g U
have₃ :
  ∀ (this : SimplyConnectedSpace.{u_1} (↑U : Type u_1)) (this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)),
    ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g U
have₄ :
  ∀ (this : SimplyConnectedSpace.{u_1} (↑U : Type u_1)) (this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)) (x₀ : X)
    (hx₀U : x₀ ∈ U), ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g U
have₅ :
  ∀ (this : SimplyConnectedSpace.{u_1} (↑U : Type u_1)) (this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)) (x₀ : X)
    (hx₀U : x₀ ∈ U) (hx₀ : g x₀ ≠ 0), ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g U
have₆ :
  ∀ (this : SimplyConnectedSpace.{u_1} (↑U : Type u_1)) (this : LocPathConnectedSpace.{u_1} (↑U : Type u_1))
    (x₀ : { x : X // x ∈ U }) (hx₀ : g (↑x₀ : X) ≠ 0), ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g U
have₇ :
  ∀ (this : SimplyConnectedSpace.{u_1} (↑U : Type u_1)) (this : LocPathConnectedSpace.{u_1} (↑U : Type u_1))
    (x₀ : { x : X // x ∈ U }) (hx₀ : g (↑x₀ : X) ≠ 0) (f : C((↑U : Type u_1), ℂ))
    (hf :
      Eq (α := (↑U : Type u_1) → ℂ) (cexp ∘ (⇑f : (a : (↑U : Type u_1)) → ℂ))
        (⇑{ toFun := U.restrict (π := fun (a : X) ↦ ℂ) g, continuous_toFun := ⋯ : C((↑U : Type u_1), ℂ) } :
          (a : (↑U : Type u_1)) → ℂ)),
    ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g U
have₈ :
  ∀ (this : SimplyConnectedSpace.{u_1} (↑U : Type u_1)) (this : LocPathConnectedSpace.{u_1} (↑U : Type u_1))
    (x₀ : { x : X // x ∈ U }) (hx₀ : g (↑x₀ : X) ≠ 0) (f : C((↑U : Type u_1), ℂ))
    (hf :
      Eq (α := (↑U : Type u_1) → ℂ) (cexp ∘ (⇑f : (a : (↑U : Type u_1)) → ℂ))
        (⇑{ toFun := U.restrict (π := fun (a : X) ↦ ℂ) g, continuous_toFun := ⋯ : C((↑U : Type u_1), ℂ) } :
          (a : (↑U : Type u_1)) → ℂ))
    (g_1 : X → ℂ) (hg : ∀ (z : (↑U : Type u_1)), g_1 (↑z : X) = (f : (a : (↑U : Type u_1)) → ℂ) z),
    ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g U
have₉ :
  ∀ (this : SimplyConnectedSpace.{u_1} (↑U : Type u_1)) (this : LocPathConnectedSpace.{u_1} (↑U : Type u_1))
    (x₀ : { x : X // x ∈ U }) (hx₀ : g (↑x₀ : X) ≠ 0) (f : C((↑U : Type u_1), ℂ))
    (hf :
      Eq (α := (↑U : Type u_1) → ℂ) (cexp ∘ (⇑f : (a : (↑U : Type u_1)) → ℂ))
        (⇑{ toFun := U.restrict (π := fun (a : X) ↦ ℂ) g, continuous_toFun := ⋯ : C((↑U : Type u_1), ℂ) } :
          (a : (↑U : Type u_1)) → ℂ))
    (g : X → ℂ) (hg : ∀ (z : (↑U : Type u_1)), g (↑z : X) = (f : (a : (↑U : Type u_1)) → ℂ) z), ContinuousOn g U
have₁₀ have₁₁ :
  ∀ (this : SimplyConnectedSpace.{u_1} (↑U : Type u_1)) (this : LocPathConnectedSpace.{u_1} (↑U : Type u_1))
    (x₀ : { x : X // x ∈ U }) (hx₀ : g (↑x₀ : X) ≠ 0) (f : C((↑U : Type u_1), ℂ))
    (hf :
      Eq (α := (↑U : Type u_1) → ℂ) (cexp ∘ (⇑f : (a : (↑U : Type u_1)) → ℂ))
        (⇑{ toFun := U.restrict (π := fun (a : X) ↦ ℂ) g, continuous_toFun := ⋯ : C((↑U : Type u_1), ℂ) } :
          (a : (↑U : Type u_1)) → ℂ))
    (g_1 : X → ℂ) (hg : ∀ (z : (↑U : Type u_1)), g_1 (↑z : X) = (f : (a : (↑U : Type u_1)) → ℂ) z),
    EqOn (cexp ∘ g_1) g U
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g U

Tactic:
classical
  have := hUc.simplyConnectedSpace
  have := hUo.locPathConnectedSpace
  rcases hUc.nonempty with ⟨x₀, hx₀U⟩
  have hx₀ : g x₀ ≠ 0 := ne_of_mem_of_not_mem (mem_image_of_mem g hx₀U) hU₀
  lift x₀ to U using hx₀U
  rcases isCoveringMapOn_exp.existsUnique_continuousMap_lifts
    ⟨U.restrict g, continuousOn_iff_continuous_restrict.mp hgc⟩ (exp_log hx₀)
    (fun x ↦ ne_of_mem_of_not_mem (mem_image_of_mem g x.2) hU₀) with ⟨f, ⟨-, hf⟩, -⟩
  obtain ⟨g, hg⟩ : ∃ g : X → ℂ, ∀ z : U, g z = f z :=
    ⟨fun z ↦ if hz : z ∈ U then f ⟨z, hz⟩ else 0, by simp⟩
  refine ⟨g, ?hg_cont, ?hg_inv⟩
  case hg_cont =>
    rw [continuousOn_iff_continuous_restrict]
    convert! map_continuous f
    ext z
    exact hg z
  case hg_inv =>
    intro x hx
    lift x to U using hx
    simpa [hg] using congr($hf x)

Premises used: IsSimplyConnected.nonempty, continuousOn_iff_continuous_restrict