case intro
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e : (fun b => some a = b) (nth (↑s) k)
⊢ C s
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s : Seq α
M : a ∈ s
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
⊢ C s
cases' M with k e
case intro
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e : (fun b => some a = b) (↑s k)
⊢ C s
case intro
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e : (fun b => some a = b) (nth (↑s) k)
⊢ C s
unfold Stream'.nth at e
case intro.zero
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e✝ : (fun b => some a = b) (↑s✝ k)
s : Seq α
e : some a = ↑s Nat.zero
⊢ C s

case intro.succ
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e✝ : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
e : some a = ↑s (Nat.succ k)
⊢ C s
case intro
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e : (fun b => some a = b) (↑s k)
⊢ C s
induction' k with k IH generalizing s
case intro.succ
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
⊢ some a = ↑s (Nat.succ k) → C s
case intro.succ
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e✝ : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
e : some a = ↑s (Nat.succ k)
⊢ C s
revert e
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
⊢ some a = ↑nil (Nat.succ k) → C nil

α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
⊢ ∀ (b : α) (s' : Seq α), some a = ↑(cons b s') (Nat.succ k) → C (cons b s')
case intro.succ
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
⊢ some a = ↑s (Nat.succ k) → C s
apply s.recOn _ fun b s' => _
case intro.zero
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e✝ : (fun b => some a = b) (↑s✝ k)
s : Seq α
e : some a = ↑s Nat.zero
TH : s = cons a (tail s)
⊢ C s
case intro.zero
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e✝ : (fun b => some a = b) (↑s✝ k)
s : Seq α
e : some a = ↑s Nat.zero
⊢ C s
have TH : s = cons a (tail s) := by
  apply destruct_eq_cons
  unfold destruct get? Functor.map
  rw [← e]
  rfl
case intro.zero
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e✝ : (fun b => some a = b) (↑s✝ k)
s : Seq α
e : some a = ↑s Nat.zero
TH : s = cons a (tail s)
⊢ C (cons a (tail s))
case intro.zero
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e✝ : (fun b => some a = b) (↑s✝ k)
s : Seq α
e : some a = ↑s Nat.zero
TH : s = cons a (tail s)
⊢ C s
rw [TH]
no goals
case intro.zero
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e✝ : (fun b => some a = b) (↑s✝ k)
s : Seq α
e : some a = ↑s Nat.zero
TH : s = cons a (tail s)
⊢ C (cons a (tail s))
apply h1 _ _ (Or.inl rfl)
case a
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e✝ : (fun b => some a = b) (↑s✝ k)
s : Seq α
e : some a = ↑s Nat.zero
⊢ destruct s = some (a, tail s)
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e✝ : (fun b => some a = b) (↑s✝ k)
s : Seq α
e : some a = ↑s Nat.zero
⊢ s = cons a (tail s)
apply destruct_eq_cons
case a
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e✝ : (fun b => some a = b) (↑s✝ k)
s : Seq α
e : some a = ↑s Nat.zero
⊢ instFunctorOption.1 (fun a' => (a', tail s)) (↑s 0) = some (a, tail s)
case a
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e✝ : (fun b => some a = b) (↑s✝ k)
s : Seq α
e : some a = ↑s Nat.zero
⊢ destruct s = some (a, tail s)
unfold destruct get? Functor.map
case a
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e✝ : (fun b => some a = b) (↑s✝ k)
s : Seq α
e : some a = ↑s Nat.zero
⊢ instFunctorOption.1 (fun a' => (a', tail s)) (some a) = some (a, tail s)
case a
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e✝ : (fun b => some a = b) (↑s✝ k)
s : Seq α
e : some a = ↑s Nat.zero
⊢ instFunctorOption.1 (fun a' => (a', tail s)) (↑s 0) = some (a, tail s)
rw [← e]
no goals
case a
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k : ℕ
e✝ : (fun b => some a = b) (↑s✝ k)
s : Seq α
e : some a = ↑s Nat.zero
⊢ instFunctorOption.1 (fun a' => (a', tail s)) (some a) = some (a, tail s)
rfl
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e✝ : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
e : some a = ↑nil (Nat.succ k)
⊢ C nil
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
⊢ some a = ↑nil (Nat.succ k) → C nil
intro e
no goals
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e✝ : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
e : some a = ↑nil (Nat.succ k)
⊢ C nil
injection e
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e✝ : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
b : α
s' : Seq α
e : some a = ↑(cons b s') (Nat.succ k)
⊢ C (cons b s')
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
⊢ ∀ (b : α) (s' : Seq α), some a = ↑(cons b s') (Nat.succ k) → C (cons b s')
intro b s' e
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e✝ : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
b : α
s' : Seq α
e : some a = ↑(cons b s') (Nat.succ k)
h_eq : ↑(cons b s') (Nat.succ k) = ↑s' k
⊢ C (cons b s')
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e✝ : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
b : α
s' : Seq α
e : some a = ↑(cons b s') (Nat.succ k)
⊢ C (cons b s')
have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' ; rfl
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e✝ : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
b : α
s' : Seq α
e : some a = ↑s' k
h_eq : ↑(cons b s') (Nat.succ k) = ↑s' k
⊢ C (cons b s')
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e✝ : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
b : α
s' : Seq α
e : some a = ↑(cons b s') (Nat.succ k)
h_eq : ↑(cons b s') (Nat.succ k) = ↑s' k
⊢ C (cons b s')
rw [h_eq] at e
no goals
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e✝ : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
b : α
s' : Seq α
e : some a = ↑s' k
h_eq : ↑(cons b s') (Nat.succ k) = ↑s' k
⊢ C (cons b s')
apply h1 _ _ (Or.inr (IH e))
case mk
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e✝ : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
b : α
val✝ : Stream' (Option α)
property✝ : IsSeq val✝
e : some a = ↑(cons b { val := val✝, property := property✝ }) (Nat.succ k)
⊢ ↑(cons b { val := val✝, property := property✝ }) (Nat.succ k) = ↑{ val := val✝, property := property✝ } k
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e✝ : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
b : α
s' : Seq α
e : some a = ↑(cons b s') (Nat.succ k)
⊢ ↑(cons b s') (Nat.succ k) = ↑s' k
cases s'
no goals
case mk
α : Type u
β : Type v
γ : Type w
C : Seq α → Prop
a : α
s✝ : Seq α
h1 : ∀ (b : α) (s' : Seq α), a = b ∨ C s' → C (cons b s')
k✝ : ℕ
e✝ : (fun b => some a = b) (↑s✝ k✝)
k : ℕ
IH : ∀ {s : Seq α}, some a = ↑s k → C s
s : Seq α
b : α
val✝ : Stream' (Option α)
property✝ : IsSeq val✝
e : some a = ↑(cons b { val := val✝, property := property✝ }) (Nat.succ k)
⊢ ↑(cons b { val := val✝, property := property✝ }) (Nat.succ k) = ↑{ val := val✝, property := property✝ } k
rfl