-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem le_of_testBit {n m : Nat} (h : ∀ i, n.testBit i = true → m.testBit i = true) : n ≤ m

Proof state:
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
⊢ n ≤ m

Tactic:
rw [← div_add_mod n 2, ← div_add_mod m 2]

Result:
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
⊢ 2 * (n / 2) + n % 2 ≤ 2 * (m / 2) + m % 2

Proof state:
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
hn : n.testBit 0 = false
⊢ n % 2 = 0

Tactic:
simp at hn

Result:
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
hn : ¬n % 2 = 1
⊢ n % 2 = 0

Proof state:
n m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
⊢ n ≤ m

Tactic:
induction n using div2Induction generalizing m

Result:
case ind
n✝ : Nat
a✝ : n✝ > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n✝ / 2).testBit i = true → m.testBit i = true) → n✝ / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n✝.testBit i = true → m.testBit i = true
⊢ n✝ ≤ m

Proof state:
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
hn : ¬n % 2 = 1
⊢ n % 2 = 0

Tactic:
omega

Result:
no goals

Proof state:
case zero
m : Nat
ih : 0 > 0 → ∀ {m : Nat}, (∀ (i : Nat), (0 / 2).testBit i = true → m.testBit i = true) → 0 / 2 ≤ m
h : ∀ (i : Nat), testBit 0 i = true → m.testBit i = true
⊢ 0 / 2 ≤ m / 2

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
⊢ n / 2 ≤ m / 2

Tactic:
rcases n with (_|n)

Result:
case zero
m : Nat
ih : 0 > 0 → ∀ {m : Nat}, (∀ (i : Nat), (0 / 2).testBit i = true → m.testBit i = true) → 0 / 2 ≤ m
h : ∀ (i : Nat), testBit 0 i = true → m.testBit i = true
⊢ 0 / 2 ≤ m / 2

case succ
m n : Nat
ih : n + 1 > 0 → ∀ {m : Nat}, (∀ (i : Nat), ((n + 1) / 2).testBit i = true → m.testBit i = true) → (n + 1) / 2 ≤ m
h : ∀ (i : Nat), (n + 1).testBit i = true → m.testBit i = true
⊢ (n + 1) / 2 ≤ m / 2

Proof state:
case true
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
hn : n.testBit 0 = true
hn2 : n % 2 = 1
hm2 : m % 2 = 1
⊢ 2 * (n / 2) + n % 2 ≤ 2 * (m / 2) + m % 2

Tactic:
omega

Result:
no goals

Proof state:
case true
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
hn : n.testBit 0 = true
⊢ 2 * (n / 2) + n % 2 ≤ 2 * (m / 2) + m % 2

Tactic:
have hn2 : n % 2 = 1 := by simpa using hn

Result:
case true
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
hn : n.testBit 0 = true
hn2 : n % 2 = 1
⊢ 2 * (n / 2) + n % 2 ≤ 2 * (m / 2) + m % 2

Proof state:
m n : Nat
ih : n + 1 > 0 → ∀ {m : Nat}, (∀ (i : Nat), ((n + 1) / 2).testBit i = true → m.testBit i = true) → (n + 1) / 2 ≤ m
h : ∀ (i : Nat), (n + 1).testBit i = true → m.testBit i = true
i : Nat
⊢ ((n + 1) / 2).testBit i = true → (m / 2).testBit i = true

Tactic:
simpa using h (i + 1)

Result:
no goals

Proof state:
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
hn : n.testBit 0 = true
hn2 : n % 2 = 1
⊢ m % 2 = 1

Tactic:
simpa using h _ hn

Result:
no goals

Proof state:
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
⊢ 2 * (n / 2) + n % 2 ≤ 2 * (m / 2) + m % 2

Tactic:
cases hn : n.testBit 0

Result:
case false
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
hn : n.testBit 0 = false
⊢ 2 * (n / 2) + n % 2 ≤ 2 * (m / 2) + m % 2

case true
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
hn : n.testBit 0 = true
⊢ 2 * (n / 2) + n % 2 ≤ 2 * (m / 2) + m % 2

Proof state:
case false
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
hn : n.testBit 0 = false
hn2 : n % 2 = 0
⊢ 2 * (n / 2) + n % 2 ≤ 2 * (m / 2) + m % 2

Tactic:
rw [hn2]

Result:
case false
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
hn : n.testBit 0 = false
hn2 : n % 2 = 0
⊢ 2 * (n / 2) + 0 ≤ 2 * (m / 2) + m % 2

Proof state:
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
hn : n.testBit 0 = true
⊢ n % 2 = 1

Tactic:
simpa using hn

Result:
no goals

Proof state:
case false
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
hn : n.testBit 0 = false
⊢ 2 * (n / 2) + n % 2 ≤ 2 * (m / 2) + m % 2

Tactic:
have hn2 : n % 2 = 0 := by simp at hn; omega

Result:
case false
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
hn : n.testBit 0 = false
hn2 : n % 2 = 0
⊢ 2 * (n / 2) + n % 2 ≤ 2 * (m / 2) + m % 2

Proof state:
case false
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
hn : n.testBit 0 = false
hn2 : n % 2 = 0
⊢ 2 * (n / 2) + 0 ≤ 2 * (m / 2) + m % 2

Tactic:
omega

Result:
no goals

Proof state:
case true
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
hn : n.testBit 0 = true
hn2 : n % 2 = 1
⊢ 2 * (n / 2) + n % 2 ≤ 2 * (m / 2) + m % 2

Tactic:
have hm2 : m % 2 = 1 := by simpa using h _ hn

Result:
case true
n : Nat
ih : n > 0 → ∀ {m : Nat}, (∀ (i : Nat), (n / 2).testBit i = true → m.testBit i = true) → n / 2 ≤ m
m : Nat
h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true
this : n / 2 ≤ m / 2
hn : n.testBit 0 = true
hn2 : n % 2 = 1
hm2 : m % 2 = 1
⊢ 2 * (n / 2) + n % 2 ≤ 2 * (m / 2) + m % 2

Proof state:
case succ
m n : Nat
ih : n + 1 > 0 → ∀ {m : Nat}, (∀ (i : Nat), ((n + 1) / 2).testBit i = true → m.testBit i = true) → (n + 1) / 2 ≤ m
h : ∀ (i : Nat), (n + 1).testBit i = true → m.testBit i = true
⊢ (n + 1) / 2 ≤ m / 2

Tactic:
exact ih (Nat.succ_pos _) fun i => by simpa using h (i + 1)

Result:
no goals