internlm/Lean-Github huggingface dataset:
Theorem: square_eq
Proof state before:
case h
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x✝ : ℝ × ℝ
⊢ realCircleMap c x✝ = Complex.measurableEquivRealProd (circleMap c x✝.1 x✝.2)
Tactic:
simp only [realCircleMap_eq_circleMap, Complex.measurableEquivRealProd,
  Complex.equivRealProd_apply, Homeomorph.toMeasurableEquiv_coe,
  ContinuousLinearEquiv.coe_toHomeomorph, Complex.equivRealProdCLM_apply]
Proof state after:
no goals
Theorem: square_eq
Proof state before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
⊢ (fun x => circleMap c x.1 x.2) '' square r0 r1 = annulus_oc c r0 r1
Tactic:
ext z
Proof state after:
case h
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
⊢ z ∈ (fun x => circleMap c x.1 x.2) '' square r0 r1 ↔ z ∈ annulus_oc c r0 r1
Theorem: square_eq
Proof state before:
case h
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
⊢ z ∈ (fun x => circleMap c x.1 x.2) '' square r0 r1 ↔ z ∈ annulus_oc c r0 r1
Tactic:
rw [mem_image]
Proof state after:
case h
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
⊢ (∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z) ↔ z ∈ annulus_oc c r0 r1
Theorem: square_eq
Proof state before:
case h
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
⊢ (∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z) ↔ z ∈ annulus_oc c r0 r1
Tactic:
constructor
Proof state after:
case h.mp
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
⊢ (∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z) → z ∈ annulus_oc c r0 r1

case h.mpr
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
⊢ z ∈ annulus_oc c r0 r1 → ∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z
Theorem: square_eq
Proof state before:
case h.mp
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
⊢ (∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z) → z ∈ annulus_oc c r0 r1
Tactic:
intro gp
Proof state after:
case h.mp
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
gp : ∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z
⊢ z ∈ annulus_oc c r0 r1
Theorem: square_eq
Proof state before:
case h.mp
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
gp : ∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z
⊢ z ∈ annulus_oc c r0 r1
Tactic:
rcases gp with ⟨⟨s, t⟩, ss, tz⟩
Proof state after:
case h.mp.intro.mk.intro
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
s t : ℝ
ss : (s, t) ∈ square r0 r1
tz : circleMap c (s, t).1 (s, t).2 = z
⊢ z ∈ annulus_oc c r0 r1
Theorem: square_eq
Proof state before:
case h.mp.intro.mk.intro
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
s t : ℝ
ss : (s, t) ∈ square r0 r1
tz : circleMap c (s, t).1 (s, t).2 = z
⊢ z ∈ annulus_oc c r0 r1
Tactic:
simp only at tz
Proof state after:
case h.mp.intro.mk.intro
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
s t : ℝ
ss : (s, t) ∈ square r0 r1
tz : circleMap c s t = z
⊢ z ∈ annulus_oc c r0 r1
Theorem: square_eq
Proof state before:
case h.mp.intro.mk.intro
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
s t : ℝ
ss : (s, t) ∈ square r0 r1
tz : circleMap c s t = z
⊢ z ∈ annulus_oc c r0 r1
Tactic:
simp only [square, prod_mk_mem_set_prod_eq, mem_Ioc] at ss
Proof state after:
case h.mp.intro.mk.intro
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
s t : ℝ
tz : circleMap c s t = z
ss : (r0 < s ∧ s ≤ r1) ∧ 0 < t ∧ t ≤ 2 * π
⊢ z ∈ annulus_oc c r0 r1
Theorem: square_eq
Proof state before:
case h.mp.intro.mk.intro
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
s t : ℝ
tz : circleMap c s t = z
ss : (r0 < s ∧ s ≤ r1) ∧ 0 < t ∧ t ≤ 2 * π
⊢ z ∈ annulus_oc c r0 r1
Tactic:
rw [← tz]
Proof state after:
case h.mp.intro.mk.intro
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
s t : ℝ
tz : circleMap c s t = z
ss : (r0 < s ∧ s ≤ r1) ∧ 0 < t ∧ t ≤ 2 * π
⊢ circleMap c s t ∈ annulus_oc c r0 r1
Theorem: square_eq
Proof state before:
case h.mp.intro.mk.intro
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
s t : ℝ
tz : circleMap c s t = z
ss : (r0 < s ∧ s ≤ r1) ∧ 0 < t ∧ t ≤ 2 * π
⊢ circleMap c s t ∈ annulus_oc c r0 r1
Tactic:
have s0 : 0 < s := by linarith
Proof state after:
case h.mp.intro.mk.intro
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
s t : ℝ
tz : circleMap c s t = z
ss : (r0 < s ∧ s ≤ r1) ∧ 0 < t ∧ t ≤ 2 * π
s0 : 0 < s
⊢ circleMap c s t ∈ annulus_oc c r0 r1
Theorem: square_eq
Proof state before:
case h.mp.intro.mk.intro
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
s t : ℝ
tz : circleMap c s t = z
ss : (r0 < s ∧ s ≤ r1) ∧ 0 < t ∧ t ≤ 2 * π
s0 : 0 < s
⊢ circleMap c s t ∈ annulus_oc c r0 r1
Tactic:
simp only [circleMap, add_comm c, annulus_oc, mem_diff, Metric.mem_closedBall,
  dist_add_self_left, norm_mul, Complex.norm_eq_abs, Complex.abs_ofReal,
  Complex.abs_exp_ofReal_mul_I, mul_one, not_le, abs_of_pos s0, ss.1, true_and]
