Theorem: float_eq_ipow (HOLFloat/Float_theorem.lean)

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
⊢ x ≠ 0 → 1 ≤ m → m < ↑(↑fmt).r → abs x = m * ↑(↑fmt).r ^ e → greatest_e fmt x = e ∧ greatest_m fmt x = m
Tactic:
intros hx hm hr he
State after:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ greatest_e fmt x = e ∧ greatest_m fmt x = m

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ greatest_e fmt x = e ∧ greatest_m fmt x = m
Tactic:
apply And.intro
State after:
case left
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ greatest_e fmt x = e

case right
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ greatest_m fmt x = m

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ greatest_e fmt x = e
Tactic:
case left =>
  rw [greatest_e]
  norm_cast
  simp only [he]
  have H : e ∈ {z : ℤ | (fmt.val.r : ℝ) ^ z ≤ abs x} := by
    rw [he]
    simp [float_real_le_1_le]
    norm_cast
  have H₁: ∀k, k ∈ {z : ℤ | (fmt.val.r : ℝ) ^ z ≤ abs x} → k ≥ e := by
    intro k hk
    rw [he] at hk
    simp_all [float_real_le_1_le]
    norm_cast
    have R_REAL_GT_1: 1 <(fmt.val.r :ℝ) := by
      simp_all only [lt_self_iff_false, ne_eq, Int.one_lt_zero_le_iff, Int.cast_lt_zero, Int.cast_eq_zero, Set.mem_setOf_eq,
      gt_iff_lt, float_radix_ipow_lt_0, le_mul_iff_one_le_left, ge_iff_le, flformat_radix_lt_1_real]
    apply ipow_monotone_le_pow  R_REAL_GT_1
    sorry
State after:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
H : e ∈ { z | ↑(↑fmt).r ^ z ≤ abs x }
H₁ : ∀ (k : ℤ), k ∈ { z | ↑(↑fmt).r ^ z ≤ abs x } → k ≥ e
⊢ supₛ { z | ↑(↑fmt).r ^ z ≤ m * ↑(↑fmt).r ^ e } = e

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ greatest_m fmt x = m
Tactic:
case right =>
  rw [greatest_m]
  sorry
State after:
no goals

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ greatest_e fmt x = e
Tactic:
rw [greatest_e]
State after:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ supₛ { z | ↑(↑fmt).r ^ z ≤ abs x } = e

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ supₛ { z | ↑(↑fmt).r ^ z ≤ abs x } = e
Tactic:
simp only [he]
State after:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ supₛ { z | ↑(↑fmt).r ^ z ≤ m * ↑(↑fmt).r ^ e } = e

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ supₛ { z | ↑(↑fmt).r ^ z ≤ m * ↑(↑fmt).r ^ e } = e
Tactic:
have H : e ∈ {z : ℤ | (fmt.val.r : ℝ) ^ z ≤ abs x} := by
  rw [he]
  simp [float_real_le_1_le]
  norm_cast
State after:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
H : e ∈ { z | ↑(↑fmt).r ^ z ≤ abs x }
⊢ supₛ { z | ↑(↑fmt).r ^ z ≤ m * ↑(↑fmt).r ^ e } = e

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
H : e ∈ { z | ↑(↑fmt).r ^ z ≤ abs x }
⊢ supₛ { z | ↑(↑fmt).r ^ z ≤ m * ↑(↑fmt).r ^ e } = e
Tactic:
have H₁: ∀k, k ∈ {z : ℤ | (fmt.val.r : ℝ) ^ z ≤ abs x} → k ≥ e := by
  intro k hk
  rw [he] at hk
  simp_all [float_real_le_1_le]
  norm_cast
  have R_REAL_GT_1: 1 <(fmt.val.r :ℝ) := by
    simp_all only [lt_self_iff_false, ne_eq, Int.one_lt_zero_le_iff, Int.cast_lt_zero, Int.cast_eq_zero, Set.mem_setOf_eq,
    gt_iff_lt, float_radix_ipow_lt_0, le_mul_iff_one_le_left, ge_iff_le, flformat_radix_lt_1_real]
  apply ipow_monotone_le_pow  R_REAL_GT_1
  sorry
