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

State before:
c : ℂ
r0 r1 : ℝ
r0p : 0 ≤ r0
⊢ InjOn (realCircleMap c) (square r0 r1)
Tactic:
intro x xs y ys e
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

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

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

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

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

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

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

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

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
y0 : 0 < y.1
⊢ x = y
Tactic:
simp only [map_mul, Complex.abs_ofReal, abs_of_pos x0, Complex.abs_exp_ofReal_mul_I, mul_one,
  abs_of_pos y0] at re
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
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
⊢ x = y

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
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
⊢ x = y
Tactic:
have ae : arg (↑x.1 * exp (x.2 * I)) = arg (↑y.1 * exp (y.2 * I)) := by rw [e]
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
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
ae : (↑x.1 * (↑x.2 * I).exp).arg = (↑y.1 * (↑y.2 * I).exp).arg
⊢ x = y

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
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
ae : (↑x.1 * (↑x.2 * I).exp).arg = (↑y.1 * (↑y.2 * I).exp).arg
⊢ x = y
Tactic:
simp [Complex.arg_real_mul _ x0, Complex.arg_real_mul _ y0] at ae
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
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
ae : (↑x.2 * I).exp.arg = (↑y.2 * I).exp.arg
⊢ x = y

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
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
ae : (↑x.2 * I).exp.arg = (↑y.2 * I).exp.arg
⊢ x = y
Tactic:
rcases arg_exp_of_im x.2 with ⟨nx, hx⟩
State after:
case intro
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
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
ae : (↑x.2 * I).exp.arg = (↑y.2 * I).exp.arg
nx : ℤ
hx : (↑x.2 * I).exp.arg = x.2 - 2 * π * ↑nx
⊢ x = y

State before:
case intro
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
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
ae : (↑x.2 * I).exp.arg = (↑y.2 * I).exp.arg
nx : ℤ
hx : (↑x.2 * I).exp.arg = x.2 - 2 * π * ↑nx
⊢ x = y
Tactic:
rcases arg_exp_of_im y.2 with ⟨ny, h⟩
State after:
case intro.intro
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
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
ae : (↑x.2 * I).exp.arg = (↑y.2 * I).exp.arg
nx : ℤ
hx : (↑x.2 * I).exp.arg = x.2 - 2 * π * ↑nx
ny : ℤ
h : (↑y.2 * I).exp.arg = y.2 - 2 * π * ↑ny
⊢ x = y

State before:
case intro.intro
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
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
ae : (↑x.2 * I).exp.arg = (↑y.2 * I).exp.arg
nx : ℤ
hx : (↑x.2 * I).exp.arg = x.2 - 2 * π * ↑nx
ny : ℤ
h : (↑y.2 * I).exp.arg = y.2 - 2 * π * ↑ny
⊢ x = y
Tactic:
rw [← ae, hx] at h
State after:
case intro.intro
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
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
ae : (↑x.2 * I).exp.arg = (↑y.2 * I).exp.arg
nx : ℤ
hx : (↑x.2 * I).exp.arg = x.2 - 2 * π * ↑nx
ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
⊢ x = y

State before:
case intro.intro
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
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
ae : (↑x.2 * I).exp.arg = (↑y.2 * I).exp.arg
nx : ℤ
hx : (↑x.2 * I).exp.arg = x.2 - 2 * π * ↑nx
ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
⊢ x = y
Tactic:
clear e ae hx
State after:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
⊢ x = y

State before:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
⊢ x = y
Tactic:
have n0 : 2 * π * (nx - ny) < 2 * π * 1 := by linarith
State after:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : 2 * π * (↑nx - ↑ny) < 2 * π * 1
⊢ x = y

State before:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : 2 * π * (↑nx - ↑ny) < 2 * π * 1
⊢ x = y
Tactic:
have n1 : 2 * π * -1 < 2 * π * (nx - ny) := by linarith
State after:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : 2 * π * (↑nx - ↑ny) < 2 * π * 1
n1 : 2 * π * -1 < 2 * π * (↑nx - ↑ny)
⊢ x = y