Proof state after:
no goals
Theorem: square_eq
Proof state before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
s t : ℝ
tz : circleMap c s t = z
ss : (r0 < s ∧ s ≤ r1) ∧ 0 < t ∧ t ≤ 2 * π
⊢ 0 < s
Tactic:
linarith
Proof state after:
no goals
Theorem: square_eq
Proof state before:
case h.mpr
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
⊢ z ∈ annulus_oc c r0 r1 → ∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z
Tactic:
intro zr
Proof state after:
case h.mpr
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
zr : z ∈ annulus_oc c r0 r1
⊢ ∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z
Theorem: square_eq
Proof state before:
case h.mpr
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
zr : z ∈ annulus_oc c r0 r1
⊢ ∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z
Tactic:
simp only [mem_diff, Metric.mem_closedBall, mem_singleton_iff, annulus_oc,
  not_le] at zr
Proof state after:
case h.mpr
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
zr : dist z c ≤ r1 ∧ r0 < dist z c
⊢ ∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z
Theorem: square_eq
Proof state before:
case h.mpr
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
zr : dist z c ≤ r1 ∧ r0 < dist z c
⊢ ∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z
Tactic:
rw [dist_comm] at zr
Proof state after:
case h.mpr
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
zr : dist c z ≤ r1 ∧ r0 < dist c z
⊢ ∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z
Theorem: square_eq
Proof state before:
case h.mpr
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
zr : dist c z ≤ r1 ∧ r0 < dist c z
⊢ ∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z
Tactic:
have zz : z ∈ sphere c (dist c z) := by
  simp only [Complex.dist_eq, mem_sphere_iff_norm, Complex.norm_eq_abs, Complex.abs.map_sub]
Proof state after:
case h.mpr
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
zr : dist c z ≤ r1 ∧ r0 < dist c z
zz : z ∈ sphere c (dist c z)
⊢ ∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z
Theorem: square_eq
Proof state before:
case h.mpr
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
zr : dist c z ≤ r1 ∧ r0 < dist c z
zz : z ∈ sphere c (dist c z)
⊢ ∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z
Tactic:
rcases circleMap_Ioc zz with ⟨t, ts, tz⟩
Proof state after:
case h.mpr.intro.intro
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
zr : dist c z ≤ r1 ∧ r0 < dist c z
zz : z ∈ sphere c (dist c z)
t : ℝ
ts : t ∈ Ioc 0 (2 * π)
tz : z = circleMap c (dist c z) t
⊢ ∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z
Theorem: square_eq
Proof state before:
case h.mpr.intro.intro
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
zr : dist c z ≤ r1 ∧ r0 < dist c z
zz : z ∈ sphere c (dist c z)
t : ℝ
ts : t ∈ Ioc 0 (2 * π)
tz : z = circleMap c (dist c z) t
⊢ ∃ x ∈ square r0 r1, circleMap c x.1 x.2 = z
Tactic:
use (dist c z, t)
Proof state after:
case h
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
zr : dist c z ≤ r1 ∧ r0 < dist c z
zz : z ∈ sphere c (dist c z)
t : ℝ
ts : t ∈ Ioc 0 (2 * π)
tz : z = circleMap c (dist c z) t
⊢ (dist c z, t) ∈ square r0 r1 ∧ circleMap c (dist c z, t).1 (dist c z, t).2 = z
Theorem: square_eq
Proof state before:
case h
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
zr : dist c z ≤ r1 ∧ r0 < dist c z
zz : z ∈ sphere c (dist c z)
t : ℝ
ts : t ∈ Ioc 0 (2 * π)
tz : z = circleMap c (dist c z) t
⊢ (dist c z, t) ∈ square r0 r1 ∧ circleMap c (dist c z, t).1 (dist c z, t).2 = z
Tactic:
simpa only [square, gt_iff_lt, not_lt, ge_iff_le, zero_lt_two, mul_pos_iff_of_pos_left,
  mem_prod, mem_Ioc, dist_pos, ne_eq, not_false_eq_true, zr, and_self, true_and,
  tz.symm, and_true] using ts
