awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g U
have 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
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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g U
have 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
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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g U
have 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
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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) 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 : 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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) 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 := sorry : C((↑U : Type u_1), ℂ) } :
        (a : (↑U : Type u_1)) → ℂ)),
  ∃ (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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) 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 := sorry : 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
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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
n : ℕ
hn : n ≠ 0
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
have rcases : ∀ (f : X → ℂ) (hfc : ContinuousOn f U) (hf : EqOn (cexp ∘ f) g U),
  ∃ (f : X → ℂ), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
Tactic: rcases exists_continuousOn_eqOn_exp_comp hUc hUo hgc hU₀ with ⟨f, hfc, hf⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
have refine_1 : ContinuousOn (Y := ℂ)
  (U.piecewise (β := fun (a : X) ↦ ℂ) (fun (x : X) ↦ cexp (f x / (↑n : ℂ))) fun (x : X) ↦
    g x ^ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ))
  U
Tactic: refine ⟨U.piecewise (exp <| f · / n) (g · ^ (1 / n : ℂ)), ?_, fun z ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
refine_1 :
  ContinuousOn (Y := ℂ)
    (U.piecewise (β := fun (a : X) ↦ ℂ) (fun (x : X) ↦ cexp (f x / (↑n : ℂ))) fun (x : X) ↦
      g x ^ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ))
    U
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
have refine_2 : ∀ (z : X),
  HPow.hPow (α := ℂ)
      (U.piecewise (β := fun (a : X) ↦ ℂ) (fun (x : X) ↦ cexp (f x / (↑n : ℂ)))
          (fun (x : X) ↦ g x ^ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)) z :
        ℂ)
      n =
    g z
Tactic: refine ⟨U.piecewise (exp <| f · / n) (g · ^ (1 / n : ℂ)), ?_, fun z ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
⊢ ContinuousOn (Y := ℂ)
    (U.piecewise (β := fun (a : X) ↦ ℂ) (fun (x : X) ↦ cexp (f x / (↑n : ℂ))) fun (x : X) ↦
      g x ^ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ))
    U
have refine_1 : ContinuousOn (Y := ℂ) (fun (x : X) ↦ cexp (f x / (↑n : ℂ))) U
Tactic: rw [continuousOn_iff_continuous_restrict, restrict_piecewise,
      ← continuousOn_iff_continuous_restrict]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
⊢ ContinuousOn (Y := ℂ) (fun (x : X) ↦ cexp (f x / (↑n : ℂ))) U
have funProp : ∀ x ∈ U, Ne (α := ℂ) (↑n : ℂ) 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
z : X
⊢ HPow.hPow (α := ℂ)
      (U.piecewise (β := fun (a : X) ↦ ℂ) (fun (x : X) ↦ cexp (f x / (↑n : ℂ)))
          (fun (x : X) ↦ g x ^ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)) z :
        ℂ)
      n =
    g z
have pos : ∀ (hz : z ∈ U),
  HPow.hPow (α := ℂ)
      (U.piecewise (β := fun (a : X) ↦ ℂ) (fun (x : X) ↦ cexp (f x / (↑n : ℂ)))
          (fun (x : X) ↦ g x ^ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)) z :
        ℂ)
      n =
    g z
Tactic: by_cases hz : z ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
z : X
pos :
  ∀ (hz : z ∈ U),
    HPow.hPow (α := ℂ)
        (U.piecewise (β := fun (a : X) ↦ ℂ) (fun (x : X) ↦ cexp (f x / (↑n : ℂ)))
            (fun (x : X) ↦ g x ^ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)) z :
          ℂ)
        n =
      g z
⊢ HPow.hPow (α := ℂ)
      (U.piecewise (β := fun (a : X) ↦ ℂ) (fun (x : X) ↦ cexp (f x / (↑n : ℂ)))
          (fun (x : X) ↦ g x ^ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)) z :
        ℂ)
      n =
    g z
