Theorem: propagate_changeVars (Lean4bits/lemmas.lean)

State before:
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β' → ℕ → Bool
i : ℕ
changeVars : β → β'
⊢ propagate init_carry next_bit (fun b => x (changeVars b)) i =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x i
Tactic:
induction' i with i ih
State after:
case zero
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β' → ℕ → Bool
changeVars : β → β'
⊢ propagate init_carry next_bit (fun b => x (changeVars b)) Nat.zero =
    propagate 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) × Bool
x : β' → ℕ → Bool
changeVars : β → β'
i : ℕ
ih :
  propagate init_carry next_bit (fun b => x (changeVars b)) i =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x i
⊢ propagate init_carry next_bit (fun b => x (changeVars b)) (Nat.succ i) =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ i)

State before:
case zero
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β' → ℕ → Bool
changeVars : β → β'
⊢ propagate init_carry next_bit (fun b => x (changeVars b)) Nat.zero =
    propagate 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) × Bool
x : β' → ℕ → Bool
changeVars : β → β'
i : ℕ
ih :
  propagate init_carry next_bit (fun b => x (changeVars b)) i =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x i
⊢ propagate init_carry next_bit (fun b => x (changeVars b)) (Nat.succ i) =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ i)
Tactic:
. rfl
State after:
case succ
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β' → ℕ → Bool
changeVars : β → β'
i : ℕ
ih :
  propagate init_carry next_bit (fun b => x (changeVars b)) i =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x i
⊢ propagate init_carry next_bit (fun b => x (changeVars b)) (Nat.succ i) =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ i)

State before:
case succ
α β α' β'✝ : Type
γ : β → Type
β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
x : β' → ℕ → Bool
changeVars : β → β'
i : ℕ
ih :
  propagate init_carry next_bit (fun b => x (changeVars b)) i =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x i
⊢ propagate init_carry next_bit (fun b => x (changeVars b)) (Nat.succ i) =
    propagate init_carry (fun carry bits => next_bit carry fun b => bits (changeVars b)) x (Nat.succ i)
Tactic:
. simp only [propagate_succ, propagateCarry_changeVars, ih]
State after:
no goals