Proof state after:
no goals
Theorem: square_eq
Proof state before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
z : ℂ
zr : dist c z ≤ r1 ∧ r0 < dist c z
⊢ z ∈ sphere c (dist c z)
Tactic:
simp only [Complex.dist_eq, mem_sphere_iff_norm, Complex.norm_eq_abs, Complex.abs.map_sub]
Proof state after:
no goals
Theorem: exp_of_im
Proof state before:
t : ℝ
⊢ (↑t * I).exp = ↑t.cos + ↑t.sin * I
Tactic:
simp [Complex.ext_iff, Complex.cos_ofReal_re, Complex.sin_ofReal_re]
Proof state after:
no goals
Theorem: Complex.cos_eq_cos
Proof state before:
t : ℝ
⊢ (↑t).cos = ↑t.cos
Tactic:
simp
Proof state after:
no goals
Theorem: Complex.sin_eq_sin
Proof state before:
t : ℝ
⊢ (↑t).sin = ↑t.sin
Tactic:
simp
Proof state after:
no goals
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
⊢ ∃ n, (↑t * I).exp.arg = t - 2 * π * ↑n
Tactic:
generalize hn : ⌈t / (2 * π) - 1 / 2⌉ = n
Proof state after:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
⊢ ∃ n, (↑t * I).exp.arg = t - 2 * π * ↑n
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
⊢ ∃ n, (↑t * I).exp.arg = t - 2 * π * ↑n
Tactic:
exists n
Proof state after:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
⊢ (↑t * I).exp.arg = t - 2 * π * ↑n
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
⊢ (↑t * I).exp.arg = t - 2 * π * ↑n
Tactic:
have en : exp (2 * π * n * I) = 1 := by
  rw [mul_comm _ (n:ℂ), mul_assoc, Complex.exp_int_mul]
  simp only [Complex.exp_two_pi_mul_I, one_zpow]
Proof state after:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
⊢ (↑t * I).exp.arg = t - 2 * π * ↑n
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
⊢ (↑t * I).exp.arg = t - 2 * π * ↑n
Tactic:
have e : exp (t * I) = exp (↑(t - 2 * π * n) * I) := by
  simp [mul_sub_right_distrib, Complex.exp_sub, en]
