Theorem: propagate_propagate
Proof state before:
α β α' β'✝ : Type
γ δ : β → Type
β' : Type
f : (a : β) → δ a → β'
n : ℕ
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
init_carry_x : (a : β) → γ a → Bool
next_bit_x : (a : β) → (γ a → Bool) → (δ a → Bool) → (γ a → Bool) × Bool
x : β' → ℕ → Bool
⊢ (next_bit
        (propagateCarry init_carry (fun c b => (next_bit c b).fst)
          (fun a => propagate (init_carry_x a) (next_bit_x a) fun d => x (f a d)) n)
        fun j =>
        (next_bit_x j (propagateCarry (init_carry_x j) (fun c b => (next_bit_x j c b).fst) (fun d => x (f j d)) n)
            fun j_1 => x (f j j_1) (n + 1)).snd).snd =
    (next_bit
        (propagateCarry (fun a => Sum.elim init_carry (fun b => init_carry_x b.fst b.snd) a)
            (fun c b =>
              Sum.elim
                (next_bit (c ∘ inl) fun a =>
                    (next_bit_x a (fun d => c (inr { fst := a, snd := d })) fun d => b (f a d)).snd).fst
                fun x =>
                Prod.fst (next_bit_x x.fst (fun d => c (inr { fst := x.fst, snd := d })) fun d => b (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 c b =>
                  Sum.elim
                    (next_bit (c ∘ inl) fun a =>
                        (next_bit_x a (fun d => c (inr { fst := a, snd := d })) fun d => b (f a d)).snd).fst
                    fun x =>
                    Prod.fst (next_bit_x x.fst (fun d => c (inr { fst := x.fst, snd := d })) fun d => b (f x.fst d))
                      x.snd)
                x n (inr { fst := a, snd := d }))
            fun d => x (f a d) (n + 1)).snd).snd
Tactic:
rw [propagateCarry_propagate]
Proof state after:
α β α' β'✝ : Type
γ δ : β → Type
β' : Type
f : (a : β) → δ a → β'
n : ℕ
init_carry : α → Bool
next_bit : (α → Bool) → (β → Bool) → (α → Bool) × Bool
init_carry_x : (a : β) → γ a → Bool
next_bit_x : (a : β) → (γ a → Bool) → (δ a → Bool) → (γ a → Bool) × Bool
x : β' → ℕ → Bool
⊢ (next_bit
        (propagateCarry (fun a => Sum.elim init_carry (fun b => init_carry_x b.fst b.snd) a)
            (fun carry bits =>
              let f := fun a => next_bit_x a (fun d => carry (inr { fst := a, snd := d })) fun d => bits (f a d);
              let g := (next_bit (carry ∘ inl) fun a => (f a).snd).fst;
              Sum.elim g fun x => Prod.fst (f x.fst) x.snd)
            x n ∘
          inl)
        fun j =>
        (next_bit_x j (propagateCarry (init_carry_x j) (fun c b => (next_bit_x j c b).fst) (fun d => x (f j d)) n)
            fun j_1 => x (f j j_1) (n + 1)).snd).snd =
    (next_bit
        (propagateCarry (fun a => Sum.elim init_carry (fun b => init_carry_x b.fst b.snd) a)
            (fun c b =>
              Sum.elim
                (next_bit (c ∘ inl) fun a =>
                    (next_bit_x a (fun d => c (inr { fst := a, snd := d })) fun d => b (f a d)).snd).fst
                fun x =>
                Prod.fst (next_bit_x x.fst (fun d => c (inr { fst := x.fst, snd := d })) fun d => b (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 c b =>
                  Sum.elim
                    (next_bit (c ∘ inl) fun a =>
                        (next_bit_x a (fun d => c (inr { fst := a, snd := d })) fun d => b (f a d)).snd).fst
                    fun x =>
                    Prod.fst (next_bit_x x.fst (fun d => c (inr { fst := x.fst, snd := d })) fun d => b (f x.fst d))
                      x.snd)
                x n (inr { fst := a, snd := d }))
            fun d => x (f a d) (n + 1)).snd).snd