internlm/Lean-Github huggingface dataset:
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
this : abs x > 0
⊢ 0 < ↑r ^ e
Tactic:
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:
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:
exact hm
Proof state after:
no goals
Theorem: float_eq_ipow
Proof 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
Proof 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
Theorem: float_eq_ipow
Proof 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
Proof 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
Theorem: float_eq_ipow
Proof 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
Proof 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
Theorem: float_eq_ipow
Proof 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
Proof state after:
no goals
Theorem: float_eq_ipow
Proof 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]
Proof 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
Theorem: float_eq_ipow
Proof 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]
Proof 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
Theorem: float_eq_ipow
Proof 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
Proof 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
Theorem: float_eq_ipow
Proof 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
Proof 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
Theorem: float_eq_ipow
Proof 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]
Proof 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 }
Theorem: float_eq_ipow
Proof 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]
Proof 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
Theorem: float_eq_ipow
Proof 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
Proof state after:
no goals
Theorem: float_eq_ipow
Proof 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
Proof 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
Theorem: float_eq_ipow
Proof 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
Proof 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
Theorem: float_eq_ipow
Proof 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]
Proof 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
Theorem: float_eq_ipow
Proof 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]
Proof 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
Theorem: float_eq_ipow
Proof 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
Proof 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
Theorem: float_eq_ipow
Proof 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
Proof state after:
no goals
Theorem: float_eq_ipow
Proof 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]
Proof state after:
no goals
Theorem: float_eq_ipow
Proof 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]
Proof 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
Theorem: float_eq_ipow
Proof 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
Proof state after:
no goals
Theorem: Int.one_lt_zero_lt
Proof state before:
i : ℤ
⊢ 1 < i → 0 < i
Tactic:
intro h
Proof state after:
i : ℤ
h : 1 < i
⊢ 0 < i
Theorem: Int.one_lt_zero_lt
Proof state before:
i : ℤ
h : 1 < i
⊢ 0 < i
Tactic:
have hz : (0: ℤ) < 1 := by simp
Proof state after:
i : ℤ
h : 1 < i
hz : 0 < 1
⊢ 0 < i
Theorem: Int.one_lt_zero_lt
Proof state before:
i : ℤ
h : 1 < i
hz : 0 < 1
⊢ 0 < i
Tactic:
apply lt_trans hz h
Proof state after:
no goals
Theorem: Int.one_lt_zero_lt
Proof state before:
i : ℤ
h : 1 < i
⊢ 0 < 1
Tactic:
simp
Proof state after:
no goals
Theorem: Int.one_lt_zero_le_iff
Proof state before:
i j : ℤ
⊢ j < i ↔ j + 1 ≤ i
Tactic:
apply Iff.intro
Proof state after:
case mp
i j : ℤ
⊢ j < i → j + 1 ≤ i

case mpr
i j : ℤ
⊢ j + 1 ≤ i → j < i
Theorem: Int.one_lt_ne_one
Proof state before:
a : ℤ
h : 1 < a
⊢ a ≠ 1
Tactic:
intro a_1
Proof state after:
a : ℤ
h : 1 < a
a_1 : a = 1
⊢ False
Theorem: Int.one_lt_ne_one
Proof state before:
a : ℤ
h : 1 < a
a_1 : a = 1
⊢ False
Tactic:
simp_all only [one_lt_zero_le_iff, ne_eq]
Proof state after:
no goals
Theorem: ipow_lt_zero
Proof state before:
r : ℝ
i : ℤ
⊢ 0 < r → 0 < r ^ i
Tactic:
intro h
Proof state after:
r : ℝ
i : ℤ
h : 0 < r
⊢ 0 < r ^ i
Theorem: ipow_lt_zero
Proof state before:
r : ℝ
i : ℤ
h : 0 < r
⊢ 0 < r ^ i
Tactic:
cases i with 
| ofNat n  =>
  simp_all only [Int.ofNat_eq_coe, zpow_coe_nat, gt_iff_lt, pow_pos]
| negSucc n =>
  simp_all only [zpow_negSucc, inv_pos, gt_iff_lt, pow_pos]
