internlm/Lean-Github huggingface dataset:
Theorem: CoveredByBalls.zero_right
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
⊢ s = ∅ → CoveredByBalls s n 0
Tactic:
intro hs
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
⊢ CoveredByBalls s n 0
Theorem: CoveredByBalls.zero_right
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
⊢ CoveredByBalls s n 0
Tactic:
have h21 : (∅ : Finset X).card ≤ n := by exact tsub_add_cancel_iff_le.mp rfl
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
h21 : ∅.card ≤ n
⊢ CoveredByBalls s n 0
Theorem: CoveredByBalls.zero_right
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
h21 : ∅.card ≤ n
⊢ CoveredByBalls s n 0
Tactic:
have h22 : s ⊆ ⋃ x ∈ (∅ : Finset X), ball x 0 := by
  simp only [not_mem_empty, ball_zero, Set.iUnion_of_empty, Set.iUnion_empty]
  exact Set.subset_empty_iff.mpr hs
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
h21 : ∅.card ≤ n
h22 : s ⊆ ⋃ x ∈ ∅, ball x 0
⊢ CoveredByBalls s n 0
Theorem: CoveredByBalls.zero_right
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
h21 : ∅.card ≤ n
h22 : s ⊆ ⋃ x ∈ ∅, ball x 0
⊢ CoveredByBalls s n 0
Tactic:
exact ⟨(∅ : Finset X), h21, h22⟩
Proof state after:
no goals
Theorem: CoveredByBalls.zero_right
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
⊢ ∅.card ≤ n
Tactic:
exact tsub_add_cancel_iff_le.mp rfl
Proof state after:
no goals
Theorem: CoveredByBalls.zero_right
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
h21 : ∅.card ≤ n
⊢ s ⊆ ⋃ x ∈ ∅, ball x 0
Tactic:
simp only [not_mem_empty, ball_zero, Set.iUnion_of_empty, Set.iUnion_empty]
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
h21 : ∅.card ≤ n
⊢ s ⊆ ∅
Theorem: CoveredByBalls.zero_right
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h1 : CoveredByBalls s n 0 → s = ∅
hs : s = ∅
h21 : ∅.card ≤ n
⊢ s ⊆ ∅
Tactic:
exact Set.subset_empty_iff.mpr hs
Proof state after:
no goals
Theorem: CoveredByBalls.trans
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h : CoveredByBalls s n r
h2 : BallsCoverBalls X r r' m
⊢ CoveredByBalls s (n * m) r'
Tactic:
cases h
Proof state after:
case mk
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : BallsCoverBalls X r r' m
balls✝ : Finset X
card_balls✝ : balls✝.card ≤ n
union_balls✝ : s ⊆ ⋃ x ∈ balls✝, ball x r
⊢ CoveredByBalls s (n * m) r'
Theorem: CoveredByBalls.trans
Proof state before:
case mk
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : BallsCoverBalls X r r' m
balls✝ : Finset X
card_balls✝ : balls✝.card ≤ n
union_balls✝ : s ⊆ ⋃ x ∈ balls✝, ball x r
⊢ CoveredByBalls s (n * m) r'
Tactic:
case mk b0 hb0 hs0
Proof state after:
case mk
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : BallsCoverBalls X r r' m
b0 : Finset X
hb0 : b0.card ≤ n
hs0 : s ⊆ ⋃ x ∈ b0, ball x r
⊢ CoveredByBalls s (n * m) r'
Theorem: CoveredByBalls.trans
Proof state before:
case mk
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ : ℝ
h2 : BallsCoverBalls X r r' m
b0 : Finset X
hb0 : b0.card ≤ n
hs0 : s ⊆ ⋃ x ∈ b0, ball x r
⊢ CoveredByBalls s (n * m) r'
Tactic:
sorry
Proof state after:
no goals
Theorem: BallCoversSelf
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
⊢ CoveredByBalls (ball x r) 1 r
Tactic:
let a : Finset X := singleton x
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
⊢ CoveredByBalls (ball x r) 1 r
Theorem: BallCoversSelf
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
⊢ CoveredByBalls (ball x r) 1 r
Tactic:
have h : a.card ≤ 1 := by rfl
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
h : a.card ≤ 1
⊢ CoveredByBalls (ball x r) 1 r
Theorem: BallCoversSelf
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
h : a.card ≤ 1
⊢ CoveredByBalls (ball x r) 1 r
Tactic:
have h2 : ball x r ⊆ ⋃ x ∈ a, ball x r := by
  simp [a]
  rfl
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
h : a.card ≤ 1
h2 : ball x r ⊆ ⋃ x ∈ a, ball x r
⊢ CoveredByBalls (ball x r) 1 r
Theorem: BallCoversSelf
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
h : a.card ≤ 1
h2 : ball x r ⊆ ⋃ x ∈ a, ball x r
⊢ CoveredByBalls (ball x r) 1 r
Tactic:
exact ⟨a, h, h2⟩
Proof state after:
no goals
Theorem: BallCoversSelf
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
⊢ a.card ≤ 1
Tactic:
rfl
Proof state after:
no goals
Theorem: BallCoversSelf
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
h : a.card ≤ 1
⊢ ball x r ⊆ ⋃ x ∈ a, ball x r
Tactic:
simp [a]
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
h : a.card ≤ 1
⊢ ball x r ⊆ ball x r
Theorem: BallCoversSelf
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r✝ r' r₁ r₂ r₃ : ℝ
x : X
r : ℝ
a : Finset X := {x}
h : a.card ≤ 1
⊢ ball x r ⊆ ball x r
Tactic:
rfl
Proof state after:
no goals
Theorem: BallsCoverBalls.pow_mul
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
k : ℕ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
⊢ BallsCoverBalls X (a ^ k * r) r (n ^ k)
Tactic:
induction k
Proof state after:
case zero
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
⊢ BallsCoverBalls X (a ^ 0 * r) r (n ^ 0)

