Theorem: propagateCarry_changeVars (Lean4bits/lemmas.lean)

State before:
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
x : β' → ℕ → Bool
i : ℕ
changeVars : β → β'
⊢ propagateCarry init_carry next_bit (fun b => x (changeVars b)) i =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x i
Tactic:
induction i
State after:
case zero
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
x : β' → ℕ → Bool
changeVars : β → β'
⊢ propagateCarry init_carry next_bit (fun b => x (changeVars b)) Nat.zero =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x Nat.zero

case succ
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
x : β' → ℕ → Bool
changeVars : β → β'
n✝ : ℕ
n_ih✝ :
  propagateCarry init_carry next_bit (fun b => x (changeVars b)) n✝ =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x n✝
⊢ propagateCarry init_carry next_bit (fun b => x (changeVars b)) (Nat.succ n✝) =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ n✝)

State before:
case zero
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
x : β' → ℕ → Bool
changeVars : β → β'
⊢ propagateCarry init_carry next_bit (fun b => x (changeVars b)) Nat.zero =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x Nat.zero

case succ
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
x : β' → ℕ → Bool
changeVars : β → β'
n✝ : ℕ
n_ih✝ :
  propagateCarry init_carry next_bit (fun b => x (changeVars b)) n✝ =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x n✝
⊢ propagateCarry init_carry next_bit (fun b => x (changeVars b)) (Nat.succ n✝) =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ n✝)
Tactic:
. simp
State after:
case succ
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
x : β' → ℕ → Bool
changeVars : β → β'
n✝ : ℕ
n_ih✝ :
  propagateCarry init_carry next_bit (fun b => x (changeVars b)) n✝ =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x n✝
⊢ propagateCarry init_carry next_bit (fun b => x (changeVars b)) (Nat.succ n✝) =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ n✝)

State before:
case succ
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
x : β' → ℕ → Bool
changeVars : β → β'
n✝ : ℕ
n_ih✝ :
  propagateCarry init_carry next_bit (fun b => x (changeVars b)) n✝ =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x n✝
⊢ propagateCarry init_carry next_bit (fun b => x (changeVars b)) (Nat.succ n✝) =
    propagateCarry init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ n✝)
Tactic:
. simp [*]
State after:
no goals