case nil
α : Type u_1
l₁ l₂ : List (Lists α)
h✝ : l₁ ⊆ l₂
h : [] ⊆ l₂
⊢ ofList [] ⊆ ofList l₂

case cons
α : Type u_1
l₁ l₂ : List (Lists α)
h✝ : l₁ ⊆ l₂
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ :: tail✝ ⊆ l₂
⊢ ofList (head✝ :: tail✝) ⊆ ofList l₂
α : Type u_1
l₁ l₂ : List (Lists α)
h : l₁ ⊆ l₂
⊢ ofList l₁ ⊆ ofList l₂
induction' l₁ with _ _ l₁_ih
case cons
α : Type u_1
l₁ l₂ : List (Lists α)
h✝ : l₁ ⊆ l₂
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ :: tail✝ ⊆ l₂
⊢ head✝ ∈ toList (ofList l₂)
case cons
α : Type u_1
l₁ l₂ : List (Lists α)
h✝ : l₁ ⊆ l₂
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ :: tail✝ ⊆ l₂
⊢ ofList (head✝ :: tail✝) ⊆ ofList l₂
refine' Subset.cons (Lists.Equiv.refl _) _ (l₁_ih (List.subset_of_cons_subset h))
case cons
α : Type u_1
l₁ l₂ : List (Lists α)
h✝ : l₁ ⊆ l₂
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ ∈ l₂ ∧ tail✝ ⊆ l₂
⊢ head✝ ∈ toList (ofList l₂)
case cons
α : Type u_1
l₁ l₂ : List (Lists α)
h✝ : l₁ ⊆ l₂
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ :: tail✝ ⊆ l₂
⊢ head✝ ∈ toList (ofList l₂)
simp at h
no goals
case cons
α : Type u_1
l₁ l₂ : List (Lists α)
h✝ : l₁ ⊆ l₂
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ ∈ l₂ ∧ tail✝ ⊆ l₂
⊢ head✝ ∈ toList (ofList l₂)
simp [h]
no goals
case nil
α : Type u_1
l₁ l₂ : List (Lists α)
h✝ : l₁ ⊆ l₂
h : [] ⊆ l₂
⊢ ofList [] ⊆ ofList l₂
exact Subset.nil