case succ
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
n✝ : ℕ
a✝ : BallsCoverBalls X (a ^ n✝ * r) r (n ^ n✝)
⊢ BallsCoverBalls X (a ^ (n✝ + 1) * r) r (n ^ (n✝ + 1))
Theorem: BallsCoverBalls.pow_mul
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
⊢ BallsCoverBalls X (a ^ 0 * r) r (n ^ 0)
Tactic:
case zero =>
  simp
  intro x
  exact BallCoversSelf x r
Proof state after:
no goals
Theorem: BallsCoverBalls.pow_mul
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
⊢ BallsCoverBalls X (a ^ (m + 1) * r) r (n ^ (m + 1))
Tactic:
case succ m h2 =>
  specialize h (r * a^m)
  rw[<- mul_assoc, mul_comm, <- mul_assoc] at h
  norm_cast
  ring_nf
  rw[mul_comm a]
  rw[mul_comm] at h2
  norm_cast at h2
  exact BallsCoverBalls.trans h h2
Proof state after:
no goals
Theorem: BallsCoverBalls.pow_mul
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
⊢ BallsCoverBalls X (a ^ 0 * r) r (n ^ 0)
Tactic:
simp
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
⊢ BallsCoverBalls X r r 1
Theorem: BallsCoverBalls.pow_mul
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
⊢ BallsCoverBalls X r r 1
Tactic:
intro x
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
x : X
⊢ CoveredByBalls (ball x r) 1 r
Theorem: BallsCoverBalls.pow_mul
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
x : X
⊢ CoveredByBalls (ball x r) 1 r
Tactic:
exact BallCoversSelf x r
Proof state after:
no goals
Theorem: BallsCoverBalls.pow_mul
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
⊢ BallsCoverBalls X (a ^ (m + 1) * r) r (n ^ (m + 1))
Tactic:
specialize h (r * a^m)
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
h : BallsCoverBalls X (a * (r * a ^ m)) (r * a ^ m) n
⊢ BallsCoverBalls X (a ^ (m + 1) * r) r (n ^ (m + 1))
Theorem: BallsCoverBalls.pow_mul
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
h : BallsCoverBalls X (a * (r * a ^ m)) (r * a ^ m) n
⊢ BallsCoverBalls X (a ^ (m + 1) * r) r (n ^ (m + 1))
Tactic:
rw[<- mul_assoc, mul_comm, <- mul_assoc] at h
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
h : BallsCoverBalls X (a ^ m * a * r) (r * a ^ m) n
⊢ BallsCoverBalls X (a ^ (m + 1) * r) r (n ^ (m + 1))
Theorem: BallsCoverBalls.pow_mul
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
h : BallsCoverBalls X (a ^ m * a * r) (r * a ^ m) n
⊢ BallsCoverBalls X (a ^ (m + 1) * r) r (n ^ (m + 1))
Tactic:
ring_nf
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
h : BallsCoverBalls X (a ^ m * a * r) (r * a ^ m) n
⊢ BallsCoverBalls X (a * a ^ m * r) r (n * n ^ m)
Theorem: BallsCoverBalls.pow_mul
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
h : BallsCoverBalls X (a ^ m * a * r) (r * a ^ m) n
⊢ BallsCoverBalls X (a * a ^ m * r) r (n * n ^ m)
Tactic:
rw[mul_comm a]
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
h : BallsCoverBalls X (a ^ m * a * r) (r * a ^ m) n
⊢ BallsCoverBalls X (a ^ m * a * r) r (n * n ^ m)
Theorem: BallsCoverBalls.pow_mul
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
h : BallsCoverBalls X (a ^ m * a * r) (r * a ^ m) n
⊢ BallsCoverBalls X (a ^ m * a * r) r (n * n ^ m)
Tactic:
rw[mul_comm] at h2
Proof state after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (r * a ^ m) r (n ^ m)
h : BallsCoverBalls X (a ^ m * a * r) (r * a ^ m) n
⊢ BallsCoverBalls X (a ^ m * a * r) r (n * n ^ m)
Theorem: BallsCoverBalls.pow_mul
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (r * a ^ m) r (n ^ m)
h : BallsCoverBalls X (a ^ m * a * r) (r * a ^ m) n
⊢ BallsCoverBalls X (a ^ m * a * r) r (n * n ^ m)
Tactic:
exact BallsCoverBalls.trans h h2
Proof state after:
no goals
Theorem: BallsCoverBalls.pow
Proof state before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
k : ℕ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
⊢ BallsCoverBalls X (a ^ k) 1 (n ^ k)
Tactic:
convert BallsCoverBalls.pow_mul h using 1
Proof state after:
case h.e'_3
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
k : ℕ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
⊢ a ^ k = a ^ k * 1
Theorem: BallsCoverBalls.pow
Proof state before:
case h.e'_3
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
k : ℕ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
⊢ a ^ k = a ^ k * 1
Tactic:
simp
Proof state after:
no goals
Theorem: ieee_to_flformat
Proof state before:
fmt : ieee_format
⊢ is_valid_flformat (mk_format fmt)
Tactic:
have h := fmt.prop
Proof state after:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ is_valid_flformat (mk_format fmt)
Theorem: ieee_to_flformat
Proof state before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ is_valid_flformat (mk_format fmt)
Tactic:
apply And.intro
Proof state after:
case left
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ 1 < (mk_format fmt).r

