awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 α)
h2 :
  append nil (join nil) = ss.think →
    Membership.mem (γ := WSeq α) (append nil (join nil)) a →
      Membership.mem (γ := WSeq α) nil a ∨ ∃ (s : WSeq α), Membership.mem (γ := WSeq (WSeq α)) nil s ∧ a ∈ s
h2₁ :
  ∀ (x : WSeq α) (s : WSeq (WSeq α)),
    append nil (cons x s).join = ss.think →
      a ∈ append nil (cons x s).join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons x s, a ∈ s_1
h2₂ :
  ∀ (s : WSeq (WSeq α)),
    append nil s.think.join = ss.think →
      a ∈ append nil s.think.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ s.think, a ∈ s_1
⊢ s.append S.join = ss.think → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
have h2₃ : ∀ (x : α) (s : WSeq α),
  (cons x s).append S.join = ss.think → a ∈ (cons x s).append S.join → a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s
Tactic: induction s using WSeq.recOn <;>
      [induction S using WSeq.recOn; skip; skip]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 α)
h2 :
  append nil (join nil) = ss.think →
    Membership.mem (γ := WSeq α) (append nil (join nil)) a →
      Membership.mem (γ := WSeq α) nil a ∨ ∃ (s : WSeq α), Membership.mem (γ := WSeq (WSeq α)) nil s ∧ a ∈ s
h2₁ :
  ∀ (x : WSeq α) (s : WSeq (WSeq α)),
    append nil (cons x s).join = ss.think →
      a ∈ append nil (cons x s).join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons x s, a ∈ s_1
h2₂ :
  ∀ (s : WSeq (WSeq α)),
    append nil s.think.join = ss.think →
      a ∈ append nil s.think.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ s.think, a ∈ s_1
h2₃ :
  ∀ (x : α) (s : WSeq α),
    (cons x s).append S.join = ss.think → a ∈ (cons x s).append S.join → a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s
⊢ s.append S.join = ss.think → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
have h2₄ : ∀ (s : WSeq α), s.think.append S.join = ss.think → a ∈ s.think.append S.join → a ∈ s.think ∨ ∃ s ∈ S, a ∈ s
Tactic: induction s using WSeq.recOn <;>
      [induction S using WSeq.recOn; skip; skip]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
