α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ (a : Lists α), a ∈ toList l₁ → a ∈ l₂
⊢ ofList (toList l₁) ⊆ l₂
α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ (a : Lists α), a ∈ toList l₁ → a ∈ l₂
⊢ l₁ ⊆ l₂
rw [← of_toList l₁]
α : Type u_1
l₁ l₂ : Lists' α true
⊢ (∀ (a : Lists α), a ∈ toList l₁ → a ∈ l₂) → ofList (toList l₁) ⊆ l₂
α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ (a : Lists α), a ∈ toList l₁ → a ∈ l₂
⊢ ofList (toList l₁) ⊆ l₂
revert H
case nil
α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ (a : Lists α), a ∈ [] → a ∈ l₂
⊢ ofList [] ⊆ l₂

case cons
α : Type u_1
l₁ l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : (∀ (a : Lists α), a ∈ t → a ∈ l₂) → ofList t ⊆ l₂
H : ∀ (a : Lists α), a ∈ h :: t → a ∈ l₂
⊢ ofList (h :: t) ⊆ l₂
α : Type u_1
l₁ l₂ : Lists' α true
⊢ (∀ (a : Lists α), a ∈ toList l₁ → a ∈ l₂) → ofList (toList l₁) ⊆ l₂
induction' toList l₁ with h t t_ih <;> intro H
no goals
case nil
α : Type u_1
l₁ l₂ : Lists' α true
H : ∀ (a : Lists α), a ∈ [] → a ∈ l₂
⊢ ofList [] ⊆ l₂
exact Subset.nil
case cons
α : Type u_1
l₁ l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : (∀ (a : Lists α), a ∈ t → a ∈ l₂) → ofList t ⊆ l₂
H : h ∈ l₂ ∧ ∀ (a : Lists α), a ∈ t → a ∈ l₂
⊢ cons h (ofList t) ⊆ l₂
case cons
α : Type u_1
l₁ l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : (∀ (a : Lists α), a ∈ t → a ∈ l₂) → ofList t ⊆ l₂
H : ∀ (a : Lists α), a ∈ h :: t → a ∈ l₂
⊢ ofList (h :: t) ⊆ l₂
simp only [ofList, List.find?, List.mem_cons, forall_eq_or_imp] at *
no goals
case cons
α : Type u_1
l₁ l₂ : Lists' α true
h : Lists α
t : List (Lists α)
t_ih : (∀ (a : Lists α), a ∈ t → a ∈ l₂) → ofList t ⊆ l₂
H : h ∈ l₂ ∧ ∀ (a : Lists α), a ∈ t → a ∈ l₂
⊢ cons h (ofList t) ⊆ l₂
exact cons_subset.2 ⟨H.1, t_ih H.2⟩