Proof state after:
no goals
Theorem: ipow_lt_zero
Proof state before:
case ofNat
r : ℝ
h : 0 < r
n : ℕ
⊢ 0 < r ^ ofNat n
Tactic:
simp_all only [Int.ofNat_eq_coe, zpow_coe_nat, gt_iff_lt, pow_pos]
Proof state after:
no goals
Theorem: ipow_lt_zero
Proof state before:
case negSucc
r : ℝ
h : 0 < r
n : ℕ
⊢ 0 < r ^ -[n+1]
Tactic:
simp_all only [zpow_negSucc, inv_pos, gt_iff_lt, pow_pos]
Proof state after:
no goals
Theorem: ipow_inv
Proof state before:
r : ℝ
i : ℕ
⊢ r ^ negOfNat i = (r ^ i)⁻¹
Tactic:
induction i
Proof state after:
case zero
r : ℝ
⊢ r ^ negOfNat Nat.zero = (r ^ Nat.zero)⁻¹

case succ
r : ℝ
n✝ : ℕ
n_ih✝ : r ^ negOfNat n✝ = (r ^ n✝)⁻¹
⊢ r ^ negOfNat (Nat.succ n✝) = (r ^ Nat.succ n✝)⁻¹
Theorem: ipow_inv
Proof state before:
r : ℝ
⊢ r ^ negOfNat Nat.zero = (r ^ Nat.zero)⁻¹
Tactic:
case zero => simp; trivial
Proof state after:
no goals
Theorem: ipow_inv
Proof state before:
r : ℝ
n✝ : ℕ
n_ih✝ : r ^ negOfNat n✝ = (r ^ n✝)⁻¹
⊢ r ^ negOfNat (Nat.succ n✝) = (r ^ Nat.succ n✝)⁻¹
Tactic:
case succ => constructor
Proof state after:
no goals
Theorem: ipow_inv
Proof state before:
r : ℝ
⊢ r ^ negOfNat Nat.zero = (r ^ Nat.zero)⁻¹
Tactic:
simp
Proof state after:
r : ℝ
⊢ r ^ negOfNat 0 = 1
Theorem: ipow_inv
Proof state before:
r : ℝ
⊢ r ^ negOfNat 0 = 1
Tactic:
trivial
Proof state after:
no goals
Theorem: ipow_inv
Proof state before:
r : ℝ
n✝ : ℕ
n_ih✝ : r ^ negOfNat n✝ = (r ^ n✝)⁻¹
⊢ r ^ negOfNat (Nat.succ n✝) = (r ^ Nat.succ n✝)⁻¹
Tactic:
constructor
Proof state after:
no goals
Theorem: ipow_neg_succ
Proof state before:
r : ℝ
i : ℕ
⊢ r ^ -[i+1] = (r ^ Nat.succ i)⁻¹
Tactic:
simp_all only [zpow_negSucc]
Proof state after:
no goals
Theorem: ipow_inv_neg
Proof state before:
r : ℝ
i : ℤ
⊢ r ≠ 0 → r ^ i = (r ^ (-i))⁻¹
Tactic:
cases i with
| ofNat n =>
    intros
    simp_all only [ne_eq, Int.ofNat_eq_coe, zpow_coe_nat, zpow_neg, inv_inv]
| negSucc n =>
    intros
    simp_all only [ne_eq, zpow_negSucc, zpow_neg, inv_inv]
