awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
w : ℂ := f z / (2 * (↑M : ℂ) - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * (↑M : ℂ) - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * (↑M : ℂ) - f z ≠ 0
calc : ‖f z‖ = ‖2 * (↑M : ℂ) * w / (1 + w)‖
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖)
have calc₁ : ‖2 * (↑M : ℂ) * w / (1 + w)‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)
Tactic: calc ‖f z‖
    _ = ‖2 * M * w / (1 + w)‖ := by rw [eq_mul_div_one_add_of_eq_div_sub hM.ne' h_denom rfl]
    _ ≤ 2 * M * ‖w‖ / (1 - ‖w‖) := by
      simp only [norm_div, norm_mul, norm_ofNat, norm_real, Real.norm_eq_abs, abs_of_pos hM]
      gcongr
      · linarith [hwR.trans_lt ((div_lt_one₀ hR).mpr hzR)]
      · simpa using norm_sub_le_norm_add 1 w
    _ = 2 * M * (‖w‖ / (1 - ‖w‖)) := by ring
    _ ≤ 2 * M * (‖z‖ / R / (1 - ‖z‖ / R)) := by gcongr; simpa [div_lt_one hR]
    _ = 2 * M * ‖z‖ / (R - ‖z‖) := by field_simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
w : ℂ := f z / (2 * (↑M : ℂ) - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * (↑M : ℂ) - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * (↑M : ℂ) - f z ≠ 0
calc : ‖f z‖ = ‖2 * (↑M : ℂ) * w / (1 + w)‖
calc₁ : ‖2 * (↑M : ℂ) * w / (1 + w)‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖)
have calc₂ : 2 * M * ‖w‖ / (1 - ‖w‖) = 2 * M * (‖w‖ / (1 - ‖w‖))
Tactic: calc ‖f z‖
    _ = ‖2 * M * w / (1 + w)‖ := by rw [eq_mul_div_one_add_of_eq_div_sub hM.ne' h_denom rfl]
    _ ≤ 2 * M * ‖w‖ / (1 - ‖w‖) := by
      simp only [norm_div, norm_mul, norm_ofNat, norm_real, Real.norm_eq_abs, abs_of_pos hM]
      gcongr
      · linarith [hwR.trans_lt ((div_lt_one₀ hR).mpr hzR)]
      · simpa using norm_sub_le_norm_add 1 w
    _ = 2 * M * (‖w‖ / (1 - ‖w‖)) := by ring
    _ ≤ 2 * M * (‖z‖ / R / (1 - ‖z‖ / R)) := by gcongr; simpa [div_lt_one hR]
    _ = 2 * M * ‖z‖ / (R - ‖z‖) := by field_simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
w : ℂ := f z / (2 * (↑M : ℂ) - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * (↑M : ℂ) - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * (↑M : ℂ) - f z ≠ 0
calc : ‖f z‖ = ‖2 * (↑M : ℂ) * w / (1 + w)‖
calc₁ : ‖2 * (↑M : ℂ) * w / (1 + w)‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)
calc₂ : 2 * M * ‖w‖ / (1 - ‖w‖) = 2 * M * (‖w‖ / (1 - ‖w‖))
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖)
have calc₃ : 2 * M * (‖w‖ / (1 - ‖w‖)) ≤ 2 * M * (‖z‖ / R / (1 - ‖z‖ / R))
Tactic: calc ‖f z‖
    _ = ‖2 * M * w / (1 + w)‖ := by rw [eq_mul_div_one_add_of_eq_div_sub hM.ne' h_denom rfl]
    _ ≤ 2 * M * ‖w‖ / (1 - ‖w‖) := by
      simp only [norm_div, norm_mul, norm_ofNat, norm_real, Real.norm_eq_abs, abs_of_pos hM]
      gcongr
      · linarith [hwR.trans_lt ((div_lt_one₀ hR).mpr hzR)]
      · simpa using norm_sub_le_norm_add 1 w
    _ = 2 * M * (‖w‖ / (1 - ‖w‖)) := by ring
    _ ≤ 2 * M * (‖z‖ / R / (1 - ‖z‖ / R)) := by gcongr; simpa [div_lt_one hR]
    _ = 2 * M * ‖z‖ / (R - ‖z‖) := by field_simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hf₂ : f 0 = 0
w : ℂ := f z / (2 * (↑M : ℂ) - f z)
hzR : ‖z‖ < R
hwR : ‖f z / (2 * (↑M : ℂ) - f z)‖ ≤ ‖z‖ / R
h_denom : 2 * (↑M : ℂ) - f z ≠ 0
calc : ‖f z‖ = ‖2 * (↑M : ℂ) * w / (1 + w)‖
calc₁ : ‖2 * (↑M : ℂ) * w / (1 + w)‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)
calc₂ : 2 * M * ‖w‖ / (1 - ‖w‖) = 2 * M * (‖w‖ / (1 - ‖w‖))
calc₃ : 2 * M * (‖w‖ / (1 - ‖w‖)) ≤ 2 * M * (‖z‖ / R / (1 - ‖z‖ / R))
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖)
have calc₄ : 2 * M * (‖z‖ / R / (1 - ‖z‖ / R)) = 2 * M * ‖z‖ / (R - ‖z‖)
Tactic: calc ‖f z‖
    _ = ‖2 * M * w / (1 + w)‖ := by rw [eq_mul_div_one_add_of_eq_div_sub hM.ne' h_denom rfl]
    _ ≤ 2 * M * ‖w‖ / (1 - ‖w‖) := by
      simp only [norm_div, norm_mul, norm_ofNat, norm_real, Real.norm_eq_abs, abs_of_pos hM]
      gcongr
      · linarith [hwR.trans_lt ((div_lt_one₀ hR).mpr hzR)]
      · simpa using norm_sub_le_norm_add 1 w
    _ = 2 * M * (‖w‖ / (1 - ‖w‖)) := by ring
    _ ≤ 2 * M * (‖z‖ / R / (1 - ‖z‖ / R)) := by gcongr; simpa [div_lt_one hR]
    _ = 2 * M * ‖z‖ / (R - ‖z‖) := by field_simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
⊢ ‖f z - f 0‖ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖)
have apply : Set.MapsTo (β := ℂ) (fun {z : ℂ} ↦ f z - f 0) (ball 0 R) {z : ℂ | z.re ≤ M + ‖f 0‖}
Tactic: apply borelCaratheodory_zero (by positivity) (by fun_prop) ?_ hR hz (by simp)
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
x : ℂ
hx : Membership.mem (γ := Set ℂ) (ball 0 R) x
⊢ (f x).re - (f 0).re ≤ M - (f 0).re
have h : (f x).re ≤ M
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
x : ℂ
hx : Membership.mem (γ := Set ℂ) (ball 0 R) x
⊢ M - (f 0).re ≤ M + ‖f 0‖
have linarith : M + ‖f 0‖ < M - (f 0).re → M + ‖f 0‖ - (M - (f 0).re) + (-(f 0).re - |(f 0).re|) + (|(f 0).re| - ‖f 0‖) = 0
Tactic: linarith [neg_le_abs (f 0).re, abs_re_le_norm (f 0)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
x : ℂ
hx : Membership.mem (γ := Set ℂ) (ball 0 R) x
⊢ (f x).re - (f 0).re ≤ M + ‖f 0‖
have calc : (f x).re - (f 0).re ≤ M - (f 0).re
Tactic: calc (f x).re - (f 0).re ≤ M - (f 0).re := by gcongr; exact hf₁ hx
      _ ≤ M + ‖f 0‖ := by linarith [neg_le_abs (f 0).re, abs_re_le_norm (f 0)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
x : ℂ
hx : Membership.mem (γ := Set ℂ) (ball 0 R) x
calc : (f x).re - (f 0).re ≤ M - (f 0).re
⊢ (f x).re - (f 0).re ≤ M + ‖f 0‖
have calc₁ : M - (f 0).re ≤ M + ‖f 0‖
Tactic: calc (f x).re - (f 0).re ≤ M - (f 0).re := by gcongr; exact hf₁ hx
      _ ≤ M + ‖f 0‖ := by linarith [neg_le_abs (f 0).re, abs_re_le_norm (f 0)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (hypothesis)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖)
have hfz : ‖f z - f 0‖ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖)
Tactic: have hfz : ‖f z - f 0‖ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖) := by
    apply borelCaratheodory_zero (by positivity) (by fun_prop) ?_ hR hz (by simp)
    intro x hx
    simp only [Set.mem_setOf_eq, sub_re]
    calc (f x).re - (f 0).re ≤ M - (f 0).re := by gcongr; exact hf₁ hx
      _ ≤ M + ‖f 0‖ := by linarith [neg_le_abs (f 0).re, abs_re_le_norm (f 0)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hfz : ‖f z - f 0‖ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖)