ej : append nil (join nil) = ss.think
m : Membership.mem (γ := WSeq α) (append nil (join nil)) a
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ (s : WSeq α), Membership.mem (γ := WSeq (WSeq α)) nil s ∧ a ∈ s
have ej₁ : nil = ss.think
Tactic: simp at ej
Cleared hypotheses: ej
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
x : WSeq α
s : WSeq (WSeq α)
ej : append nil (cons x s).join = ss.think
m : a ∈ append nil (cons x s).join
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons x s, a ∈ s_1
have ej₁ : (x.append s.join).think = ss.think
Tactic: simp at ej
Cleared hypotheses: ej
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
ej : append nil s.think.join = ss.think
m : a ∈ append nil s.think.join
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ s.think, a ∈ s_1
have ej₁ : s.join.think = ss.think
Tactic: simp at ej
Cleared hypotheses: ej
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
x : α
s : WSeq α
ej : (cons x s).append S.join = ss.think
m : a ∈ (cons x s).append S.join
⊢ a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s
have ej₁ : cons x (s.append S.join) = ss.think
Tactic: simp at ej
Cleared hypotheses: ej
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
s : WSeq α
ej : s.think.append S.join = ss.think
m : a ∈ s.think.append S.join
⊢ a ∈ s.think ∨ ∃ s ∈ S, a ∈ s
have ej₁ : (s.append S.join).think = ss.think
Tactic: simp at ej
Cleared hypotheses: ej
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
m : Membership.mem (γ := WSeq α) (append nil (join nil)) a
ej : nil = ss.think
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ (s : WSeq α), Membership.mem (γ := WSeq (WSeq α)) nil s ∧ a ∈ s
have this : Seq.destruct nil = Seq.destruct ss.think
Tactic: have := congr_arg Seq.destruct ej
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
x : WSeq α
s : WSeq (WSeq α)
m : a ∈ append nil (cons x s).join
ej : (x.append s.join).think = ss.think
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons x s, a ∈ s_1
have this : Seq.destruct (x.append s.join).think = Seq.destruct ss.think
Tactic: have := congr_arg Seq.destruct ej
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
m : a ∈ append nil s.think.join
ej : s.join.think = ss.think
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ s.think, a ∈ s_1
have this : Seq.destruct s.join.think = Seq.destruct ss.think
Tactic: have := congr_arg Seq.destruct ej
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
x : α
s : WSeq α
m : a ∈ (cons x s).append S.join
ej : cons x (s.append S.join) = ss.think
⊢ a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s
have this : Seq.destruct (cons x (s.append S.join)) = Seq.destruct ss.think
Tactic: have := congr_arg Seq.destruct ej
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
s : WSeq α
m : a ∈ s.think.append S.join
ej : (s.append S.join).think = ss.think
⊢ a ∈ s.think ∨ ∃ s ∈ S, a ∈ s
have this : Seq.destruct (s.append S.join).think = Seq.destruct ss.think
Tactic: have := congr_arg Seq.destruct ej
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
x : WSeq α
s : WSeq (WSeq α)
m : a ∈ append nil (cons x s).join
ej : (x.append s.join).think = ss.think
this : Seq.destruct (x.append s.join).think = Seq.destruct ss.think
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons x s, a ∈ s_1
have this₁ : x.append s.join = ss
Tactic: simp at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
m : a ∈ append nil s.think.join
ej : s.join.think = ss.think
this : Seq.destruct s.join.think = Seq.destruct ss.think
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ s.think, a ∈ s_1
have this₁ : s.join = ss
Tactic: simp at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
s : WSeq α
m : a ∈ s.think.append S.join
ej : (s.append S.join).think = ss.think
this : Seq.destruct (s.append S.join).think = Seq.destruct ss.think
⊢ a ∈ s.think ∨ ∃ s ∈ S, a ∈ s
have this₁ : s.append S.join = ss
Tactic: simp at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
x : WSeq α
s : WSeq (WSeq α)
m : a ∈ append nil (cons x s).join
ej : (x.append s.join).think = ss.think
this : x.append s.join = ss
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons x s, a ∈ s_1
have IH₁ : ∀ (s_1 : WSeq α) (S : WSeq (WSeq α)),
  s_1.append S.join = x.append s.join → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s
Tactic: subst ss
Cleared hypotheses: ss, IH, ej, this
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
ss : WSeq α
IH : ∀ (s : WSeq α) (S : WSeq (WSeq α)), s.append S.join = ss → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
x : WSeq α
s : WSeq (WSeq α)
m : a ∈ append nil (cons x s).join
ej : (x.append s.join).think = ss.think
this : x.append s.join = ss
IH₁ :
  ∀ (s_1 : WSeq α) (S : WSeq (WSeq α)),
    s_1.append S.join = x.append s.join → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons x s, a ∈ s_1
have ej₁ : (x.append s.join).think = (x.append s.join).think
Tactic: subst ss
Cleared hypotheses: ss, IH, ej, this
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
m : a ∈ append nil s.think.join
ej : s.join.think = ss.think
this : s.join = ss
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ s.think, a ∈ s_1
have IH₁ : ∀ (s_1 : WSeq α) (S : WSeq (WSeq α)), s_1.append S.join = s.join → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s
Tactic: subst ss
Cleared hypotheses: ss, IH, ej, this
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
m : a ∈ append nil s.think.join
ej : s.join.think = ss.think
this : s.join = ss
IH₁ :
  ∀ (s_1 : WSeq α) (S : WSeq (WSeq α)), s_1.append S.join = s.join → a ∈ s_1.append S.join → a ∈ s_1 ∨ ∃ s ∈ S, a ∈ s
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ s.think, a ∈ s_1
have ej₁ : s.join.think = s.join.think
Tactic: subst ss
Cleared hypotheses: ss, IH, ej, this
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
s : WSeq α
m : a ∈ s.think.append S.join
ej : (s.append S.join).think = ss.think
this : s.append S.join = ss
⊢ a ∈ s.think ∨ ∃ s ∈ S, a ∈ s
have IH₁ : ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
  s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
