case empty
α : Type u_1
⊢ ∀ {a : Multiset α}, a ∈ Sections 0 ↔ Rel (fun s a => a ∈ s) 0 a

case cons
α : Type u_1
a✝¹ : Multiset α
s✝ : Multiset (Multiset α)
a✝ : ∀ {a : Multiset α}, a ∈ Sections s✝ ↔ Rel (fun s a => a ∈ s) s✝ a
⊢ ∀ {a : Multiset α}, a ∈ Sections (a✝¹ ::ₘ s✝) ↔ Rel (fun s a => a ∈ s) (a✝¹ ::ₘ s✝) a
α : Type u_1
s : Multiset (Multiset α)
⊢ ∀ {a : Multiset α}, a ∈ Sections s ↔ Rel (fun s a => a ∈ s) s a
induction s using Multiset.induction_on
case cons
α : Type u_1
a✝¹ : Multiset α
s✝ : Multiset (Multiset α)
a✝ : ∀ {a : Multiset α}, a ∈ Sections s✝ ↔ Rel (fun s a => a ∈ s) s✝ a
⊢ ∀ {a : Multiset α}, a ∈ Sections (a✝¹ ::ₘ s✝) ↔ Rel (fun s a => a ∈ s) (a✝¹ ::ₘ s✝) a
case empty
α : Type u_1
⊢ ∀ {a : Multiset α}, a ∈ Sections 0 ↔ Rel (fun s a => a ∈ s) 0 a

case cons
α : Type u_1
a✝¹ : Multiset α
s✝ : Multiset (Multiset α)
a✝ : ∀ {a : Multiset α}, a ∈ Sections s✝ ↔ Rel (fun s a => a ∈ s) s✝ a
⊢ ∀ {a : Multiset α}, a ∈ Sections (a✝¹ ::ₘ s✝) ↔ Rel (fun s a => a ∈ s) (a✝¹ ::ₘ s✝) a
case empty => simp
no goals
case cons
α : Type u_1
a✝¹ : Multiset α
s✝ : Multiset (Multiset α)
a✝ : ∀ {a : Multiset α}, a ∈ Sections s✝ ↔ Rel (fun s a => a ∈ s) s✝ a
⊢ ∀ {a : Multiset α}, a ∈ Sections (a✝¹ ::ₘ s✝) ↔ Rel (fun s a => a ∈ s) (a✝¹ ::ₘ s✝) a
case cons a a' ih => simp [ih, rel_cons_left, eq_comm]
no goals
α : Type u_1
⊢ ∀ {a : Multiset α}, a ∈ Sections 0 ↔ Rel (fun s a => a ∈ s) 0 a
simp
no goals
α : Type u_1
a : Multiset α
a' : Multiset (Multiset α)
ih : ∀ {a : Multiset α}, a ∈ Sections a' ↔ Rel (fun s a => a ∈ s) a' a
⊢ ∀ {a_1 : Multiset α}, a_1 ∈ Sections (a ::ₘ a') ↔ Rel (fun s a => a ∈ s) (a ::ₘ a') a_1
simp [ih, rel_cons_left, eq_comm]