Theorem: cond_propagate (Lean4bits/lemmas.lean)

State before:
α✝ β✝ α'✝ β'✝ : Type
γ✝ : β✝ → Type
α α' β β' : Type
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
init_carry' : α' → Bool
next_bit' : (α' → Bool) → (β' → Bool) → (α' → Bool) × Bool
γ : Type
fβ : β → γ
fβ' : β' → γ
x : γ → ℕ → Bool
b : Bool
⊢ (bif b then propagate init_carry next_bit fun b => x (fβ b) else propagate init_carry' next_bit' fun b => x (fβ' b)) =
    propagate
      (let_fun this := Bool.rec (motive := fun x => (bif x then α else α') → Bool) init_carry' init_carry b;
      this)
      (let_fun this :=
        Bool.rec (motive := fun x =>
          ((bif x then α else α') → Bool) → ((bif x then β else β') → Bool) → ((bif x then α else α') → Bool) × Bool)
          next_bit' next_bit b;
      this)
      (let_fun this :=
        Bool.rec (motive := fun x => (bif x then β else β') → ℕ → Bool) (fun b => x (fβ' b)) (fun b => x (fβ b)) b;
      this)
Tactic:
cases b <;> rfl
State after:
no goals