-- Mathlib/Data/Seq/Seq.lean
theorem of_mem_append {s₁ s₂ : Seq α} {a : α} (h : a ∈ append s₁ s₂) : a ∈ s₁ ∨ a ∈ s₂

Proof state:
case cons.inr.intro
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
i2 : t₁.append s₂ = s'
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
rcases o with e' | IH

Result:
case cons.inr.intro.inl
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
i2 : t₁.append s₂ = s'
e' : a = b
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

case cons.inr.intro.inr
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
i2 : t₁.append s₂ = s'
IH : ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Proof state:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁.append s₂
⊢ a ∈ s₁.append s₂ → a ∈ s₁ ∨ a ∈ s₂

Tactic:
generalize e : append s₁ s₂ = ss

Result:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁.append s₂
ss : Seq α
e : s₁.append s₂ = ss
⊢ a ∈ ss → a ∈ s₁ ∨ a ∈ s₂

Proof state:
α : Type u
s₁ s₂ : Seq α
a : α
h✝ : a ∈ s₁.append s₂
ss : Seq α
e : s₁.append s₂ = ss
h : a ∈ ss
⊢ a ∈ s₁ ∨ a ∈ s₂

Tactic:
revert s₁

Result:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
⊢ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = ss → a ∈ s₁ ∨ a ∈ s₂

Proof state:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁.append s₂
⊢ a ∈ s₁ ∨ a ∈ s₂

Tactic:
have := h

Result:
α : Type u
s₁ s₂ : Seq α
a : α
h this : a ∈ s₁.append s₂
⊢ a ∈ s₁ ∨ a ∈ s₂

Proof state:
case cons.inr
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
obtain ⟨i1, i2⟩ := show c = b ∧ append t₁ s₂ = s' by simpa

Result:
case cons.inr.intro
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
i2 : t₁.append s₂ = s'
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Proof state:
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
⊢ c = b ∧ t₁.append s₂ = s'

Tactic:
simpa

Result:
no goals

Proof state:
case cons.inr.intro.inr
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
i2 : t₁.append s₂ = s'
IH : ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
exact Or.imp_left (mem_cons_of_mem _) (IH m i2)

Result:
no goals

Proof state:
case cons.inr.intro.inl
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
i1 : c = b
i2 : t₁.append s₂ = s'
e' : a = b
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
simp [i1, e']

Result:
no goals

Proof state:
case cons
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
⊢ a ∈ (cons c t₁).append s₂ → (cons c t₁).append s₂ = cons b s' → a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
intro m e

Result:
case cons
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Proof state:
case nil.h
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
m : a ∈ nil.append s₂
e✝ : nil.append s₂ = cons b s'
⊢ a ∈ s₂

Tactic:
simpa using m

Result:
no goals

Proof state:
case nil
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
m : a ∈ nil.append s₂
e✝ : nil.append s₂ = cons b s'
⊢ a ∈ nil ∨ a ∈ s₂

Tactic:
apply Or.inr

Result:
case nil.h
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
m : a ∈ nil.append s₂
e✝ : nil.append s₂ = cons b s'
⊢ a ∈ s₂

Proof state:
case cons.inl
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
e' : a = c
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
rw [e']

Result:
case cons.inl
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
e' : a = c
⊢ c ∈ cons c t₁ ∨ c ∈ s₂

Proof state:
case cons
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Tactic:
rcases show a = c ∨ a ∈ append t₁ s₂ by simpa using m with e' | m

Result:
case cons.inl
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
e' : a = c
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

case cons.inr
α : Type u
s₂ : Seq α
a : α
ss : Seq α
h : a ∈ ss
b : α
s' : Seq α
o : a = b ∨ ∀ {s₁ : Seq α}, a ∈ s₁.append s₂ → s₁.append s₂ = s' → a ∈ s₁ ∨ a ∈ s₂
c : α
t₁ : Seq α
m✝ : a ∈ (cons c t₁).append s₂
e : (cons c t₁).append s₂ = cons b s'
this : ((cons c t₁).append s₂).destruct = (cons b s').destruct
m : a ∈ t₁.append s₂
⊢ a ∈ cons c t₁ ∨ a ∈ s₂

Proof state:
α : Type u
s₁ s₂ : Seq α
a : α
h this : a ∈ s₁.append s₂
⊢ a ∈ s₁ ∨ a ∈ s₂

Tactic:
revert this

Result:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁.append s₂
⊢ a ∈ s₁.append s₂ → a ∈ s₁ ∨ a ∈ s₂

Proof state:
α : Type u
s₁ s₂ : Seq α
a : α
h : a ∈ s₁.append s₂
ss : Seq α
e : s₁.append s₂ = ss
⊢ a ∈ ss → a ∈ s₁ ∨ a ∈ s₂

Tactic:
intro h

Result:
α : Type u
s₁ s₂ : Seq α
a : α
h✝ : a ∈ s₁.append s₂
ss : Seq α
e : s₁.append s₂ = ss
h : a ∈ ss
⊢ a ∈ s₁ ∨ a ∈ s₂