internlm/Lean-Github huggingface dataset:
Theorem: Bool.majoritySelect_fin
Proof state before:
⊢ majoritySelect (decide (↑0 = 1)) (decide (↑0 = 1)) (decide (↑0 = 1)) = decide ((↑0 + ↑0 + ↑0) / 2 = 1)
Tactic:
decide
Proof state after:
no goals
Theorem: Bool.majoritySelect_fin
Proof state before:
⊢ majoritySelect (decide (↑0 = 1)) (decide (↑0 = 1)) (decide (↑1 = 1)) = decide ((↑0 + ↑0 + ↑1) / 2 = 1)
Tactic:
decide
Proof state after:
no goals
Theorem: Bool.majoritySelect_fin
Proof state before:
⊢ majoritySelect (decide (↑0 = 1)) (decide (↑1 = 1)) (decide (↑0 = 1)) = decide ((↑0 + ↑1 + ↑0) / 2 = 1)
Tactic:
decide
Proof state after:
no goals
Theorem: Bool.majoritySelect_fin
Proof state before:
⊢ majoritySelect (decide (↑0 = 1)) (decide (↑1 = 1)) (decide (↑1 = 1)) = decide ((↑0 + ↑1 + ↑1) / 2 = 1)
Tactic:
decide
Proof state after:
no goals
Theorem: Bool.majoritySelect_fin
Proof state before:
⊢ majoritySelect (decide (↑1 = 1)) (decide (↑0 = 1)) (decide (↑0 = 1)) = decide ((↑1 + ↑0 + ↑0) / 2 = 1)
Tactic:
decide
Proof state after:
no goals
Theorem: Bool.majoritySelect_fin
Proof state before:
⊢ majoritySelect (decide (↑1 = 1)) (decide (↑0 = 1)) (decide (↑1 = 1)) = decide ((↑1 + ↑0 + ↑1) / 2 = 1)
Tactic:
decide
Proof state after:
no goals
Theorem: Bool.majoritySelect_fin
Proof state before:
⊢ majoritySelect (decide (↑1 = 1)) (decide (↑1 = 1)) (decide (↑0 = 1)) = decide ((↑1 + ↑1 + ↑0) / 2 = 1)
Tactic:
decide
Proof state after:
no goals
Theorem: Bool.majoritySelect_fin
Proof state before:
⊢ majoritySelect (decide (↑1 = 1)) (decide (↑1 = 1)) (decide (↑1 = 1)) = decide ((↑1 + ↑1 + ↑1) / 2 = 1)
Tactic:
decide
Proof state after:
no goals
Theorem: Bool.xor₃_fin
Proof state before:
⊢ xor₃ (decide (↑0 = 1)) (decide (↑0 = 1)) (decide (↑0 = 1)) = decide ((↑0 + ↑0 + ↑0) % 2 = 1)
Tactic:
decide
Proof state after:
no goals
Theorem: Bool.xor₃_fin
Proof state before:
⊢ xor₃ (decide (↑0 = 1)) (decide (↑0 = 1)) (decide (↑1 = 1)) = decide ((↑0 + ↑0 + ↑1) % 2 = 1)
Tactic:
decide
Proof state after:
no goals
Theorem: Bool.xor₃_fin
Proof state before:
⊢ xor₃ (decide (↑0 = 1)) (decide (↑1 = 1)) (decide (↑0 = 1)) = decide ((↑0 + ↑1 + ↑0) % 2 = 1)
Tactic:
decide
Proof state after:
no goals
Theorem: Bool.xor₃_fin
Proof state before:
⊢ xor₃ (decide (↑0 = 1)) (decide (↑1 = 1)) (decide (↑1 = 1)) = decide ((↑0 + ↑1 + ↑1) % 2 = 1)
Tactic:
decide
Proof state after:
no goals
Theorem: Bool.xor₃_fin
Proof state before:
⊢ xor₃ (decide (↑1 = 1)) (decide (↑0 = 1)) (decide (↑0 = 1)) = decide ((↑1 + ↑0 + ↑0) % 2 = 1)
Tactic:
decide
Proof state after:
no goals
Theorem: Bool.xor₃_fin
Proof state before:
⊢ xor₃ (decide (↑1 = 1)) (decide (↑0 = 1)) (decide (↑1 = 1)) = decide ((↑1 + ↑0 + ↑1) % 2 = 1)
Tactic:
decide
Proof state after:
no goals
Theorem: Bool.xor₃_fin
Proof state before:
⊢ xor₃ (decide (↑1 = 1)) (decide (↑1 = 1)) (decide (↑0 = 1)) = decide ((↑1 + ↑1 + ↑0) % 2 = 1)
Tactic:
decide
Proof state after:
no goals
Theorem: Bool.xor₃_fin
Proof state before:
⊢ xor₃ (decide (↑1 = 1)) (decide (↑1 = 1)) (decide (↑1 = 1)) = decide ((↑1 + ↑1 + ↑1) % 2 = 1)
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.not_mod2_eq_zero
Proof state before:
n : ℕ
⊢ ¬n % 2 = 0 ↔ n % 2 = 1
Tactic:
cases n using binaryRec with
| z => simp
| f b _ _ => cases b <;> simp [← Nat.two_mul, Nat.mul_add_mod]
Proof state after:
no goals
Theorem: Nat.not_mod2_eq_zero
Proof state before:
case z