case right
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ (mk_format fmt).r % 2 = 0 ∧ 1 < (mk_format fmt).p
Theorem: ieee_to_flformat
Proof state before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ 1 < (mk_format fmt).r
Tactic:
case left =>
  apply h.left
Proof state after:
no goals
Theorem: ieee_to_flformat
Proof state before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ (mk_format fmt).r % 2 = 0 ∧ 1 < (mk_format fmt).p
Tactic:
case right =>
  apply And.intro
  case left =>
    apply h.right.left
  case right =>
    apply h.right.right.left
Proof state after:
no goals
Theorem: ieee_to_flformat
Proof state before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ 1 < (mk_format fmt).r
Tactic:
apply h.left
Proof state after:
no goals
Theorem: ieee_to_flformat
Proof state before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ (mk_format fmt).r % 2 = 0 ∧ 1 < (mk_format fmt).p
Tactic:
apply And.intro
Proof state after:
case left
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ (mk_format fmt).r % 2 = 0

case right
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ 1 < (mk_format fmt).p
Theorem: ieee_to_flformat
Proof state before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ (mk_format fmt).r % 2 = 0
Tactic:
case left =>
  apply h.right.left
Proof state after:
no goals
Theorem: ieee_to_flformat
Proof state before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ 1 < (mk_format fmt).p
Tactic:
case right =>
  apply h.right.right.left
