-- Mathlib/SetTheory/Lists.lean
theorem cons_subset {a} {l₁ l₂ : Lists' α true} : Lists'.cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂

Proof state:
case cons.mk
α : Type u_1
l₁ l₂ : Lists' α true
a' a'✝ : Lists α
l✝ : Lists' α true
e : a' ~ a'✝
m : a'✝ ∈ l₂.toList
s : l✝.Subset l₂
fst✝ : Bool
snd✝ : Lists' α fst✝
h' : cons ⟨fst✝, snd✝⟩ l₁ = cons a' l✝
⊢ ⟨fst✝, snd✝⟩ ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
cases a'

Result:
case cons.mk.mk
α : Type u_1
l₁ l₂ : Lists' α true
a'✝ : Lists α
l✝ : Lists' α true
m : a'✝ ∈ l₂.toList
s : l✝.Subset l₂
fst✝¹ : Bool
snd✝¹ : Lists' α fst✝¹
fst✝ : Bool
snd✝ : Lists' α fst✝
e : ⟨fst✝, snd✝⟩ ~ a'✝
h' : cons ⟨fst✝¹, snd✝¹⟩ l₁ = cons ⟨fst✝, snd✝⟩ l✝
⊢ ⟨fst✝¹, snd✝¹⟩ ∈ l₂ ∧ l₁ ⊆ l₂

Proof state:
case cons.mk.mk.refl
α : Type u_1
l₁ l₂ : Lists' α true
a'✝ : Lists α
m : a'✝ ∈ l₂.toList
fst✝ : Bool
snd✝ : Lists' α fst✝
e : ⟨fst✝, snd✝⟩ ~ a'✝
s : l₁.Subset l₂
⊢ ⟨fst✝, snd✝⟩ ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
exact ⟨⟨_, m, e⟩, s⟩

Result:
no goals

Proof state:
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
h : cons a l₁ ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
generalize h' : Lists'.cons a l₁ = l₁' at h

Result:
α : Type u_1
a : Lists α
l₁ l₂ l₁' : Lists' α true
h' : cons a l₁ = l₁'
h : l₁' ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂

Proof state:
case cons
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
a' a'✝ : Lists α
l✝ : Lists' α true
e : a' ~ a'✝
h' : cons a l₁ = cons a' l✝
m : a'✝ ∈ l₂.toList
s : l✝.Subset l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
cases a

Result:
case cons.mk
α : Type u_1
l₁ l₂ : Lists' α true
a' a'✝ : Lists α
l✝ : Lists' α true
e : a' ~ a'✝
m : a'✝ ∈ l₂.toList
s : l✝.Subset l₂
fst✝ : Bool
snd✝ : Lists' α fst✝
h' : cons ⟨fst✝, snd✝⟩ l₁ = cons a' l✝
⊢ ⟨fst✝, snd✝⟩ ∈ l₂ ∧ l₁ ⊆ l₂

Proof state:
case nil.mk
α : Type u_1
l₁ l₂ : Lists' α true
fst✝ : Bool
snd✝ : Lists' α fst✝
h' : cons ⟨fst✝, snd✝⟩ l₁ = nil
⊢ ⟨fst✝, snd✝⟩ ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
cases h'

Result:
no goals

Proof state:
case cons.mk.mk
α : Type u_1
l₁ l₂ : Lists' α true
a'✝ : Lists α
l✝ : Lists' α true
m : a'✝ ∈ l₂.toList
s : l✝.Subset l₂
fst✝¹ : Bool
snd✝¹ : Lists' α fst✝¹
fst✝ : Bool
snd✝ : Lists' α fst✝
e : ⟨fst✝, snd✝⟩ ~ a'✝
h' : cons ⟨fst✝¹, snd✝¹⟩ l₁ = cons ⟨fst✝, snd✝⟩ l✝
⊢ ⟨fst✝¹, snd✝¹⟩ ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
cases h'

Result:
case cons.mk.mk.refl
α : Type u_1
l₁ l₂ : Lists' α true
a'✝ : Lists α
m : a'✝ ∈ l₂.toList
fst✝ : Bool
snd✝ : Lists' α fst✝
e : ⟨fst✝, snd✝⟩ ~ a'✝
s : l₁.Subset l₂
⊢ ⟨fst✝, snd✝⟩ ∈ l₂ ∧ l₁ ⊆ l₂

Proof state:
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
⊢ cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
refine ⟨fun h => ?_, fun ⟨⟨a', m, e⟩, s⟩ => Subset.cons e m s⟩

Result:
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
h : cons a l₁ ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂

Proof state:
α : Type u_1
a : Lists α
l₁ l₂ l₁' : Lists' α true
h' : cons a l₁ = l₁'
h : l₁' ⊆ l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
obtain - | @⟨a', _, _, _, e, m, s⟩ := h

Result:
case nil
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
h' : cons a l₁ = nil
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂

case cons
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
a' a'✝ : Lists α
l✝ : Lists' α true
e : a' ~ a'✝
h' : cons a l₁ = cons a' l✝
m : a'✝ ∈ l₂.toList
s : l✝.Subset l₂
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂

Proof state:
case nil
α : Type u_1
a : Lists α
l₁ l₂ : Lists' α true
h' : cons a l₁ = nil
⊢ a ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
cases a

Result:
case nil.mk
α : Type u_1
l₁ l₂ : Lists' α true
fst✝ : Bool
snd✝ : Lists' α fst✝
h' : cons ⟨fst✝, snd✝⟩ l₁ = nil
⊢ ⟨fst✝, snd✝⟩ ∈ l₂ ∧ l₁ ⊆ l₂