Theorem: Forest.roots_subset_support (Algorithm/Data/Forest.lean)

State before:
α : Type u_1
f : Forest α
⊢ f.roots ⊆ f.support
Tactic:
induction f with
| nil => rfl
| node a c s _ ihs =>
  exact Set.insert_subset_insert (Set.subset_union_of_subset_right ihs _)
State after:
no goals

State before:
case nil
α : Type u_1
⊢ nil.roots ⊆ nil.support
Tactic:
rfl
State after:
no goals

State before:
case node
α : Type u_1
a : α
c s : Forest α
child_ih✝ : c.roots ⊆ c.support
ihs : s.roots ⊆ s.support
⊢ (node a c s).roots ⊆ (node a c s).support
Tactic:
exact Set.insert_subset_insert (Set.subset_union_of_subset_right ihs _)
State after:
no goals