awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : X → ℂ
hgc : ContinuousOn g_1 U
hU₀ : 0 ∉ g_1 '' U
this_1 : SimplyConnectedSpace.{u_1} (↑U : Type u_1)
this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)
x₀ : { x : X // x ∈ U }
hx₀ : g_1 (↑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_1, 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
⊢ Continuous (X := (↑U : Type u_1)) (Y := ℂ) (⇑f : (a : (↑U : Type u_1)) → ℂ)

Tactic:
map_continuous f

Premises used: ContinuousMapClass.map_continuous
-- 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_1 : X → ℂ
hgc : ContinuousOn g_1 U
hU₀ : 0 ∉ g_1 '' U
this_1 : SimplyConnectedSpace.{u_1} (↑U : Type u_1)
this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)
x₀ : { x : X // x ∈ U }
hx₀ : g_1 (↑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_1, 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
h : U.restrict (π := fun (a : X) ↦ ℂ) g = (⇑f : (a : (↑U : Type u_1)) → ℂ)
⊢ Continuous (U.restrict (π := fun (a : X) ↦ ℂ) g)

Tactic:
convert! map_continuous f

Premises used: ContinuousMapClass.map_continuous
-- 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_1 : X → ℂ
hgc : ContinuousOn g_1 U
hU₀ : 0 ∉ g_1 '' U
this_1 : SimplyConnectedSpace.{u_1} (↑U : Type u_1)
this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)
x₀ : { x : X // x ∈ U }
hx₀ : g_1 (↑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_1, 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
h : ∀ (z : (↑U : Type u_1)), U.restrict (π := fun (a : X) ↦ ℂ) g z = (f : (a : (↑U : Type u_1)) → ℂ) z
⊢ U.restrict (π := fun (a : X) ↦ ℂ) g = (⇑f : (a : (↑U : Type u_1)) → ℂ)

Tactic:
ext z
-- 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_1 : X → ℂ
hgc : ContinuousOn g_1 U
hU₀ : 0 ∉ g_1 '' U
this_1 : SimplyConnectedSpace.{u_1} (↑U : Type u_1)
this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)
x₀ : { x : X // x ∈ U }
hx₀ : g_1 (↑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_1, 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
z : (↑U : Type u_1)
⊢ U.restrict (π := fun (a : X) ↦ ℂ) g z = (f : (a : (↑U : Type u_1)) → ℂ) z

Tactic:
hg z

Premises used: Set.restrict
-- 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_1 : X → ℂ
hgc : ContinuousOn g_1 U
hU₀ : 0 ∉ g_1 '' U
this_1 : SimplyConnectedSpace.{u_1} (↑U : Type u_1)
this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)
x₀ : { x : X // x ∈ U }
hx₀ : g_1 (↑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_1, 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
z : (↑U : Type u_1)
⊢ U.restrict (π := fun (a : X) ↦ ℂ) g z = (f : (a : (↑U : Type u_1)) → ℂ) z

Tactic:
exact hg z
-- 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_1 : X → ℂ
hgc : ContinuousOn g_1 U
hU₀ : 0 ∉ g_1 '' U
this_1 : SimplyConnectedSpace.{u_1} (↑U : Type u_1)
this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)
x₀ : { x : X // x ∈ U }
hx₀ : g_1 (↑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_1, 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

Tactic:
case hg_cont =>
    rw [continuousOn_iff_continuous_restrict]
    convert! map_continuous f
    ext z
    exact hg z

Premises used: continuousOn_iff_continuous_restrict, ContinuousMapClass.map_continuous
-- 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_1 : X → ℂ
hgc : ContinuousOn g_1 U
hU₀ : 0 ∉ g_1 '' U
this_1 : SimplyConnectedSpace.{u_1} (↑U : Type u_1)
this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)
x₀ : { x : X // x ∈ U }
hx₀ : g_1 (↑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_1, 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
x : X
hx : x ∈ U
⊢ x ∈ U

Tactic:
hx
-- 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_1 : X → ℂ
hgc : ContinuousOn g_1 U
hU₀ : 0 ∉ g_1 '' U
this_1 : SimplyConnectedSpace.{u_1} (↑U : Type u_1)
this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)
x₀ : { x : X // x ∈ U }
hx₀ : g_1 (↑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_1, 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
x : X
hx : x ∈ U
lift : ∀ (x : { x : X // x ∈ U }), (cexp ∘ g) (↑x : X) = g_1 (↑x : X)
⊢ (cexp ∘ g) x = g_1 x

Tactic:
lift x to U using hx
-- 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_1 : X → ℂ
hgc : ContinuousOn g_1 U
hU₀ : 0 ∉ g_1 '' U
this_1 : SimplyConnectedSpace.{u_1} (↑U : Type u_1)
this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)
x₀ : { x : X // x ∈ U }
hx₀ : g_1 (↑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_1, 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
x : { x : X // x ∈ U }
⊢ (cexp ∘ g) (↑x : X) = g_1 (↑x : X)

Tactic:
simpa [hg] using congr($hf x)
-- 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_1 : X → ℂ
hgc : ContinuousOn g_1 U
hU₀ : 0 ∉ g_1 '' U
this_1 : SimplyConnectedSpace.{u_1} (↑U : Type u_1)
this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)
x₀ : { x : X // x ∈ U }
hx₀ : g_1 (↑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_1, 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
case case₁ : ∀ ⦃x : X⦄ (hx : x ∈ U), (cexp ∘ g) x = g_1 x
case₂ : ∀ (x : { x : X // x ∈ U }), (cexp ∘ g) (↑x : X) = g_1 (↑x : X)
⊢ EqOn (cexp ∘ g) g_1 U

Tactic:
case hg_inv =>
    intro x hx
    lift x to U using hx
    simpa [hg] using congr($hf x)
-- 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
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

Tactic:
rcases exists_continuousOn_eqOn_exp_comp hUc hUo hgc hU₀ with ⟨f, hfc, hf⟩

Premises used: Complex.exists_continuousOn_eqOn_exp_comp
-- 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
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

Tactic:
⟨U.piecewise (exp <| f · / n) (g · ^ (1 / n : ℂ)), ?_, fun z ↦ ?_⟩

Premises used: HDiv.hDiv, Nat.cast, HPow.hPow, And.intro, Exists.intro, Complex.exp, Set.piecewise, OfNat.ofNat
-- 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
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
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
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x

Tactic:
refine ⟨U.piecewise (exp <| f · / n) (g · ^ (1 / n : ℂ)), ?_, fun z ↦ ?_⟩
-- 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
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
refine_1 : ContinuousOn (Y := ℂ) (fun (x : X) ↦ cexp (f x / (↑n : ℂ))) 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:
rw [continuousOn_iff_continuous_restrict, restrict_piecewise,
      ← continuousOn_iff_continuous_restrict]

Premises used: Set.restrict_piecewise, continuousOn_iff_continuous_restrict
-- 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
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
funProp : ∀ x ∈ U, Ne (α := ℂ) (↑n : ℂ) 0
⊢ ContinuousOn (Y := ℂ) (fun (x : X) ↦ cexp (f x / (↑n : ℂ))) U

Tactic:
fun_prop
-- 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
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
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
⊢ 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
-- 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
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
z : X
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:
simp [hz, ← exp_nat_mul, mul_div_cancel₀ (b := ↑n) (f z) (mod_cast hn), ← hf hz,
        Function.comp_apply]

Premises used: mul_div_cancel₀, Function.comp_apply, Complex.exp_nat_mul
-- 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
n : ℕ
hn : n ≠ 0
f : X → ℂ
hfc : ContinuousOn f U
hf : EqOn (cexp ∘ f) g U
z : X
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:
simp [hz, ← cpow_mul_nat, hn]

Premises used: Complex.cpow_mul_nat
-- 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
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
refine_2 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
⊢ ∃ (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]

Premises used: Set.restrict_piecewise, Complex.cpow_mul_nat, Complex.exists_continuousOn_eqOn_exp_comp, continuousOn_iff_continuous_restrict, Function.comp_apply, Complex.exp_nat_mul
-- 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
n : ℕ+
⊢ 0 ∉ UnitDisc.coe ∘ g '' U

Tactic:
simpa using hU₀
-- 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
n : ℕ+
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
⊢ ∃ (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⟩

Premises used: Continuous.comp_continuousOn, PNat.ne_zero, Complex.UnitDisc.continuous_coe, Complex.exists_continuousOn_pow_eq
-- 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
n : ℕ+
f : X → ℂ
hfc : ContinuousOn f U
hf : ∀ (x : X), f x ^ (↑n : ℕ) = (UnitDisc.coe ∘ g) x
this : ∀ (x : X), ‖f x‖ < 1
⊢ ∀ (i : X), ‖f i‖ < 1

Tactic:
this
-- 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
n : ℕ+
f : X → ℂ
hfc : ContinuousOn f U
hf : ∀ (x : X), f x ^ (↑n : ℕ) = (UnitDisc.coe ∘ g) x
this : ∀ (x : X), ‖f x‖ < 1
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
⊢ ∃ (f : X → 𝔻), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x

Tactic:
lift f to X → 𝔻 using this
-- 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
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

Tactic:
⟨f, isEmbedding_coe.continuousOn_iff.mpr hfc, fun x ↦ ?_⟩

Premises used: Iff.mpr, Complex.UnitDisc.isEmbedding_coe, Topology.IsEmbedding.continuousOn_iff, And.intro, Exists.intro
-- 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
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
refine : ∀ (x : X), f x ^ n = g x
⊢ ∃ (f : X → 𝔻), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x

Tactic:
refine ⟨f, isEmbedding_coe.continuousOn_iff.mpr hfc, fun x ↦ ?_⟩
-- 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
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
x : X
⊢ f x ^ n = g x

Tactic:
simpa only [← coe_pow, Function.comp_apply, coe_inj] using hf x

Premises used: Complex.UnitDisc.coe_pow, Function.comp_apply, Complex.UnitDisc.coe_inj
-- 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
n : ℕ+
f : X → ℂ
hfc : ContinuousOn f U
hf : ∀ (x : X), f x ^ (↑n : ℕ) = (UnitDisc.coe ∘ g) x
suffices : ∀ (x : X), ‖f x‖ < 1
⊢ ∃ (f : X → 𝔻), ContinuousOn f U ∧ ∀ (x : X), f x ^ n = g x

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
-- 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
n : ℕ+
f : X → ℂ
hfc : ContinuousOn f U
hf : ∀ (x : X), f x ^ (↑n : ℕ) = (UnitDisc.coe ∘ g) x
x : X
rw : ‖(UnitDisc.coe ∘ g) x‖ < 1
⊢ ‖f x‖ < 1

Tactic:
rw [← pow_lt_one_iff_of_nonneg (norm_nonneg _) n.ne_zero, ← norm_pow, hf]

Premises used: norm_pow, PNat.ne_zero, pow_lt_one_iff_of_nonneg, norm_nonneg
-- 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
n : ℕ+
f : X → ℂ
hfc : ContinuousOn f U
hf : ∀ (x : X), f x ^ (↑n : ℕ) = (UnitDisc.coe ∘ g) x
x : X
⊢ ‖(UnitDisc.coe ∘ g) x‖ < 1

Tactic:
(g x).norm_lt_one

Premises used: Complex.UnitDisc.norm_lt_one, Complex.UnitDisc.coe
-- 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
n : ℕ+
f : X → ℂ
hfc : ContinuousOn f U
hf : ∀ (x : X), f x ^ (↑n : ℕ) = (UnitDisc.coe ∘ g) x
x : X
⊢ ‖(UnitDisc.coe ∘ g) x‖ < 1

Tactic:
exact (g x).norm_lt_one

Premises used: Complex.UnitDisc.norm_lt_one
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
⊢ canonicalFactor R w = fun (z : ℂ) ↦
    (HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) / ((↑R : ℂ) * (z - w))

Tactic:
rfl

Premises used: Complex.canonicalFactor, rfl
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w z : ℂ
⊢ canonicalFactor R w z =
    (HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) / ((↑R : ℂ) * (z - w))

Tactic:
rfl

Premises used: Complex.canonicalFactor, rfl
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w : ℂ
⊢ canonicalFactor R w w = 0

Tactic:
simp [canonicalFactor_apply]

Premises used: Complex.canonicalFactor_apply
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w x : ℂ
hx : Membership.mem (γ := Set ℂ) Set.univ x
⊢ MeromorphicAt (E := ℂ)
    (fun (z : ℂ) ↦
      (HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) /
        ((↑R : ℂ) * (z - w)))
    x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w x : ℂ
hx : Membership.mem (γ := Set ℂ) {w}ᶜ x
inl :
  AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      (HPow.hPow (β := ℕ) (↑0 : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) /
        ((↑0 : ℂ) * (z - w)))
    x
inr :
  ∀ (h : R ≠ 0),
    AnalyticAt ℂ (F := ℂ)
      (fun (z : ℂ) ↦
        (HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) /
          ((↑R : ℂ) * (z - w)))
      x
⊢ AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      (HPow.hPow (β := ℕ) (↑R : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) /
        ((↑R : ℂ) * (z - w)))
    x

Tactic:
obtain (rfl | h) := eq_or_ne R 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
w x : ℂ
hx : Membership.mem (γ := Set ℂ) {w}ᶜ x
⊢ AnalyticAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦
      (HPow.hPow (β := ℕ) (↑0 : ℂ) 2 - HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z) /
        ((↑0 : ℂ) * (z - w)))
    x

Tactic:
simpa using analyticAt_const

Premises used: analyticAt_const
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w x : ℂ
hx : Membership.mem (γ := Set ℂ) {w}ᶜ x
h : R ≠ 0
⊢ x - w ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.CanonicalDecomposition
Goal:
R : ℝ
w x : ℂ
hx : Membership.mem (γ := Set ℂ) {w}ᶜ x
h : R ≠ 0
⊢ x - w ≠ 0

Tactic:
have : x - w ≠ 0 := by grind