-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem ne_implies_bit_diff {x y : Nat} (p : x ≠ y) : ∃ i, testBit x i ≠ testBit y i

Proof state:
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
p : x ≠ y
ypos : y > 0
lsb_diff : ¬x % 2 = y % 2
⊢ ∃ i, x.testBit i ≠ y.testBit i

Tactic:
apply Exists.intro 0

Result:
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
p : x ≠ y
ypos : y > 0
lsb_diff : ¬x % 2 = y % 2
⊢ x.testBit 0 ≠ y.testBit 0

Proof state:
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
p : 2 * (x / 2) + x % 2 ≠ 2 * (y / 2) + y % 2
ypos : y > 0
lsb_diff : x % 2 = y % 2
⊢ ∃ i, x.testBit i ≠ y.testBit i

Tactic:
simp only [ne_eq, lsb_diff, Nat.add_right_cancel_iff,
  Nat.zero_lt_succ, Nat.mul_left_cancel_iff] at p

Result:
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
ypos : y > 0
lsb_diff : x % 2 = y % 2
p : ¬x / 2 = y / 2
⊢ ∃ i, x.testBit i ≠ y.testBit i

Proof state:
case ind
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
p : x ≠ y
⊢ ∃ i, x.testBit i ≠ y.testBit i

Tactic:
cases Nat.eq_zero_or_pos y with
| inl yz =>
  simp only [yz, Nat.zero_testBit, Bool.eq_false_iff]
  simp only [yz] at p
  have ⟨i,ip⟩  := ne_zero_implies_bit_true p
  apply Exists.intro i
  simp [ip]
| inr ypos =>
  if lsb_diff : x % 2 = y % 2 then
    rw [←Nat.div_add_mod x 2, ←Nat.div_add_mod y 2] at p
    simp only [ne_eq, lsb_diff, Nat.add_right_cancel_iff,
      Nat.zero_lt_succ, Nat.mul_left_cancel_iff] at p
    have ⟨i, ieq⟩  := hyp ypos p
    apply Exists.intro (i+1)
    simpa
  else
    apply Exists.intro 0
    simp only [testBit_zero]
    revert lsb_diff
    cases mod_two_eq_zero_or_one x with | _ p =>
      cases mod_two_eq_zero_or_one y with | _ q =>
        simp [p,q]

Result:
no goals

Proof state:
case ind.inl
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
yz : y = 0
p : x ≠ 0
i : Nat
ip : x.testBit i = true
⊢ x.testBit i ≠ false

Tactic:
simp [ip]

Result:
no goals

Proof state:
case ind.inl
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
p : x ≠ y
yz : y = 0
⊢ ∃ i, x.testBit i ≠ false

Tactic:
simp only [yz] at p

Result:
case ind.inl
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
yz : y = 0
p : x ≠ 0
⊢ ∃ i, x.testBit i ≠ false

Proof state:
case ind.inr
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
p : x ≠ y
ypos : y > 0
⊢ ∃ i, x.testBit i ≠ y.testBit i

Tactic:
if lsb_diff : x % 2 = y % 2 then
  rw [←Nat.div_add_mod x 2, ←Nat.div_add_mod y 2] at p
  simp only [ne_eq, lsb_diff, Nat.add_right_cancel_iff,
    Nat.zero_lt_succ, Nat.mul_left_cancel_iff] at p
  have ⟨i, ieq⟩  := hyp ypos p
  apply Exists.intro (i+1)
  simpa
else
  apply Exists.intro 0
  simp only [testBit_zero]
  revert lsb_diff
  cases mod_two_eq_zero_or_one x with | _ p =>
    cases mod_two_eq_zero_or_one y with | _ q =>
      simp [p,q]

Result:
no goals

Proof state:
case ind.inl
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
yz : y = 0
p : x ≠ 0
⊢ ∃ i, x.testBit i ≠ false

Tactic:
have ⟨i,ip⟩  := ne_zero_implies_bit_true p

Result:
case ind.inl
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
yz : y = 0
p : x ≠ 0
i : Nat
ip : x.testBit i = true
⊢ ∃ i, x.testBit i ≠ false

Proof state:
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
ypos : y > 0
lsb_diff : x % 2 = y % 2
p : ¬x / 2 = y / 2
i : Nat
ieq : (x / 2).testBit i ≠ (y / 2).testBit i
⊢ x.testBit (i + 1) ≠ y.testBit (i + 1)