⊢ ¬0 % 2 = 0 ↔ 0 % 2 = 1
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.not_mod2_eq_zero
Proof state before:
case f
b : Bool
n✝ : ℕ
a✝ : bit b n✝ = n✝ → (¬bit b n✝ % 2 = 0 ↔ bit b n✝ % 2 = 1)
⊢ ¬bit b n✝ % 2 = 0 ↔ bit b n✝ % 2 = 1
Tactic:
cases b <;> simp [← Nat.two_mul, Nat.mul_add_mod]
Proof state after:
no goals
Theorem: Nat.log_mul
Proof state before:
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n) = log b n + 1
Tactic:
apply le_antisymm
Proof state after:
case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n) ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Theorem: Nat.log_mul
Proof state before:
case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n) ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply le_of_eq_of_le
Proof state after:
case a.h₁
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n) = ?a.b✝

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ ?a.b✝ ≤ log b n + 1

case a.b
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ ℕ

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Theorem: Nat.log_mul
Proof state before:
case a.h₁
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n) = ?a.b✝

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ ?a.b✝ ≤ log b n + 1

case a.b
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ ℕ

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply Nat.log_of_one_lt_of_le hb
Proof state after:
case a.h₁
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ≤ b * n

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) + 1 ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Theorem: Nat.log_mul
Proof state before:
case a.h₁
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ≤ b * n

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) + 1 ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply le_of_eq_of_le
Proof state after:
case a.h₁.h₁
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b = ?a.h₁.b✝

case a.h₁.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ ?a.h₁.b✝ ≤ b * n

case a.h₁.b
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ ℕ

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) + 1 ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Theorem: Nat.log_mul
Proof state before:
case a.h₁.h₁
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b = ?a.h₁.b✝

case a.h₁.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ ?a.h₁.b✝ ≤ b * n

