Theorem: size_of_le_of_lt (Fl/Lemmas.lean)

State before:
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ Nat.size x = n
Tactic:
apply Nat.le_antisymm
State after:
case h₁
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ Nat.size x ≤ n

case h₂
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ n ≤ Nat.size x

State before:
case h₁
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ Nat.size x ≤ n

case h₂
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ n ≤ Nat.size x
Tactic:
. rewrite [Nat.size_le]
  exact hr
State after:
case h₂
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ n ≤ Nat.size x

State before:
case h₂
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ n ≤ Nat.size x
Tactic:
. apply Nat.le_of_pred_lt
  rewrite [← Nat.sub_one, Nat.lt_size]
  exact hl
State after:
no goals

State before:
case h₁
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ Nat.size x ≤ n
Tactic:
rewrite [Nat.size_le]
State after:
case h₁
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ x < 2 ^ n

State before:
case h₁
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ x < 2 ^ n
Tactic:
exact hr
State after:
no goals

State before:
case h₂
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ n ≤ Nat.size x
Tactic:
apply Nat.le_of_pred_lt
State after:
case h₂.a
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ Nat.pred n < Nat.size x

State before:
case h₂.a
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ Nat.pred n < Nat.size x
Tactic:
rewrite [← Nat.sub_one, Nat.lt_size]
State after:
case h₂.a
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ 2 ^ (n - 1) ≤ x

State before:
case h₂.a
x n : ℕ
hl : 2 ^ (n - 1) ≤ x
hr : x < 2 ^ n
⊢ 2 ^ (n - 1) ≤ x
Tactic:
exact hl
State after:
no goals