no goals
α : Type u_1
β : Type ?u.2554
γ : Type ?u.2557
δ : Type ?u.2560
a : α
S : Multiset (Multiset α)
⊢ a ∈ join 0 ↔ ∃ s, s ∈ 0 ∧ a ∈ s
simp
no goals
α : Type u_1
β : Type ?u.2554
γ : Type ?u.2557
δ : Type ?u.2560
a : α
S : Multiset (Multiset α)
⊢ ∀ ⦃a_1 : Multiset α⦄ {s : Multiset (Multiset α)},
    (a ∈ join s ↔ ∃ s_1, s_1 ∈ s ∧ a ∈ s_1) → (a ∈ join (a_1 ::ₘ s) ↔ ∃ s_1, s_1 ∈ a_1 ::ₘ s ∧ a ∈ s_1)
simp (config := { contextual := true }) [or_and_right, exists_or]