awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
⊢ ‖f z / (2 * (↑M : ℂ) - f z)‖ ≤ ‖z‖ / R

Tactic:
have hwR := by simpa only [dist_zero_right, div_one, mul_comm (1 / R), mul_one_div]
    using schwarz_applied hM hf hf₁ hz hf₂
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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 : 2 * (↑M : ℂ) = f z
⊢ False

Tactic:
simpa [← h, hM] using hf₁ hz
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
⊢ 2 * (↑M : ℂ) - f z ≠ 0

Tactic:
have h_denom : 2 * M - f z ≠ 0 := sub_ne_zero_of_ne (fun h => by simpa [← h, hM] using hf₁ hz)
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
rw rw₁ : ‖2 * (↑M : ℂ) * (f z / (2 * (↑M : ℂ) - f z)) / (1 + f z / (2 * (↑M : ℂ) - f z))‖ = ‖2 * (↑M : ℂ) * w / (1 + w)‖
⊢ ‖f z‖ = ‖2 * (↑M : ℂ) * w / (1 + w)‖

Tactic:
rw [eq_mul_div_one_add_of_eq_div_sub hM.ne' h_denom rfl]

Premises used: _private.0.Complex.eq_mul_div_one_add_of_eq_div_sub, LT.lt.ne', rfl
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
simp : 2 * M * ‖w‖ / ‖1 + w‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)
⊢ ‖2 * (↑M : ℂ) * w / (1 + w)‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)

Tactic:
simp only [norm_div, norm_mul, norm_ofNat, norm_real, Real.norm_eq_abs, abs_of_pos hM]

Premises used: norm_mul, Complex.norm_real, Complex.norm_ofNat, norm_div, abs_of_pos, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
hd : 0 < 1 - ‖w‖
hdb : 1 - ‖w‖ ≤ ‖1 + w‖
⊢ 2 * M * ‖w‖ / ‖1 + w‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
linarith : 1 - ‖w‖ ≤ 0 → 1 - ‖w‖ - 0 + (1 * ‖f z / (2 * (↑M : ℂ) - f z)‖ - HMul.hMul (α := ℝ) 1 1) = 0
⊢ 0 < 1 - ‖w‖

Tactic:
linarith [hwR.trans_lt ((div_lt_one₀ hR).mpr hzR)]

Premises used: Iff.mpr, LE.le.trans_lt, div_lt_one₀
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
⊢ 1 - ‖w‖ ≤ ‖1 + w‖

Tactic:
simpa using norm_sub_le_norm_add 1 w

Premises used: norm_sub_le_norm_add, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
⊢ 2 * M * ‖w‖ / (1 - ‖w‖) = 2 * M * (‖w‖ / (1 - ‖w‖))

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
hbc : 0 < 1 - ‖z‖ / R
⊢ 2 * M * (‖w‖ / (1 - ‖w‖)) ≤ 2 * M * (‖z‖ / R / (1 - ‖z‖ / R))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
⊢ 0 < 1 - ‖z‖ / R

Tactic:
simpa [div_lt_one hR]

Premises used: div_lt_one
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
⊢ 2 * M * (‖z‖ / R / (1 - ‖z‖ / R)) = 2 * M * ‖z‖ / (R - ‖z‖)

Tactic:
field_simp
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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))
calc₄ : 2 * M * (‖z‖ / R / (1 - ‖z‖ / R)) = 2 * M * ‖z‖ / (R - ‖z‖)
⊢ ‖f z‖ ≤ 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

Premises used: Norm.norm, HSub.hSub, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
⊢ 0 < M + ‖f 0‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
⊢ DifferentiableOn ℂ (F := ℂ) (fun {z : ℂ} ↦ f z - f 0) (ball 0 R)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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 0 - f 0 = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
apply : Set.MapsTo (β := ℂ) (fun {z : ℂ} ↦ f z - f 0) (ball 0 R) {z : ℂ | z.re ≤ M + ‖f 0‖}
⊢ ‖f z - f 0‖ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖)

Tactic:
apply borelCaratheodory_zero (by positivity) (by fun_prop) ?_ hR hz (by simp)

Premises used: Complex.borelCaratheodory_zero
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
h : (f x).re ≤ M
⊢ (f x).re - (f 0).re ≤ M - (f 0).re

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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 ≤ M

Tactic:
hf₁ hx

Premises used: Set.Mem
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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 ≤ M

Tactic:
exact hf₁ hx
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
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
⊢ M - (f 0).re ≤ M + ‖f 0‖

Tactic:
linarith [neg_le_abs (f 0).re, abs_re_le_norm (f 0)]

