case nil
ι : Type ?u.892330
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f g : α → β
a : Multiset α
⊢ Disjoint (List.sum []) a ↔ ∀ (b : Multiset α), b ∈ [] → Disjoint b a

case cons
ι : Type ?u.892330
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f g : α → β
a b : Multiset α
bs : List (Multiset α)
ih : Disjoint (List.sum bs) a ↔ ∀ (b : Multiset α), b ∈ bs → Disjoint b a
⊢ Disjoint (List.sum (b :: bs)) a ↔ ∀ (b_1 : Multiset α), b_1 ∈ b :: bs → Disjoint b_1 a
ι : Type ?u.892330
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f g : α → β
a : Multiset α
l : List (Multiset α)
⊢ Disjoint (List.sum l) a ↔ ∀ (b : Multiset α), b ∈ l → Disjoint b a
induction' l with b bs ih
no goals
case nil
ι : Type ?u.892330
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f g : α → β
a : Multiset α
⊢ Disjoint (List.sum []) a ↔ ∀ (b : Multiset α), b ∈ [] → Disjoint b a
simp only [zero_disjoint, List.not_mem_nil, IsEmpty.forall_iff, forall_const, List.sum_nil]
case cons
ι : Type ?u.892330
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f g : α → β
a b : Multiset α
bs : List (Multiset α)
ih : Disjoint (List.sum bs) a ↔ ∀ (b : Multiset α), b ∈ bs → Disjoint b a
⊢ Disjoint b a ∧ Disjoint (List.sum bs) a ↔ Disjoint b a ∧ ∀ (a_1 : Multiset α), a_1 ∈ bs → Disjoint a_1 a
case cons
ι : Type ?u.892330
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f g : α → β
a b : Multiset α
bs : List (Multiset α)
ih : Disjoint (List.sum bs) a ↔ ∀ (b : Multiset α), b ∈ bs → Disjoint b a
⊢ Disjoint (List.sum (b :: bs)) a ↔ ∀ (b_1 : Multiset α), b_1 ∈ b :: bs → Disjoint b_1 a
simp_rw [List.sum_cons, disjoint_add_left, List.mem_cons, forall_eq_or_imp]
no goals
case cons
ι : Type ?u.892330
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f g : α → β
a b : Multiset α
bs : List (Multiset α)
ih : Disjoint (List.sum bs) a ↔ ∀ (b : Multiset α), b ∈ bs → Disjoint b a
⊢ Disjoint b a ∧ Disjoint (List.sum bs) a ↔ Disjoint b a ∧ ∀ (a_1 : Multiset α), a_1 ∈ bs → Disjoint a_1 a
simp [and_congr_left_iff, iff_self_iff, ih]