State before:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : 2 * π * (↑nx - ↑ny) < 2 * π * 1
n1 : 2 * π * -1 < 2 * π * (↑nx - ↑ny)
⊢ x = y
Tactic:
have hn : (nx : ℝ) - ny = ↑(nx - ny) := by simp only [Int.cast_sub]
State after:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : 2 * π * (↑nx - ↑ny) < 2 * π * 1
n1 : 2 * π * -1 < 2 * π * (↑nx - ↑ny)
hn : ↑nx - ↑ny = ↑(nx - ny)
⊢ x = y

State before:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : 2 * π * (↑nx - ↑ny) < 2 * π * 1
n1 : 2 * π * -1 < 2 * π * (↑nx - ↑ny)
hn : ↑nx - ↑ny = ↑(nx - ny)
⊢ x = y
Tactic:
have hn1 : (-1 : ℝ) = ↑(-1 : ℤ) := by norm_num
State after:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : 2 * π * (↑nx - ↑ny) < 2 * π * 1
n1 : 2 * π * -1 < 2 * π * (↑nx - ↑ny)
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
⊢ x = y

State before:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : 2 * π * (↑nx - ↑ny) < 2 * π * 1
n1 : 2 * π * -1 < 2 * π * (↑nx - ↑ny)
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
⊢ x = y
Tactic:
have h1 : (1 : ℝ) = ↑(1 : ℤ) := by norm_num
State after:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : 2 * π * (↑nx - ↑ny) < 2 * π * 1
n1 : 2 * π * -1 < 2 * π * (↑nx - ↑ny)
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
⊢ x = y

State before:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : 2 * π * (↑nx - ↑ny) < 2 * π * 1
n1 : 2 * π * -1 < 2 * π * (↑nx - ↑ny)
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
⊢ x = y
Tactic:
rw [mul_lt_mul_left Real.two_pi_pos, hn] at n0 n1
State after:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : ↑(nx - ny) < 1
n1 : -1 < ↑(nx - ny)
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
⊢ x = y

State before:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : ↑(nx - ny) < 1
n1 : -1 < ↑(nx - ny)
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
⊢ x = y
Tactic:
rw [hn1] at n1
State after:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : ↑(nx - ny) < 1
n1 : ↑(-1) < ↑(nx - ny)
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
⊢ x = y

State before:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : ↑(nx - ny) < 1
n1 : ↑(-1) < ↑(nx - ny)
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
⊢ x = y
Tactic:
rw [h1] at n0
State after:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : ↑(nx - ny) < ↑1
n1 : ↑(-1) < ↑(nx - ny)
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
⊢ x = y

State before:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : ↑(nx - ny) < ↑1
n1 : ↑(-1) < ↑(nx - ny)
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
⊢ x = y
Tactic:
rw [Int.cast_lt] at n0 n1
State after:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : nx - ny < 1
n1 : -1 < nx - ny
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
⊢ x = y

State before:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : nx - ny < 1
n1 : -1 < nx - ny
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
⊢ x = y
Tactic:
have n : nx = ny := by linarith
State after:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : nx - ny < 1
n1 : -1 < nx - ny
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
n : nx = ny
⊢ x = y

State before:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : nx - ny < 1
n1 : -1 < nx - ny
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
n : nx = ny
⊢ x = y
Tactic:
rw [n] at h
State after:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑ny = y.2 - 2 * π * ↑ny
n0 : nx - ny < 1
n1 : -1 < nx - ny
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
n : nx = ny
⊢ x = y

State before:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑ny = y.2 - 2 * π * ↑ny
n0 : nx - ny < 1
n1 : -1 < nx - ny
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
n : nx = ny
⊢ x = y
Tactic:
have i : x.2 = y.2 := by linarith
State after:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑ny = y.2 - 2 * π * ↑ny
n0 : nx - ny < 1
n1 : -1 < nx - ny
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
n : nx = ny
i : x.2 = y.2
⊢ x = y

