Theorem: ls_eq_propagate (Lean4bits/lemmas.lean)

State before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
⊢ lsSeq x = propagate (fun x => false) (fun carry x => (x, carry ())) fun x_1 => x
Tactic:
ext n
State after:
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ lsSeq x n = propagate (fun x => false) (fun carry x => (x, carry ())) (fun x_1 => x) n

State before:
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ lsSeq x n = propagate (fun x => false) (fun carry x => (x, carry ())) (fun x_1 => x) n
Tactic:
match n with
| 0 => rfl
| 1 => rfl
| n+2 => simp [lsSeq, propagate_succ]
State after:
no goals

State before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ lsSeq x 0 = propagate (fun x => false) (fun carry x => (x, carry ())) (fun x_1 => x) 0
Tactic:
rfl
State after:
no goals

State before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ lsSeq x 1 = propagate (fun x => false) (fun carry x => (x, carry ())) (fun x_1 => x) 1
Tactic:
rfl
State after:
no goals

State before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n✝ n : ℕ
⊢ lsSeq x (n + 2) = propagate (fun x => false) (fun carry x => (x, carry ())) (fun x_1 => x) (n + 2)
Tactic:
simp [lsSeq, propagate_succ]
State after:
no goals