Tactic: subst ss
Cleared hypotheses: ss, IH, ej, this
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss_1 : WSeq α
h : a ∈ ss_1
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 (WSeq α)
s : WSeq α
m : a ∈ s.think.append S.join
ej : (s.append S.join).think = ss.think
this : s.append S.join = ss
IH₁ :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
⊢ a ∈ s.think ∨ ∃ s ∈ S, a ∈ s
have ej₁ : (s.append S.join).think = (s.append S.join).think
Tactic: subst ss
Cleared hypotheses: ss, IH, ej, this
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
m : a ∈ append nil (cons s S).join
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
ej : (s.append S.join).think = (s.append S.join).think
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons s S, a ∈ s_1
have h₁ : ∃ s_1 ∈ cons s S, a ∈ s_1
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
s : WSeq α
S : WSeq (WSeq α)
m : a ∈ append nil (cons s S).join
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
ej : (s.append S.join).think = (s.append S.join).think
⊢ ∃ s_1 ∈ cons s S, a ∈ s_1
have h₁ : ∀ (m : a ∈ s.append S.join), a ∈ s ∨ ∃ a_1 ∈ S, a ∈ a_1
Tactic: simp only [join_cons, nil_append, mem_think, mem_cons_iff, exists_eq_or_imp] at m ⊢
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
m : a ∈ append nil S.think.join
IH : ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)), s.append S_1.join = S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
ej : S.join.think = S.join.think
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s ∈ S.think, a ∈ s
have h₁ : ∃ s ∈ S.think, a ∈ s
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
m : a ∈ append nil S.think.join
IH : ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)), s.append S_1.join = S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
ej : S.join.think = S.join.think
⊢ ∃ s ∈ S.think, a ∈ s
have m₁ : a ∈ S.join
Tactic: replace m : a ∈ S.join := by simpa using m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
IH : ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)), s.append S_1.join = S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
ej : S.join.think = S.join.think
m : a ∈ S.join
⊢ ∃ s ∈ S.think, a ∈ s
have h₁ : ∀ (s : WSeq α) (sS : s ∈ S) (as : a ∈ s), ∃ s ∈ S.think, a ∈ s
Tactic: rcases (IH nil S (by simp) (by simp [m])).resolve_left (notMem_nil _) with ⟨s, sS, as⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
s : WSeq α
m : a ∈ s.think.append S.join
IH :
  ∀ (s_1 : WSeq α) (S_1 : WSeq (WSeq α)),
    s_1.append S_1.join = s.append S.join → a ∈ s_1.append S_1.join → a ∈ s_1 ∨ ∃ s ∈ S_1, a ∈ s
ej : (s.append S.join).think = (s.append S.join).think
⊢ a ∈ s.think ∨ ∃ s ∈ S, a ∈ s
have h2 : ∀ (m : a ∈ s.append S.join), a ∈ s ∨ ∃ s ∈ S, a ∈ s
Tactic: simp only [think_append, mem_think] at m IH ⊢
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ (map f s).destruct = Computation.map (Option.map (Prod.map f (map f))) s.destruct
have bisim : Computation.IsBisimulation.{v} (α := Option (β × WSeq β)) fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
  ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
Tactic: apply
    Computation.eq_of_bisim fun c1 c2 =>
      ∃ s,
        c1 = destruct (map f s) ∧
          c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s)
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : WSeq α
bisim :
  Computation.IsBisimulation.{v} (α := Option (β × WSeq β)) fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
    ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