have neg : ∀ (hz : z ∉ U),
  HPow.hPow (α := ℂ)
      (U.piecewise (β := fun (a : X) ↦ ℂ) (fun (x : X) ↦ cexp (f x / (↑n : ℂ)))
          (fun (x : X) ↦ g x ^ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)) z :
        ℂ)
      n =
    g z
Tactic: by_cases hz : z ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
n : ℕ
hn : n ≠ 0
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
have rcases : ∀ (f : X → ℂ) (hfc : ContinuousOn f U) (hf : EqOn (cexp ∘ f) g U),
  ∃ (f : X → ℂ), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
Tactic: classical
  rcases exists_continuousOn_eqOn_exp_comp hUc hUo hgc hU₀ with ⟨f, hfc, hf⟩
  refine ⟨U.piecewise (exp <| f · / n) (g · ^ (1 / n : ℂ)), ?_, fun z ↦ ?_⟩
  · rw [continuousOn_iff_continuous_restrict, restrict_piecewise,
      ← continuousOn_iff_continuous_restrict]
    fun_prop
  · by_cases hz : z ∈ U
    · simp [hz, ← exp_nat_mul, mul_div_cancel₀ (b := ↑n) (f z) (mod_cast hn), ← hf hz,
        Function.comp_apply]
    · simp [hz, ← cpow_mul_nat, hn]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
n : ℕ
hn : n ≠ 0
rcases :
  ∀ (f : X → ℂ) (hfc : ContinuousOn f U) (hf : EqOn (cexp ∘ f) g U),
    ∃ (f : X → ℂ), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
have refine_1 : ∀ (f : X → ℂ) (hfc : ContinuousOn f U) (hf : EqOn (cexp ∘ f) g U),
  ContinuousOn (Y := ℂ)
    (U.piecewise (β := fun (a : X) ↦ ℂ) (fun (x : X) ↦ cexp (f x / (↑n : ℂ))) fun (x : X) ↦
      g x ^ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ))
    U
Tactic: classical
  rcases exists_continuousOn_eqOn_exp_comp hUc hUo hgc hU₀ with ⟨f, hfc, hf⟩
  refine ⟨U.piecewise (exp <| f · / n) (g · ^ (1 / n : ℂ)), ?_, fun z ↦ ?_⟩
  · rw [continuousOn_iff_continuous_restrict, restrict_piecewise,
      ← continuousOn_iff_continuous_restrict]
    fun_prop
  · by_cases hz : z ∈ U
    · simp [hz, ← exp_nat_mul, mul_div_cancel₀ (b := ↑n) (f z) (mod_cast hn), ← hf hz,
        Function.comp_apply]
    · simp [hz, ← cpow_mul_nat, hn]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
n : ℕ
hn : n ≠ 0
rcases :
  ∀ (f : X → ℂ) (hfc : ContinuousOn f U) (hf : EqOn (cexp ∘ f) g U),
    ∃ (f : X → ℂ), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
refine_1 :
  ∀ (f : X → ℂ) (hfc : ContinuousOn f U) (hf : EqOn (cexp ∘ f) g U),
    ContinuousOn (Y := ℂ)
      (U.piecewise (β := fun (a : X) ↦ ℂ) (fun (x : X) ↦ cexp (f x / (↑n : ℂ))) fun (x : X) ↦
        g x ^ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ))
      U
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
have refine_2 : ∀ (f : X → ℂ) (hfc : ContinuousOn f U) (hf : EqOn (cexp ∘ f) g U) (z : X),
  HPow.hPow (α := ℂ)
      (U.piecewise (β := fun (a : X) ↦ ℂ) (fun (x : X) ↦ cexp (f x / (↑n : ℂ)))
          (fun (x : X) ↦ g x ^ HDiv.hDiv (α := ℂ) 1 (↑n : ℂ)) z :
        ℂ)
      n =
    g z