Proof state after:
no goals
Theorem: ipow_inv_neg
Proof state before:
case ofNat
r : ℝ
n : ℕ
⊢ r ≠ 0 → r ^ ofNat n = (r ^ (-ofNat n))⁻¹
Tactic:
intros
Proof state after:
case ofNat
r : ℝ
n : ℕ
a✝ : r ≠ 0
⊢ r ^ ofNat n = (r ^ (-ofNat n))⁻¹
Theorem: ipow_inv_neg
Proof state before:
case ofNat
r : ℝ
n : ℕ
a✝ : r ≠ 0
⊢ r ^ ofNat n = (r ^ (-ofNat n))⁻¹
Tactic:
simp_all only [ne_eq, Int.ofNat_eq_coe, zpow_coe_nat, zpow_neg, inv_inv]
Proof state after:
no goals
Theorem: ipow_inv_neg
Proof state before:
case negSucc
r : ℝ
n : ℕ
⊢ r ≠ 0 → r ^ -[n+1] = (r ^ (- -[n+1]))⁻¹
Tactic:
intros
Proof state after:
case negSucc
r : ℝ
n : ℕ
a✝ : r ≠ 0
⊢ r ^ -[n+1] = (r ^ (- -[n+1]))⁻¹
Theorem: ipow_inv_neg
Proof state before:
case negSucc
r : ℝ
n : ℕ
a✝ : r ≠ 0
⊢ r ^ -[n+1] = (r ^ (- -[n+1]))⁻¹
Tactic:
simp_all only [ne_eq, zpow_negSucc, zpow_neg, inv_inv]
Proof state after:
no goals
Theorem: ipow_add_exp
Proof state before:
r : ℝ
u v : ℤ
⊢ r ≠ 0 → r ^ u * r ^ v = r ^ (u + v)
Tactic:
sorry
Proof state after:
no goals
Theorem: ipow_to_one
Proof state before:
r : ℝ
⊢ r ^ 1 = r
Tactic:
simp
Proof state after:
no goals
Theorem: ipow_to_zero
Proof state before:
r : ℝ
⊢ r ^ 0 = 1
Tactic:
simp
Proof state after:
no goals
Theorem: ipow_le_one
Proof state before:
r : ℝ
i : ℤ
⊢ 1 ≤ r → 0 ≤ i → 1 ≤ r ^ i
Tactic:
sorry
Proof state after:
no goals
Theorem: ipow_lt_one
Proof state before:
r : ℝ
i : ℤ
⊢ 1 < r → 0 < i → 1 < r ^ i
Tactic:
sorry
Proof state after:
no goals
Theorem: ipow_le_sum
Proof state before:
i : ℕ
r n : ℝ
⊢ 2 ≤ r → 0 ≤ i → ∃ e, n ≤ r ^ e
Tactic:
sorry
Proof state after:
no goals
Theorem: ipow_le_real_two
Proof state before:
r z : ℝ
⊢ 0 < z → 2 ≤ r → ∃ e, r ^ e ≤ z
Tactic:
sorry
Proof state after:
no goals
Theorem: ipow_monotone
Proof state before:
r : ℝ
u v : ℤ
⊢ 1 ≤ r → u ≤ v → r ^ u ≤ r ^ v
Tactic:
sorry
Proof state after:
no goals
Theorem: ipow_monotone_pow
Proof state before:
r : ℝ
u v : ℤ
⊢ 1 ≤ r → r ^ u ≤ r ^ v → u ≤ v
Tactic:
sorry
Proof state after:
no goals
Theorem: ipow_monotone_lt
Proof state before:
r : ℝ
u v : ℤ
⊢ 1 < r → u < v → r ^ u < r ^ v
Tactic:
intro a a_1
Proof state after:
r : ℝ
u v : ℤ
a : 1 < r
a_1 : u < v
⊢ r ^ u < r ^ v
Theorem: ipow_monotone_lt
Proof state before:
r : ℝ
u v : ℤ
a : 1 < r
a_1 : u < v
⊢ r ^ u < r ^ v
Tactic:
simp_all only [ne_eq, gt_iff_lt, zpow_lt_iff_lt]
Proof state after:
no goals
Theorem: ipow_monotone_lt_pow
Proof state before:
r : ℝ
u v : ℤ
⊢ 1 < r → r ^ u < r ^ v → u < v
Tactic:
intro a a_1
Proof state after:
r : ℝ
u v : ℤ
a : 1 < r
a_1 : r ^ u < r ^ v
⊢ u < v
Theorem: ipow_monotone_lt_pow
Proof state before:
r : ℝ
u v : ℤ
a : 1 < r
a_1 : r ^ u < r ^ v
⊢ u < v
Tactic:
simp_all only [ne_eq, gt_iff_lt, zpow_lt_iff_lt, one_lt_zero_le_iff]
Proof state after:
no goals
Theorem: ipow_monotone_le_pow
Proof state before:
r : ℝ
u v : ℤ
⊢ 1 < r → r ^ u ≤ r ^ v → u ≤ v
Tactic:
intro a a_1
Proof state after:
r : ℝ
u v : ℤ
a : 1 < r
a_1 : r ^ u ≤ r ^ v
⊢ u ≤ v
Theorem: ipow_monotone_le_pow
Proof state before:
r : ℝ
u v : ℤ
a : 1 < r
a_1 : r ^ u ≤ r ^ v
⊢ u ≤ v
Tactic:
simp_all only [ne_eq, gt_iff_lt, zpow_le_iff_le]
Proof state after:
no goals
Theorem: ipow_monotone_le
Proof state before:
r : ℝ
u v : ℤ
⊢ 1 < r → u ≤ v → r ^ u ≤ r ^ v
Tactic:
intro a a_1
Proof state after:
r : ℝ
u v : ℤ
a : 1 < r
a_1 : u ≤ v
⊢ r ^ u ≤ r ^ v
Theorem: ipow_monotone_le
Proof state before:
r : ℝ
u v : ℤ
a : 1 < r
a_1 : u ≤ v
⊢ r ^ u ≤ r ^ v
Tactic:
simp_all only [ne_eq, gt_iff_lt, zpow_le_iff_le]
Proof state after:
no goals
Theorem: ipow_monotone_two
Proof state before:
r : ℝ
u v : ℤ
⊢ 2 ≤ r → u ≤ v → r ^ u ≤ r ^ v
Tactic:
sorry
Proof state after:
no goals
Theorem: ipow_mul_inv_eq_one
Proof state before:
r : ℝ
i : ℤ
⊢ 0 < r → r ^ i * r ^ (-i) = 1
Tactic:
sorry
Proof state after:
no goals
Theorem: ipow_le_real
Proof state before:
r z : ℝ
⊢ 2 ≤ r → ∃ e, z ≤ r ^ e
Tactic:
intros h
Proof state after:
r z : ℝ
h : 2 ≤ r
⊢ ∃ e, z ≤ r ^ e
Theorem: ipow_le_real
Proof state before:
r z : ℝ
h : 2 ≤ r
⊢ ∃ e, z ≤ r ^ e
Tactic:
sorry
Proof state after:
no goals
Theorem: flformat_to_fformat
Proof state before:
float : flformat
⊢ is_valid_fformat ↑float
Tactic:
apply And.intro
Proof state after:
case left
float : flformat
⊢ 1 < (↑float).r

