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

State before:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Tactic:
have hc : c * c⁻¹ = 1 := by
  apply mul_inv_cancel
  exact ne_of_gt c_pos
State after:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c

State before:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Tactic:
have h_abs_c : |c| = c := abs_of_pos c_pos
State after:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c

State before:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Tactic:
have := abs_mul (c⁻¹ * x - round (c⁻¹ * x)) c
State after:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |(c⁻¹ * x - ↑(round (c⁻¹ * x))) * c| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c

State before:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |(c⁻¹ * x - ↑(round (c⁻¹ * x))) * c| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Tactic:
rw [sub_mul] at this
State after:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c⁻¹ * x * c - ↑(round (c⁻¹ * x)) * c| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c

State before:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c⁻¹ * x * c - ↑(round (c⁻¹ * x)) * c| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Tactic:
rw [mul_comm] at this
State after:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c * (c⁻¹ * x) - ↑(round (c⁻¹ * x)) * c| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c

State before:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c * (c⁻¹ * x) - ↑(round (c⁻¹ * x)) * c| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Tactic:
rw [← mul_assoc] at this
State after:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c * c⁻¹ * x - ↑(round (c⁻¹ * x)) * c| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c

State before:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c * c⁻¹ * x - ↑(round (c⁻¹ * x)) * c| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Tactic:
rw [hc, one_mul, mul_comm] at this
State after:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |x - c * ↑(round (c⁻¹ * x))| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c

State before:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |x - c * ↑(round (c⁻¹ * x))| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |x - c * ↑(round (c⁻¹ * x))| ≤ 2⁻¹ * c
Tactic:
rw [this]
State after:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |x - c * ↑(round (c⁻¹ * x))| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c| ≤ 2⁻¹ * c

State before:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |x - c * ↑(round (c⁻¹ * x))| = |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c|
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c| ≤ 2⁻¹ * c
Tactic:
clear this
State after:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c| ≤ 2⁻¹ * c

State before:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c| ≤ 2⁻¹ * c
Tactic:
have := abs_sub_round (c⁻¹ * x)
State after:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c⁻¹ * x - ↑(round (c⁻¹ * x))| ≤ 1 / 2
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c| ≤ 2⁻¹ * c

State before:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c⁻¹ * x - ↑(round (c⁻¹ * x))| ≤ 1 / 2
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| * |c| ≤ 2⁻¹ * c
Tactic:
rw [h_abs_c]
State after:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c⁻¹ * x - ↑(round (c⁻¹ * x))| ≤ 1 / 2
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| * c ≤ 2⁻¹ * c

State before:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c⁻¹ * x - ↑(round (c⁻¹ * x))| ≤ 1 / 2
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| * c ≤ 2⁻¹ * c
Tactic:
rw [mul_le_mul_right c_pos]
State after:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c⁻¹ * x - ↑(round (c⁻¹ * x))| ≤ 1 / 2
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| ≤ 2⁻¹

State before:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
hc : c * c⁻¹ = 1
h_abs_c : |c| = c
this : |c⁻¹ * x - ↑(round (c⁻¹ * x))| ≤ 1 / 2
⊢ |c⁻¹ * x - ↑(round (c⁻¹ * x))| ≤ 2⁻¹
Tactic:
rwa [one_div] at this
State after:
no goals

State before:
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
⊢ c * c⁻¹ = 1
Tactic:
apply mul_inv_cancel
State after:
case h
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
⊢ c ≠ 0

State before:
case h
a b c✝ : ℤα
c x : ℝ
c_pos : c > 0
⊢ c ≠ 0
Tactic:
exact ne_of_gt c_pos
State after:
no goals