Tactic:
simpa

Result:
no goals

Proof state:
case ind.inl
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
yz : y = 0
p : x ≠ 0
i : Nat
ip : x.testBit i = true
⊢ ∃ i, x.testBit i ≠ false

Tactic:
apply Exists.intro i

Result:
case ind.inl
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
yz : y = 0
p : x ≠ 0
i : Nat
ip : x.testBit i = true
⊢ x.testBit i ≠ false

Proof state:
x y : Nat
p : x ≠ y
⊢ ∃ i, x.testBit i ≠ y.testBit i

Tactic:
induction y using Nat.div2Induction generalizing x with
| ind y hyp =>
  cases Nat.eq_zero_or_pos y with
  | inl yz =>
    simp only [yz, Nat.zero_testBit, Bool.eq_false_iff]
    simp only [yz] at p
    have ⟨i,ip⟩  := ne_zero_implies_bit_true p
    apply Exists.intro i
    simp [ip]
  | inr ypos =>
    if lsb_diff : x % 2 = y % 2 then
      rw [←Nat.div_add_mod x 2, ←Nat.div_add_mod y 2] at p
      simp only [ne_eq, lsb_diff, Nat.add_right_cancel_iff,
        Nat.zero_lt_succ, Nat.mul_left_cancel_iff] at p
      have ⟨i, ieq⟩  := hyp ypos p
      apply Exists.intro (i+1)
      simpa
    else
      apply Exists.intro 0
      simp only [testBit_zero]
      revert lsb_diff
      cases mod_two_eq_zero_or_one x with | _ p =>
        cases mod_two_eq_zero_or_one y with | _ q =>
          simp [p,q]

Result:
no goals

Proof state:
case ind.inl
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
p : x ≠ y
yz : y = 0
⊢ ∃ i, x.testBit i ≠ y.testBit i

Tactic:
simp only [yz, Nat.zero_testBit, Bool.eq_false_iff]

Result:
case ind.inl
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
p : x ≠ y
yz : y = 0
⊢ ∃ i, x.testBit i ≠ false

Proof state:
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
p : x ≠ y
ypos : y > 0
lsb_diff : ¬x % 2 = y % 2
⊢ decide (x % 2 = 1) ≠ decide (y % 2 = 1)

Tactic:
revert lsb_diff

Result:
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
p : x ≠ y
ypos : y > 0
⊢ ¬x % 2 = y % 2 → decide (x % 2 = 1) ≠ decide (y % 2 = 1)

Proof state:
case inr.inr
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
p✝ : x ≠ y
ypos : y > 0
p : x % 2 = 1
q : y % 2 = 1
⊢ ¬x % 2 = y % 2 → decide (x % 2 = 1) ≠ decide (y % 2 = 1)

Tactic:
simp [p,q]

Result:
no goals

Proof state:
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
p : x ≠ y
ypos : y > 0
lsb_diff : x % 2 = y % 2
⊢ ∃ i, x.testBit i ≠ y.testBit i

Tactic:
rw [←Nat.div_add_mod x 2, ←Nat.div_add_mod y 2] at p

Result:
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
p : 2 * (x / 2) + x % 2 ≠ 2 * (y / 2) + y % 2
ypos : y > 0
lsb_diff : x % 2 = y % 2
⊢ ∃ i, x.testBit i ≠ y.testBit i

Proof state:
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
p : x ≠ y
ypos : y > 0
lsb_diff : ¬x % 2 = y % 2
⊢ x.testBit 0 ≠ y.testBit 0

Tactic:
simp only [testBit_zero]

Result:
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
p : x ≠ y
ypos : y > 0
lsb_diff : ¬x % 2 = y % 2
⊢ decide (x % 2 = 1) ≠ decide (y % 2 = 1)

Proof state:
y : Nat
hyp : y > 0 → ∀ {x : Nat}, x ≠ y / 2 → ∃ i, x.testBit i ≠ (y / 2).testBit i
x : Nat
p : x ≠ y
ypos : y > 0
⊢ ¬x % 2 = y % 2 → decide (x % 2 = 1) ≠ decide (y % 2 = 1)

Tactic:
cases mod_two_eq_zero_or_one x with | _ p =>
  cases mod_two_eq_zero_or_one y with | _ q =>
    simp [p,q]

Result:
no goals