Theorem: propagate_succ2 (Lean4bits/lemmas.lean)

State before:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β → ℕ → Bool
i : ℕ
⊢ propagate init_carry next_bit x (i + 1) =
    (next_bit (propagateCarry2 init_carry (fun c b => (next_bit c b).fst) x (i + 1)) fun j => x j (i + 1)).snd
Tactic:
rw [propagateCarry2_succ, ← propagateAux_fst_eq_carry]
State after:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β → ℕ → Bool
i : ℕ
⊢ propagate init_carry next_bit x (i + 1) =
    (next_bit (propagateAux init_carry (fun c b => next_bit c b) x i).fst fun j => x j (i + 1)).snd

State before:
α β α' β' : Type
γ : β → Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β → ℕ → Bool
i : ℕ
⊢ propagate init_carry next_bit x (i + 1) =
    (next_bit (propagateAux init_carry (fun c b => next_bit c b) x i).fst fun j => x j (i + 1)).snd
Tactic:
rfl
State after:
no goals