Theorem: float_greatest_e_exists (HOLFloat/Float_theorem.lean)

State before:
fmt : flformat
x : ℝ
e : ℤ
⊢ x ≠ 0 → e = greatest_e fmt x → is_greatest_e fmt x e
Tactic:
have ⟨fmt_val, FMT⟩ := fmt
State after:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
⊢ x ≠ 0 → e = greatest_e { val := fmt_val, property := FMT } x → is_greatest_e { val := fmt_val, property := FMT } x e

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
⊢ x ≠ 0 → e = greatest_e { val := fmt_val, property := FMT } x → is_greatest_e { val := fmt_val, property := FMT } x e
Tactic:
intro hx he
State after:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = greatest_e { val := fmt_val, property := FMT } x
⊢ is_greatest_e { val := fmt_val, property := FMT } x e

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = greatest_e { val := fmt_val, property := FMT } x
⊢ is_greatest_e { val := fmt_val, property := FMT } x e
Tactic:
simp only [greatest_e, is_greatest_e] at *
State after:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ ↑fmt_val.r ^ e ≤ abs x ∧ ∀ (e' : ℤ), ↑fmt_val.r ^ e' ≤ abs x → e' ≤ e

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ ↑fmt_val.r ^ e ≤ abs x ∧ ∀ (e' : ℤ), ↑fmt_val.r ^ e' ≤ abs x → e' ≤ e
Tactic:
apply And.intro
State after:
case left
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ ↑fmt_val.r ^ e ≤ abs x

case right
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ ∀ (e' : ℤ), ↑fmt_val.r ^ e' ≤ abs x → e' ≤ e

State before:
case left
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ ↑fmt_val.r ^ e ≤ abs x

case right
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ ∀ (e' : ℤ), ↑fmt_val.r ^ e' ≤ abs x → e' ≤ e
Tactic:
have R_GT_1 : 1 < fmt_val.r := FMT.left
State after:
case left
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ ↑fmt_val.r ^ e ≤ abs x

case right
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ ∀ (e' : ℤ), ↑fmt_val.r ^ e' ≤ abs x → e' ≤ e

State before:
case left
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ ↑fmt_val.r ^ e ≤ abs x

case right
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ ∀ (e' : ℤ), ↑fmt_val.r ^ e' ≤ abs x → e' ≤ e
Tactic:
suffices e ∈  { z : ℤ | (fmt_val.r : ℝ) ^ z ≤ abs x } by {
  have H := this.out;
  have R_GT_1 : 1 < fmt_val.r := FMT.left;
  norm_cast at H;
}
State after:
case left
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ e ∈ { z | ↑fmt_val.r ^ z ≤ abs x }

case right
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ ∀ (e' : ℤ), ↑fmt_val.r ^ e' ≤ abs x → e' ≤ e

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ e ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
Tactic:
case left =>
  norm_cast
  rw[he];
  apply Int.csupₛ_mem;
  case h1 => {
   
    simp[Set.Nonempty];
    apply pow_le_real
    norm_cast
    aesop_subst he
    simp_all only [ne_eq, Int.one_lt_zero_le_iff, Int.one_lt_ne_one, not_false_iff]
    aesop_subst he
    simp_all only [ne_eq, Int.one_lt_zero_le_iff, not_false_iff]
  }
  case h2 => {
    simp [BddAbove]
    simp [Set.Nonempty]
    simp [upperBounds]
    existsi e
    intro a ha
    have hpa : a ∈ {z : ℤ | (fmt_val.r : ℝ) ^ z ≤ |x| } → a ≤ e := by
      simp
      norm_cast at *
      intro A_IN_SET
      sorry
    aesop_subst he
    simp_all only [ne_eq, Int.one_lt_zero_le_iff, Int.cast_eq_zero, Set.mem_setOf_eq, forall_true_left]
  }
State after:
no goals

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ ∀ (e' : ℤ), ↑fmt_val.r ^ e' ≤ abs x → e' ≤ e
Tactic:
case right =>
  intro e1 hp
  aesop_subst he
  have he1: e1 ∈ { z | (fmt_val.r: ℝ) ^ z ≤ abs x } :=  by
    simp_all only [ne_eq, Int.cast_eq_zero, Set.mem_setOf_eq]
  apply le_csupₛ
  case h₂ =>
    simp_all only [ne_eq, Int.cast_eq_zero, Set.mem_setOf_eq]
  case h₁ =>
    sorry
State after:
no goals

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
this : e ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ ↑fmt_val.r ^ e ≤ abs x
Tactic:
have H := this.out
State after:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
this : e ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
H : ↑fmt_val.r ^ e ≤ abs x
⊢ ↑fmt_val.r ^ e ≤ abs x

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
this : e ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
H : ↑fmt_val.r ^ e ≤ abs x
⊢ ↑fmt_val.r ^ e ≤ abs x
Tactic:
have R_GT_1 : 1 < fmt_val.r := FMT.left
State after:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1✝ : 1 < fmt_val.r
this : e ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
H : ↑fmt_val.r ^ e ≤ abs x
R_GT_1 : 1 < fmt_val.r
⊢ ↑fmt_val.r ^ e ≤ abs x

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1✝ : 1 < fmt_val.r
this : e ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
H : ↑fmt_val.r ^ e ≤ abs x
R_GT_1 : 1 < fmt_val.r
⊢ ↑fmt_val.r ^ e ≤ abs x
Tactic:
norm_cast at H
State after:
no goals

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ e ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
Tactic:
rw[he]
State after:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ supₛ { z | ↑fmt_val.r ^ z ≤ abs x } ∈ { z | ↑fmt_val.r ^ z ≤ abs x }

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ supₛ { z | ↑fmt_val.r ^ z ≤ abs x } ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
Tactic:
apply Int.csupₛ_mem
State after:
case h1
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ Set.Nonempty { z | ↑fmt_val.r ^ z ≤ abs x }

case h2
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ BddAbove { z | ↑fmt_val.r ^ z ≤ abs x }

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ Set.Nonempty { z | ↑fmt_val.r ^ z ≤ abs x }
Tactic:
case h1 => {
 
  simp[Set.Nonempty];
  apply pow_le_real
  norm_cast
  aesop_subst he
  simp_all only [ne_eq, Int.one_lt_zero_le_iff, Int.one_lt_ne_one, not_false_iff]
  aesop_subst he
  simp_all only [ne_eq, Int.one_lt_zero_le_iff, not_false_iff]
}
State after:
no goals

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ BddAbove { z | ↑fmt_val.r ^ z ≤ abs x }
Tactic:
case h2 => {
  simp [BddAbove]
  simp [Set.Nonempty]
  simp [upperBounds]
  existsi e
  intro a ha
  have hpa : a ∈ {z : ℤ | (fmt_val.r : ℝ) ^ z ≤ |x| } → a ≤ e := by
    simp
    norm_cast at *
    intro A_IN_SET
    sorry
  aesop_subst he
  simp_all only [ne_eq, Int.one_lt_zero_le_iff, Int.cast_eq_zero, Set.mem_setOf_eq, forall_true_left]
}
State after:
no goals

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ Set.Nonempty { z | ↑fmt_val.r ^ z ≤ abs x }
Tactic:
simp[Set.Nonempty]
State after:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ ∃ z, ↑fmt_val.r ^ z ≤ abs x

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ ∃ z, ↑fmt_val.r ^ z ≤ abs x
Tactic:
apply pow_le_real
State after:
case ha1
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ ↑fmt_val.r ≠ 1

case hx0
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ x ≠ 0

State before:
case ha1
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ ↑fmt_val.r ≠ 1

case hx0
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ x ≠ 0
Tactic:
norm_cast
State after:
case ha1
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ ¬fmt_val.r = 1

case hx0
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ x ≠ 0

State before:
case ha1
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ ¬fmt_val.r = 1

case hx0
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ x ≠ 0
Tactic:
aesop_subst he
State after:
case ha1
fmt : flformat
x : ℝ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
R_GT_1 : 1 < fmt_val.r
⊢ ¬fmt_val.r = 1

case hx0
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ x ≠ 0

State before:
case ha1
fmt : flformat
x : ℝ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
R_GT_1 : 1 < fmt_val.r
⊢ ¬fmt_val.r = 1

case hx0
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ x ≠ 0
Tactic:
simp_all only [ne_eq, Int.one_lt_zero_le_iff, Int.one_lt_ne_one, not_false_iff]
State after:
case hx0
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ x ≠ 0

State before:
case hx0
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ x ≠ 0
Tactic:
aesop_subst he
State after:
case hx0
fmt : flformat
x : ℝ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
R_GT_1 : 1 < fmt_val.r
⊢ x ≠ 0

State before:
case hx0
fmt : flformat
x : ℝ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
R_GT_1 : 1 < fmt_val.r
⊢ x ≠ 0
Tactic:
simp_all only [ne_eq, Int.one_lt_zero_le_iff, not_false_iff]
State after:
no goals

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ BddAbove { z | ↑fmt_val.r ^ z ≤ abs x }
Tactic:
simp [BddAbove]
State after:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ Set.Nonempty (upperBounds { z | ↑fmt_val.r ^ z ≤ abs x })

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ Set.Nonempty (upperBounds { z | ↑fmt_val.r ^ z ≤ abs x })
Tactic:
simp [Set.Nonempty]
State after:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ ∃ x_1, x_1 ∈ upperBounds { z | ↑fmt_val.r ^ z ≤ abs x }

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ ∃ x_1, x_1 ∈ upperBounds { z | ↑fmt_val.r ^ z ≤ abs x }
Tactic:
simp [upperBounds]
State after:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ ∃ x_1, ∀ ⦃a : ℤ⦄, ↑fmt_val.r ^ a ≤ abs x → a ≤ x_1

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ ∃ x_1, ∀ ⦃a : ℤ⦄, ↑fmt_val.r ^ a ≤ abs x → a ≤ x_1
Tactic:
existsi e
State after:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ ∀ ⦃a : ℤ⦄, ↑fmt_val.r ^ a ≤ abs x → a ≤ e

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
⊢ ∀ ⦃a : ℤ⦄, ↑fmt_val.r ^ a ≤ abs x → a ≤ e
Tactic:
intro a ha
State after:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
a : ℤ
ha : ↑fmt_val.r ^ a ≤ abs x
⊢ a ≤ e

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
a : ℤ
ha : ↑fmt_val.r ^ a ≤ abs x
⊢ a ≤ e
Tactic:
have hpa : a ∈ {z : ℤ | (fmt_val.r : ℝ) ^ z ≤ |x| } → a ≤ e := by
  simp
  norm_cast at *
  intro A_IN_SET
  sorry
State after:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
a : ℤ
ha : ↑fmt_val.r ^ a ≤ abs x
hpa : a ∈ { z | ↑fmt_val.r ^ z ≤ abs x } → a ≤ e
⊢ a ≤ e

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
a : ℤ
ha : ↑fmt_val.r ^ a ≤ abs x
hpa : a ∈ { z | ↑fmt_val.r ^ z ≤ abs x } → a ≤ e
⊢ a ≤ e
Tactic:
aesop_subst he
State after:
fmt : flformat
x : ℝ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
R_GT_1 : 1 < fmt_val.r
a : ℤ
ha : ↑fmt_val.r ^ a ≤ abs x
hpa : a ∈ { z | ↑fmt_val.r ^ z ≤ abs x } → a ≤ supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ a ≤ supₛ { z | ↑fmt_val.r ^ z ≤ abs x }

State before:
fmt : flformat
x : ℝ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
R_GT_1 : 1 < fmt_val.r
a : ℤ
ha : ↑fmt_val.r ^ a ≤ abs x
hpa : a ∈ { z | ↑fmt_val.r ^ z ≤ abs x } → a ≤ supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ a ≤ supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
Tactic:
simp_all only [ne_eq, Int.one_lt_zero_le_iff, Int.cast_eq_zero, Set.mem_setOf_eq, forall_true_left]
State after:
no goals

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
a : ℤ
ha : ↑fmt_val.r ^ a ≤ abs x
⊢ a ∈ { z | ↑fmt_val.r ^ z ≤ abs x } → a ≤ e
Tactic:
simp
State after:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
a : ℤ
ha : ↑fmt_val.r ^ a ≤ abs x
⊢ ↑fmt_val.r ^ a ≤ abs x → a ≤ e

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
R_GT_1 : 1 < fmt_val.r
a : ℤ
ha : ↑fmt_val.r ^ a ≤ abs x
⊢ ↑fmt_val.r ^ a ≤ abs x → a ≤ e
Tactic:
norm_cast at *
State after:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
a : ℤ
ha : ↑fmt_val.r ^ a ≤ abs x
hx : ¬x = 0
R_GT_1 : 1 < fmt_val.r
⊢ ↑fmt_val.r ^ a ≤ abs x → a ≤ e

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
a : ℤ
ha : ↑fmt_val.r ^ a ≤ abs x
hx : ¬x = 0
R_GT_1 : 1 < fmt_val.r
⊢ ↑fmt_val.r ^ a ≤ abs x → a ≤ e
Tactic:
intro A_IN_SET
State after:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
a : ℤ
ha : ↑fmt_val.r ^ a ≤ abs x
hx : ¬x = 0
R_GT_1 : 1 < fmt_val.r
A_IN_SET : ↑fmt_val.r ^ a ≤ abs x
⊢ a ≤ e

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
a : ℤ
ha : ↑fmt_val.r ^ a ≤ abs x
hx : ¬x = 0
R_GT_1 : 1 < fmt_val.r
A_IN_SET : ↑fmt_val.r ^ a ≤ abs x
⊢ a ≤ e
Tactic:
sorry
State after:
no goals

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ ∀ (e' : ℤ), ↑fmt_val.r ^ e' ≤ abs x → e' ≤ e
Tactic:
intro e1 hp
State after:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
e1 : ℤ
hp : ↑fmt_val.r ^ e1 ≤ abs x
⊢ e1 ≤ e

State before:
fmt : flformat
x : ℝ
e : ℤ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
he : e = supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
e1 : ℤ
hp : ↑fmt_val.r ^ e1 ≤ abs x
⊢ e1 ≤ e
Tactic:
aesop_subst he
State after:
fmt : flformat
x : ℝ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
e1 : ℤ
hp : ↑fmt_val.r ^ e1 ≤ abs x
⊢ e1 ≤ supₛ { z | ↑fmt_val.r ^ z ≤ abs x }

State before:
fmt : flformat
x : ℝ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
e1 : ℤ
hp : ↑fmt_val.r ^ e1 ≤ abs x
⊢ e1 ≤ supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
Tactic:
have he1: e1 ∈ { z | (fmt_val.r: ℝ) ^ z ≤ abs x } :=  by
  simp_all only [ne_eq, Int.cast_eq_zero, Set.mem_setOf_eq]
State after:
fmt : flformat
x : ℝ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
e1 : ℤ
hp : ↑fmt_val.r ^ e1 ≤ abs x
he1 : e1 ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ e1 ≤ supₛ { z | ↑fmt_val.r ^ z ≤ abs x }

State before:
fmt : flformat
x : ℝ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
e1 : ℤ
hp : ↑fmt_val.r ^ e1 ≤ abs x
he1 : e1 ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ e1 ≤ supₛ { z | ↑fmt_val.r ^ z ≤ abs x }
Tactic:
apply le_csupₛ
State after:
case h₁
fmt : flformat
x : ℝ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
e1 : ℤ
hp : ↑fmt_val.r ^ e1 ≤ abs x
he1 : e1 ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ BddAbove { z | ↑fmt_val.r ^ z ≤ abs x }

case h₂
fmt : flformat
x : ℝ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
e1 : ℤ
hp : ↑fmt_val.r ^ e1 ≤ abs x
he1 : e1 ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ e1 ∈ { z | ↑fmt_val.r ^ z ≤ abs x }

State before:
fmt : flformat
x : ℝ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
e1 : ℤ
hp : ↑fmt_val.r ^ e1 ≤ abs x
he1 : e1 ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ e1 ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
Tactic:
case h₂ =>
  simp_all only [ne_eq, Int.cast_eq_zero, Set.mem_setOf_eq]
State after:
no goals

State before:
fmt : flformat
x : ℝ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
e1 : ℤ
hp : ↑fmt_val.r ^ e1 ≤ abs x
he1 : e1 ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ BddAbove { z | ↑fmt_val.r ^ z ≤ abs x }
Tactic:
case h₁ =>
  sorry
State after:
no goals

State before:
fmt : flformat
x : ℝ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
e1 : ℤ
hp : ↑fmt_val.r ^ e1 ≤ abs x
⊢ e1 ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
Tactic:
simp_all only [ne_eq, Int.cast_eq_zero, Set.mem_setOf_eq]
State after:
no goals

State before:
fmt : flformat
x : ℝ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
e1 : ℤ
hp : ↑fmt_val.r ^ e1 ≤ abs x
he1 : e1 ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ e1 ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
Tactic:
simp_all only [ne_eq, Int.cast_eq_zero, Set.mem_setOf_eq]
State after:
no goals

State before:
fmt : flformat
x : ℝ
fmt_val : format
FMT : is_valid_flformat fmt_val
hx : x ≠ 0
e1 : ℤ
hp : ↑fmt_val.r ^ e1 ≤ abs x
he1 : e1 ∈ { z | ↑fmt_val.r ^ z ≤ abs x }
⊢ BddAbove { z | ↑fmt_val.r ^ z ≤ abs x }
Tactic:
sorry
State after:
no goals