Proof state after:
no goals
Theorem: ieee_to_flformat
Proof state before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ (mk_format fmt).r % 2 = 0
Tactic:
apply h.right.left
Proof state after:
no goals
Theorem: ieee_to_flformat
Proof state before:
fmt : ieee_format
h : is_valid_ieee_format ↑fmt
⊢ 1 < (mk_format fmt).p
Tactic:
apply h.right.right.left
Proof state after:
no goals
Theorem: float_real_le_1_le
Proof state before:
x : ℝ
m : ℤ
⊢ 0 < x → 1 ≤ m → x ≤ ↑m * x
Tactic:
intro h₁ h₂
Proof state after:
x : ℝ
m : ℤ
h₁ : 0 < x
h₂ : 1 ≤ m
⊢ x ≤ ↑m * x
Theorem: float_real_le_1_le
Proof state before:
x : ℝ
m : ℤ
h₁ : 0 < x
h₂ : 1 ≤ m
⊢ x ≤ ↑m * x
Tactic:
rw [le_mul_iff_one_le_left]
Proof state after:
x : ℝ
m : ℤ
h₁ : 0 < x
h₂ : 1 ≤ m
⊢ 1 ≤ ↑m

x : ℝ
m : ℤ
h₁ : 0 < x
h₂ : 1 ≤ m
⊢ 0 < x
Theorem: float_real_le_1_le
Proof state before:
x : ℝ
m : ℤ
h₁ : 0 < x
h₂ : 1 ≤ m
⊢ 1 ≤ ↑m