State before:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑ny = y.2 - 2 * π * ↑ny
n0 : nx - ny < 1
n1 : -1 < nx - ny
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
n : nx = ny
i : x.2 = y.2
⊢ x = y
Tactic:
have g : (x.1, x.2) = (y.1, y.2) := by rw [re, i]
State after:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑ny = y.2 - 2 * π * ↑ny
n0 : nx - ny < 1
n1 : -1 < nx - ny
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
n : nx = ny
i : x.2 = y.2
g : (x.1, x.2) = (y.1, y.2)
⊢ x = y

State before:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑ny = y.2 - 2 * π * ↑ny
n0 : nx - ny < 1
n1 : -1 < nx - ny
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
n : nx = ny
i : x.2 = y.2
g : (x.1, x.2) = (y.1, y.2)
⊢ x = y
Tactic:
simp only [Prod.mk.eta] at g
State after:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑ny = y.2 - 2 * π * ↑ny
n0 : nx - ny < 1
n1 : -1 < nx - ny
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
n : nx = ny
i : x.2 = y.2
g : x = y
⊢ x = y

State before:
case intro.intro
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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑ny = y.2 - 2 * π * ↑ny
n0 : nx - ny < 1
n1 : -1 < nx - ny
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
n : nx = ny
i : x.2 = y.2
g : x = y
⊢ x = y
Tactic:
exact g
State after:
no goals

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
⊢ Complex.abs (↑x.1 * (↑x.2 * I).exp) = Complex.abs (↑y.1 * (↑y.2 * I).exp)
Tactic:
rw [e]
State after:
no goals

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)
⊢ 0 < x.1
Tactic:
linarith
State after:
no goals

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
⊢ 0 < y.1
Tactic:
linarith
State after:
no goals

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
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
⊢ (↑x.1 * (↑x.2 * I).exp).arg = (↑y.1 * (↑y.2 * I).exp).arg
Tactic:
rw [e]
State after:
no goals

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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
⊢ 2 * π * (↑nx - ↑ny) < 2 * π * 1
Tactic:
linarith
State after:
no goals

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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : 2 * π * (↑nx - ↑ny) < 2 * π * 1
⊢ 2 * π * -1 < 2 * π * (↑nx - ↑ny)
Tactic:
linarith
State after:
no goals

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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : 2 * π * (↑nx - ↑ny) < 2 * π * 1
n1 : 2 * π * -1 < 2 * π * (↑nx - ↑ny)
⊢ ↑nx - ↑ny = ↑(nx - ny)
Tactic:
simp only [Int.cast_sub]
State after:
no goals

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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : 2 * π * (↑nx - ↑ny) < 2 * π * 1
n1 : 2 * π * -1 < 2 * π * (↑nx - ↑ny)
hn : ↑nx - ↑ny = ↑(nx - ny)
⊢ -1 = ↑(-1)
Tactic:
norm_num
State after:
no goals

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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : 2 * π * (↑nx - ↑ny) < 2 * π * 1
n1 : 2 * π * -1 < 2 * π * (↑nx - ↑ny)
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
⊢ 1 = ↑1
Tactic:
norm_num
State after:
no goals

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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑nx = y.2 - 2 * π * ↑ny
n0 : nx - ny < 1
n1 : -1 < nx - ny
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
⊢ nx = ny
Tactic:
linarith
State after:
no goals

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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑ny = y.2 - 2 * π * ↑ny
n0 : nx - ny < 1
n1 : -1 < nx - ny
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
n : nx = ny
⊢ x.2 = y.2
Tactic:
linarith
State after:
no goals

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 * π
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.1
nx ny : ℤ
h : x.2 - 2 * π * ↑ny = y.2 - 2 * π * ↑ny
n0 : nx - ny < 1
n1 : -1 < nx - ny
hn : ↑nx - ↑ny = ↑(nx - ny)
hn1 : -1 = ↑(-1)
h1 : 1 = ↑1
n : nx = ny
i : x.2 = y.2
⊢ (x.1, x.2) = (y.1, y.2)
Tactic:
rw [re, i]
State after:
no goals