Theorem: circleMap_Ioc (Ray/Hartogs/FubiniBall.lean)

State before:
c z : ℂ
r : ℝ
zs : z ∈ sphere c r
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t
Tactic:
by_cases rp : r < 0
State after:
case pos
c z : ℂ
r : ℝ
zs : z ∈ sphere c r
rp : r < 0
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t

case neg
c z : ℂ
r : ℝ
zs : z ∈ sphere c r
rp : ¬r < 0
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t

State before:
case neg
c z : ℂ
r : ℝ
zs : z ∈ sphere c r
rp : ¬r < 0
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t
Tactic:
simp only [not_lt] at rp
State after:
case neg
c z : ℂ
r : ℝ
zs : z ∈ sphere c r
rp : 0 ≤ r
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t

State before:
case neg
c z : ℂ
r : ℝ
zs : z ∈ sphere c r
rp : 0 ≤ r
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t
Tactic:
rw [←abs_of_nonneg rp, ← range_circleMap, mem_range] at zs
State after:
case neg
c z : ℂ
r : ℝ
zs : ∃ y, circleMap c r y = z
rp : 0 ≤ r
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t

State before:
case neg
c z : ℂ
r : ℝ
zs : ∃ y, circleMap c r y = z
rp : 0 ≤ r
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t
Tactic:
rcases zs with ⟨t, ht⟩
State after:
case neg.intro
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t

State before:
case neg.intro
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t
Tactic:
generalize ha : 2 * π = a
State after:
case neg.intro
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
⊢ ∃ t ∈ Ioc 0 a, z = circleMap c r t

State before:
case neg.intro
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
⊢ ∃ t ∈ Ioc 0 a, z = circleMap c r t
Tactic:
have ap : a > 0 := by rw [←ha]; bound
State after:
case neg.intro
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
⊢ ∃ t ∈ Ioc 0 a, z = circleMap c r t

State before:
case neg.intro
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
⊢ ∃ t ∈ Ioc 0 a, z = circleMap c r t
Tactic:
generalize hs : t + a - a * ⌈t / a⌉ = s
State after:
case neg.intro
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ ∃ t ∈ Ioc 0 a, z = circleMap c r t

State before:
case neg.intro
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ ∃ t ∈ Ioc 0 a, z = circleMap c r t
Tactic:
use s
State after:
case h
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ s ∈ Ioc 0 a ∧ z = circleMap c r s

State before:
case h
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ s ∈ Ioc 0 a ∧ z = circleMap c r s
Tactic:
constructor
State after:
case h.left
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ s ∈ Ioc 0 a

case h.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ z = circleMap c r s

State before:
case pos
c z : ℂ
r : ℝ
zs : z ∈ sphere c r
rp : r < 0
⊢ ∃ t ∈ Ioc 0 (2 * π), z = circleMap c r t
Tactic:
simp only [Metric.sphere_eq_empty.mpr rp, mem_empty_iff_false] at zs
State after:
no goals

State before:
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
⊢ a > 0
Tactic:
rw [←ha]
State after:
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
⊢ 2 * π > 0

State before:
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
⊢ 2 * π > 0
Tactic:
bound
State after:
no goals

State before:
case h.left
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ s ∈ Ioc 0 a
Tactic:
simp only [mem_Ioc, sub_pos, tsub_le_iff_right, ← hs]
State after:
case h.left
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a * ↑⌈t / a⌉ < t + a ∧ t + a ≤ a + a * ↑⌈t / a⌉

State before:
case h.left
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a * ↑⌈t / a⌉ < t + a ∧ t + a ≤ a + a * ↑⌈t / a⌉
Tactic:
constructor
State after:
case h.left.left
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a * ↑⌈t / a⌉ < t + a

case h.left.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ t + a ≤ a + a * ↑⌈t / a⌉

State before:
case h.left.left
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a * ↑⌈t / a⌉ < t + a
Tactic:
calc a * ⌈t / a⌉
  _ < a * (t / a + 1) := by bound
  _ = a / a * t + a := by ring
  _ = t + a := by field_simp [ap.ne']
State after:
no goals

State before:
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a * ↑⌈t / a⌉ < a * (t / a + 1)
Tactic:
bound
State after:
no goals

State before:
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a * (t / a + 1) = a / a * t + a
Tactic:
ring
State after:
no goals

State before:
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a / a * t + a = t + a
Tactic:
field_simp [ap.ne']
State after:
no goals

State before:
case h.left.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ t + a ≤ a + a * ↑⌈t / a⌉
Tactic:
calc a + a * ⌈t / a⌉
  _ ≥ a + a * (t / a) := by bound
  _ = a / a * t + a := by ring
  _ = t + a := by field_simp [ap.ne']
State after:
no goals

State before:
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a + a * ↑⌈t / a⌉ ≥ a + a * (t / a)
Tactic:
bound
State after:
no goals

State before:
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ a + a * (t / a) = a / a * t + a
Tactic:
ring
State after:
no goals

State before:
case h.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ z = circleMap c r s
Tactic:
simp only [←ht, circleMap, Complex.ofReal_sub, Complex.ofReal_add, Complex.ofReal_mul,
  Complex.ofReal_intCast, add_right_inj, mul_eq_mul_left_iff, Complex.ofReal_eq_zero, ← hs]
State after:
case h.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ (↑t * I).exp = ((↑t + ↑a - ↑a * ↑⌈t / a⌉) * I).exp ∨ r = 0

State before:
case h.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ (↑t * I).exp = ((↑t + ↑a - ↑a * ↑⌈t / a⌉) * I).exp ∨ r = 0
Tactic:
rw [mul_sub_right_distrib, right_distrib, Complex.exp_sub, Complex.exp_add]
State after:
case h.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ (↑t * I).exp = (↑t * I).exp * (↑a * I).exp / (↑a * ↑⌈t / a⌉ * I).exp ∨ r = 0

State before:
case h.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ (↑t * I).exp = (↑t * I).exp * (↑a * I).exp / (↑a * ↑⌈t / a⌉ * I).exp ∨ r = 0
Tactic:
rw [mul_comm _ (⌈_⌉:ℂ), mul_assoc, Complex.exp_int_mul, ← ha]
State after:
case h.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ (↑t * I).exp = (↑t * I).exp * (↑(2 * π) * I).exp / (↑(2 * π) * I).exp ^ ⌈t / (2 * π)⌉ ∨ r = 0

State before:
case h.right
c z : ℂ
r : ℝ
rp : 0 ≤ r
t : ℝ
ht : circleMap c r t = z
a : ℝ
ha : 2 * π = a
ap : a > 0
s : ℝ
hs : t + a - a * ↑⌈t / a⌉ = s
⊢ (↑t * I).exp = (↑t * I).exp * (↑(2 * π) * I).exp / (↑(2 * π) * I).exp ^ ⌈t / (2 * π)⌉ ∨ r = 0
Tactic:
simp only [Complex.ofReal_mul, Complex.ofReal_ofNat, Complex.exp_two_pi_mul_I, mul_one,
  one_zpow, div_one, true_or]
State after:
no goals