Theorem: propagateCarry_propagate
Proof state before:
case h.e__bits.h.e_self.e__carry.zero
α β α' β'✝ : Type
γ δ : β → Type
β' : Type
f : (a : β) → δ a → β'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
init_carry_x : (a : β) → γ a → Bool
next_bit_x : (a : β) → (γ a → Bool) → (δ a → Bool) → (γ a → Bool) × Bool
x : β' → ℕ → Bool
a : α
b : β
⊢ propagateCarry (init_carry_x b) (fun c b_1 => (next_bit_x b c b_1).fst) (fun d => x (f b d)) Nat.zero = fun d =>
    propagateCarry (fun a => Sum.elim init_carry (fun b => init_carry_x b.fst b.snd) a)
      (fun carry bits =>
        Sum.elim
          (next_bit (carry ∘ inl) fun a =>
            (next_bit_x a (fun d => carry (inr { fst := a, snd := d })) fun d => bits (f a d)).snd)
          fun x =>
          Prod.fst (next_bit_x x.fst (fun d => carry (inr { fst := x.fst, snd := d })) fun d => bits (f x.fst d)) x.snd)
      x Nat.zero (inr { fst := b, snd := d })

case h.e__bits.h.e_self.e__carry.succ
α β α' β'✝ : Type
γ δ : β → Type
β' : Type
f : (a : β) → δ a → β'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
init_carry_x : (a : β) → γ a → Bool
next_bit_x : (a : β) → (γ a → Bool) → (δ a → Bool) → (γ a → Bool) × Bool
x : β' → ℕ → Bool
a : α
b : β
n : ℕ
ih :
  propagateCarry (init_carry_x b) (fun c b_1 => (next_bit_x b c b_1).fst) (fun d => x (f b d)) n = fun d =>
    propagateCarry (fun a => Sum.elim init_carry (fun b => init_carry_x b.fst b.snd) a)
      (fun carry bits =>
        Sum.elim
          (next_bit (carry ∘ inl) fun a =>
            (next_bit_x a (fun d => carry (inr { fst := a, snd := d })) fun d => bits (f a d)).snd)
          fun x =>
          Prod.fst (next_bit_x x.fst (fun d => carry (inr { fst := x.fst, snd := d })) fun d => bits (f x.fst d)) x.snd)
      x n (inr { fst := b, snd := d })
⊢ propagateCarry (init_carry_x b) (fun c b_1 => (next_bit_x b c b_1).fst) (fun d => x (f b d)) (Nat.succ n) = fun d =>
    propagateCarry (fun a => Sum.elim init_carry (fun b => init_carry_x b.fst b.snd) a)
      (fun carry bits =>
        Sum.elim
          (next_bit (carry ∘ inl) fun a =>
            (next_bit_x a (fun d => carry (inr { fst := a, snd := d })) fun d => bits (f a d)).snd)
          fun x =>
          Prod.fst (next_bit_x x.fst (fun d => carry (inr { fst := x.fst, snd := d })) fun d => bits (f x.fst d)) x.snd)
      x (Nat.succ n) (inr { fst := b, snd := d })
Tactic:
. simp
Proof state after:
case h.e__bits.h.e_self.e__carry.succ
α β α' β'✝ : Type
γ δ : β → Type
β' : Type
f : (a : β) → δ a → β'
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → α → Bool
init_carry_x : (a : β) → γ a → Bool
next_bit_x : (a : β) → (γ a → Bool) → (δ a → Bool) → (γ a → Bool) × Bool
x : β' → ℕ → Bool
a : α
b : β
n : ℕ
ih :
  propagateCarry (init_carry_x b) (fun c b_1 => (next_bit_x b c b_1).fst) (fun d => x (f b d)) n = fun d =>
    propagateCarry (fun a => Sum.elim init_carry (fun b => init_carry_x b.fst b.snd) a)
      (fun carry bits =>
        Sum.elim
          (next_bit (carry ∘ inl) fun a =>
            (next_bit_x a (fun d => carry (inr { fst := a, snd := d })) fun d => bits (f a d)).snd)
          fun x =>
          Prod.fst (next_bit_x x.fst (fun d => carry (inr { fst := x.fst, snd := d })) fun d => bits (f x.fst d)) x.snd)
      x n (inr { fst := b, snd := d })
⊢ propagateCarry (init_carry_x b) (fun c b_1 => (next_bit_x b c b_1).fst) (fun d => x (f b d)) (Nat.succ n) = fun d =>
    propagateCarry (fun a => Sum.elim init_carry (fun b => init_carry_x b.fst b.snd) a)
      (fun carry bits =>
        Sum.elim
          (next_bit (carry ∘ inl) fun a =>
            (next_bit_x a (fun d => carry (inr { fst := a, snd := d })) fun d => bits (f a d)).snd)
          fun x =>
          Prod.fst (next_bit_x x.fst (fun d => carry (inr { fst := x.fst, snd := d })) fun d => bits (f x.fst d)) x.snd)
      x (Nat.succ n) (inr { fst := b, snd := d })