State after:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
H : e ∈ { z | ↑(↑fmt).r ^ z ≤ abs x }
H₁ : ∀ (k : ℤ), k ∈ { z | ↑(↑fmt).r ^ z ≤ abs x } → k ≥ e
⊢ supₛ { z | ↑(↑fmt).r ^ z ≤ m * ↑(↑fmt).r ^ e } = e

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ e ∈ { z | ↑(↑fmt).r ^ z ≤ abs x }
Tactic:
rw [he]
State after:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ e ∈ { z | ↑(↑fmt).r ^ z ≤ m * ↑(↑fmt).r ^ e }

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ e ∈ { z | ↑(↑fmt).r ^ z ≤ m * ↑(↑fmt).r ^ e }
Tactic:
simp [float_real_le_1_le]
State after:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ 1 ≤ m

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ 1 ≤ m
Tactic:
norm_cast
State after:
no goals

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
H : e ∈ { z | ↑(↑fmt).r ^ z ≤ abs x }
⊢ ∀ (k : ℤ), k ∈ { z | ↑(↑fmt).r ^ z ≤ abs x } → k ≥ e
Tactic:
intro k hk
State after:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
H : e ∈ { z | ↑(↑fmt).r ^ z ≤ abs x }
k : ℤ
hk : k ∈ { z | ↑(↑fmt).r ^ z ≤ abs x }
⊢ k ≥ e

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
H : e ∈ { z | ↑(↑fmt).r ^ z ≤ abs x }
k : ℤ
hk : k ∈ { z | ↑(↑fmt).r ^ z ≤ abs x }
⊢ k ≥ e
Tactic:
rw [he] at hk
State after:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
H : e ∈ { z | ↑(↑fmt).r ^ z ≤ abs x }
k : ℤ
hk : k ∈ { z | ↑(↑fmt).r ^ z ≤ m * ↑(↑fmt).r ^ e }
⊢ k ≥ e

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
H : e ∈ { z | ↑(↑fmt).r ^ z ≤ abs x }
k : ℤ
hk : k ∈ { z | ↑(↑fmt).r ^ z ≤ m * ↑(↑fmt).r ^ e }
⊢ k ≥ e
Tactic:
simp_all [float_real_le_1_le]
State after:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
k : ℤ
hx : ¬x = 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
hk : ↑(↑fmt).r ^ k ≤ m * ↑(↑fmt).r ^ e
⊢ e ≤ k

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
k : ℤ
hx : ¬x = 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
hk : ↑(↑fmt).r ^ k ≤ m * ↑(↑fmt).r ^ e
⊢ e ≤ k
Tactic:
have R_REAL_GT_1: 1 <(fmt.val.r :ℝ) := by
  simp_all only [lt_self_iff_false, ne_eq, Int.one_lt_zero_le_iff, Int.cast_lt_zero, Int.cast_eq_zero, Set.mem_setOf_eq,
  gt_iff_lt, float_radix_ipow_lt_0, le_mul_iff_one_le_left, ge_iff_le, flformat_radix_lt_1_real]
State after:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
k : ℤ
hx : ¬x = 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
hk : ↑(↑fmt).r ^ k ≤ m * ↑(↑fmt).r ^ e
R_REAL_GT_1 : 1 < ↑(↑fmt).r
⊢ e ≤ k

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
k : ℤ
hx : ¬x = 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
hk : ↑(↑fmt).r ^ k ≤ m * ↑(↑fmt).r ^ e
R_REAL_GT_1 : 1 < ↑(↑fmt).r
⊢ e ≤ k
Tactic:
apply ipow_monotone_le_pow  R_REAL_GT_1
State after:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
k : ℤ
hx : ¬x = 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
hk : ↑(↑fmt).r ^ k ≤ m * ↑(↑fmt).r ^ e
R_REAL_GT_1 : 1 < ↑(↑fmt).r
⊢ ↑(↑fmt).r ^ e ≤ ↑(↑fmt).r ^ k

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
k : ℤ
hx : ¬x = 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
hk : ↑(↑fmt).r ^ k ≤ m * ↑(↑fmt).r ^ e
R_REAL_GT_1 : 1 < ↑(↑fmt).r
⊢ ↑(↑fmt).r ^ e ≤ ↑(↑fmt).r ^ k
Tactic:
sorry
State after:
no goals

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
k : ℤ
hx : ¬x = 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
hk : ↑(↑fmt).r ^ k ≤ m * ↑(↑fmt).r ^ e
⊢ 1 < ↑(↑fmt).r
Tactic:
simp_all only [lt_self_iff_false, ne_eq, Int.one_lt_zero_le_iff, Int.cast_lt_zero, Int.cast_eq_zero, Set.mem_setOf_eq,
gt_iff_lt, float_radix_ipow_lt_0, le_mul_iff_one_le_left, ge_iff_le, flformat_radix_lt_1_real]
State after:
no goals

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ greatest_m fmt x = m
Tactic:
rw [greatest_m]
State after:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ supₛ { m | m * ↑((↑fmt).r ^ greatest_e fmt x) ≤ abs x } = m

State before:
fmt : flformat
x : ℝ
e : ℤ
m : ℝ
hx : x ≠ 0
hm : 1 ≤ m
hr : m < ↑(↑fmt).r
he : abs x = m * ↑(↑fmt).r ^ e
⊢ supₛ { m | m * ↑((↑fmt).r ^ greatest_e fmt x) ≤ abs x } = m
Tactic:
sorry
State after:
no goals