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

State before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
⊢ ⇑Complex.measurableEquivRealProd.symm ⁻¹' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1
Tactic:
rw [← MeasurableEquiv.image_eq_preimage]
State after:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
⊢ ⇑Complex.measurableEquivRealProd '' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1

State before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
⊢ ⇑Complex.measurableEquivRealProd '' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1
Tactic:
have e : realCircleMap c =
    fun x : ℝ × ℝ ↦ Complex.measurableEquivRealProd (circleMap c x.1 x.2) := by
  funext
  simp only [realCircleMap_eq_circleMap, Complex.measurableEquivRealProd,
    Complex.equivRealProd_apply, Homeomorph.toMeasurableEquiv_coe,
    ContinuousLinearEquiv.coe_toHomeomorph, Complex.equivRealProdCLM_apply]
State after:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
⊢ ⇑Complex.measurableEquivRealProd '' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1

State before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
i : (fun x => circleMap c x.1 x.2) '' square r0 r1 = annulus_oc c r0 r1
⊢ ⇑Complex.measurableEquivRealProd '' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1
Tactic:
have im := image_comp Complex.measurableEquivRealProd (fun x : ℝ × ℝ ↦ circleMap c x.1 x.2)
  (square r0 r1)
State after:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
i : (fun x => circleMap c x.1 x.2) '' square r0 r1 = annulus_oc c r0 r1
im :
  (⇑Complex.measurableEquivRealProd ∘ fun x => circleMap c x.1 x.2) '' square r0 r1 =
    ⇑Complex.measurableEquivRealProd '' ((fun x => circleMap c x.1 x.2) '' square r0 r1)
⊢ ⇑Complex.measurableEquivRealProd '' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1

State before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
i : (fun x => circleMap c x.1 x.2) '' square r0 r1 = annulus_oc c r0 r1
im :
  (⇑Complex.measurableEquivRealProd ∘ fun x => circleMap c x.1 x.2) '' square r0 r1 =
    ⇑Complex.measurableEquivRealProd '' ((fun x => circleMap c x.1 x.2) '' square r0 r1)
⊢ ⇑Complex.measurableEquivRealProd '' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1
Tactic:
simp only [Function.comp] at im
State after:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
i : (fun x => circleMap c x.1 x.2) '' square r0 r1 = annulus_oc c r0 r1
im :
  (fun a => Complex.measurableEquivRealProd (circleMap c a.1 a.2)) '' square r0 r1 =
    ⇑Complex.measurableEquivRealProd '' ((fun x => circleMap c x.1 x.2) '' square r0 r1)
⊢ ⇑Complex.measurableEquivRealProd '' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1

State before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
e : realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
i : (fun x => circleMap c x.1 x.2) '' square r0 r1 = annulus_oc c r0 r1
im :
  (fun a => Complex.measurableEquivRealProd (circleMap c a.1 a.2)) '' square r0 r1 =
    ⇑Complex.measurableEquivRealProd '' ((fun x => circleMap c x.1 x.2) '' square r0 r1)
⊢ ⇑Complex.measurableEquivRealProd '' annulus_oc c r0 r1 = realCircleMap c '' square r0 r1
Tactic:
simp only [e, im, i]
State after:
no goals

State before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
⊢ realCircleMap c = fun x => Complex.measurableEquivRealProd (circleMap c x.1 x.2)
Tactic:
funext
State after:
case h
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
x✝ : ℝ × ℝ
⊢ realCircleMap c x✝ = Complex.measurableEquivRealProd (circleMap c x✝.1 x✝.2)

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]
State after:
no goals

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

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]
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

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

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

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

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

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

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]
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

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

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]
State after:
no goals

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
State after:
no goals

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

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

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

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]
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

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

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)
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

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
State after:
no goals

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]
State after:
no goals