rintro ⟨_, _⟩ i ⟨⟨⟩, ⟨⟩⟩
case hg
α✝ : Type u_1
σ : Stream' α✝
⊢ ∀ (a : Stream' α✝ × ℕ) (a' : ℕ),
    (match a with
      | (σ', c) => σ' = drop (a' + a' / 2) σ ∧ c = (a' + 1) % 2) →
      match
        match a with
        | (σ, 0) => (tail (tail σ), 3 - 2)
        | (σ, Nat.succ m) => (tail σ, m) with
      | (σ', c) => σ' = drop (a' + 1 + (a' + 1) / 2) σ ∧ c = (a' + 1 + 1) % 2
case hg.mk.intro.refl.refl
α✝ : Type u_1
σ : Stream' α✝
i : ℕ
⊢ match
    match (drop (i + i / 2) σ, (i + 1) % 2) with
    | (σ, 0) => (tail (tail σ), 3 - 2)
    | (σ, Nat.succ m) => (tail σ, m) with
  | (σ', c) => σ' = drop (i + 1 + (i + 1) / 2) σ ∧ c = (i + 1 + 1) % 2