Premises used: Complex.re, Complex.abs_re_le_norm, neg_le_abs, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
calc₁ : M - (f 0).re ≤ M + ‖f 0‖
⊢ (f x).re - (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)]

Premises used: Complex.re, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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‖)

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)]
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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‖)
linarith : R - ‖z‖ = 0 → R - ‖z‖ - 0 + (‖z‖ - R) = 0
⊢ R - ‖z‖ ≠ 0

Tactic:
linarith [mem_ball_zero_iff.mp hz]

Premises used: Iff.mp, mem_ball_zero_iff
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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

Tactic:
have h_denom_ne : R - ‖z‖ ≠ 0 := by linarith [mem_ball_zero_iff.mp hz]
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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‖ ≤ ‖f z - f 0‖ + ‖f 0‖

Tactic:
norm_le_norm_sub_add _ _

Premises used: norm_le_norm_sub_add
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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 - f 0‖ + ‖f 0‖ ≤ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖) + ‖f 0‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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
field_simp : 2 * (M + ‖f 0‖) * ‖z‖ + ‖f 0‖ * (R - ‖z‖) = 2 * M * ‖z‖ + ‖f 0‖ * (R + ‖z‖)
⊢ 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖) + ‖f 0‖ = 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖)

Tactic:
field_simp
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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‖ + ‖f 0‖ * (R - ‖z‖) = 2 * M * ‖z‖ + ‖f 0‖ * (R + ‖z‖)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.BorelCaratheodory
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‖
calc₁ : 2 * (M + ‖f 0‖) * ‖z‖ / (R - ‖z‖) + ‖f 0‖ = 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖)
⊢ ‖f z‖ ≤ 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

Premises used: Norm.norm, HSub.hSub, norm_le_norm_sub_add, HAdd.hAdd, 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
⊢ SimplyConnectedSpace.{u_1} (↑U : Type u_1)

Tactic:
have := hUc.simplyConnectedSpace
-- 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
this : SimplyConnectedSpace.{u_1} (↑U : Type u_1)
⊢ LocPathConnectedSpace.{u_1} (↑U : Type u_1)

Tactic:
have := hUo.locPathConnectedSpace
-- 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
this_1 : SimplyConnectedSpace.{u_1} (↑U : Type u_1)
this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)
rcases : ∀ (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

Tactic:
rcases hUc.nonempty with ⟨x₀, hx₀U⟩

Premises used: IsSimplyConnected.nonempty
-- 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
this_1 : SimplyConnectedSpace.{u_1} (↑U : Type u_1)
this : LocPathConnectedSpace.{u_1} (↑U : Type u_1)
x₀ : X
hx₀U : x₀ ∈ U
⊢ g x₀ ≠ 0

Tactic:
have hx₀ : g x₀ ≠ 0 := ne_of_mem_of_not_mem (mem_image_of_mem g hx₀U) 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
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
⊢ x₀ ∈ U

Tactic:
hx₀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
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
lift : ∀ (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

Tactic:
lift x₀ to U using hx₀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
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
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 := ⋯ : 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

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⟩, -⟩

Premises used: ContinuousMap.mk, ne_of_mem_of_not_mem, Complex.isCoveringMapOn_exp, Set.mem_image_of_mem, continuousOn_iff_continuous_restrict, Iff.mp, IsCoveringMapOn.existsUnique_continuousMap_lifts, Set.restrict, Complex.exp_log, Subtype.property
-- 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
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)) → ℂ)
⊢ ∀ (z : (↑U : Type u_1)),
    Eq (α := ℂ)
      ((fun (z : X) ↦
            (if hz : z ∈ U then (f : (a : (↑U : Type u_1)) → ℂ) (Subtype.mk (p := fun (x : X) ↦ x ∈ U) z hz) else 0 :
              ℂ))
          (↑z : X) :
        ℂ)
      ((f : (a : (↑U : Type u_1)) → ℂ) z : ℂ)

Tactic:
simp
-- 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
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)) → ℂ)
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
⊢ ∃ (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⟩
-- 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
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g_1 U

Tactic:
⟨g, ?hg_cont, ?hg_inv⟩

Premises used: 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_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
refine₁ : EqOn (cexp ∘ g) g_1 U
⊢ ∃ (f : X → ℂ), ContinuousOn f U ∧ EqOn (cexp ∘ f) g_1 U

Tactic:
refine ⟨g, ?hg_cont, ?hg_inv⟩
-- 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
rw : Continuous (U.restrict (π := fun (a : X) ↦ ℂ) g)
⊢ ContinuousOn g U

Tactic:
rw [continuousOn_iff_continuous_restrict]

Premises used: continuousOn_iff_continuous_restrict