Theorem: propagateCarry_propagate (Lean4bits/lemmas.lean)

State before:
α β α' β'✝ : 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
⊢ propagateCarry init_carry next_bit (fun a => propagate (init_carry_x a) (next_bit_x a) fun d => x (f a d)) (n + 1) =
    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;
          Sum.elim g fun x => Prod.fst (f x.fst) x.snd)
        x (n + 1) ∘
      inl
Tactic:
have := propagateCarry_propagate f n
State after:
α β α' β'✝ : 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
this :
  ∀ (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),
    propagateCarry init_carry next_bit (fun a => propagate (init_carry_x a) (next_bit_x a) fun d => x (f a d)) n =
      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;
            Sum.elim g fun x => Prod.fst (f x.fst) x.snd)
          x n ∘
        inl
⊢ propagateCarry init_carry next_bit (fun a => propagate (init_carry_x a) (next_bit_x a) fun d => x (f a d)) (n + 1) =
    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;
          Sum.elim g fun x => Prod.fst (f x.fst) x.snd)
        x (n + 1) ∘
      inl

State before:
α β α' β'✝ : 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
this :
  ∀ (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),
    propagateCarry init_carry next_bit (fun a => propagate (init_carry_x a) (next_bit_x a) fun d => x (f a d)) n =
      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;
            Sum.elim g fun x => Prod.fst (f x.fst) x.snd)
          x n ∘
        inl
⊢ propagateCarry init_carry next_bit (fun a => propagate (init_carry_x a) (next_bit_x a) fun d => x (f a d)) (n + 1) =
    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;
          Sum.elim g fun x => Prod.fst (f x.fst) x.snd)
        x (n + 1) ∘
      inl
Tactic:
simp only [propagateCarry, propagate_succ, elim_inl, Nat.add] at *
State after:
α β α' β'✝ : 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
this :
  ∀ (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),
    propagateCarry init_carry next_bit (fun a => propagate (init_carry_x a) (next_bit_x a) fun d => x (f a d)) n =
      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
⊢ (next_bit
      (propagateCarry init_carry next_bit (fun a => propagate (init_carry_x a) (next_bit_x a) fun d => x (f a d)) n)
      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) =
    (Sum.elim
        (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)
        fun x_1 =>
        Prod.fst
          (next_bit_x x_1.fst
            (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 := x_1.fst, snd := d }))
            fun d => x (f x_1.fst d) (n + 1))
          x_1.snd) ∘
      inl

State before:
α β α' β'✝ : 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
this :
  ∀ (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),
    propagateCarry init_carry next_bit (fun a => propagate (init_carry_x a) (next_bit_x a) fun d => x (f a d)) n =
      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
⊢ (next_bit
      (propagateCarry init_carry next_bit (fun a => propagate (init_carry_x a) (next_bit_x a) fun d => x (f a d)) n)
      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) =
    (Sum.elim
        (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)
        fun x_1 =>
        Prod.fst
          (next_bit_x x_1.fst
            (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 := x_1.fst, snd := d }))
            fun d => x (f x_1.fst d) (n + 1))
          x_1.snd) ∘
      inl
Tactic:
conv_lhs => simp only [this]
State after:
α β α' β'✝ : 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
this :
  ∀ (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),
    propagateCarry init_carry next_bit (fun a => propagate (init_carry_x a) (next_bit_x a) fun d => x (f a d)) n =
      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
⊢ (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) =
    (Sum.elim
        (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)
        fun x_1 =>
        Prod.fst
          (next_bit_x x_1.fst
            (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 := x_1.fst, snd := d }))
            fun d => x (f x_1.fst d) (n + 1))
          x_1.snd) ∘
      inl

State before:
α β α' β'✝ : 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
this :
  ∀ (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),
    propagateCarry init_carry next_bit (fun a => propagate (init_carry_x a) (next_bit_x a) fun d => x (f a d)) n =
      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
⊢ (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) =
    (Sum.elim
        (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)
        fun x_1 =>
        Prod.fst
          (next_bit_x x_1.fst
            (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 := x_1.fst, snd := d }))
            fun d => x (f x_1.fst d) (n + 1))
          x_1.snd) ∘
      inl
Tactic:
clear this
State after:
α β α' β'✝ : 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
⊢ (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) =
    (Sum.elim
        (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)
        fun x_1 =>
        Prod.fst
          (next_bit_x x_1.fst
            (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 := x_1.fst, snd := d }))
            fun d => x (f x_1.fst d) (n + 1))
          x_1.snd) ∘
      inl

State before:
α β α' β'✝ : 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
⊢ (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) =
    (Sum.elim
        (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)
        fun x_1 =>
        Prod.fst
          (next_bit_x x_1.fst
            (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 := x_1.fst, snd := d }))
            fun d => x (f x_1.fst d) (n + 1))
          x_1.snd) ∘
      inl
Tactic:
dsimp
State after:
α β α' β'✝ : 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
⊢ (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) =
    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

State before:
α β α' β'✝ : 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
⊢ (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) =
    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
Tactic:
ext a
State after:
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

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
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

State before:
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
Tactic:
ext b
State after:
case h.e__bits.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 : α
b : β
⊢ (next_bit_x b (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 j => x (f b j) (n + 1)).snd =
    (next_bit_x b
        (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 }))
        fun d => x (f b d) (n + 1)).snd

State before:
case h.e__bits.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 : α
b : β
⊢ (next_bit_x b (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 j => x (f b j) (n + 1)).snd =
    (next_bit_x b
        (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 }))
        fun d => x (f b d) (n + 1)).snd
Tactic:
congr
State after:
case h.e__bits.h.e_self.e__carry
α β α' β'✝ : 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 : α
b : β
⊢ 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 })

State before:
case h.e__bits.h.e_self.e__carry
α β α' β'✝ : 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 : α
b : β
⊢ 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 })
Tactic:
induction' n with n ih
State after:
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 })

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
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 })

State before:
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 [ih]
State after:
no goals