⊢ R - ‖z‖ ≠ 0
have linarith : R - ‖z‖ = 0 → R - ‖z‖ - 0 + (‖z‖ - R) = 0
Tactic: linarith [mem_ball_zero_iff.mp hz]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (hypothesis)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hfz : ‖f z - f 0‖ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖)
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖)
have h_denom_ne : R - ‖z‖ ≠ 0
Tactic: have h_denom_ne : R - ‖z‖ ≠ 0 := by linarith [mem_ball_zero_iff.mp hz]
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hfz : ‖f z - f 0‖ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖)
h_denom_ne : R - ‖z‖ ≠ 0
⊢ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖) + ‖f 0‖ = 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖)
have field_simp : 2 * (M + ‖f 0‖) * ‖z‖ + ‖f 0‖ * (R - ‖z‖) = 2 * M * ‖z‖ + ‖f 0‖ * (R + ‖z‖)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hfz : ‖f z - f 0‖ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖)
h_denom_ne : R - ‖z‖ ≠ 0
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖)
have calc : ‖f z - f 0‖ + ‖f 0‖ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖) + ‖f 0‖
Tactic: calc ‖f z‖ ≤ ‖f z - f 0‖ + ‖f 0‖ := norm_le_norm_sub_add _ _
    _ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖) + ‖f 0‖ := by gcongr
    _ = 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖) := by field_simp; ring
