awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
s : WSeq α
⊢ Computation.destruct
      (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'))
        ([], cons a s)) =
    Sum.inr
      (List.cons a <$>
        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'))
          ([], s))
have simp : Computation.corec
    (fun (x : List α × WSeq α) ↦
      match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct x.2 with
      | none => Sum.inl x.1.reverse
      | some (none, s') => Sum.inr (x.1, s')
      | some (some a, s') => Sum.inr (a :: x.1, s'))
    ([a], s) =
  List.cons a <$>
    Computation.corec
      (fun (x : List α × WSeq α) ↦
        match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct x.2 with
        | none => Sum.inl x.1.reverse
        | some (none, s') => Sum.inr (x.1, s')
        | some (some a, s') => Sum.inr (a :: x.1, s'))
      ([], s)
Tactic: simp only [toList'_cons, Computation.destruct_think, Sum.inr.injEq]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
s : WSeq α
⊢ Computation.corec
      (fun (x : List α × WSeq α) ↦
        match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct x.2 with
        | none => Sum.inl x.1.reverse
        | some (none, s') => Sum.inr (x.1, s')
        | some (some a, s') => Sum.inr (a :: x.1, s'))
      ([a], s) =
    List.cons a <$>
      Computation.corec
        (fun (x : List α × WSeq α) ↦
          match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct x.2 with
          | none => Sum.inl x.1.reverse
          | some (none, s') => Sum.inr (x.1, s')
          | some (some a, s') => Sum.inr (a :: x.1, s'))
        ([], s)
have rw : (fun (x : List α) ↦ [a].reverse ++ x) <$> s.toList =
  List.cons a <$>
    Computation.corec
      (fun (x : List α × WSeq α) ↦
        match (motive := Option (Seq1 (Option α)) → List α ⊕ List α × WSeq α) Seq.destruct x.2 with
        | none => Sum.inl x.1.reverse
        | some (none, s') => Sum.inr (x.1, s')
        | some (some a, s') => Sum.inr (a :: x.1, s'))
      ([], s)
Tactic: rw [toList'_map]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
l : List α
⊢ l ∈ (↑l : WSeq α).toList
have nil : Membership.mem (γ := Computation (List α)) (toList (↑[] : WSeq α)) []
Tactic: induction l with
  | nil => simp
  | cons a l IH => simpa [ret_mem] using think_mem (Computation.mem_map _ IH)
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
l : List α
nil : Membership.mem (γ := Computation (List α)) (toList (↑[] : WSeq α)) []
⊢ l ∈ (↑l : WSeq α).toList
have cons : ∀ (a : α) (l : List α) (IH : l ∈ (↑l : WSeq α).toList), a :: l ∈ (↑(a :: l) : WSeq α).toList
Tactic: induction l with
  | nil => simp
  | cons a l IH => simpa [ret_mem] using think_mem (Computation.mem_map _ IH)
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : Seq α
⊢ (↑s : WSeq α).destruct.destruct = Sum.inl (Option.map (fun (a : α) ↦ (a, (↑s.tail : WSeq α))) s.head)
have simp : Eq.{u + 1} (α := Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
  (match (motive := Option (α × WSeq α) ⊕ WSeq α → Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
      match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
        Option.map (fun (a' : Option α) ↦ (a', (some <$> s).tail)) ((some <$> s).get? 0) with
      | none => Sum.inl none
      | some (none, s') => Sum.inr s'
      | some (some a, s') => Sum.inl (some (a, s')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Computation.corec
          (fun (s : WSeq α) ↦
            match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
              Option.map (fun (a' : Option α) ↦ (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b) :
    Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
  (Sum.inl (Option.map (fun (a : α) ↦ (a, some <$> s.tail)) (s.get? 0)) :
    Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
Tactic: simp only [destruct, Seq.destruct, Option.map_eq_map, ofSeq, Computation.corec_eq, rmap,
      Seq.head]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : Seq α
⊢ Eq.{u + 1} (α := Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (match (motive := Option (α × WSeq α) ⊕ WSeq α → Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
        match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
          Option.map (fun (a' : Option α) ↦ (a', (some <$> s).tail)) ((some <$> s).get? 0) with
        | none => Sum.inl none
        | some (none, s') => Sum.inr s'
        | some (some a, s') => Sum.inl (some (a, s')) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Computation.corec
            (fun (s : WSeq α) ↦
              match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
                Option.map (fun (a' : Option α) ↦ (a', Seq.tail s)) (Seq.get? s 0) with
              | none => Sum.inl none
              | some (none, s') => Sum.inr s'
              | some (some a, s') => Sum.inl (some (a, s')))
            b) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (Sum.inl (Option.map (fun (a : α) ↦ (a, some <$> s.tail)) (s.get? 0)) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
have rw : Eq.{u + 1} (α := Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
  (match (motive := Option (α × WSeq α) ⊕ WSeq α → Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
      match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
        Option.map (fun (a' : Option α) ↦ (a', (some <$> s).tail)) (some <$> s.get? 0) with
      | none => Sum.inl none
      | some (none, s') => Sum.inr s'
      | some (some a, s') => Sum.inl (some (a, s')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Computation.corec
          (fun (s : WSeq α) ↦
            match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
              Option.map (fun (a' : Option α) ↦ (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b) :
    Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
  (Sum.inl (Option.map (fun (a : α) ↦ (a, some <$> s.tail)) (s.get? 0)) :
    Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
Tactic: rw [show Seq.get? (some <$> s) 0 = some <$> Seq.get? s 0 by apply Seq.map_get?]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : Seq α
⊢ Eq.{u + 1} (α := Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (match (motive := Option (α × WSeq α) ⊕ WSeq α → Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
        match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
          Option.map (fun (a' : Option α) ↦ (a', (some <$> s).tail)) (some <$> s.get? 0) with
        | none => Sum.inl none
        | some (none, s') => Sum.inr s'
        | some (some a, s') => Sum.inl (some (a, s')) with
      | Sum.inl a => Sum.inl a
      | Sum.inr b =>
        Sum.inr
          (Computation.corec
            (fun (s : WSeq α) ↦
              match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
                Option.map (fun (a' : Option α) ↦ (a', Seq.tail s)) (Seq.get? s 0) with
              | none => Sum.inl none
              | some (none, s') => Sum.inr s'
              | some (some a, s') => Sum.inl (some (a, s')))
            b) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
    (Sum.inl (Option.map (fun (a : α) ↦ (a, some <$> s.tail)) (s.get? 0)) :
      Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
have none : Eq.{u + 1} (α := Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
  (match (motive := Option (α × WSeq α) ⊕ WSeq α → Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
      match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
        Option.map (fun (a' : Option α) ↦ (a', (some <$> s).tail)) (some <$> none) with
      | none => Sum.inl none
      | some (none, s') => Sum.inr s'
      | some (some a, s') => Sum.inl (some (a, s')) with
    | Sum.inl a => Sum.inl a
    | Sum.inr b =>
      Sum.inr
        (Computation.corec
          (fun (s : WSeq α) ↦
            match (motive := Option (Seq1 (Option α)) → Option (α × WSeq α) ⊕ WSeq α)
              Option.map (fun (a' : Option α) ↦ (a', Seq.tail s)) (Seq.get? s 0) with
            | none => Sum.inl none
            | some (none, s') => Sum.inr s'
            | some (some a, s') => Sum.inl (some (a, s')))
          b) :
    Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
  (Sum.inl (Option.map (fun (a : α) ↦ (a, some <$> s.tail)) none) :
    Option (α × WSeq α) ⊕ Computation (Option (α × WSeq α)))
Tactic: rcases Seq.get? s 0 with - | a
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : Seq α
⊢ (↑s : WSeq α).head = Computation.pure s.head
have simp : Computation.pure (Option.map (comp (β := α × WSeq α) Prod.fst fun (a : α) ↦ (a, (↑s.tail : WSeq α))) s.head) =
  Computation.pure s.head
Tactic: simp only [head, Option.map_eq_map, destruct_ofSeq, Computation.map_pure, Option.map_map]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : Seq α
⊢ Computation.pure (Option.map (comp (β := α × WSeq α) Prod.fst fun (a : α) ↦ (a, (↑s.tail : WSeq α))) s.head) =
    Computation.pure s.head
have none : Eq.{u + 1} (α := Computation (Option α))
  (Computation.pure (Option.map (α := α) (comp (β := α × WSeq α) Prod.fst fun (a : α) ↦ (a, (↑s.tail : WSeq α))) none))
  (Computation.pure none)
Tactic: cases Seq.head s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : Seq α
none :
  Eq.{u + 1} (α := Computation (Option α))
    (Computation.pure
      (Option.map (α := α) (comp (β := α × WSeq α) Prod.fst fun (a : α) ↦ (a, (↑s.tail : WSeq α))) Option.none))
    (Computation.pure Option.none)
⊢ Computation.pure (Option.map (comp (β := α × WSeq α) Prod.fst fun (a : α) ↦ (a, (↑s.tail : WSeq α))) s.head) =
    Computation.pure s.head
have some : ∀ (val : α),
  Computation.pure (Option.map (comp (β := α × WSeq α) Prod.fst fun (a : α) ↦ (a, (↑s.tail : WSeq α))) (some val)) =
    Computation.pure (some val)
Tactic: cases Seq.head s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : Seq α
⊢ (↑s : WSeq α).tail = (↑s.tail : WSeq α)
have simp : Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd
    (Option.map (fun (a : α) ↦ (a, (↑s.tail : WSeq α))) s.head) =
  (↑s.tail : WSeq α)
Tactic: simp only [tail, destruct_ofSeq, map_pure', flatten_pure]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : Seq α
⊢ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd
      (Option.map (fun (a : α) ↦ (a, (↑s.tail : WSeq α))) s.head) =
    (↑s.tail : WSeq α)
have nil : Eq.{u + 1} (α := WSeq α)
  (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) nil Prod.snd
      (Option.map (fun (a : α) ↦ (a, (↑(Seq.tail Seq.nil) : WSeq α))) (Seq.head Seq.nil)) :
    WSeq α)
  ((↑(Seq.tail Seq.nil) : WSeq α) : WSeq α)
Tactic: induction s using Seq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : Seq α
nil :
  Eq.{u + 1} (α := WSeq α)
    (Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) WSeq.nil Prod.snd
        (Option.map (fun (a : α) ↦ (a, (↑(Seq.tail Seq.nil) : WSeq α))) (Seq.head Seq.nil)) :
      WSeq α)
    ((↑(Seq.tail Seq.nil) : WSeq α) : WSeq α)
⊢ Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) WSeq.nil Prod.snd
      (Option.map (fun (a : α) ↦ (a, (↑s.tail : WSeq α))) s.head) =
    (↑s.tail : WSeq α)
have cons : ∀ (x : α) (s : Seq α),
  Option.rec (motive := fun (x : Option (α × WSeq α)) ↦ WSeq α) WSeq.nil Prod.snd
      (Option.map (fun (a : α) ↦ (a, (↑(Seq.cons x s).tail : WSeq α))) (Seq.cons x s).head) =
    (↑(Seq.cons x s).tail : WSeq α)
Tactic: induction s using Seq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ ((↑s : WSeq α).drop n).tail = (↑(s.drop n).tail : WSeq α)
have rw : (↑(s.drop n) : WSeq α).tail = (↑(s.drop n).tail : WSeq α)
Tactic: rw [dropn_ofSeq s n, tail_ofSeq]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
rw : (↑(s.drop n) : WSeq α).tail = (↑(s.drop n).tail : WSeq α)
⊢ ((↑s : WSeq α).drop n).tail = (↑(s.drop n).tail : WSeq α)
have rw₁ : (↑(s.drop n).tail : WSeq α) = (↑(s.drop n).tail : WSeq α)
Tactic: rw [dropn_ofSeq s n, tail_ofSeq]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
⊢ ((↑s : WSeq α).drop n).head = Computation.pure (s.get? n)
have rw : (↑(s.drop n) : WSeq α).head = Computation.pure (s.get? n)
Tactic: rw [dropn_ofSeq, head_ofSeq, Seq.head_dropn]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
rw : (↑(s.drop n) : WSeq α).head = Computation.pure (s.get? n)
⊢ ((↑s : WSeq α).drop n).head = Computation.pure (s.get? n)
have rw₁ : Computation.pure (s.drop n).head = Computation.pure (s.get? n)
Tactic: rw [dropn_ofSeq, head_ofSeq, Seq.head_dropn]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s : Seq α
n : ℕ
rw : (↑(s.drop n) : WSeq α).head = Computation.pure (s.get? n)
rw₁ : Computation.pure (s.drop n).head = Computation.pure (s.get? n)
⊢ ((↑s : WSeq α).drop n).head = Computation.pure (s.get? n)
have rw₂ : Computation.pure (s.get? n) = Computation.pure (s.get? n)
Tactic: rw [dropn_ofSeq, head_ofSeq, Seq.head_dropn]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Seq.map (Option.map (g ∘ f)) s = Seq.map (Option.map g) (Seq.map (Option.map f) s)
have rw : Seq.map (Option.map (g ∘ f)) s = Seq.map (Option.map g ∘ Option.map f) s
Tactic: rw [← Seq.map_comp]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Seq.map (Option.map (g ∘ f)) s = Seq.map (Option.map g ∘ Option.map f) s
have h : Seq.map (Option.map (g ∘ f)) = Seq.map (Option.map g ∘ Option.map f)
Tactic: apply congr_fun
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Seq.map (Option.map (g ∘ f)) = Seq.map (Option.map g ∘ Option.map f)
have h : Option.map (g ∘ f) = Option.map g ∘ Option.map f
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
⊢ Option.map (g ∘ f) = Option.map g ∘ Option.map f
have h : ∀ (a : γ), Option.map (g ∘ f) none = some a ↔ (Option.map g ∘ Option.map f) none = some a
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : WSeq α
h : ∀ (a : γ), Option.map (g ∘ f) none = some a ↔ (Option.map g ∘ Option.map f) none = some a
⊢ Option.map (g ∘ f) = Option.map g ∘ Option.map f
have h₁ : ∀ (val : α) (a : γ), Option.map (g ∘ f) (some val) = some a ↔ (Option.map g ∘ Option.map f) (some val) = some a
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
⊢ ∀ {S : WSeq (WSeq α)}, a ∈ S.join → ∃ s ∈ S, a ∈ s
have ss : ∀ (ss : WSeq α),
  a ∈ ss → ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
Tactic: suffices
    ∀ ss : WSeq α,
      a ∈ ss → ∀ s S, append s (join S) = ss → a ∈ append s (join S) → a ∈ s ∨ ∃ s, s ∈ S ∧ a ∈ s
    from fun S h => (this _ h nil S (by simp) (by simp [h])).resolve_left (notMem_nil _)
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
⊢ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
have h1 : ∀ (b : α) (s' : WSeq α),
  (a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = s' → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s) →
    ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = cons b s' → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
Tactic: apply mem_rec_on h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
h1 :
  ∀ (b : α) (s' : WSeq α),
    (a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = s' → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s) →
      ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = cons b s' → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
⊢ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
have h2 : ∀ (s : WSeq α),
  (∀ (s_1 : WSeq α) (S : WSeq (WSeq α)), s_1.append S.join = s → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s) →
    ∀ (s_1 : WSeq α) (S : WSeq (WSeq α)), s_1.append S.join = s.think → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s
Tactic: apply mem_rec_on h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
⊢ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
have h1 : ∀ (b : α) (ss : WSeq α)
  (o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s)
  (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = cons b ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
Tactic: apply mem_rec_on h <;> [intro b ss o; intro ss IH]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
h1 :
  ∀ (b : α) (ss : WSeq α)
    (o :
      a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s)
    (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = cons b ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
⊢ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
have h2 : ∀ (ss : WSeq α)
  (IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s)
  (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss.think → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
Tactic: apply mem_rec_on h <;> [intro b ss o; intro ss IH]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
s : WSeq α
S : WSeq (WSeq α)
⊢ s.append S.join = cons b ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
have h1 : append nil S.join = cons b ss → a ∈ append nil S.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s ∈ S, a ∈ s
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
s : WSeq α
S : WSeq (WSeq α)
h1 : append nil S.join = cons b ss → a ∈ append nil S.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s ∈ S, a ∈ s
⊢ s.append S.join = cons b ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
have h1₁ : ∀ (x : α) (s : WSeq α),
  (cons x s).append S.join = cons b ss → a ∈ (cons x s).append S.join → a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
s : WSeq α
S : WSeq (WSeq α)
h1 : append nil S.join = cons b ss → a ∈ append nil S.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s ∈ S, a ∈ s
h1₁ :
  ∀ (x : α) (s : WSeq α),
    (cons x s).append S.join = cons b ss → a ∈ (cons x s).append S.join → a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s
⊢ s.append S.join = cons b ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
have h1₂ : ∀ (s : WSeq α), s.think.append S.join = cons b ss → a ∈ s.think.append S.join → a ∈ s.think ∨ ∃ s ∈ S, a ∈ s
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
⊢ append nil S.join = cons b ss → a ∈ append nil S.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s ∈ S, a ∈ s
have h1 : append nil (join nil) = cons b ss →
  Membership.mem (γ := WSeq α) (append nil (join nil)) a →
    Membership.mem (γ := WSeq α) nil a ∨ ∃ (s : WSeq α), Membership.mem (γ := WSeq (WSeq α)) nil s ∧ a ∈ s
Tactic: induction S using WSeq.recOn
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
h1 :
  append nil (join nil) = cons b ss →
    Membership.mem (γ := WSeq α) (append nil (join nil)) a →
      Membership.mem (γ := WSeq α) nil a ∨ ∃ (s : WSeq α), Membership.mem (γ := WSeq (WSeq α)) nil s ∧ a ∈ s
⊢ append nil S.join = cons b ss → a ∈ append nil S.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s ∈ S, a ∈ s
have h1₁ : ∀ (x : WSeq α) (s : WSeq (WSeq α)),
  append nil (cons x s).join = cons b ss →
    a ∈ append nil (cons x s).join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons x s, a ∈ s_1
Tactic: induction S using WSeq.recOn
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
b : α
ss : WSeq α
o : a = b ∨ ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
S : WSeq (WSeq α)
h1 :
  append nil (join nil) = cons b ss →
    Membership.mem (γ := WSeq α) (append nil (join nil)) a →
      Membership.mem (γ := WSeq α) nil a ∨ ∃ (s : WSeq α), Membership.mem (γ := WSeq (WSeq α)) nil s ∧ a ∈ s
h1₁ :
  ∀ (x : WSeq α) (s : WSeq (WSeq α)),
    append nil (cons x s).join = cons b ss →
      a ∈ append nil (cons x s).join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons x s, a ∈ s_1
⊢ append nil S.join = cons b ss → a ∈ append nil S.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s ∈ S, a ∈ s
have h1₂ : ∀ (s : WSeq (WSeq α)),
  append nil s.think.join = cons b ss →
    a ∈ append nil s.think.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ s.think, a ∈ s_1
Tactic: induction S using WSeq.recOn
Cleared hypotheses: S