Theorem: decr_eq_propagate (Lean4bits/lemmas.lean)

State before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
⊢ decrSeq x =
    propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (bits ()) (carry ())))
      fun x_1 => x
Tactic:
ext n
State after:
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ decrSeq x n =
    propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (bits ()) (carry ())))
      (fun x_1 => x) n

State before:
case h
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ decrSeq x n =
    propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (bits ()) (carry ())))
      (fun x_1 => x) n
Tactic:
match n with
| 0 => simp [decrSeq, decrSeqAux]
| 1 => simp [decrSeq, decrSeqAux, propagate, propagateAux]
| n+2 => simp [decrSeq, decrSeqAux, decrSeqAux_eq_propagateCarry, propagate_succ]
State after:
no goals

State before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ decrSeq x 0 =
    propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (bits ()) (carry ())))
      (fun x_1 => x) 0
Tactic:
simp [decrSeq, decrSeqAux]
State after:
no goals

State before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n : ℕ
⊢ decrSeq x 1 =
    propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (bits ()) (carry ())))
      (fun x_1 => x) 1
Tactic:
simp [decrSeq, decrSeqAux, propagate, propagateAux]
State after:
no goals

State before:
α β α' β' : Type
γ : β → Type
x : ℕ → Bool
n✝ n : ℕ
⊢ decrSeq x (n + 2) =
    propagate (fun x => true) (fun carry bits => (fun x => !bits () && carry (), _root_.xor (bits ()) (carry ())))
      (fun x_1 => x) (n + 2)
Tactic:
simp [decrSeq, decrSeqAux, decrSeqAux_eq_propagateCarry, propagate_succ]
State after:
no goals