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
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 (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 <;>
      [induction S using WSeq.recOn; skip; skip]
Cleared hypotheses: s, 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 (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
⊢ s.append S.join = cons b ss → a ∈ s.append S.join → a ∈ s ∨ ∃ 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 <;>
      [induction S using WSeq.recOn; skip; skip]
Cleared hypotheses: s, 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 (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
⊢ s.append S.join = cons b ss → a ∈ s.append S.join → a ∈ s ∨ ∃ 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 <;>
      [induction S using WSeq.recOn; skip; skip]
Cleared hypotheses: s, 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 (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
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
⊢ 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 <;>
      [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
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 (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
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
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 <;>
      [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
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
ej : append nil (join nil) = cons b ss
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 = cons b ss
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
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
x : WSeq α
s : WSeq (WSeq α)
ej : append nil (cons x s).join = cons b ss
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 = cons b ss
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
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 α)
ej : append nil s.think.join = cons b ss
m : a ∈ append nil s.think.join
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ s.think, a ∈ s_1
have ej₁ : s.join.think = cons b ss
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
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 α)
x : α
s : WSeq α
ej : (cons x s).append S.join = cons b ss
m : a ∈ (cons x s).append S.join
⊢ a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s
have ej₁ : cons x (s.append S.join) = cons b ss
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
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 α)
s : WSeq α
ej : s.think.append S.join = cons b ss
m : a ∈ s.think.append S.join
⊢ a ∈ s.think ∨ ∃ s ∈ S, a ∈ s
have ej₁ : (s.append S.join).think = cons b ss
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
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
m : Membership.mem (γ := WSeq α) (append nil (join nil)) a
ej : nil = cons b ss
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ (s : WSeq α), Membership.mem (γ := WSeq (WSeq α)) nil s ∧ a ∈ s
have this : Seq.destruct nil = Seq.destruct (cons b ss)
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
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
x : WSeq α
s : WSeq (WSeq α)
m : a ∈ append nil (cons x s).join
ej : (x.append s.join).think = cons b ss
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ cons x s, a ∈ s_1
have this : Seq.destruct (x.append s.join).think = Seq.destruct (cons b ss)
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
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 α)
m : a ∈ append nil s.think.join
ej : s.join.think = cons b ss
⊢ Membership.mem (γ := WSeq α) nil a ∨ ∃ s_1 ∈ s.think, a ∈ s_1
have this : Seq.destruct s.join.think = Seq.destruct (cons b ss)
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
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 α)
x : α
s : WSeq α
m : a ∈ (cons x s).append S.join
ej : cons x (s.append S.join) = cons b ss
⊢ a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s
have this : Seq.destruct (cons x (s.append S.join)) = Seq.destruct (cons b ss)
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
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 α)
s : WSeq α
m : a ∈ s.think.append S.join
ej : (s.append S.join).think = cons b ss
⊢ a ∈ s.think ∨ ∃ s ∈ S, a ∈ s
have this : Seq.destruct (s.append S.join).think = Seq.destruct (cons b ss)
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
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 α)
x : α
s : WSeq α
m : a ∈ (cons x s).append S.join
ej : cons x (s.append S.join) = cons b ss
this : Seq.destruct (cons x (s.append S.join)) = Seq.destruct (cons b ss)
⊢ a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s
have this₁ : x = b ∧ 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
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 α)
x : α
s : WSeq α
m : a ∈ (cons x s).append S.join
ej : cons x (s.append S.join) = cons b ss
this : x = b ∧ s.append S.join = ss
⊢ a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s
have left : x = b
Tactic: cases 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
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 α)
x : α
s : WSeq α
m : a ∈ (cons x s).append S.join
ej : cons x (s.append S.join) = cons b ss
this : x = b ∧ s.append S.join = ss
left : x = b
⊢ a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s
have right : s.append S.join = ss
Tactic: cases 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
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 α)
x : α
s_1 : WSeq α
m : a ∈ (cons x s_1).append S.join
ej : cons x (s_1.append S.join) = cons b ss
b' : x = b
s : s_1.append S.join = ss
⊢ a ∈ cons x s_1 ∨ ∃ s ∈ S, a ∈ s
have o₁ : a = x ∨
  ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
    s.append S_1.join = s_1.append S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