case a.h₁.b
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ ℕ

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) + 1 ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply (mul_one _).symm
Proof state after:
case a.h₁.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b * 1 ≤ b * n

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) + 1 ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Theorem: Nat.log_mul
Proof state before:
case a.h₁.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b * 1 ≤ b * n

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) + 1 ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply mul_le_mul (le_refl _) hn (zero_le _) (zero_le _)
Proof state after:
case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) + 1 ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Theorem: Nat.log_mul
Proof state before:
case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) + 1 ≤ log b n + 1

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply Nat.succ_le_succ
Proof state after:
case a.h₂.a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) ≤ log b n

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Theorem: Nat.log_mul
Proof state before:
case a.h₂.a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b (b * n / b) ≤ log b n

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply Nat.log_mono_right
Proof state after:
case a.h₂.a.h
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b * n / b ≤ n

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Theorem: Nat.log_mul
Proof state before:
case a.h₂.a.h
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b * n / b ≤ n

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply le_of_eq
Proof state after:
case a.h₂.a.h.a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b * n / b = n

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Theorem: Nat.log_mul
Proof state before:
case a.h₂.a.h.a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b * n / b = n

case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
rw [Nat.mul_div_right _ (lt_trans zero_lt_one hb)]
Proof state after:
case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Theorem: Nat.log_mul
Proof state before:
case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ log b n + 1 ≤ log b (b * n)
Tactic:
apply Nat.le_log_of_pow_le hb
Proof state after:
case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ^ (log b n + 1) ≤ b * n
Theorem: Nat.log_mul
Proof state before:
case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ^ (log b n + 1) ≤ b * n
Tactic:
rw [Nat.pow_succ, mul_comm]
Proof state after:
case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b * b ^ log b n ≤ b * n
Theorem: Nat.log_mul
Proof state before:
case a
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b * b ^ log b n ≤ b * n
Tactic:
apply mul_le_mul
Proof state after:
case a.h₁
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ≤ b

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ^ log b n ≤ n

case a.c0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b ^ log b n

case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b
Theorem: Nat.log_mul
Proof state before:
case a.h₁
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ≤ b

case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ^ log b n ≤ n

case a.c0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b ^ log b n

case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b
Tactic:
apply le_refl
Proof state after:
case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ^ log b n ≤ n

case a.c0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b ^ log b n

case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b
Theorem: Nat.log_mul
Proof state before:
case a.h₂
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ b ^ log b n ≤ n

case a.c0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b ^ log b n

case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b
Tactic:
apply Nat.pow_log_le_self
Proof state after:
case a.h₂.hx
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ n ≠ 0

case a.c0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b ^ log b n

case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b
Theorem: Nat.log_mul
Proof state before:
case a.h₂.hx
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ n ≠ 0

case a.c0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b ^ log b n

case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b
Tactic:
apply ne_of_lt' (Nat.lt_of_succ_le hn)
Proof state after:
case a.c0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b ^ log b n

case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b
Theorem: Nat.log_mul
Proof state before:
case a.c0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b ^ log b n

case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b
Tactic:
apply zero_le
Proof state after:
case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b
Theorem: Nat.log_mul
Proof state before:
case a.b0
b n : ℕ
hb : 1 < b
hn : 1 ≤ n
⊢ 0 ≤ b
Tactic:
apply zero_le
Proof state after:
no goals
Theorem: Nat.log_mul_add
Proof state before:
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b (b * n + c) = log b n + 1
Tactic:
apply le_antisymm
Proof state after:
case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b (b * n + c) ≤ log b n + 1

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Theorem: Nat.log_mul_add
Proof state before:
case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b (b * n + c) ≤ log b n + 1

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply le_of_eq_of_le
Proof state after:
case a.h₁
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b (b * n + c) = ?a.b✝

case a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ?a.b✝ ≤ log b n + 1

case a.b
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ℕ

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Theorem: Nat.log_mul_add
Proof state before:
case a.h₁
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b (b * n + c) = ?a.b✝

case a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ?a.b✝ ≤ log b n + 1

case a.b
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ℕ

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply Nat.log_of_one_lt_of_le hb
Proof state after:
case a.h₁
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ b ≤ b * n + c

case a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b ((b * n + c) / b) + 1 ≤ log b n + 1

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Theorem: Nat.log_mul_add
Proof state before:
case a.h₁
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ b ≤ b * n + c

case a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b ((b * n + c) / b) + 1 ≤ log b n + 1

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply add_le_add _ (zero_le _)
Proof state after:
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ b ≤ b * n

