ι : Type ?u.865375
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
f : α → Multiset β
s : Finset α
b : β
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (b ∈ ∑ x in s, f x ↔ ∃ a, a ∈ s ∧ b ∈ f a) → (b ∈ ∑ x in insert a s, f x ↔ ∃ a_3, a_3 ∈ insert a s ∧ b ∈ f a_3)
ι : Type ?u.865375
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
f : α → Multiset β
s : Finset α
b : β
⊢ b ∈ ∑ x in s, f x ↔ ∃ a, a ∈ s ∧ b ∈ f a
refine' s.induction_on (by simp) _
no goals
ι : Type ?u.865375
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
f : α → Multiset β
s : Finset α
b : β
⊢ b ∈ ∑ x in ∅, f x ↔ ∃ a, a ∈ ∅ ∧ b ∈ f a
simp
ι : Type ?u.865375
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
f : α → Multiset β
s : Finset α
b : β
a : α
t : Finset α
hi : ¬a ∈ t
ih : b ∈ ∑ x in t, f x ↔ ∃ a, a ∈ t ∧ b ∈ f a
⊢ b ∈ ∑ x in insert a t, f x ↔ ∃ a_1, a_1 ∈ insert a t ∧ b ∈ f a_1
ι : Type ?u.865375
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
f : α → Multiset β
s : Finset α
b : β
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (b ∈ ∑ x in s, f x ↔ ∃ a, a ∈ s ∧ b ∈ f a) → (b ∈ ∑ x in insert a s, f x ↔ ∃ a_3, a_3 ∈ insert a s ∧ b ∈ f a_3)
intro a t hi ih
no goals
ι : Type ?u.865375
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
f : α → Multiset β
s : Finset α
b : β
a : α
t : Finset α
hi : ¬a ∈ t
ih : b ∈ ∑ x in t, f x ↔ ∃ a, a ∈ t ∧ b ∈ f a
⊢ b ∈ ∑ x in insert a t, f x ↔ ∃ a_1, a_1 ∈ insert a t ∧ b ∈ f a_1
simp [sum_insert hi, ih, or_and_right, exists_or]