internlm/Lean-Github huggingface dataset:
Theorem: float_greatest_e_exists
Proof 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;
}
Proof 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
Theorem: float_greatest_e_exists
Proof 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]
  }
Proof state after:
no goals
Theorem: float_greatest_e_exists
Proof 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
Proof state after:
no goals
Theorem: float_greatest_e_exists
Proof 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
Proof 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
Theorem: float_greatest_e_exists
Proof 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
Proof 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
Theorem: float_greatest_e_exists
Proof 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
Proof state after:
no goals
Theorem: float_greatest_e_exists
Proof 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]
Proof 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 }
Theorem: float_greatest_e_exists
Proof 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
Proof 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 }
Theorem: float_greatest_e_exists
Proof 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]
}
Proof state after:
no goals
Theorem: float_greatest_e_exists
Proof 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]
}
Proof state after:
no goals
Theorem: float_greatest_e_exists
Proof 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]
Proof 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
Theorem: float_greatest_e_exists
Proof 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
Proof 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
Theorem: float_greatest_e_exists
Proof 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
Proof 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
Theorem: float_greatest_e_exists
Proof 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
Proof 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
Theorem: float_greatest_e_exists
Proof 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]
Proof 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
Theorem: float_greatest_e_exists
Proof 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
Proof 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
Theorem: float_greatest_e_exists
Proof 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]
Proof state after:
no goals
Theorem: float_greatest_e_exists
Proof 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]
Proof 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 })
Theorem: float_greatest_e_exists
Proof 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]
Proof 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 }
Theorem: float_greatest_e_exists
Proof 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]
Proof 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
Theorem: float_greatest_e_exists
Proof 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
Proof 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
Theorem: float_greatest_e_exists
Proof 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
Proof 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
Theorem: float_greatest_e_exists
Proof 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
Proof 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
Theorem: float_greatest_e_exists
Proof 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
Proof 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 }
Theorem: float_greatest_e_exists
Proof 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]
Proof state after:
no goals
Theorem: float_greatest_e_exists
Proof 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
Proof 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
Theorem: float_greatest_e_exists
Proof 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 *
Proof 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
Theorem: float_greatest_e_exists
Proof 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
Proof 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
Theorem: float_greatest_e_exists
Proof 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
Proof state after:
no goals
Theorem: float_greatest_e_exists
Proof 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
Proof 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
Theorem: float_greatest_e_exists
Proof 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
Proof 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 }
Theorem: float_greatest_e_exists
Proof 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]
Proof 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 }
Theorem: float_greatest_e_exists
Proof 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ₛ
Proof 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 }
Theorem: float_greatest_e_exists
Proof 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]
Proof state after:
no goals
Theorem: float_greatest_e_exists
Proof 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
Proof state after:
no goals
Theorem: float_greatest_e_exists
Proof 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]
Proof state after:
no goals
Theorem: float_greatest_e_exists
Proof 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]
Proof state after:
no goals
Theorem: float_greatest_e_exists
Proof 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
Proof state after:
no goals
Theorem: float_greatest_m_exists
Proof state before:
fmt : flformat
x : ℝ
m : ℤ
⊢ x ≠ 0 → greatest_m fmt x = ↑m → is_greatest_m fmt x m ∧ 1 ≤ m ∧ m < (↑fmt).r
Tactic:
sorry
Proof state after:
no goals
Theorem: is_greatest_e_exist_greatest_e
Proof state before:
x : ℝ
fmt : flformat
e : ℤ
⊢ x ≠ 0 → is_greatest_e fmt x e → greatest_e fmt x = e
Tactic:
intro hx he
Proof state after:
x : ℝ
fmt : flformat
e : ℤ
hx : x ≠ 0
he : is_greatest_e fmt x e
⊢ greatest_e fmt x = e
Theorem: is_greatest_e_exist_greatest_e
Proof state before:
x : ℝ
fmt : flformat
e : ℤ
hx : x ≠ 0
he : is_greatest_e fmt x e
⊢ greatest_e fmt x = e
Tactic:
simp_all only [is_greatest_e, greatest_e]
Proof state after:
x : ℝ
fmt : flformat
e : ℤ
hx : x ≠ 0
he : ↑(↑fmt).r ^ e ≤ abs x ∧ ∀ (e' : ℤ), ↑(↑fmt).r ^ e' ≤ abs x → e' ≤ e
⊢ supₛ { z | ↑(↑fmt).r ^ z ≤ abs x } = e
Theorem: is_greatest_e_exist_greatest_e
Proof state before:
x : ℝ
fmt : flformat
e : ℤ
hx : x ≠ 0
he : ↑(↑fmt).r ^ e ≤ abs x ∧ ∀ (e' : ℤ), ↑(↑fmt).r ^ e' ≤ abs x → e' ≤ e
⊢ supₛ { z | ↑(↑fmt).r ^ z ≤ abs x } = e
Tactic:
sorry
Proof state after:
no goals
Theorem: float_normalize_real
Proof state before:
fmt : flformat
x : ℝ
⊢ x < 0 → x = greatest_m fmt x * ↑(↑fmt).r ^ greatest_e fmt x + greatest_r fmt x
Tactic:
intro h
Proof state after:
fmt : flformat
x : ℝ
h : x < 0
⊢ x = greatest_m fmt x * ↑(↑fmt).r ^ greatest_e fmt x + greatest_r fmt x
Theorem: float_normalize_real
Proof state before:
fmt : flformat
x : ℝ
h : x < 0
⊢ x = greatest_m fmt x * ↑(↑fmt).r ^ greatest_e fmt x + greatest_r fmt x
Tactic:
sorry
Proof state after:
no goals
Theorem: float_pow_int_eq_le
Proof state before:
r : ℤ
x : ℝ
m e : ℤ
⊢ x ≠ 0 → 1 ≤ m → abs x = ↑m * ↑r ^ e → ↑r ^ e ≤ abs x
Tactic:
intro hx hm he
Proof state after:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ ↑r ^ e ≤ abs x
Theorem: float_pow_int_eq_le
Proof state before:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ ↑r ^ e ≤ abs x
Tactic:
rw [he]
Proof state after:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ ↑r ^ e ≤ ↑m * ↑r ^ e
Theorem: float_pow_int_eq_le
Proof state before:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ ↑r ^ e ≤ ↑m * ↑r ^ e
Tactic:
apply float_real_le_1_le
Proof state after:
case a
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ 0 < ↑r ^ e

case a
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ 1 ≤ m
Theorem: float_pow_int_eq_le
Proof state before:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ 0 < ↑r ^ e
Tactic:
case a =>
  norm_cast
  suffices abs x > 0 by simp_all only [lt_self_iff_false, ne_eq, Int.cast_lt_zero, Int.one_lt_zero_le_iff, Int.cast_eq_zero, gt_iff_lt, Int.cast_pos, zero_add, zero_lt_mul_left]
  simp; exact hx
Proof state after:
no goals
Theorem: float_pow_int_eq_le
Proof state before:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ 1 ≤ m
Tactic:
case a =>
  exact hm
Proof state after:
no goals
Theorem: float_pow_int_eq_le
Proof state before:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ 0 < ↑r ^ e
Tactic:
suffices abs x > 0 by simp_all only [lt_self_iff_false, ne_eq, Int.cast_lt_zero, Int.one_lt_zero_le_iff, Int.cast_eq_zero, gt_iff_lt, Int.cast_pos, zero_add, zero_lt_mul_left]
Proof state after:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ abs x > 0
Theorem: float_pow_int_eq_le
Proof state before:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ abs x > 0
Tactic:
simp
Proof state after:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ ¬x = 0
Theorem: float_pow_int_eq_le
Proof state before:
r : ℤ
x : ℝ
m e : ℤ
hx : x ≠ 0
hm : 1 ≤ m
he : abs x = ↑m * ↑r ^ e
⊢ ¬x = 0
Tactic:
exact hx
Proof state after:
no goals