case a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b ((b * n + c) / b) + 1 ≤ log b n + 1

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Theorem: Nat.log_mul_add
Proof state before:
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ b ≤ b * n

case a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b ((b * n + c) / b) + 1 ≤ log b n + 1

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply le_of_eq_of_le
Proof state after:
case h₁
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ b = ?b

case h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ?b ≤ b * n

case b
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ℕ

case a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b ((b * n + c) / b) + 1 ≤ log b n + 1

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Theorem: Nat.log_mul_add
Proof state before:
case h₁
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ b = ?b

case h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ?b ≤ b * n

case b
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ℕ

case a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b ((b * n + c) / b) + 1 ≤ log b n + 1

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply (mul_one _).symm
Proof state after:
case h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ b * 1 ≤ b * n

case a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b ((b * n + c) / b) + 1 ≤ log b n + 1

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Theorem: Nat.log_mul_add
Proof state before:
case h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ b * 1 ≤ b * n

case a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b ((b * n + c) / b) + 1 ≤ log b n + 1

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply mul_le_mul (le_refl _) hn (zero_le _) (zero_le _)
Proof state after:
case a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b ((b * n + c) / b) + 1 ≤ log b n + 1

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Theorem: Nat.log_mul_add
Proof state before:
case a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b ((b * n + c) / b) + 1 ≤ log b n + 1

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply Nat.succ_le_succ
Proof state after:
case a.h₂.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b ((b * n + c) / b) ≤ log b n

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Theorem: Nat.log_mul_add
Proof state before:
case a.h₂.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b ((b * n + c) / b) ≤ log b n

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply Nat.log_mono_right
Proof state after:
case a.h₂.a.h
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ (b * n + c) / b ≤ n

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Theorem: Nat.log_mul_add
Proof state before:
case a.h₂.a.h
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ (b * n + c) / b ≤ n

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply le_of_eq
Proof state after:
case a.h₂.a.h.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ (b * n + c) / b = n

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Theorem: Nat.log_mul_add
Proof state before:
case a.h₂.a.h.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ (b * n + c) / b = n

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply Eq.trans
Proof state after:
case a.h₂.a.h.a.h₁
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ (b * n + c) / b = ?a.h₂.a.h.a.b✝

case a.h₂.a.h.a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ?a.h₂.a.h.a.b✝ = n

case a.h₂.a.h.a.b
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ℕ

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Theorem: Nat.log_mul_add
Proof state before:
case a.h₂.a.h.a.h₁
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ (b * n + c) / b = ?a.h₂.a.h.a.b✝

case a.h₂.a.h.a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ?a.h₂.a.h.a.b✝ = n

case a.h₂.a.h.a.b
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ℕ

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply Nat.mul_add_div (lt_trans zero_lt_one hb)
Proof state after:
case a.h₂.a.h.a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ n + c / b = n

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Theorem: Nat.log_mul_add
Proof state before:
case a.h₂.a.h.a.h₂
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ n + c / b = n

case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply congrArg _ (Nat.div_eq_of_lt hc)
Proof state after:
case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Theorem: Nat.log_mul_add
Proof state before:
case a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ log b (b * n + c)
Tactic:
apply le_trans
Proof state after:
case a.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ ?a.b✝

case a.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ?a.b✝ ≤ log b (b * n + c)

case a.b
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ℕ
Theorem: Nat.log_mul_add
Proof state before:
case a.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b n + 1 ≤ ?a.b✝

case a.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ?a.b✝ ≤ log b (b * n + c)