⊢ (map f s).destruct = Computation.map (Option.map (Prod.map f (map f))) s.destruct
have r : ∃ (s_1 : WSeq α),
  (map f s).destruct = (map f s_1).destruct ∧
    Computation.map (Option.map (Prod.map f (map f))) s.destruct =
      Computation.map (Option.map (Prod.map f (map f))) s_1.destruct
Tactic: apply
    Computation.eq_of_bisim fun c1 c2 =>
      ∃ s,
        c1 = destruct (map f s) ∧
          c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s)
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
h : ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
      ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    c1.destruct c2.destruct
have bisim : ∀ (s : WSeq α) (h : c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct),
  BisimO
    (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
      ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    c1.destruct c2.destruct
Tactic: obtain ⟨s, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s_1 : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
      ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    c1.destruct c2.destruct
have bisim : BisimO
  (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
    ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
  (map f s).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) s.destruct).destruct
Tactic: rw [h.left, h.right]
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s_1 : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
      ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f s).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) s.destruct).destruct
have induction : ∀ (h : c1 = (map f nil).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct nil)),
  BisimO
    (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
      ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f nil).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) (destruct nil)).destruct
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s_1 : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
induction :
  ∀ (h : c1 = (map f nil).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct nil)),
    BisimO
      (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
        ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
      (map f nil).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) (destruct nil)).destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
      ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f s).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) s.destruct).destruct
have induction₁ : ∀ (x : α) (s : WSeq α)
  (h : c1 = (map f (cons x s)).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (cons x s).destruct),
  BisimO
    (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
      ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f (cons x s)).destruct.destruct
    (Computation.map (Option.map (Prod.map f (map f))) (cons x s).destruct).destruct
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
β : Type v
f : α → β
s_1 : WSeq α
c1 c2 : Computation (Option (β × WSeq β))
s : WSeq α
h : c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct
induction :
  ∀ (h : c1 = (map f nil).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct nil)),
    BisimO
      (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
        ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
      (map f nil).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) (destruct nil)).destruct
induction₁ :
  ∀ (x : α) (s : WSeq α)
    (h : c1 = (map f (cons x s)).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (cons x s).destruct),
    BisimO
      (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
        ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
      (map f (cons x s)).destruct.destruct
      (Computation.map (Option.map (Prod.map f (map f))) (cons x s).destruct).destruct
⊢ BisimO
    (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
      ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f s).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) s.destruct).destruct
have bisim : ∀ (s : WSeq α)
  (h : c1 = (map f s.think).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.think.destruct),
  BisimO
    (fun (c1 c2 : Computation (Option (β × WSeq β))) ↦
      ∃ (s : WSeq α), c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct)
    (map f s.think).destruct.destruct (Computation.map (Option.map (Prod.map f (map f))) s.think.destruct).destruct
Tactic: induction s using WSeq.recOn
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s t : WSeq α
⊢ (s.append t).destruct = s.destruct.bind (destruct_append.aux t)
have c1 : Computation.IsBisimulation.{u} (α := Option (α × WSeq α)) fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
  ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
Tactic: apply
    Computation.eq_of_bisim
      (fun c1 c2 =>
        ∃ s t, c1 = destruct (append s t) ∧ c2 = (destruct s).bind (destruct_append.aux t))
      _ ⟨s, t, rfl, rfl⟩
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
s t : WSeq α
c1 c2 : Computation (Option (α × WSeq α))
h : ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)
⊢ BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    c1.destruct c2.destruct
have rcases : ∀ (s t : WSeq α) (h : c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t)),
  BisimO
    (fun (c1 c2 : Computation (Option (α × WSeq α))) ↦
      ∃ (s : WSeq α) (t : WSeq α), c1 = (s.append t).destruct ∧ c2 = s.destruct.bind (destruct_append.aux t))
    c1.destruct c2.destruct
Tactic: rcases h with ⟨s, t, h⟩
Cleared hypotheses: h