α : Type u
β : Type v
γ : Type w
s₁ s₂ : Seq α
a : α
h this : a ∈ append s₁ s₂
⊢ a ∈ s₁ ∨ a ∈ s₂
α : Type u
β : Type v
γ : Type w
s₁ s₂ : Seq α
a : α
h : a ∈ append s₁ s₂
⊢ a ∈ s₁ ∨ a ∈ s₂
have := h
α : Type u
β : Type v
γ : Type w
s₁ s₂ : Seq α
a : α
h : a ∈ append s₁ s₂
⊢ a ∈ append s₁ s₂ → a ∈ s₁ ∨ a ∈ s₂
α : Type u
β : Type v
γ : Type w
s₁ s₂ : Seq α
a : α
h this : a ∈ append s₁ s₂
⊢ a ∈ s₁ ∨ a ∈ s₂
revert this
α : Type u
β : Type v
γ : Type w
s₁ s₂ : Seq α
a : α
h : a ∈ append s₁ s₂
ss : Seq α
e : append s₁ s₂ = ss
⊢ a ∈ ss → a ∈ s₁ ∨ a ∈ s₂
α : Type u
β : Type v
γ : Type w
s₁ s₂ : Seq α
a : α
h : a ∈ append s₁ s₂
⊢ a ∈ append s₁ s₂ → a ∈ s₁ ∨ a ∈ s₂
generalize e : append s₁ s₂ = ss
α : Type u
β : Type v
γ : Type w
s₁ s₂ : Seq α
a : α
h✝ : a ∈ append s₁ s₂
ss : Seq α
e : append s₁ s₂ = ss
h : a ∈ ss
⊢ a ∈ s₁ ∨ a ∈ s₂
α : Type u
β : Type v
γ : Type w
s₁ s₂ : Seq α
a : α
h : a ∈ append s₁ s₂
ss : Seq α
e : append s₁ s₂ = ss
⊢ a ∈ ss → a ∈ s₁ ∨ a ∈ s₂
intro h
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
⊢ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = ss → a ∈ s₁ ∨ a ∈ s₂
α : Type u
β : Type v
γ : Type w
s₁ s₂ : Seq α
a : α
h✝ : a ∈ append s₁ s₂
ss : Seq α
e : append s₁ s₂ = ss
h : a ∈ ss
⊢ a ∈ s₁ ∨ a ∈ s₂
revert s₁
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
⊢ ∀ (b : α) (s' : Seq α),
    (a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂) →
      ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = cons b s' → a ∈ s₁ ∨ a ∈ s₂
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
⊢ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = ss → a ∈ s₁ ∨ a ∈ s₂
apply mem_rec_on h _
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
⊢ a ∈ append s₁ s₂ → append s₁ s₂ = cons b s' → a ∈ s₁ ∨ a ∈ s₂
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
⊢ ∀ (b : α) (s' : Seq α),
    (a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂) →
      ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = cons b s' → a ∈ s₁ ∨ a ∈ s₂
intro b s' o s₁
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
⊢ a ∈ append nil s₂ → append nil s₂ = cons b s' → a ∈ nil ∨ a ∈ s₂

α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
⊢ ∀ (c : α) (t₁ : Seq α), a ∈ append (cons c t₁) s₂ → append (cons c t₁) s₂ = cons b s' → a ∈ cons c t₁ ∨ a ∈ s₂
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
⊢ a ∈ append s₁ s₂ → append s₁ s₂ = cons b s' → a ∈ s₁ ∨ a ∈ s₂
apply s₁.recOn _ fun c t₁ => _
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
m : a ∈ append nil s₂
e✝ : append nil s₂ = cons b s'
⊢ a ∈ nil ∨ a ∈ s₂
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
⊢ a ∈ append nil s₂ → append nil s₂ = cons b s' → a ∈ nil ∨ a ∈ s₂
intro m _
case h
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
m : a ∈ append nil s₂
e✝ : append nil s₂ = cons b s'
⊢ a ∈ s₂
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
m : a ∈ append nil s₂
e✝ : append nil s₂ = cons b s'
⊢ a ∈ nil ∨ a ∈ s₂
apply Or.inr
no goals
case h
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
m : a ∈ append nil s₂
e✝ : append nil s₂ = cons b s'
⊢ a ∈ s₂
simpa using m
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
c : α
t₁ : Seq α
m : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
⊢ ∀ (c : α) (t₁ : Seq α), a ∈ append (cons c t₁) s₂ → append (cons c t₁) s₂ = cons b s' → a ∈ cons c t₁ ∨ a ∈ s₂
intro c t₁ m e
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
c : α
t₁ : Seq α
m : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
this : destruct (append (cons c t₁) s₂) = destruct (cons b s')
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
c : α
t₁ : Seq α
m : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
have this := congr_arg destruct e
case inl
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
c : α
t₁ : Seq α
m : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
this : destruct (append (cons c t₁) s₂) = destruct (cons b s')
e' : a = c
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

case inr
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
this : destruct (append (cons c t₁) s₂) = destruct (cons b s')
m : a ∈ append t₁ s₂
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
c : α
t₁ : Seq α
m : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
this : destruct (append (cons c t₁) s₂) = destruct (cons b s')
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
cases' show a = c ∨ a ∈ append t₁ s₂ by simpa using m with e' m
no goals
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
c : α
t₁ : Seq α
m : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
this : destruct (append (cons c t₁) s₂) = destruct (cons b s')
⊢ a = c ∨ a ∈ append t₁ s₂
simpa using m
case inl
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
c : α
t₁ : Seq α
m : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
this : destruct (append (cons c t₁) s₂) = destruct (cons b s')
e' : a = c
⊢ c ∈ cons c t₁ ∨ c ∈ s₂
case inl
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
c : α
t₁ : Seq α
m : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
this : destruct (append (cons c t₁) s₂) = destruct (cons b s')
e' : a = c
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
rw [e']
no goals
case inl
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
c : α
t₁ : Seq α
m : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
this : destruct (append (cons c t₁) s₂) = destruct (cons b s')
e' : a = c
⊢ c ∈ cons c t₁ ∨ c ∈ s₂
exact Or.inl (mem_cons _ _)
case inr.intro
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
this : destruct (append (cons c t₁) s₂) = destruct (cons b s')
m : a ∈ append t₁ s₂
i1 : c = b
i2 : append t₁ s₂ = s'
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
case inr
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
this : destruct (append (cons c t₁) s₂) = destruct (cons b s')
m : a ∈ append t₁ s₂
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
cases' show c = b ∧ append t₁ s₂ = s' by simpa with i1 i2
case inr.intro.inl
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' s₁ : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
this : destruct (append (cons c t₁) s₂) = destruct (cons b s')
m : a ∈ append t₁ s₂
i1 : c = b
i2 : append t₁ s₂ = s'
e' : a = b
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

case inr.intro.inr
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' s₁ : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
this : destruct (append (cons c t₁) s₂) = destruct (cons b s')
m : a ∈ append t₁ s₂
i1 : c = b
i2 : append t₁ s₂ = s'
IH : ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
case inr.intro
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
this : destruct (append (cons c t₁) s₂) = destruct (cons b s')
m : a ∈ append t₁ s₂
i1 : c = b
i2 : append t₁ s₂ = s'
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
cases' o with e' IH
no goals
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
s₁ : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
this : destruct (append (cons c t₁) s₂) = destruct (cons b s')
m : a ∈ append t₁ s₂
⊢ c = b ∧ append t₁ s₂ = s'
simpa
no goals
case inr.intro.inl
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' s₁ : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
this : destruct (append (cons c t₁) s₂) = destruct (cons b s')
m : a ∈ append t₁ s₂
i1 : c = b
i2 : append t₁ s₂ = s'
e' : a = b
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
simp [i1, e']
no goals
case inr.intro.inr
α : Type u
β : Type v
γ : Type w
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' s₁ : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ append (cons c t₁) s₂
e : append (cons c t₁) s₂ = cons b s'
this : destruct (append (cons c t₁) s₂) = destruct (cons b s')
m : a ∈ append t₁ s₂
i1 : c = b
i2 : append t₁ s₂ = s'
IH : ∀ {s₁ : Seq α}, a ∈ append s₁ s₂ → append s₁ s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
⊢ a ∈ cons c t₁ ∨ a ∈ s₂
exact Or.imp_left (mem_cons_of_mem _) (IH m i2)