case a.b
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ ℕ
Tactic:
rw [← Nat.log_mul hb hn]
Proof state after:
case a.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b (b * n) ≤ log b (b * n + c)
Theorem: Nat.log_mul_add
Proof state before:
case a.a
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ log b (b * n) ≤ log b (b * n + c)
Tactic:
apply Nat.log_mono_right
Proof state after:
case a.a.h
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ b * n ≤ b * n + c
Theorem: Nat.log_mul_add
Proof state before:
case a.a.h
b n c : ℕ
hb : 1 < b
hn : 1 ≤ n
hc : c < b
⊢ b * n ≤ b * n + c
Tactic:
apply le_add_right
Proof state after:
no goals
Theorem: Nat.size_le_succ_log
Proof state before:
n : ℕ
⊢ size n ≤ log 2 n + 1
Tactic:
refine binaryRec' (n := n) ?hz ?hi
Proof state after:
case hz
n : ℕ
⊢ size 0 ≤ log 2 0 + 1

case hi
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), (n = 0 → b = true) → size n ≤ log 2 n + 1 → size (bit b n) ≤ log 2 (bit b n) + 1
Theorem: Nat.size_le_succ_log
Proof state before:
case hz
n : ℕ
⊢ size 0 ≤ log 2 0 + 1

case hi
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), (n = 0 → b = true) → size n ≤ log 2 n + 1 → size (bit b n) ≤ log 2 (bit b n) + 1
Tactic:
exact zero_le _
Proof state after:
case hi
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), (n = 0 → b = true) → size n ≤ log 2 n + 1 → size (bit b n) ≤ log 2 (bit b n) + 1
Theorem: Nat.size_le_succ_log
Proof state before:
case hi
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), (n = 0 → b = true) → size n ≤ log 2 n + 1 → size (bit b n) ≤ log 2 (bit b n) + 1
Tactic:
intro b n hb ih
Proof state after:
case hi
n✝ : ℕ
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ log 2 n + 1
⊢ size (bit b n) ≤ log 2 (bit b n) + 1
Theorem: Nat.size_le_succ_log
Proof state before:
case hi
n✝ : ℕ
b : Bool
n : ℕ
hb : n = 0 → b = true
ih : size n ≤ log 2 n + 1
⊢ size (bit b n) ≤ log 2 (bit b n) + 1
Tactic:
cases n
Proof state after:
case hi.zero
n : ℕ
b : Bool
hb : zero = 0 → b = true
ih : size zero ≤ log 2 zero + 1
⊢ size (bit b zero) ≤ log 2 (bit b zero) + 1

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ size (bit b (succ n✝)) ≤ log 2 (bit b (succ n✝)) + 1
Theorem: Nat.size_le_succ_log
Proof state before:
case hi.zero
n : ℕ
b : Bool
hb : zero = 0 → b = true
ih : size zero ≤ log 2 zero + 1
⊢ size (bit b zero) ≤ log 2 (bit b zero) + 1

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ size (bit b (succ n✝)) ≤ log 2 (bit b (succ n✝)) + 1
Tactic:
cases b <;> simp
Proof state after:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ size (bit b (succ n✝)) ≤ log 2 (bit b (succ n✝)) + 1
Theorem: Nat.size_le_succ_log
Proof state before:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ size (bit b (succ n✝)) ≤ log 2 (bit b (succ n✝)) + 1
Tactic:
rw [size_bit, bit_val, Nat.log_mul_add]
Proof state after:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ succ (size (succ n✝)) ≤ log 2 (succ n✝) + 1 + 1

case hi.succ.hb
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 < 2

case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0
Theorem: Nat.size_le_succ_log
Proof state before:
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ succ (size (succ n✝)) ≤ log 2 (succ n✝) + 1 + 1

case hi.succ.hb
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 < 2

case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0
Tactic:
apply Nat.succ_le_succ ih
Proof state after:
case hi.succ.hb
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 < 2

case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0
Theorem: Nat.size_le_succ_log
Proof state before:
case hi.succ.hb
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 < 2

case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0
Tactic:
apply one_lt_two
Proof state after:
case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) ≤ log 2 (succ n✝) + 1
⊢ bit b (succ n✝) ≠ 0