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

State before:
α : Type u_1
σ : Stream' α
⊢ dropEveryNth 2 σ = even σ
Tactic:
simp [even, dropEveryNth, corec']
State after:
α : Type u_1
σ : Stream' α
⊢ corec (fun x => head x.fst)
      (fun x =>
        match x with
        | (σ, 0) => (tail (tail σ), 0)
        | (σ, Nat.succ m) => (tail σ, m))
      (σ, 0) =
    corec (fun s => head s) (fun s => tail (tail s)) σ

State before:
α : Type u_1
σ : Stream' α
⊢ corec (fun x => head x.fst)
      (fun x =>
        match x with
        | (σ, 0) => (tail (tail σ), 0)
        | (σ, Nat.succ m) => (tail σ, m))
      (σ, 0) =
    corec (fun s => head s) (fun s => tail (tail s)) σ
Tactic:
apply corec_bisim (fun ⟨σ, n⟩ σ' => σ = σ' ∧ n = 0)
State after:
case hf
α : Type u_1
σ : Stream' α
⊢ ∀ (a : Stream' α × ℕ) (a' : Stream' α),
    (match a with
      | (σ, n) => σ = a' ∧ n = 0) →
      head a.fst = head a'

case hg
α : Type u_1
σ : Stream' α
⊢ ∀ (a : Stream' α × ℕ) (a' : Stream' α),
    (match a with
      | (σ, n) => σ = a' ∧ n = 0) →
      match
        match a with
        | (σ, 0) => (tail (tail σ), 0)
        | (σ, Nat.succ m) => (tail σ, m) with
      | (σ, n) => σ = tail (tail a') ∧ n = 0

case a
α : Type u_1
σ : Stream' α
⊢ match (σ, 0) with
  | (σ_1, n) => σ_1 = σ ∧ n = 0

State before:
case hf
α : Type u_1
σ : Stream' α
⊢ ∀ (a : Stream' α × ℕ) (a' : Stream' α),
    (match a with
      | (σ, n) => σ = a' ∧ n = 0) →
      head a.fst = head a'
Tactic:
rintro ⟨σ, n⟩ σ' ⟨⟨⟩, ⟨⟩⟩
State after:
case hf.mk.intro.refl.refl
α : Type u_1
σ✝ σ : Stream' α
⊢ head (σ, 0).fst = head σ

State before:
case hf.mk.intro.refl.refl
α : Type u_1
σ✝ σ : Stream' α
⊢ head (σ, 0).fst = head σ
Tactic:
simp [drop, head, nth]
State after:
no goals

State before:
case hg
α : Type u_1
σ : Stream' α
⊢ ∀ (a : Stream' α × ℕ) (a' : Stream' α),
    (match a with
      | (σ, n) => σ = a' ∧ n = 0) →
      match
        match a with
        | (σ, 0) => (tail (tail σ), 0)
        | (σ, Nat.succ m) => (tail σ, m) with
      | (σ, n) => σ = tail (tail a') ∧ n = 0
Tactic:
rintro ⟨σ, n⟩ σ' ⟨⟨⟩, ⟨⟩⟩
State after:
case hg.mk.intro.refl.refl
α : Type u_1
σ✝ σ : Stream' α
⊢ match
    match (σ, 0) with
    | (σ, 0) => (tail (tail σ), 0)
    | (σ, Nat.succ m) => (tail σ, m) with
  | (σ_1, n) => σ_1 = tail (tail σ) ∧ n = 0

State before:
case hg.mk.intro.refl.refl
α : Type u_1
σ✝ σ : Stream' α
⊢ match
    match (σ, 0) with
    | (σ, 0) => (tail (tail σ), 0)
    | (σ, Nat.succ m) => (tail σ, m) with
  | (σ_1, n) => σ_1 = tail (tail σ) ∧ n = 0
Tactic:
simp [tail, nth]
State after:
no goals

State before:
case a
α : Type u_1
σ : Stream' α
⊢ match (σ, 0) with
  | (σ_1, n) => σ_1 = σ ∧ n = 0
Tactic:
exact ⟨rfl, rfl⟩
State after:
no goals