Theorem: Stream'.sum_dropEveryNth (ListPowersProblem/StreamLemmas.lean)

State before:
α : Type ?u.21002
σ✝ : Stream' α
n : ℕ
σ : Stream' ℕ
⊢ corec Prod.fst (fun x => (x.fst + head x.snd, tail x.snd))
      (head σ,
        corec (fun x => head x.fst)
          (fun x =>
            match x with
            | (σ, 0) => (tail (tail σ), n - 2)
            | (σ, Nat.succ m) => (tail σ, m))
          (match (σ, n - 2) with
          | (σ, 0) => (tail (tail σ), n - 2)
          | (σ, Nat.succ m) => (tail σ, m))) =
    corec (fun x => head x.fst)
      (fun x =>
        match x with
        | (σ, 0) => (tail (tail σ), n - 2)
        | (σ, Nat.succ m) => (tail σ, m))
      (corec Prod.fst (fun x => (x.fst + head x.snd, tail x.snd))
          (head (σ - maskEveryNth n σ), tail (σ - maskEveryNth n σ)),
        n - 2)
Tactic:
have :
    (match (σ, n - 2) with
      | (σ, 0) => (head σ, tail (tail σ), n - 2)
      | (σ, Nat.succ m) => (head σ, tail σ, m)).fst 
    = head σ := by
  rcases n with ⟨⟩|⟨⟩|⟨⟩|_ <;> rfl
State after:
α : Type ?u.21002
σ✝ : Stream' α
n : ℕ
σ : Stream' ℕ
this :
  (match (σ, n - 2) with
      | (σ, 0) => (head σ, tail (tail σ), n - 2)
      | (σ, Nat.succ m) => (head σ, tail σ, m)).fst =
    head σ
⊢ corec Prod.fst (fun x => (x.fst + head x.snd, tail x.snd))
      (head σ,
        corec (fun x => head x.fst)
          (fun x =>
            match x with
            | (σ, 0) => (tail (tail σ), n - 2)
            | (σ, Nat.succ m) => (tail σ, m))
          (match (σ, n - 2) with
          | (σ, 0) => (tail (tail σ), n - 2)
          | (σ, Nat.succ m) => (tail σ, m))) =
    corec (fun x => head x.fst)
      (fun x =>
        match x with
        | (σ, 0) => (tail (tail σ), n - 2)
        | (σ, Nat.succ m) => (tail σ, m))
      (corec Prod.fst (fun x => (x.fst + head x.snd, tail x.snd))
          (head (σ - maskEveryNth n σ), tail (σ - maskEveryNth n σ)),
        n - 2)

State before:
α : Type ?u.21002
σ✝ : Stream' α
n : ℕ
σ : Stream' ℕ
this :
  (match (σ, n - 2) with
      | (σ, 0) => (head σ, tail (tail σ), n - 2)
      | (σ, Nat.succ m) => (head σ, tail σ, m)).fst =
    head σ
⊢ corec Prod.fst (fun x => (x.fst + head x.snd, tail x.snd))
      (head σ,
        corec (fun x => head x.fst)
          (fun x =>
            match x with
            | (σ, 0) => (tail (tail σ), n - 2)
            | (σ, Nat.succ m) => (tail σ, m))
          (match (σ, n - 2) with
          | (σ, 0) => (tail (tail σ), n - 2)
          | (σ, Nat.succ m) => (tail σ, m))) =
    corec (fun x => head x.fst)
      (fun x =>
        match x with
        | (σ, 0) => (tail (tail σ), n - 2)
        | (σ, Nat.succ m) => (tail σ, m))
      (corec Prod.fst (fun x => (x.fst + head x.snd, tail x.snd))
          (head (σ - maskEveryNth n σ), tail (σ - maskEveryNth n σ)),
        n - 2)
Tactic:
sorry
State after:
no goals

State before:
α : Type ?u.21002
σ✝ : Stream' α
n : ℕ
σ : Stream' ℕ
⊢ (match (σ, n - 2) with
      | (σ, 0) => (head σ, tail (tail σ), n - 2)
      | (σ, Nat.succ m) => (head σ, tail σ, m)).fst =
    head σ
Tactic:
rcases n with ⟨⟩|⟨⟩|⟨⟩|_ <;> rfl
State after:
no goals