-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem bitwise_mul_two_pow (of_false_false : f false false = false

Proof state:
case neg
f : Bool → Bool → Bool
x y n : Nat
of_false_false : autoParam (f false false = false) _auto✝
i : Nat
hn : ¬n ≤ i
⊢ (decide (n ≤ i) && f (x.testBit (i - n)) (y.testBit (i - n))) =
    f (decide (n ≤ i) && x.testBit (i - n)) (decide (n ≤ i) && y.testBit (i - n))

Tactic:
simp [hn, of_false_false]

Result:
no goals

Proof state:
f : Bool → Bool → Bool
x y n : Nat
of_false_false : autoParam (f false false = false) _auto✝
⊢ bitwise f x y * 2 ^ n = bitwise f (x * 2 ^ n) (y * 2 ^ n)

Tactic:
apply Nat.eq_of_testBit_eq

Result:
case pred
f : Bool → Bool → Bool
x y n : Nat
of_false_false : autoParam (f false false = false) _auto✝
⊢ ∀ (i : Nat), (bitwise f x y * 2 ^ n).testBit i = (bitwise f (x * 2 ^ n) (y * 2 ^ n)).testBit i

Proof state:
case pred
f : Bool → Bool → Bool
x y n : Nat
of_false_false : autoParam (f false false = false) _auto✝
i : Nat
⊢ (decide (n ≤ i) && f (x.testBit (i - n)) (y.testBit (i - n))) =
    f (decide (n ≤ i) && x.testBit (i - n)) (decide (n ≤ i) && y.testBit (i - n))

Tactic:
by_cases hn : n ≤ i

Result:
case pos
f : Bool → Bool → Bool
x y n : Nat
of_false_false : autoParam (f false false = false) _auto✝
i : Nat
hn : n ≤ i
⊢ (decide (n ≤ i) && f (x.testBit (i - n)) (y.testBit (i - n))) =
    f (decide (n ≤ i) && x.testBit (i - n)) (decide (n ≤ i) && y.testBit (i - n))

case neg
f : Bool → Bool → Bool
x y n : Nat
of_false_false : autoParam (f false false = false) _auto✝
i : Nat
hn : ¬n ≤ i
⊢ (decide (n ≤ i) && f (x.testBit (i - n)) (y.testBit (i - n))) =
    f (decide (n ≤ i) && x.testBit (i - n)) (decide (n ≤ i) && y.testBit (i - n))

Proof state:
case pred
f : Bool → Bool → Bool
x y n : Nat
of_false_false : autoParam (f false false = false) _auto✝
⊢ ∀ (i : Nat),
    (decide (n ≤ i) && f (x.testBit (i - n)) (y.testBit (i - n))) =
      f (decide (n ≤ i) && x.testBit (i - n)) (decide (n ≤ i) && y.testBit (i - n))

Tactic:
intro i

Result:
case pred
f : Bool → Bool → Bool
x y n : Nat
of_false_false : autoParam (f false false = false) _auto✝
i : Nat
⊢ (decide (n ≤ i) && f (x.testBit (i - n)) (y.testBit (i - n))) =
    f (decide (n ≤ i) && x.testBit (i - n)) (decide (n ≤ i) && y.testBit (i - n))

Proof state:
case pred
f : Bool → Bool → Bool
x y n : Nat
of_false_false : autoParam (f false false = false) _auto✝
⊢ ∀ (i : Nat), (bitwise f x y * 2 ^ n).testBit i = (bitwise f (x * 2 ^ n) (y * 2 ^ n)).testBit i

Tactic:
simp only [testBit_mul_two_pow, testBit_bitwise of_false_false, Bool.if_false_right]

Result:
case pred
f : Bool → Bool → Bool
x y n : Nat
of_false_false : autoParam (f false false = false) _auto✝
⊢ ∀ (i : Nat),
    (decide (n ≤ i) && f (x.testBit (i - n)) (y.testBit (i - n))) =
      f (decide (n ≤ i) && x.testBit (i - n)) (decide (n ≤ i) && y.testBit (i - n))

Proof state:
case pos
f : Bool → Bool → Bool
x y n : Nat
of_false_false : autoParam (f false false = false) _auto✝
i : Nat
hn : n ≤ i
⊢ (decide (n ≤ i) && f (x.testBit (i - n)) (y.testBit (i - n))) =
    f (decide (n ≤ i) && x.testBit (i - n)) (decide (n ≤ i) && y.testBit (i - n))

Tactic:
simp [hn]

Result:
no goals