α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = even (s₁ ⋈ s₂)
⊢ head (even (s₁ ⋈ s₂)) = head s₁ ∧ (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) (tail (even (s₁ ⋈ s₂))) (tail s₁)
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = even (s₁ ⋈ s₂)
⊢ head s₁' = head s₁ ∧ (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) (tail s₁') (tail s₁)
rw [h₁]
case left
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = even (s₁ ⋈ s₂)
⊢ head (even (s₁ ⋈ s₂)) = head s₁

case right
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = even (s₁ ⋈ s₂)
⊢ (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) (tail (even (s₁ ⋈ s₂))) (tail s₁)
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = even (s₁ ⋈ s₂)
⊢ head (even (s₁ ⋈ s₂)) = head s₁ ∧ (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) (tail (even (s₁ ⋈ s₂))) (tail s₁)
constructor
no goals
case left
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = even (s₁ ⋈ s₂)
⊢ head (even (s₁ ⋈ s₂)) = head s₁
rfl
no goals
case right
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = even (s₁ ⋈ s₂)
⊢ (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) (tail (even (s₁ ⋈ s₂))) (tail s₁)
exact ⟨tail s₂, by rw [interleave_eq, even_cons_cons, tail_cons]⟩
no goals
α : Type u
β : Type v
δ : Type w
s₁✝ s₂✝ s₁' s₁ : Stream' α
x✝ : (fun s₁' s₁ => ∃ s₂, s₁' = even (s₁ ⋈ s₂)) s₁' s₁
s₂ : Stream' α
h₁ : s₁' = even (s₁ ⋈ s₂)
⊢ tail (even (s₁ ⋈ s₂)) = even (tail s₁ ⋈ tail s₂)
rw [interleave_eq, even_cons_cons, tail_cons]