Theorem: propagateCarry_propagate
Proof state before:
case h
α β α' β'✝ : Type
γ δ : β → Type
β' : Type
f : (a : β) → δ a → β'
n : ℕ
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 : α
⊢ next_bit
      (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 ∘
        inl)
      (fun i =>
        (next_bit_x i (propagateCarry (init_carry_x i) (fun c b => (next_bit_x i c b).fst) (fun d => x (f i d)) n)
            fun j => x (f i j) (n + 1)).snd)
      a =
    next_bit
      (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 ∘
        inl)
      (fun a =>
        (next_bit_x a
            (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 := a, snd := d }))
            fun d => x (f a d) (n + 1)).snd)
      a
Tactic:
congr
Proof state after:
case h.e__bits
α β α' β'✝ : Type
γ δ : β → Type
β' : Type
f : (a : β) → δ a → β'
n : ℕ
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 : α
⊢ (fun i =>
      (next_bit_x i (propagateCarry (init_carry_x i) (fun c b => (next_bit_x i c b).fst) (fun d => x (f i d)) n)
          fun j => x (f i j) (n + 1)).snd) =
    fun a =>
    (next_bit_x a
        (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 := a, snd := d }))
        fun d => x (f a d) (n + 1)).snd