Theorem: xor_eq_propagate (Lean4bits/lemmas.lean)

State before:
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
⊢ xorSeq x y =
    propagate Empty.elim (fun x y => (Empty.elim, _root_.xor (y true) (y false))) fun b => bif b then x else y
Tactic:
ext n
State after:
case h
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ xorSeq x y n =
    propagate Empty.elim (fun x y => (Empty.elim, _root_.xor (y true) (y false))) (fun b => bif b then x else y) n

State before:
case h
α β α' β' : Type
γ : β → Type
x y : ℕ → Bool
n : ℕ
⊢ xorSeq x y n =
    propagate Empty.elim (fun x y => (Empty.elim, _root_.xor (y true) (y false))) (fun b => bif b then x else y) n
Tactic:
cases n <;> simp [propagate, propagateAux, xorSeq]
State after:
no goals