internlm/Lean-Github huggingface dataset:
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
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
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
x0 : 0 < x.1
y0 : 0 < y.1
re : x.1 = y.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
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]
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
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
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
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
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
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
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
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⟩
Proof 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
Theorem: rcm_inj
Proof 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⟩
Proof 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
Theorem: rcm_inj
Proof 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
Proof 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
Theorem: rcm_inj
Proof 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
Proof 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
Theorem: rcm_inj
Proof 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
Proof 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
Theorem: rcm_inj
Proof 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
Proof 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
Theorem: rcm_inj
Proof 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]
Proof 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
Theorem: rcm_inj
Proof 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
Proof 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
Theorem: rcm_inj
Proof 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
Proof 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
Theorem: rcm_inj
Proof 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
Proof 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
Theorem: rcm_inj
Proof 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
Proof 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
Theorem: rcm_inj
Proof 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
Proof 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
Theorem: rcm_inj
Proof 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
Proof 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
Theorem: rcm_inj
Proof 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
Proof 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
Theorem: rcm_inj
Proof 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
Proof 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
Theorem: rcm_inj
Proof 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
Proof 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
Theorem: rcm_inj
Proof 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]
Proof 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
Theorem: rcm_inj
Proof 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
Proof 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
Theorem: rcm_inj
Proof 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
Proof state after:
no goals
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
⊢ Complex.abs (↑x.1 * (↑x.2 * I).exp) = Complex.abs (↑y.1 * (↑y.2 * I).exp)
Tactic:
rw [e]
Proof state after:
no goals
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)
⊢ 0 < x.1
Tactic:
linarith
Proof state after:
no goals
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
⊢ 0 < y.1
Tactic:
linarith
Proof state after:
no goals
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
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]
Proof state after:
no goals
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 * π
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
Proof state after:
no goals
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 * π
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
Proof state after:
no goals
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 * π
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]
Proof state after:
no goals
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 * π
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
Proof state after:
no goals
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 * π
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
Proof state after:
no goals
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 * π
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
Proof state after:
no goals
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 * π
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
Proof state after:
no goals
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 * π
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]
Proof state after:
no goals
Theorem: measurable_symm_equiv_inverse
Proof state before:
z : ℂ
⊢ Complex.measurableEquivRealProd.symm (Complex.equivRealProd z) = z
Tactic:
simp only [Complex.equivRealProd_apply]
Proof state after:
z : ℂ
⊢ Complex.measurableEquivRealProd.symm (z.re, z.im) = z
Theorem: measurable_symm_equiv_inverse
Proof state before:
z : ℂ
⊢ Complex.measurableEquivRealProd.symm (z.re, z.im) = z
Tactic:
rw [Complex.measurableEquivRealProd, Homeomorph.toMeasurableEquiv_symm_coe]
Proof state after:
z : ℂ
⊢ Complex.equivRealProdCLM.toHomeomorph.symm (z.re, z.im) = z
Theorem: measurable_symm_equiv_inverse
Proof state before:
z : ℂ
⊢ Complex.equivRealProdCLM.toHomeomorph.symm (z.re, z.im) = z
Tactic:
simp only [ContinuousLinearEquiv.symm_toHomeomorph, ContinuousLinearEquiv.coe_toHomeomorph]
Proof state after:
z : ℂ
⊢ Complex.equivRealProdCLM.symm (z.re, z.im) = z
Theorem: measurable_symm_equiv_inverse
Proof state before:
z : ℂ
⊢ Complex.equivRealProdCLM.symm (z.re, z.im) = z
Tactic:
apply Complex.ext
Proof state after:
case a
z : ℂ
⊢ (Complex.equivRealProdCLM.symm (z.re, z.im)).re = z.re

case a
z : ℂ
⊢ (Complex.equivRealProdCLM.symm (z.re, z.im)).im = z.im
Theorem: measurable_symm_equiv_inverse
Proof state before:
case a
z : ℂ
⊢ (Complex.equivRealProdCLM.symm (z.re, z.im)).re = z.re
Tactic:
simp only [Complex.equivRealProdCLM_symm_apply_re]
Proof state after:
no goals
Theorem: measurable_symm_equiv_inverse
Proof state before:
case a
z : ℂ
⊢ (Complex.equivRealProdCLM.symm (z.re, z.im)).im = z.im
Tactic:
simp only [Complex.equivRealProdCLM_symm_apply_im]
Proof state after:
no goals
Theorem: continuous_circleMap_full
Proof state before:
c : ℂ
⊢ Continuous fun x => circleMap c x.1 x.2
Tactic:
continuity
Proof state after:
no goals
Theorem: invert_toReal
Proof state before:
x : ENNReal
y : ℝ
yp : y > 0
⊢ x.toReal = y → x = ENNReal.ofReal y
Tactic:
intro h
Proof state after:
x : ENNReal
y : ℝ
yp : y > 0
h : x.toReal = y
⊢ x = ENNReal.ofReal y
Theorem: invert_toReal
Proof state before:
x : ENNReal
y : ℝ
yp : y > 0
h : x.toReal = y
⊢ x = ENNReal.ofReal y
Tactic:
rw [← h]
Proof state after:
x : ENNReal
y : ℝ
yp : y > 0
h : x.toReal = y
⊢ x = ENNReal.ofReal x.toReal