simp [tail, drop, nth]
case hg.mk.intro.refl.refl.succ
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ (match (drop (i + i / 2) σ, Nat.succ n✝) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).fst =
      drop (i + 1 + (i + 1) / 2) σ ∧
    (match (drop (i + i / 2) σ, Nat.succ n✝) with
        | (σ, 0) => (tail (tail σ), 1)
        | (σ, Nat.succ m) => (tail σ, m)).snd =
      (Nat.succ n✝ + 1 % 2) % 2
case hg.mk.intro.refl.refl.succ
α✝ : Type u_1
σ : Stream' α✝
i n✝ : ℕ
h : (i + 1) % 2 = Nat.succ n✝
⊢ ((fun i_1 => σ (i_1 + 1 + (i + i / 2))) = fun i_1 => σ (i_1 + (i + 1 + (i + 1) / 2))) ∧ n✝ = (Nat.succ n✝ + 1) % 2