Tactic: classical
  rcases exists_continuousOn_eqOn_exp_comp hUc hUo hgc hU₀ with ⟨f, hfc, hf⟩
  refine ⟨U.piecewise (exp <| f · / n) (g · ^ (1 / n : ℂ)), ?_, fun z ↦ ?_⟩
  · rw [continuousOn_iff_continuous_restrict, restrict_piecewise,
      ← continuousOn_iff_continuous_restrict]
    fun_prop
  · by_cases hz : z ∈ U
    · simp [hz, ← exp_nat_mul, mul_div_cancel₀ (b := ↑n) (f z) (mod_cast hn), ← hf hz,
        Function.comp_apply]
    · simp [hz, ← cpow_mul_nat, hn]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
n : ℕ+
⊢ ∃ (f : X → 𝔻), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
have rcases : ∀ (f : X → ℂ) (hfc : ContinuousOn f U) (hf : ∀ (x : X), f x ^ (↑n : ℕ) = (UnitDisc.coe ∘ g) x),
  ∃ (f : X → 𝔻), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
Tactic: rcases exists_continuousOn_pow_eq hUc hUo
    (continuous_coe.comp_continuousOn hgc)
    (by simpa using hU₀) n.ne_zero with ⟨f, hfc, hf⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
n : ℕ+
f : X → ℂ
hfc : ContinuousOn f U
hf : ∀ (x : X), f x ^ (↑n : ℕ) = (UnitDisc.coe ∘ g) x
this : ∀ (x : X), ‖f x‖ < 1
⊢ ∃ (f : X → 𝔻), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
have lift : ∀ (f : (i : X) → 𝔻) (hfc : ContinuousOn (Y := ℂ) (fun (i : X) ↦ (↑(f i) : ℂ)) U)
  (hf : ∀ (x : X), HPow.hPow (α := ℂ) ((fun (i : X) ↦ (↑(f i) : ℂ)) x) (↑n : ℕ) = (UnitDisc.coe ∘ g) x),
  ∃ (f : X → 𝔻), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
Tactic: lift f to X → 𝔻 using this
Cleared hypotheses: f, hfc, hf, this
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
n : ℕ+
f : (i : X) → 𝔻
hfc : ContinuousOn (Y := ℂ) (fun (i : X) ↦ (↑(f i) : ℂ)) U
hf : ∀ (x : X), HPow.hPow (α := ℂ) ((fun (i : X) ↦ (↑(f i) : ℂ)) x) (↑n : ℕ) = (UnitDisc.coe ∘ g) x
⊢ ∃ (f : X → 𝔻), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
have refine : ∀ (x : X), f x ^ n = g x
Tactic: refine ⟨f, isEmbedding_coe.continuousOn_iff.mpr hfc, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
n : ℕ+
f : X → ℂ
hfc : ContinuousOn f U
hf : ∀ (x : X), f x ^ (↑n : ℕ) = (UnitDisc.coe ∘ g) x
⊢ ∃ (f : X → 𝔻), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x
have suffices : ∀ (x : X), ‖f x‖ < 1
Tactic: suffices ∀ x, ‖f x‖ < 1 by
    lift f to X → 𝔻 using this
    refine ⟨f, isEmbedding_coe.continuousOn_iff.mpr hfc, fun x ↦ ?_⟩
    simpa only [← coe_pow, Function.comp_apply, coe_inj] using hf x
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (goal)
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
n : ℕ+
f : X → ℂ
hfc : ContinuousOn f U
hf : ∀ (x : X), f x ^ (↑n : ℕ) = (UnitDisc.coe ∘ g) x
x : X
⊢ ‖f x‖ < 1
have rw : ‖(UnitDisc.coe ∘ g) x‖ < 1
Tactic: rw [← pow_lt_one_iff_of_nonneg (norm_nonneg _) n.ne_zero, ← norm_pow, hf]