Theorem: propagateCarry_propagateCarry_add (Lean4bits/lemmas.lean)

State before:
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
x : β → ℕ → Bool
init_carry : α → Bool
_next_carry : (α → Bool) → (β → Bool) → α → Bool
⊢ propagateCarry2 (propagateCarry2 init_carry _next_carry x 0) _next_carry (fun b k => x b (k + 0)) 0 =
    propagateCarry2 init_carry _next_carry x (0 + 0)
Tactic:
simp [propagateCarry2]
State after:
no goals

State before:
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
x : β → ℕ → Bool
init_carry : α → Bool
next_carr : (α → Bool) → (β → Bool) → α → Bool
n : ℕ
⊢ propagateCarry2 (propagateCarry2 init_carry next_carr x (n + 1)) next_carr (fun b k => x b (k + (n + 1))) 0 =
    propagateCarry2 init_carry next_carr x (0 + (n + 1))
Tactic:
simp [propagateCarry, propagateCarry2_succ]
State after:
no goals

State before:
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry✝ : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
x : β → ℕ → Bool
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
n i : ℕ
⊢ propagateCarry2 (propagateCarry2 init_carry next_carry x n) next_carry (fun b k => x b (k + n)) (i + 1) =
    propagateCarry2 init_carry next_carry x (i + 1 + n)
Tactic:
rw [propagateCarry2, add_assoc,
  propagateCarry_propagateCarry_add _ _ _ _ i]
State after:
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry✝ : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
x : β → ℕ → Bool
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
n i : ℕ
⊢ (next_carry (propagateCarry2 init_carry next_carry x (i + n)) fun i_1 => x i_1 (i + n)) =
    propagateCarry2 init_carry next_carry x (i + (1 + n))

State before:
α β α' β' : Type
γ : β → Type
init_carry✝ : α → Bool
next_carry✝ : (α → Bool) → (β → Bool) → α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
inst✝¹ : Fintype α
inst✝ : Fintype α'
x : β → ℕ → Bool
init_carry : α → Bool
next_carry : (α → Bool) → (β → Bool) → α → Bool
n i : ℕ
⊢ (next_carry (propagateCarry2 init_carry next_carry x (i + n)) fun i_1 => x i_1 (i + n)) =
    propagateCarry2 init_carry next_carry x (i + (1 + n))
Tactic:
simp only [Nat.one_add, Nat.add_one, Nat.succ_add, Nat.add_succ,
  add_zero, propagateCarry2, zero_add]
State after:
no goals