x : ℝ
m : ℤ
h₁ : 0 < x
h₂ : 1 ≤ m
⊢ 0 < x
Tactic:
norm_cast
Proof state after:
x : ℝ
m : ℤ
h₁ : 0 < x
h₂ : 1 ≤ m
⊢ 0 < x
Theorem: float_real_le_1_le
Proof state before:
x : ℝ
m : ℤ
h₁ : 0 < x
h₂ : 1 ≤ m
⊢ 0 < x
Tactic:
exact h₁
Proof state after:
no goals
Theorem: flformat_radix_lt_0
Proof state before:
fmt : flformat
⊢ 0 < (↑fmt).r
Tactic:
linarith [fmt.prop.left]
Proof state after:
no goals
Theorem: flformat_radix_lt_1
Proof state before:
fmt : flformat
⊢ 1 < (↑fmt).r
Tactic:
linarith [fmt.prop.left]
Proof state after:
no goals
Theorem: flformat_radix_le_2
Proof state before:
fmt : flformat
⊢ 2 ≤ (↑fmt).r
Tactic:
linarith [fmt.prop.left]
Proof state after:
no goals
Theorem: flformat_radix_lt_0_real
Proof state before:
fmt : flformat
⊢ 0 < ↑(↑fmt).r
Tactic:
norm_cast
Proof state after:
fmt : flformat
⊢ 0 < (↑fmt).r
Theorem: flformat_radix_lt_0_real
Proof state before:
fmt : flformat
⊢ 0 < (↑fmt).r
Tactic:
linarith [fmt.prop.left]
Proof state after:
no goals
Theorem: flformat_radix_lt_1_real
Proof state before:
fmt : flformat
⊢ 1 < ↑(↑fmt).r
Tactic:
norm_cast
Proof state after:
fmt : flformat
⊢ 1 < (↑fmt).r
Theorem: flformat_radix_lt_1_real
Proof state before:
fmt : flformat
⊢ 1 < (↑fmt).r
Tactic:
linarith [fmt.prop.left]
Proof state after:
no goals
Theorem: flformat_radix_le_2_real
Proof state before:
fmt : flformat
⊢ 2 ≤ ↑(↑fmt).r
Tactic:
norm_cast
Proof state after:
fmt : flformat
⊢ 2 ≤ (↑fmt).r
Theorem: flformat_radix_le_2_real
Proof state before:
fmt : flformat
⊢ 2 ≤ (↑fmt).r
Tactic:
linarith [Int.lt_add_one_iff.2 fmt.prop.left, fmt.prop.left]
Proof state after:
no goals
Theorem: float_radix_ipow_lt_0
Proof state before:
fmt : flformat
e : ℤ
⊢ 0 < ↑(↑fmt).r ^ e
Tactic:
have h : 0 < fmt.val.r := by apply Int.one_lt_zero_lt; exact fmt.prop.left
Proof state after:
fmt : flformat
e : ℤ
h : 0 < (↑fmt).r
⊢ 0 < ↑(↑fmt).r ^ e
Theorem: float_radix_ipow_lt_0
Proof state before:
fmt : flformat
e : ℤ
h : 0 < (↑fmt).r
⊢ 0 < ↑(↑fmt).r ^ e
Tactic:
apply ipow_lt_zero
Proof state after:
case a
fmt : flformat
e : ℤ
h : 0 < (↑fmt).r
⊢ 0 < ↑(↑fmt).r
Theorem: float_radix_ipow_lt_0
Proof state before:
case a
fmt : flformat
e : ℤ
h : 0 < (↑fmt).r
⊢ 0 < ↑(↑fmt).r
Tactic:
simp_all only [Int.one_lt_zero_le_iff, zero_add, Int.cast_pos]
Proof state after:
no goals
Theorem: float_radix_ipow_lt_0
Proof state before:
fmt : flformat
e : ℤ
⊢ 0 < (↑fmt).r
Tactic:
apply Int.one_lt_zero_lt
Proof state after:
case a
fmt : flformat
e : ℤ
⊢ 1 < (↑fmt).r
Theorem: float_radix_ipow_lt_0
Proof state before:
case a
fmt : flformat
e : ℤ
⊢ 1 < (↑fmt).r
Tactic:
exact fmt.prop.left
Proof state after:
no goals
Theorem: float_ipow_le_real
Proof state before:
fmt : flformat
x : ℝ
⊢ ∃ e, x ≤ ↑(↑fmt).r ^ e
Tactic:
apply ipow_le_real
Proof state after:
case a
fmt : flformat
x : ℝ
⊢ 2 ≤ ↑(↑fmt).r
Theorem: float_ipow_le_real
Proof state before:
case a
fmt : flformat
x : ℝ
⊢ 2 ≤ ↑(↑fmt).r
Tactic:
simp [flformat_radix_le_2]
Proof state after:
no goals
Theorem: float_ipow_le_real_2
Proof state before:
fmt : flformat
x : ℝ
⊢ 0 < x → ∃ e, x ≤ ↑(↑fmt).r ^ e
Tactic:
intros
Proof state after:
fmt : flformat
x : ℝ
a✝ : 0 < x
⊢ ∃ e, x ≤ ↑(↑fmt).r ^ e
Theorem: float_ipow_le_real_2
Proof state before:
fmt : flformat
x : ℝ
a✝ : 0 < x
⊢ ∃ e, x ≤ ↑(↑fmt).r ^ e
Tactic:
apply ipow_le_real
Proof state after:
case a
fmt : flformat
x : ℝ
a✝ : 0 < x
⊢ 2 ≤ ↑(↑fmt).r
Theorem: float_ipow_le_real_2
Proof state before:
case a
fmt : flformat
x : ℝ
a✝ : 0 < x
⊢ 2 ≤ ↑(↑fmt).r
Tactic:
simp_all only [flformat_radix_le_2_real]
Proof state after:
no goals
Theorem: pow_le_real
Proof state before:
a x : ℝ
ha1 : a ≠ 1
hx0 : x ≠ 0
ha0 : ¬a ≤ 0
hal1 : a < 1
k : ℕ
hk : (abs x)⁻¹ < a⁻¹ ^ k
⊢ (abs x)⁻¹ < (a ^ k)⁻¹
Tactic:
simpa using hk
Proof state after:
no goals
Theorem: pow_le_real
Proof state before:
a x : ℝ
ha1 : a ≠ 1
hx0 : x ≠ 0
ha0 : ¬a ≤ 0
hal1 : ¬a < 1
k : ℕ
hk : (abs x)⁻¹ < a ^ k
⊢ (abs x)⁻¹ < (a ^ (-↑k))⁻¹
Tactic:
simpa
Proof state after:
no goals
Theorem: float_int_bounded
Proof state before:
α✝ : Type u_1
s : Set α✝
S : ℤ → Prop
b : ℤ
⊢ Set.Nonempty s → (∀ (e : ℤ), e ∈ setOf S → e ≤ b) → ∃ e', is_sup_int S e'
Tactic:
intro hn ha
Proof state after:
α✝ : Type u_1
s : Set α✝
S : ℤ → Prop
b : ℤ
hn : Set.Nonempty s
ha : ∀ (e : ℤ), e ∈ setOf S → e ≤ b
⊢ ∃ e', is_sup_int S e'
Theorem: float_int_bounded
Proof state before:
α✝ : Type u_1
s : Set α✝
S : ℤ → Prop
b : ℤ
hn : Set.Nonempty s
ha : ∀ (e : ℤ), e ∈ setOf S → e ≤ b
⊢ ∃ e', is_sup_int S e'
Tactic:
simp [setOf] at ha
Proof state after:
α✝ : Type u_1
s : Set α✝
S : ℤ → Prop
b : ℤ
hn : Set.Nonempty s
ha : ∀ (e : ℤ), e ∈ S → e ≤ b
⊢ ∃ e', is_sup_int S e'
Theorem: float_int_bounded
Proof state before:
α✝ : Type u_1
s : Set α✝
S : ℤ → Prop
b : ℤ
hn : Set.Nonempty s
ha : ∀ (e : ℤ), e ∈ S → e ≤ b
⊢ ∃ e', is_sup_int S e'
Tactic:
simp [is_sup_int, IsLUB, IsLeast, lowerBounds, upperBounds]
Proof state after:
α✝ : Type u_1
s : Set α✝
S : ℤ → Prop
b : ℤ
hn : Set.Nonempty s
ha : ∀ (e : ℤ), e ∈ S → e ≤ b
⊢ ∃ e', (∀ ⦃a : ℤ⦄, a ∈ S → a ≤ e') ∧ ∀ ⦃a : ℤ⦄, (∀ ⦃a_1 : ℤ⦄, a_1 ∈ S → a_1 ≤ a) → e' ≤ a
Theorem: float_int_bounded
Proof state before:
α✝ : Type u_1
s : Set α✝
S : ℤ → Prop
b : ℤ
hn : Set.Nonempty s
ha : ∀ (e : ℤ), e ∈ S → e ≤ b
⊢ ∃ e', (∀ ⦃a : ℤ⦄, a ∈ S → a ≤ e') ∧ ∀ ⦃a : ℤ⦄, (∀ ⦃a_1 : ℤ⦄, a_1 ∈ S → a_1 ≤ a) → e' ≤ a
Tactic:
sorry
Proof state after:
no goals
Theorem: float_greatest_e_exists
Proof 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
Proof 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
Theorem: float_greatest_e_exists
Proof 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
Proof 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
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 = 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 *
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 }
⊢ ↑fmt_val.r ^ e ≤ 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 }
⊢ ↑fmt_val.r ^ e ≤ abs x ∧ ∀ (e' : ℤ), ↑fmt_val.r ^ e' ≤ abs x → e' ≤ e
Tactic:
apply And.intro
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 }
⊢ ↑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
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 }
⊢ ↑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
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
⊢ ↑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