case right
float : flformat
⊢ (↑float).r % 2 = 0 ∧ 0 < (↑float).p
Theorem: flformat_to_fformat
Proof state before:
float : flformat
⊢ 1 < (↑float).r
Tactic:
case left => 
  exact float.prop.left
Proof state after:
no goals
Theorem: flformat_to_fformat
Proof state before:
float : flformat
⊢ (↑float).r % 2 = 0 ∧ 0 < (↑float).p
Tactic:
case right => 
  apply And.intro
  case left  =>
    exact float.prop.right.left
  case right =>
    apply Int.one_lt_zero_lt
    exact float.prop.right.right
Proof state after:
no goals
Theorem: flformat_to_fformat
Proof state before:
float : flformat
⊢ 1 < (↑float).r
Tactic:
exact float.prop.left
Proof state after:
no goals
Theorem: flformat_to_fformat
Proof state before:
float : flformat
⊢ (↑float).r % 2 = 0 ∧ 0 < (↑float).p
Tactic:
apply And.intro
Proof state after:
case left
float : flformat
⊢ (↑float).r % 2 = 0

case right
float : flformat
⊢ 0 < (↑float).p
Theorem: flformat_to_fformat
Proof state before:
float : flformat
⊢ (↑float).r % 2 = 0
Tactic:
case left  =>
  exact float.prop.right.left