-- Lean 4 proof step from Mathlib.Analysis.Complex.BorelCaratheodory (goal)
Goal:
f : ℂ → ℂ
M R : ℝ
z : ℂ
hM : 0 < M
hf : DifferentiableOn ℂ f (ball 0 R)
hf₁ : Set.MapsTo f (ball 0 R) {z : ℂ | z.re ≤ M}
hR : 0 < R
hz : Membership.mem (γ := Set ℂ) (ball 0 R) z
hfz : ‖f z - f 0‖ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖)
h_denom_ne : R - ‖z‖ ≠ 0
calc : ‖f z - f 0‖ + ‖f 0‖ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖) + ‖f 0‖
⊢ ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖)
have calc₁ : 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖) + ‖f 0‖ = 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖)
Tactic: calc ‖f z‖ ≤ ‖f z - f 0‖ + ‖f 0‖ := norm_le_norm_sub_add _ _
    _ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖) + ‖f 0‖ := by gcongr
    _ = 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖) := by field_simp; ring
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (hypothesis)
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
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g U
have this : SimplyConnectedSpace.{u_1} (↑U : Type u_1)
Tactic: have := hUc.simplyConnectedSpace
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (hypothesis)
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
this : SimplyConnectedSpace.{u_1} (↑U : Type u_1)
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g U
have this₁ : LocPathConnectedSpace.{u_1} (↑U : Type u_1)
Tactic: have := hUo.locPathConnectedSpace
-- 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
this_1 : 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 rcases : ∀ (x₀ : X) (hx₀U : x₀ ∈ U), ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g U
Tactic: rcases hUc.nonempty with ⟨x₀, hx₀U⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.BranchLogRoot (hypothesis)
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
this_1 : 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 hx₀ : g x₀ ≠ 0
Tactic: have hx₀ : g x₀ ≠ 0 := ne_of_mem_of_not_mem (mem_image_of_mem g hx₀U) hU₀
-- 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
this_1 : 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 lift : ∀ (x₀ : { x : X // x ∈ U }) (hx₀ : g (↑x₀ : X) ≠ 0), ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g U
Tactic: lift x₀ to U using hx₀U
Cleared hypotheses: x₀, hx₀U, hx₀
-- 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
this_1 : 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 rcases : ∀ (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: 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⟩, -⟩
-- 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
this_1 : 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 obtain : ∀ (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: 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⟩
-- 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_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
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g_1 U
have refine : ContinuousOn g U
Tactic: refine ⟨g, ?hg_cont, ?hg_inv⟩
-- 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_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
refine : ContinuousOn g U
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g_1 U
have refine₁ : EqOn (cexp ∘ g) g_1 U
Tactic: refine ⟨g, ?hg_cont, ?hg_inv⟩
-- 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_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
have rw : Continuous (U.restrict (π := fun (a : X) ↦ ℂ) g)
Tactic: rw [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_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 (U.restrict (π := fun (a : X) ↦ ℂ) g)
have h : U.restrict (π := fun (a : X) ↦ ℂ) g = (⇑f : (a : (↑U : Type u_1)) → ℂ)
Tactic: convert! map_continuous f
-- 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_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
⊢ U.restrict (π := fun (a : X) ↦ ℂ) g = (⇑f : (a : (↑U : Type u_1)) → ℂ)
have h : ∀ (z : (↑U : Type u_1)), U.restrict (π := fun (a : X) ↦ ℂ) g z = (f : (a : (↑U : Type u_1)) → ℂ) z
Tactic: ext 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_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
⊢ (cexp ∘ g) x = g_1 x
have lift : ∀ (x : { x : X // x ∈ U }), (cexp ∘ g) (↑x : X) = g_1 (↑x : X)
Tactic: lift x to U using hx
Cleared hypotheses: x, hx
-- 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_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
⊢ EqOn (cexp ∘ g) g_1 U
have case : ∀ ⦃x : X⦄, x ∈ U → (cexp ∘ g) x = g_1 x
Tactic: 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_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
⊢ EqOn (cexp ∘ g) g_1 U
have case₂ : ∀ (x : { x : X // x ∈ U }), (cexp ∘ g) (↑x : X) = g_1 (↑x : X)
Tactic: 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
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g U
have have : ∀ (this : SimplyConnectedSpace.{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)