Theorem: ℤα.self_sub_round_sq (Mordell4/Rt7Ring.lean)

State before:
a b c : ℤα
x : ℝ
⊢ (x - ↑(round x)) ^ 2 ≤ 2⁻¹ ^ 2
Tactic:
rw [sq_le_sq]
State after:
a b c : ℤα
x : ℝ
⊢ |x - ↑(round x)| ≤ |2⁻¹|

State before:
a b c : ℤα
x : ℝ
⊢ |x - ↑(round x)| ≤ |2⁻¹|
Tactic:
have bound := abs_sub_round x
State after:
a b c : ℤα
x : ℝ
bound : |x - ↑(round x)| ≤ 1 / 2
⊢ |x - ↑(round x)| ≤ |2⁻¹|

State before:
a b c : ℤα
x : ℝ
bound : |x - ↑(round x)| ≤ 1 / 2
⊢ |x - ↑(round x)| ≤ |2⁻¹|
Tactic:
have : |(2⁻¹ : ℝ)| = 1 / 2 := by
  simp only [one_div, abs_eq_self, inv_nonneg, zero_le_bit0, zero_le_one]
  norm_num
State after:
a b c : ℤα
x : ℝ
bound : |x - ↑(round x)| ≤ 1 / 2
this : |2⁻¹| = 1 / 2
⊢ |x - ↑(round x)| ≤ |2⁻¹|

State before:
a b c : ℤα
x : ℝ
bound : |x - ↑(round x)| ≤ 1 / 2
this : |2⁻¹| = 1 / 2
⊢ |x - ↑(round x)| ≤ |2⁻¹|
Tactic:
rwa [this]
State after:
no goals

State before:
a b c : ℤα
x : ℝ
bound : |x - ↑(round x)| ≤ 1 / 2
⊢ |2⁻¹| = 1 / 2
Tactic:
simp only [one_div, abs_eq_self, inv_nonneg, zero_le_bit0, zero_le_one]
State after:
a b c : ℤα
x : ℝ
bound : |x - ↑(round x)| ≤ 1 / 2
⊢ 0 ≤ 2

State before:
a b c : ℤα
x : ℝ
bound : |x - ↑(round x)| ≤ 1 / 2
⊢ 0 ≤ 2
Tactic:
norm_num
State after:
no goals