Theorem: one_eq_propagate (Lean4bits/lemmas.lean)

State before:
α β α' β' : Type
γ : β → Type
⊢ oneSeq = propagate (fun x => true) (fun f x => (fun x => false, f ())) Empty.elim
Tactic:
ext n
State after:
case h
α β α' β' : Type
γ : β → Type
n : ℕ
⊢ oneSeq n = propagate (fun x => true) (fun f x => (fun x => false, f ())) Empty.elim n

State before:
case h
α β α' β' : Type
γ : β → Type
n : ℕ
⊢ oneSeq n = propagate (fun x => true) (fun f x => (fun x => false, f ())) Empty.elim n
Tactic:
match n with
| 0 => rfl
| 1 => rfl
| n+2 => simp [oneSeq, propagate_succ]
State after:
no goals

State before:
α β α' β' : Type
γ : β → Type
n : ℕ
⊢ oneSeq 0 = propagate (fun x => true) (fun f x => (fun x => false, f ())) Empty.elim 0
Tactic:
rfl
State after:
no goals

State before:
α β α' β' : Type
γ : β → Type
n : ℕ
⊢ oneSeq 1 = propagate (fun x => true) (fun f x => (fun x => false, f ())) Empty.elim 1
Tactic:
rfl
State after:
no goals

State before:
α β α' β' : Type
γ : β → Type
n✝ n : ℕ
⊢ oneSeq (n + 2) = propagate (fun x => true) (fun f x => (fun x => false, f ())) Empty.elim (n + 2)
Tactic:
simp [oneSeq, propagate_succ]
State after:
no goals