Tactic: substs b' ss
Cleared hypotheses: b, ss, o, ej, b', s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (hypothesis)
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 α)
x : α
s_1 : WSeq α
m : a ∈ (cons x s_1).append S.join
ej : cons x (s_1.append S.join) = cons b ss
b' : x = b
s : s_1.append S.join = ss
o₁ :
  a = x ∨
    ∀ (s : WSeq α) (S_1 : WSeq (WSeq α)),
      s.append S_1.join = s_1.append S.join → a ∈ s.append S_1.join → a ∈ s ∨ ∃ s ∈ S_1, a ∈ s
⊢ a ∈ cons x s_1 ∨ ∃ s ∈ S, a ∈ s
have ej₁ : cons x (s_1.append S.join) = cons x (s_1.append S.join)
Tactic: substs b' ss
Cleared hypotheses: b, ss, o, ej, b', s
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x : α
s : WSeq α
m : a ∈ (cons x s).append S.join
o :
  a = x ∨
    ∀ (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 : cons x (s.append S.join) = cons x (s.append S.join)
⊢ a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s
have simp : ∀ (m : a = x ∨ a ∈ s.append S.join), (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s
Tactic: simp only [cons_append, mem_cons_iff] 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 α)
x : α
s : WSeq α
m : a ∈ (cons x s).append S.join
o :
  a = x ∨
    ∀ (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 : cons x (s.append S.join) = cons x (s.append S.join)
⊢ a ∈ cons x s ∨ ∃ s ∈ S, a ∈ s
have simp? : ∀ (m : a = x ∨ a ∈ s.append S.join), (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s
Tactic: simp? at m ⊢ says simp only [cons_append, mem_cons_iff] 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 α)
x : α
s : WSeq α
o :
  a = x ∨
    ∀ (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 : cons x (s.append S.join) = cons x (s.append S.join)
m : a = x ∨ a ∈ s.append S.join
⊢ (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s
have inl : ∀ (e : a = x), (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s
Tactic: rcases o with e | IH
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x : α
s : WSeq α
o :
  a = x ∨
    ∀ (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 : cons x (s.append S.join) = cons x (s.append S.join)
m : a = x ∨ a ∈ s.append S.join
inl : ∀ (e : a = x), (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s
⊢ (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s
have inr : ∀
  (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 = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s
Tactic: rcases o with e | IH
Cleared hypotheses: o
-- Lean 4 proof step from Mathlib.Data.WSeq.Basic (goal)
Goal:
α : Type u
a : α
ss : WSeq α
h : a ∈ ss
S : WSeq (WSeq α)
x : α
s : WSeq α
ej : cons x (s.append S.join) = cons x (s.append S.join)
m : a = x ∨ a ∈ s.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
⊢ (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s
have inr : ∀ (e : a = x), (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s
Tactic: rcases m with e | 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 α)
x : α
s : WSeq α
ej : cons x (s.append S.join) = cons x (s.append S.join)
m : a = x ∨ a ∈ s.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
inr : ∀ (e : a = x), (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s
⊢ (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s
have inr₁ : ∀ (m : a ∈ s.append S.join), (a = x ∨ a ∈ s) ∨ ∃ s ∈ S, a ∈ s
Tactic: rcases m with e | m
Cleared hypotheses: m
-- 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 α)
⊢ s.append S.join = ss.think → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
have h2 : append nil S.join = ss.think → 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
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 S.join = ss.think → a ∈ append nil S.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s ∈ S, a ∈ s
⊢ 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
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 S.join = ss.think → a ∈ append nil S.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s ∈ S, a ∈ s
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
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 (WSeq α)
⊢ append nil S.join = ss.think → a ∈ append nil S.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s ∈ S, a ∈ s
have 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
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
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 α)
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
⊢ append nil S.join = ss.think → a ∈ append nil S.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s ∈ S, a ∈ s
have 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
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
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 α)
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
⊢ append nil S.join = ss.think → a ∈ append nil S.join → Membership.mem (γ := WSeq α) nil a ∨ ∃ s ∈ S, a ∈ s
have 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
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
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
have 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
Tactic: induction s using WSeq.recOn <;>
      [induction S using WSeq.recOn; skip; skip]
Cleared hypotheses: s, 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
⊢ s.append S.join = ss.think → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
have 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
Tactic: induction s using WSeq.recOn <;>
      [induction S using WSeq.recOn; skip; skip]
Cleared hypotheses: s, 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
⊢ s.append S.join = ss.think → a ∈ s.append S.join → a ∈ s ∨ ∃ s ∈ S, a ∈ s
have 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
Tactic: induction s using WSeq.recOn <;>
      [induction S using WSeq.recOn; skip; skip]
Cleared hypotheses: s, S