Theorem: ℤω.norm_sub_nearestℤω_self_lt (Mordell4/Eisenstein.lean)

State before:
a b c : ℤω
z : ℂ
⊢ ↑normSq (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)) < 1
Tactic:
have hre := re_sub_nearest z
State after:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
⊢ ↑normSq (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)) < 1

State before:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
⊢ ↑normSq (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)) < 1
Tactic:
have him := im_sub_nearest z
State after:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
⊢ ↑normSq (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)) < 1

State before:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
⊢ ↑normSq (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)) < 1
Tactic:
unfold normSq
State after:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
⊢ ↑{ toZeroHom := { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1 },
          map_one' := normSq.proof_2, map_mul' := normSq.proof_3 }
      (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)) <
    1

State before:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
⊢ ↑{ toZeroHom := { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1 },
          map_one' := normSq.proof_2, map_mul' := normSq.proof_3 }
      (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)) <
    1
Tactic:
dsimp
State after:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
⊢ (z.re - (↑inclusion (nearestℤω z)).re) * (z.re - (↑inclusion (nearestℤω z)).re) +
      (z.im - (↑inclusion (nearestℤω z)).im) * (z.im - (↑inclusion (nearestℤω z)).im) <
    1

State before:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
⊢ (z.re - (↑inclusion (nearestℤω z)).re) * (z.re - (↑inclusion (nearestℤω z)).re) +
      (z.im - (↑inclusion (nearestℤω z)).im) * (z.im - (↑inclusion (nearestℤω z)).im) <
    1
Tactic:
simp only [← pow_two]
State after:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1

State before:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1
Tactic:
have arith : (2 : ℝ)⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2 < 1 :=
  by
  ring_nf
  simp only [one_div, rt3_sq]
  norm_num
State after:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
arith : 2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2 < 1
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1

State before:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
arith : 2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2 < 1
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1
Tactic:
have near := add_le_add hre him
State after:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
arith : 2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2 < 1
near :
  (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 + (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤
    2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1

State before:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
arith : 2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2 < 1
near :
  (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 + (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤
    2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1
Tactic:
have := lt_of_le_of_lt near arith
State after:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
arith : 2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2 < 1
near :
  (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 + (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤
    2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2
this : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 + (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 < 1
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1

State before:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
arith : 2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2 < 1
near :
  (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 + (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤
    2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2
this : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 + (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 < 1
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1
Tactic:
clear near arith hre him
State after:
a b c : ℤω
z : ℂ
this : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 + (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 < 1
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1

State before:
a b c : ℤω
z : ℂ
this : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 + (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 < 1
⊢ (z.re - (↑inclusion (nearestℤω z)).re) ^ 2 + (z.im - (↑inclusion (nearestℤω z)).im) ^ 2 < 1
Tactic:
rwa [sub_re, sub_im] at this
State after:
no goals

State before:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
⊢ 2⁻¹ ^ 2 + (4⁻¹ * rt3) ^ 2 < 1
Tactic:
ring_nf
State after:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
⊢ ↑(ofNat 1) / ↑4 + rt3 ^ 2 * (↑(ofNat 1) / ↑16) < 1

State before:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
⊢ ↑(ofNat 1) / ↑4 + rt3 ^ 2 * (↑(ofNat 1) / ↑16) < 1
Tactic:
simp only [one_div, rt3_sq]
State after:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
⊢ ↑(ofNat 1) / ↑4 + 3 * (↑(ofNat 1) / ↑16) < 1

State before:
a b c : ℤω
z : ℂ
hre : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).re ^ 2 ≤ 2⁻¹ ^ 2
him : (z - OneHom.toFun (↑↑inclusion) (nearestℤω z)).im ^ 2 ≤ (4⁻¹ * rt3) ^ 2
⊢ ↑(ofNat 1) / ↑4 + 3 * (↑(ofNat 1) / ↑16) < 1
Tactic:
norm_num
State after:
no goals