awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
n : ℕ
⊢ ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
have zero : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) 0), a ∈ s
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
n : ℕ
zero : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) 0), a ∈ s
⊢ ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
have succ : ∀ (n : ℕ),
  (∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s) →
    ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) (n + 1)), a ∈ s
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
s : WSeq α
⊢ ∀ (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) 0), a ∈ s
have zero : ∀ (this : Membership.mem (γ := WSeq α) (tail nil) a)
  (e : some (some a) = (↑(tail nil) : Stream' (Option (Option α))) 0), Membership.mem (γ := WSeq α) nil a
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
s : WSeq α
zero :
  ∀ (this : Membership.mem (γ := WSeq α) (tail nil) a)
    (e : some (some a) = (↑(tail nil) : Stream' (Option (Option α))) 0), Membership.mem (γ := WSeq α) nil a
⊢ ∀ (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) 0), a ∈ s
have zero₁ : ∀ (x : α) (s : WSeq α) (this : a ∈ (cons x s).tail)
  (e : some (some a) = (↑(cons x s).tail : Stream' (Option (Option α))) 0), a ∈ cons x s
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
s : WSeq α
zero :
  ∀ (this : Membership.mem (γ := WSeq α) (tail nil) a)
    (e : some (some a) = (↑(tail nil) : Stream' (Option (Option α))) 0), Membership.mem (γ := WSeq α) nil a
zero₁ :
  ∀ (x : α) (s : WSeq α) (this : a ∈ (cons x s).tail)
    (e : some (some a) = (↑(cons x s).tail : Stream' (Option (Option α))) 0), a ∈ cons x s
⊢ ∀ (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) 0), a ∈ s
have zero₂ : ∀ (s : WSeq α) (this : a ∈ s.think.tail) (e : some (some a) = (↑s.think.tail : Stream' (Option (Option α))) 0),
  a ∈ s.think
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
s : WSeq α
⊢ ∀ (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) (n + 1)), a ∈ s
have succ : ∀ (this : Membership.mem (γ := WSeq α) (tail nil) a)
  (e : some (some a) = (↑(tail nil) : Stream' (Option (Option α))) (n + 1)), Membership.mem (γ := WSeq α) nil a
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
s : WSeq α
succ :
  ∀ (this : Membership.mem (γ := WSeq α) (tail nil) a)
    (e : some (some a) = (↑(tail nil) : Stream' (Option (Option α))) (n + 1)), Membership.mem (γ := WSeq α) nil a
⊢ ∀ (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) (n + 1)), a ∈ s
have succ₁ : ∀ (x : α) (s : WSeq α) (this : a ∈ (cons x s).tail)
  (e : some (some a) = (↑(cons x s).tail : Stream' (Option (Option α))) (n + 1)), a ∈ cons x s
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
s : WSeq α
succ :
  ∀ (this : Membership.mem (γ := WSeq α) (tail nil) a)
    (e : some (some a) = (↑(tail nil) : Stream' (Option (Option α))) (n + 1)), Membership.mem (γ := WSeq α) nil a
succ₁ :
  ∀ (x : α) (s : WSeq α) (this : a ∈ (cons x s).tail)
    (e : some (some a) = (↑(cons x s).tail : Stream' (Option (Option α))) (n + 1)), a ∈ cons x s
⊢ ∀ (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) (n + 1)), a ∈ s
have succ₂ : ∀ (s : WSeq α) (this : a ∈ s.think.tail) (e : some (some a) = (↑s.think.tail : Stream' (Option (Option α))) (n + 1)),
  a ∈ s.think
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
⊢ ∀ (this : Membership.mem (γ := WSeq α) (tail nil) a)
    (e : some (some a) = (↑(tail nil) : Stream' (Option (Option α))) 0), Membership.mem (γ := WSeq α) nil a
have zero : ∀ (this : Membership.mem (γ := WSeq α) nil a) (e : some (some a) = Seq.get? nil 0), Membership.mem (γ := WSeq α) nil a
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a x : α
s : WSeq α
⊢ ∀ (this : a ∈ (cons x s).tail) (e : some (some a) = (↑(cons x s).tail : Stream' (Option (Option α))) 0), a ∈ cons x s
have zero : ∀ (this : a ∈ s) (e : some (some a) = Seq.get? s 0), a = x ∨ a ∈ s
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
s : WSeq α
⊢ ∀ (this : a ∈ s.think.tail) (e : some (some a) = (↑s.think.tail : Stream' (Option (Option α))) 0), a ∈ s.think
have zero : ∀ (this : a ∈ s.tail) (e : some (some a) = Seq.get? s.tail.think 0), a ∈ s
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
⊢ ∀ (this : Membership.mem (γ := WSeq α) (tail nil) a)
    (e : some (some a) = (↑(tail nil) : Stream' (Option (Option α))) (n + 1)), Membership.mem (γ := WSeq α) nil a
have succ : ∀ (this : Membership.mem (γ := WSeq α) nil a) (e : some (some a) = Seq.get? nil (n + 1)),
  Membership.mem (γ := WSeq α) nil a
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
x : α
s : WSeq α
⊢ ∀ (this : a ∈ (cons x s).tail) (e : some (some a) = (↑(cons x s).tail : Stream' (Option (Option α))) (n + 1)),
    a ∈ cons x s
have succ : ∀ (this : a ∈ s) (e : some (some a) = Seq.get? s (n + 1)), a = x ∨ a ∈ s
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
s : WSeq α
⊢ ∀ (this : a ∈ s.think.tail) (e : some (some a) = (↑s.think.tail : Stream' (Option (Option α))) (n + 1)), a ∈ s.think
have succ : ∀ (this : a ∈ s.tail) (e : some (some a) = Seq.get? s.tail.think (n + 1)), a ∈ s
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = Seq.get? s.tail.think (n + 1)
⊢ a ∈ s
have apply : some (some a) = (↑s.tail : Stream' (Option (Option α))) n
Tactic: apply IH m
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = Seq.get? s.tail.think (n + 1)
⊢ some (some a) = (↑s.tail : Stream' (Option (Option α))) n
have rw : Seq.get? s.tail.think (n + 1) = (↑s.tail : Stream' (Option (Option α))) n
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α} (this : a ∈ s.tail) (e : some (some a) = (↑s.tail : Stream' (Option (Option α))) n), a ∈ s
s : WSeq α
m : a ∈ s.tail
e : some (some a) = Seq.get? s.tail.think (n + 1)
⊢ Seq.get? s.tail.think (n + 1) = (↑s.tail : Stream' (Option (Option α))) n
have mk : ∀ (val : Stream' (Option (Option α))) (property : val.IsSeq),
  Seq.get? (think (Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) val property)) (n + 1) =
    (↑(Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) val property) : Stream' (Option (Option α))) n
Tactic: cases tail s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
n : ℕ
⊢ some a ∈ s.get? n → a ∈ s
have zero : ∀ {s : WSeq α}, some a ∈ s.get? 0 → a ∈ s
Tactic: induction n generalizing s
Cleared hypotheses: s, n
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
n : ℕ
zero : ∀ {s : WSeq α}, some a ∈ s.get? 0 → a ∈ s
⊢ some a ∈ s.get? n → a ∈ s
have succ : ∀ (n : ℕ), (∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s) → ∀ {s : WSeq α}, some a ∈ s.get? (n + 1) → a ∈ s
Tactic: induction n generalizing s
Cleared hypotheses: s, n
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
⊢ a ∈ s
have rcases : ∀ (o : Option (α × WSeq α)) (h1 : o ∈ (s.drop 0).destruct) (h2 : Prod.fst <$> o = some a), a ∈ s
Tactic: rcases Computation.exists_of_mem_map h with ⟨o, h1, h2⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
o : Option (α × WSeq α)
h1 : o ∈ (s.drop 0).destruct
h2 : Prod.fst <$> o = some a
⊢ a ∈ s
have none : ∀ (h1 : none ∈ (s.drop 0).destruct) (h2 : Functor.map (α := α × WSeq α) Prod.fst none = some a), a ∈ s
Tactic: rcases o with - | o
Cleared hypotheses: o, h1, h2
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
o : Option (α × WSeq α)
h1 : o ∈ (s.drop 0).destruct
h2 : Prod.fst <$> o = some a
none :
  ∀ (h1 : Option.none ∈ (s.drop 0).destruct) (h2 : Functor.map (α := α × WSeq α) Prod.fst Option.none = some a), a ∈ s
⊢ a ∈ s
have some : ∀ (o : α × WSeq α) (h1 : some o ∈ (s.drop 0).destruct) (h2 : Prod.fst <$> some o = some a), a ∈ s
Tactic: rcases o with - | o
Cleared hypotheses: o, h1, h2
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
o : α × WSeq α
h1 : some o ∈ (s.drop 0).destruct
h2 : Prod.fst <$> some o = some a
⊢ a ∈ s
have h' : o.1 = a
Tactic: injection h2 with h'
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
s : WSeq α
h : some a ∈ s.get? 0
o : α × WSeq α
h1 : some o ∈ (s.drop 0).destruct
h' : o.1 = a
⊢ a ∈ s
have some : ∀ (a' : α) (s' : WSeq α) (h1 : some (a', s') ∈ (s.drop 0).destruct) (h' : (a', s').1 = a), a ∈ s
Tactic: obtain ⟨a', s'⟩ := o
Cleared hypotheses: o, h1, h'
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n + 1)
⊢ a ∈ s
have this : some a ∈ s.tail.get? n → a ∈ s.tail
Tactic: have := @IH (tail s)
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
n : ℕ
IH : ∀ {s : WSeq α}, some a ∈ s.get? n → a ∈ s
s : WSeq α
h : some a ∈ s.get? (n + 1)
this : some a ∈ s.tail.get? n → a ∈ s.tail
⊢ a ∈ s
have this₁ : some a ∈ s.get? (n + 1) → a ∈ s.tail
Tactic: rw [get?_tail] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h : a ∈ s
⊢ ∃ (n : ℕ), some a ∈ s.get? n
have h1 : ∀ (b : α) (s' : WSeq α), (a = b ∨ ∃ (n : ℕ), some a ∈ s'.get? n) → ∃ (n : ℕ), some a ∈ (cons b s').get? n
Tactic: apply mem_rec_on h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h : a ∈ s
h1 : ∀ (b : α) (s' : WSeq α), (a = b ∨ ∃ (n : ℕ), some a ∈ s'.get? n) → ∃ (n : ℕ), some a ∈ (cons b s').get? n
⊢ ∃ (n : ℕ), some a ∈ s.get? n
have h2 : ∀ (s : WSeq α), (∃ (n : ℕ), some a ∈ s.get? n) → ∃ (n : ℕ), some a ∈ s.think.get? n
Tactic: apply mem_rec_on h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
a' : α
s' : WSeq α
h : a = a' ∨ ∃ (n : ℕ), some a ∈ s'.get? n
⊢ ∃ (n : ℕ), some a ∈ (cons a' s').get? n
have h1 : ∀ (h : a = a'), ∃ (n : ℕ), some a ∈ (cons a' s').get? n
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
a' : α
s' : WSeq α
h : a = a' ∨ ∃ (n : ℕ), some a ∈ s'.get? n
h1 : ∀ (h : a = a'), ∃ (n : ℕ), some a ∈ (cons a' s').get? n
⊢ ∃ (n : ℕ), some a ∈ (cons a' s').get? n
have h1₁ : ∀ (h : ∃ (n : ℕ), some a ∈ s'.get? n), ∃ (n : ℕ), some a ∈ (cons a' s').get? n
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ ∃ (n : ℕ), some a ∈ (cons a' s').get? n
have h1 : some a ∈ (cons a' s').get? 0
Tactic: exists 0
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a ∈ (cons a' s').get? 0
have h1 : some a ∈ Computation.pure (some a')
Tactic: simp only [get?, drop, head_cons]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
a' : α
s' : WSeq α
h : a = a'
⊢ some a ∈ Computation.pure (some a')
have h1 : some a' ∈ Computation.pure (some a')
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
a' : α
s' : WSeq α
h : ∃ (n : ℕ), some a ∈ s'.get? n
⊢ ∃ (n : ℕ), some a ∈ (cons a' s').get? n
have h1 : ∀ (n : ℕ) (h : some a ∈ s'.get? n), ∃ (n : ℕ), some a ∈ (cons a' s').get? n
Tactic: obtain ⟨n, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
a' : α
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ ∃ (n : ℕ), some a ∈ (cons a' s').get? n
have h1 : some a ∈ (cons a' s').get? (n + 1)
Tactic: exists n + 1
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
s' : WSeq α
h : ∃ (n : ℕ), some a ∈ s'.get? n
⊢ ∃ (n : ℕ), some a ∈ s'.think.get? n
have h2 : ∀ (n : ℕ) (h : some a ∈ s'.get? n), ∃ (n : ℕ), some a ∈ s'.think.get? n
Tactic: obtain ⟨n, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ ∃ (n : ℕ), some a ∈ s'.think.get? n
have h2 : some a ∈ s'.think.get? n
Tactic: exists n
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
s' : WSeq α
n : ℕ
h : some a ∈ s'.get? n
⊢ some a ∈ s'.think.get? n
have h2 : some a ∈ (s'.drop n).head.think
Tactic: simp only [get?, dropn_think, head_think]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
⊢ ∃ (s' : WSeq α), some (a, s') ∈ (s.drop n).destruct
have rcases : ∀ (o : Option (α × WSeq α)) (om : o ∈ (s.drop n).destruct), ∃ (s' : WSeq α), some (a, s') ∈ (s.drop n).destruct
Tactic: rcases (head_terminates_iff _).1 ⟨⟨_, h⟩⟩ with ⟨⟨o, om⟩⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
o : Option (α × WSeq α)
om : o ∈ (s.drop n).destruct
⊢ ∃ (s' : WSeq α), some (a, s') ∈ (s.drop n).destruct
have this : Prod.fst <$> o = some a
Tactic: have := Computation.mem_unique (Computation.mem_map _ om) h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
o : Option (α × WSeq α)
om : o ∈ (s.drop n).destruct
this : Prod.fst <$> o = some a
⊢ ∃ (s' : WSeq α), some (a, s') ∈ (s.drop n).destruct
have none : ∀ (om : none ∈ (s.drop n).destruct) (this : Functor.map (α := α × WSeq α) Prod.fst none = some a),
  ∃ (s' : WSeq α), some (a, s') ∈ (s.drop n).destruct
Tactic: rcases o with - | o
Cleared hypotheses: o, om, this
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
o : Option (α × WSeq α)
om : o ∈ (s.drop n).destruct
this : Prod.fst <$> o = some a
none :
  ∀ (om : Option.none ∈ (s.drop n).destruct) (this : Functor.map (α := α × WSeq α) Prod.fst Option.none = some a),
    ∃ (s' : WSeq α), some (a, s') ∈ (s.drop n).destruct
⊢ ∃ (s' : WSeq α), some (a, s') ∈ (s.drop n).destruct
have some : ∀ (o : α × WSeq α) (om : some o ∈ (s.drop n).destruct) (this : Prod.fst <$> some o = some a),
  ∃ (s' : WSeq α), some (a, s') ∈ (s.drop n).destruct
Tactic: rcases o with - | o
Cleared hypotheses: o, om, this
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
o : α × WSeq α
om : some o ∈ (s.drop n).destruct
this : Prod.fst <$> some o = some a
⊢ ∃ (s' : WSeq α), some (a, s') ∈ (s.drop n).destruct
have i : o.1 = a
Tactic: injection this with i
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
o : α × WSeq α
om : some o ∈ (s.drop n).destruct
i : o.1 = a
⊢ ∃ (s' : WSeq α), some (a, s') ∈ (s.drop n).destruct
have some : ∀ (a' : α) (s' : WSeq α) (om : some (a', s') ∈ (s.drop n).destruct) (i : (a', s').1 = a),
  ∃ (s' : WSeq α), some (a, s') ∈ (s.drop n).destruct
Tactic: obtain ⟨a', s'⟩ := o
Cleared hypotheses: o, om, i
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
s : WSeq α
a : α
h_1 : a ∈ s
n : ℕ
h : some a ∈ s.get? n
a' : α
s' : WSeq α
om : some (a', s') ∈ (s.drop n).destruct
i : a' = a
⊢ ∃ (s' : WSeq α), some (a, s') ∈ (s.drop n).destruct
have om₁ : some (a, s') ∈ (s.drop n).destruct
Tactic: rw [i] at om
Cleared hypotheses: om, i
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f (Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al)
⊢ ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al, f a = b
have let : ∀ (o : Option α) (om : o ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al)
  (oe : Option.map f o = some b), ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al, f a = b
Tactic: let ⟨o, om, oe⟩ := Seq.exists_of_mem_map h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f (Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al)
o : Option α
om : o ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al
oe : Option.map f o = some b
⊢ ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al, f a = b
have none : ∀ (om : none ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al)
  (oe : Option.map f none = some b),
  ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al, f a = b
Tactic: rcases o with - | a
Cleared hypotheses: o, om, oe
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f (Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al)
o : Option α
om : o ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al
oe : Option.map f o = some b
none :
  ∀ (om : Option.none ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al)
    (oe : Option.map f Option.none = some b),
    ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al, f a = b
⊢ ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al, f a = b
have some : ∀ (a : α) (om : some a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al)
  (oe : Option.map f (some a) = some b),
  ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al, f a = b
Tactic: rcases o with - | a
Cleared hypotheses: o, om, oe
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
β : Type v
f : α → β
b : β
g : Stream' (Option (Option α))
al : g.IsSeq
h : b ∈ map f (Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al)
a : α
om : some a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al
oe : Option.map f (some a) = some b
⊢ ∃ a ∈ Subtype.mk (p := fun (f : Stream' (Option (Option α))) ↦ f.IsSeq) g al, f a = b
have h' : f a = b
Tactic: injection oe with h'
Cleared hypotheses: oe
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
l : List α
s : WSeq α
⊢ Eq (α := Computation (List α))
    (Computation.corec
      (fun (x : List α × WSeq α) ↦
        match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
        | (l, s) =>
          match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
          | none => Sum.inl l.reverse
          | some (none, s') => Sum.inr (l, s')
          | some (some a, s') => Sum.inr (a :: l, s'))
      (l, s))
    ((fun (x : List α) ↦ l.reverse ++ x) <$> s.toList)
have c1 : Computation.IsBisimulation.{u} (α := List α) fun (c1 c2 : Computation (List α)) ↦
  ∃ (l' : List α) (s : WSeq α),
    c1 =
        Computation.corec
          (fun (x : List α × WSeq α) ↦
            match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
            | (l, s) =>
              match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l' ++ l, s) ∧
      c2 =
        Computation.map (fun (x : List α) ↦ l.reverse ++ x)
          (Computation.corec
            (fun (x : List α × WSeq α) ↦
              match (motive := List α × WSeq α → List α ⊕ List α × WSeq α) x with
              | (l, s) =>
                match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct s with
                | none => Sum.inl l.reverse
                | some (none, s') => Sum.inr (l, s')
                | some (some a, s') => Sum.inr (a :: l, s'))
            (l', s))
Tactic: refine
    Computation.eq_of_bisim
      (fun c1 c2 =>
        ∃ (l' : List α) (s : WSeq α),
          c1 = Computation.corec (fun ⟨l, s⟩ =>
            match Seq.destruct s with
            | none => Sum.inl l.reverse
            | some (none, s') => Sum.inr (l, s')
            | some (some a, s') => Sum.inr (a::l, s')) (l' ++ l, s) ∧
            c2 = Computation.map (l.reverse ++ ·) (Computation.corec (fun ⟨l, s⟩ =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a::l, s')) (l', s)))
      ?_ ⟨[], s, rfl, rfl⟩