Proof state after:
no goals
Theorem: flformat_to_fformat
Proof state before:
float : flformat
⊢ 0 < (↑float).p
Tactic:
case right =>
  apply Int.one_lt_zero_lt
  exact float.prop.right.right
Proof state after:
no goals
Theorem: flformat_to_fformat
Proof state before:
float : flformat
⊢ (↑float).r % 2 = 0
Tactic:
exact float.prop.right.left
Proof state after:
no goals
Theorem: flformat_to_fformat
Proof state before:
float : flformat
⊢ 0 < (↑float).p
Tactic:
apply Int.one_lt_zero_lt
Proof state after:
case a
float : flformat
⊢ 1 < (↑float).p
Theorem: flformat_to_fformat
Proof state before:
case a
float : flformat
⊢ 1 < (↑float).p
Tactic:
exact float.prop.right.right
Proof state after:
no goals
Theorem: fformat_valid_imp_radix_lt_one
Proof state before:
fmt : format
⊢ is_valid_fformat fmt → 1 < fmt.r
Tactic:
intro h
Proof state after:
fmt : format
h : is_valid_fformat fmt
⊢ 1 < fmt.r
Theorem: fformat_valid_imp_radix_lt_one
Proof state before:
fmt : format
h : is_valid_fformat fmt
⊢ 1 < fmt.r
Tactic:
exact h.left
Proof state after:
no goals
Theorem: fformat_valid_imp_radix_even
Proof state before:
fmt : format
⊢ is_valid_fformat fmt → fmt.r % 2 = 0
Tactic:
intro h
Proof state after:
fmt : format
h : is_valid_fformat fmt
⊢ fmt.r % 2 = 0
Theorem: fformat_valid_imp_radix_even
Proof state before:
fmt : format
h : is_valid_fformat fmt
⊢ fmt.r % 2 = 0
Tactic:
exact h.right.left
Proof state after:
no goals
Theorem: fformat_valid_imp_prec_lt_0
Proof state before:
fmt : format
⊢ is_valid_fformat fmt → 0 < fmt.p
Tactic:
intro h
Proof state after:
fmt : format
h : is_valid_fformat fmt
⊢ 0 < fmt.p
Theorem: fformat_valid_imp_prec_lt_0
Proof state before:
fmt : format
h : is_valid_fformat fmt
⊢ 0 < fmt.p
Tactic:
exact h.right.right
Proof state after:
no goals
Theorem: fformat_radix_lt_1
Proof state before:
⊢ ∀ (fmt : fformat), 1 < (↑fmt).r
Tactic:
intro h
Proof state after:
h : fformat
⊢ 1 < (↑h).r
Theorem: fformat_radix_lt_1
Proof state before:
h : fformat
⊢ 1 < (↑h).r
Tactic:
exact h.prop.left
Proof state after:
no goals
Theorem: fformat_radix_lt_0
Proof state before:
⊢ ∀ (fmt : fformat), 0 < (↑fmt).r
Tactic:
intro h
Proof state after:
h : fformat
⊢ 0 < (↑h).r
Theorem: fformat_radix_lt_0
Proof state before:
h : fformat
⊢ 0 < (↑h).r
Tactic:
have h₁ := h.prop.left
Proof state after:
h : fformat
h₁ : 1 < (↑h).r
⊢ 0 < (↑h).r
Theorem: fformat_radix_lt_0
Proof state before:
h : fformat
h₁ : 1 < (↑h).r
⊢ 0 < (↑h).r
Tactic:
have h₂ : 0 < (1 : Int) := by trivial
Proof state after:
h : fformat
h₁ : 1 < (↑h).r
h₂ : 0 < 1
⊢ 0 < (↑h).r
Theorem: fformat_radix_lt_0
Proof state before:
h : fformat
h₁ : 1 < (↑h).r
h₂ : 0 < 1
⊢ 0 < (↑h).r
Tactic:
apply Int.lt_trans h₂ h₁
Proof state after:
no goals
Theorem: fformat_radix_lt_0
Proof state before:
h : fformat
h₁ : 1 < (↑h).r
⊢ 0 < 1
Tactic:
trivial
Proof state after:
no goals
Theorem: gt_zero_ne_zero
Proof state before:
x : ℤ
⊢ 1 < x → x ≠ 0
Tactic:
intros h h₁
Proof state after:
x : ℤ
h : 1 < x
h₁ : x = 0
⊢ False
Theorem: gt_zero_ne_zero
Proof state before:
x : ℤ
h : 1 < x
h₁ : x = 0
⊢ False
Tactic:
simp [h₁] at h
Proof state after:
no goals
Theorem: fformat_radix_ne_0
Proof state before:
⊢ ∀ (fmt : fformat), (↑fmt).r ≠ 0
Tactic:
intro h
Proof state after:
h : fformat
⊢ (↑h).r ≠ 0
Theorem: fformat_radix_ne_0
Proof state before:
h : fformat
⊢ (↑h).r ≠ 0
Tactic:
have h₁ := h.prop.left
Proof state after:
h : fformat
h₁ : 1 < (↑h).r
⊢ (↑h).r ≠ 0
Theorem: fformat_radix_ne_0
Proof state before:
h : fformat
h₁ : 1 < (↑h).r
⊢ (↑h).r ≠ 0
Tactic:
apply gt_zero_ne_zero
Proof state after:
case a
h : fformat
h₁ : 1 < (↑h).r
⊢ 1 < (↑h).r
Theorem: fformat_radix_ne_0
Proof state before:
case a
h : fformat
h₁ : 1 < (↑h).r
⊢ 1 < (↑h).r
Tactic:
trivial
Proof state after:
no goals
Theorem: fformat_radix_even
Proof state before:
fmt : fformat
⊢ (↑fmt).r % 2 = 0
Tactic:
simp [fmt.prop.right.left]
Proof state after:
no goals
Theorem: fformat_prec_lt_0
Proof state before:
fmt : fformat
⊢ 0 < (↑fmt).p
Tactic:
have h := fmt.prop.right.right
Proof state after:
fmt : fformat
h : 0 < (↑fmt).p
⊢ 0 < (↑fmt).p
Theorem: fformat_prec_lt_0
Proof state before:
fmt : fformat
h : 0 < (↑fmt).p
⊢ 0 < (↑fmt).p
Tactic:
exact h
Proof state after:
no goals
Theorem: fformat_radix_ipow_le_0
Proof state before:
fmt : fformat
e : ℤ
⊢ (↑fmt).r ^ e ≠ 0
Tactic:
simp [HPow.hPow, Pow.pow, pow_int]
Proof state after:
fmt : fformat
e : ℤ
⊢ ¬↑(↑fmt).r ^ e = 0
Theorem: fformat_radix_ipow_le_0
Proof state before:
fmt : fformat
e : ℤ
⊢ ¬↑(↑fmt).r ^ e = 0
Tactic:
cases e with
| ofNat n =>
  simp [pow_ne_zero]
| negSucc n =>
simp_all only [zpow_negSucc, inv_eq_zero, add_pos_iff, or_true, pow_eq_zero_iff, Int.cast_eq_zero, fformat_radix_lt_1,
  gt_zero_ne_zero, not_false_iff]
Proof state after:
no goals
Theorem: fformat_radix_ipow_le_0
Proof state before:
case ofNat
fmt : fformat
n : ℕ
⊢ ¬↑(↑fmt).r ^ Int.ofNat n = 0
Tactic:
simp [pow_ne_zero]
Proof state after:
no goals
Theorem: fformat_radix_ipow_le_0
Proof state before:
case negSucc
fmt : fformat
n : ℕ
⊢ ¬↑(↑fmt).r ^ Int.negSucc n = 0
Tactic:
simp_all only [zpow_negSucc, inv_eq_zero, add_pos_iff, or_true, pow_eq_zero_iff, Int.cast_eq_zero, fformat_radix_lt_1,
gt_zero_ne_zero, not_false_iff]
Proof state after:
no goals