Proof state after:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ (↑t * I).exp.arg = t - 2 * π * ↑n
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
ts : t - 2 * π * ↑n ∈ Ioc (-π) π
⊢ (↑t * I).exp.arg = t - 2 * π * ↑n
Tactic:
rw [e, exp_of_im, ← Complex.cos_eq_cos, ← Complex.sin_eq_sin, Complex.arg_cos_add_sin_mul_I ts]
Proof state after:
no goals
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
⊢ (2 * ↑π * ↑n * I).exp = 1
Tactic:
rw [mul_comm _ (n:ℂ), mul_assoc, Complex.exp_int_mul]
Proof state after:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
⊢ (2 * ↑π * I).exp ^ n = 1
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
⊢ (2 * ↑π * I).exp ^ n = 1
Tactic:
simp only [Complex.exp_two_pi_mul_I, one_zpow]
Proof state after:
no goals
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
⊢ (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
Tactic:
simp [mul_sub_right_distrib, Complex.exp_sub, en]
Proof state after:
no goals
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ t - 2 * π * ↑n ∈ Ioc (-π) π
Tactic:
simp only [mem_Ioc, neg_lt_sub_iff_lt_add, tsub_le_iff_right]
Proof state after:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ 2 * π * ↑n < π + t ∧ t ≤ π + 2 * π * ↑n
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ 2 * π * ↑n < π + t ∧ t ≤ π + 2 * π * ↑n
Tactic:
constructor
Proof state after:
case left
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ 2 * π * ↑n < π + t

case right
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ t ≤ π + 2 * π * ↑n
Theorem: arg_exp_of_im
Proof state before:
case left
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ 2 * π * ↑n < π + t
Tactic:
have h : ↑n < t * (2 * π)⁻¹ - 1 / 2 + 1 := by rw [← hn]; exact Int.ceil_lt_add_one _
Proof state after:
case left
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n < t * (2 * π)⁻¹ - 1 / 2 + 1
⊢ 2 * π * ↑n < π + t
Theorem: arg_exp_of_im
Proof state before:
case left
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n < t * (2 * π)⁻¹ - 1 / 2 + 1
⊢ 2 * π * ↑n < π + t
Tactic:
calc 2 * π * ↑n
  _ < 2 * π * (t * (2 * π)⁻¹ - 1 / 2 + 1) := by bound
  _ = π + 2 * π * (2 * π)⁻¹ * t := by ring
  _ = π + t := by field_simp [Real.two_pi_pos.ne']
Proof state after:
no goals
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ ↑n < t * (2 * π)⁻¹ - 1 / 2 + 1
Tactic:
rw [← hn]
Proof state after:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ ↑⌈t / (2 * π) - 1 / 2⌉ < t * (2 * π)⁻¹ - 1 / 2 + 1
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ ↑⌈t / (2 * π) - 1 / 2⌉ < t * (2 * π)⁻¹ - 1 / 2 + 1
Tactic:
exact Int.ceil_lt_add_one _
Proof state after:
no goals
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n < t * (2 * π)⁻¹ - 1 / 2 + 1
⊢ 2 * π * ↑n < 2 * π * (t * (2 * π)⁻¹ - 1 / 2 + 1)
Tactic:
bound
Proof state after:
no goals
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n < t * (2 * π)⁻¹ - 1 / 2 + 1
⊢ 2 * π * (t * (2 * π)⁻¹ - 1 / 2 + 1) = π + 2 * π * (2 * π)⁻¹ * t
Tactic:
ring
Proof state after:
no goals
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n < t * (2 * π)⁻¹ - 1 / 2 + 1
⊢ π + 2 * π * (2 * π)⁻¹ * t = π + t
Tactic:
field_simp [Real.two_pi_pos.ne']
Proof state after:
no goals
Theorem: arg_exp_of_im
Proof state before:
case right
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ t ≤ π + 2 * π * ↑n
Tactic:
have h : ↑n ≥ t * (2 * π)⁻¹ - 1 / 2 := by rw [← hn]; exact Int.le_ceil _
Proof state after:
case right
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n ≥ t * (2 * π)⁻¹ - 1 / 2
⊢ t ≤ π + 2 * π * ↑n
Theorem: arg_exp_of_im
Proof state before:
case right
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n ≥ t * (2 * π)⁻¹ - 1 / 2
⊢ t ≤ π + 2 * π * ↑n
Tactic:
calc π + 2 * π * ↑n
  _ ≥ π + 2 * π * (t * (2 * π)⁻¹ - 1 / 2) := by bound
  _ = 2 * π * (2 * π)⁻¹ * t := by ring
  _ = t := by field_simp [Real.two_pi_pos.ne']
Proof state after:
no goals
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ ↑n ≥ t * (2 * π)⁻¹ - 1 / 2
Tactic:
rw [← hn]
Proof state after:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ ↑⌈t / (2 * π) - 1 / 2⌉ ≥ t * (2 * π)⁻¹ - 1 / 2
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
⊢ ↑⌈t / (2 * π) - 1 / 2⌉ ≥ t * (2 * π)⁻¹ - 1 / 2
Tactic:
exact Int.le_ceil _
Proof state after:
no goals
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n ≥ t * (2 * π)⁻¹ - 1 / 2
⊢ π + 2 * π * ↑n ≥ π + 2 * π * (t * (2 * π)⁻¹ - 1 / 2)
Tactic:
bound
Proof state after:
no goals
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n ≥ t * (2 * π)⁻¹ - 1 / 2
⊢ π + 2 * π * (t * (2 * π)⁻¹ - 1 / 2) = 2 * π * (2 * π)⁻¹ * t
Tactic:
ring
Proof state after:
no goals
Theorem: arg_exp_of_im
Proof state before:
t : ℝ
n : ℤ
hn : ⌈t / (2 * π) - 1 / 2⌉ = n
en : (2 * ↑π * ↑n * I).exp = 1
e : (↑t * I).exp = (↑(t - 2 * π * ↑n) * I).exp
h : ↑n ≥ t * (2 * π)⁻¹ - 1 / 2
⊢ 2 * π * (2 * π)⁻¹ * t = t
Tactic:
field_simp [Real.two_pi_pos.ne']
Proof state after:
no goals
Theorem: rcm_inj
Proof state before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
⊢ InjOn (realCircleMap c) (square r0 r1)
Tactic:
intro x xs y ys e
Proof state after:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x : ℝ × ℝ
xs : x ∈ square r0 r1
y : ℝ × ℝ
ys : y ∈ square r0 r1
e : realCircleMap c x = realCircleMap c y
⊢ x = y
Theorem: rcm_inj
Proof state before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x : ℝ × ℝ
xs : x ∈ square r0 r1
y : ℝ × ℝ
ys : y ∈ square r0 r1
e : realCircleMap c x = realCircleMap c y
⊢ x = y
Tactic:
simp [square] at xs ys
Proof state after:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x y : ℝ × ℝ
e : realCircleMap c x = realCircleMap c y
xs : (r0 < x.1 ∧ x.1 ≤ r1) ∧ 0 < x.2 ∧ x.2 ≤ 2 * π
ys : (r0 < y.1 ∧ y.1 ≤ r1) ∧ 0 < y.2 ∧ y.2 ≤ 2 * π
⊢ x = y
Theorem: rcm_inj
Proof state before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x y : ℝ × ℝ
e : realCircleMap c x = realCircleMap c y
xs : (r0 < x.1 ∧ x.1 ≤ r1) ∧ 0 < x.2 ∧ x.2 ≤ 2 * π
ys : (r0 < y.1 ∧ y.1 ≤ r1) ∧ 0 < y.2 ∧ y.2 ≤ 2 * π
⊢ x = y
Tactic:
simp_rw [realCircleMap_eq_circleMap, Equiv.apply_eq_iff_eq] at e
Proof state after:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x y : ℝ × ℝ
xs : (r0 < x.1 ∧ x.1 ≤ r1) ∧ 0 < x.2 ∧ x.2 ≤ 2 * π
ys : (r0 < y.1 ∧ y.1 ≤ r1) ∧ 0 < y.2 ∧ y.2 ≤ 2 * π
e : circleMap c x.1 x.2 = circleMap c y.1 y.2
⊢ x = y
Theorem: rcm_inj
Proof state before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x y : ℝ × ℝ
xs : (r0 < x.1 ∧ x.1 ≤ r1) ∧ 0 < x.2 ∧ x.2 ≤ 2 * π
ys : (r0 < y.1 ∧ y.1 ≤ r1) ∧ 0 < y.2 ∧ y.2 ≤ 2 * π
e : circleMap c x.1 x.2 = circleMap c y.1 y.2
⊢ x = y
Tactic:
simp_rw [circleMap] at e
Proof state after:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x y : ℝ × ℝ
xs : (r0 < x.1 ∧ x.1 ≤ r1) ∧ 0 < x.2 ∧ x.2 ≤ 2 * π
ys : (r0 < y.1 ∧ y.1 ≤ r1) ∧ 0 < y.2 ∧ y.2 ≤ 2 * π
e : c + ↑x.1 * (↑x.2 * I).exp = c + ↑y.1 * (↑y.2 * I).exp
⊢ x = y
Theorem: rcm_inj
Proof state before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x y : ℝ × ℝ
xs : (r0 < x.1 ∧ x.1 ≤ r1) ∧ 0 < x.2 ∧ x.2 ≤ 2 * π
ys : (r0 < y.1 ∧ y.1 ≤ r1) ∧ 0 < y.2 ∧ y.2 ≤ 2 * π
e : c + ↑x.1 * (↑x.2 * I).exp = c + ↑y.1 * (↑y.2 * I).exp
⊢ x = y
Tactic:
simp at e
Proof state after:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x y : ℝ × ℝ
xs : (r0 < x.1 ∧ x.1 ≤ r1) ∧ 0 < x.2 ∧ x.2 ≤ 2 * π
ys : (r0 < y.1 ∧ y.1 ≤ r1) ∧ 0 < y.2 ∧ y.2 ≤ 2 * π
e : ↑x.1 * (↑x.2 * I).exp = ↑y.1 * (↑y.2 * I).exp
⊢ x = y
Theorem: rcm_inj
Proof state before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x y : ℝ × ℝ
xs : (r0 < x.1 ∧ x.1 ≤ r1) ∧ 0 < x.2 ∧ x.2 ≤ 2 * π
ys : (r0 < y.1 ∧ y.1 ≤ r1) ∧ 0 < y.2 ∧ y.2 ≤ 2 * π
e : ↑x.1 * (↑x.2 * I).exp = ↑y.1 * (↑y.2 * I).exp
⊢ x = y
Tactic:
have re : abs (↑x.1 * exp (x.2 * I)) = abs (↑y.1 * exp (y.2 * I)) := by rw [e]
Proof state after:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x y : ℝ × ℝ
xs : (r0 < x.1 ∧ x.1 ≤ r1) ∧ 0 < x.2 ∧ x.2 ≤ 2 * π
ys : (r0 < y.1 ∧ y.1 ≤ r1) ∧ 0 < y.2 ∧ y.2 ≤ 2 * π
e : ↑x.1 * (↑x.2 * I).exp = ↑y.1 * (↑y.2 * I).exp
re : Complex.abs (↑x.1 * (↑x.2 * I).exp) = Complex.abs (↑y.1 * (↑y.2 * I).exp)
⊢ x = y
Theorem: rcm_inj
Proof state before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x y : ℝ × ℝ
xs : (r0 < x.1 ∧ x.1 ≤ r1) ∧ 0 < x.2 ∧ x.2 ≤ 2 * π
ys : (r0 < y.1 ∧ y.1 ≤ r1) ∧ 0 < y.2 ∧ y.2 ≤ 2 * π
e : ↑x.1 * (↑x.2 * I).exp = ↑y.1 * (↑y.2 * I).exp
re : Complex.abs (↑x.1 * (↑x.2 * I).exp) = Complex.abs (↑y.1 * (↑y.2 * I).exp)
⊢ x = y
Tactic:
have x0 : 0 < x.1 := by linarith
Proof state after:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x y : ℝ × ℝ
xs : (r0 < x.1 ∧ x.1 ≤ r1) ∧ 0 < x.2 ∧ x.2 ≤ 2 * π
ys : (r0 < y.1 ∧ y.1 ≤ r1) ∧ 0 < y.2 ∧ y.2 ≤ 2 * π
e : ↑x.1 * (↑x.2 * I).exp = ↑y.1 * (↑y.2 * I).exp
re : Complex.abs (↑x.1 * (↑x.2 * I).exp) = Complex.abs (↑y.1 * (↑y.2 * I).exp)
x0 : 0 < x.1
⊢ x = y
Theorem: rcm_inj
Proof state before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x y : ℝ × ℝ
xs : (r0 < x.1 ∧ x.1 ≤ r1) ∧ 0 < x.2 ∧ x.2 ≤ 2 * π
ys : (r0 < y.1 ∧ y.1 ≤ r1) ∧ 0 < y.2 ∧ y.2 ≤ 2 * π
e : ↑x.1 * (↑x.2 * I).exp = ↑y.1 * (↑y.2 * I).exp
re : Complex.abs (↑x.1 * (↑x.2 * I).exp) = Complex.abs (↑y.1 * (↑y.2 * I).exp)
x0 : 0 < x.1
⊢ x = y
Tactic:
have y0 : 0 < y.1 := by linarith
Proof state after:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x y : ℝ × ℝ
xs : (r0 < x.1 ∧ x.1 ≤ r1) ∧ 0 < x.2 ∧ x.2 ≤ 2 * π
ys : (r0 < y.1 ∧ y.1 ≤ r1) ∧ 0 < y.2 ∧ y.2 ≤ 2 * π
e : ↑x.1 * (↑x.2 * I).exp = ↑y.1 * (↑y.2 * I).exp
re : Complex.abs (↑x.1 * (↑x.2 * I).exp) = Complex.abs (↑y.1 * (↑y.2 * I).exp)
x0 : 0 < x.1
y0 : 0 < y.1
⊢ x = y