case empty
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
⊢ x ∈ Finset.sup ∅ f ↔ ∃ v, v ∈ ∅ ∧ x ∈ f v

case insert
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
⊢ x ∈ Finset.sup (insert a s) f ↔ ∃ v, v ∈ insert a s ∧ x ∈ f v
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
x : β
⊢ x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
induction' s using Finset.induction_on with a s has hxs
no goals
case empty
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
⊢ x ∈ Finset.sup ∅ f ↔ ∃ v, v ∈ ∅ ∧ x ∈ f v
simp
case insert
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
⊢ x ∈ f a ∨ x ∈ Finset.sup s f ↔ ∃ v, v ∈ insert a s ∧ x ∈ f v
case insert
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
⊢ x ∈ Finset.sup (insert a s) f ↔ ∃ v, v ∈ insert a s ∧ x ∈ f v
rw [Finset.sup_insert, Multiset.sup_eq_union, Multiset.mem_union]
case insert.mp
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
⊢ x ∈ f a ∨ x ∈ Finset.sup s f → ∃ v, v ∈ insert a s ∧ x ∈ f v

case insert.mpr
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
⊢ (∃ v, v ∈ insert a s ∧ x ∈ f v) → x ∈ f a ∨ x ∈ Finset.sup s f
case insert
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
⊢ x ∈ f a ∨ x ∈ Finset.sup s f ↔ ∃ v, v ∈ insert a s ∧ x ∈ f v
constructor
case insert.mp
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hxi : x ∈ f a ∨ x ∈ Finset.sup s f
⊢ ∃ v, v ∈ insert a s ∧ x ∈ f v
case insert.mp
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
⊢ x ∈ f a ∨ x ∈ Finset.sup s f → ∃ v, v ∈ insert a s ∧ x ∈ f v
intro hxi
case insert.mp.inl
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hf : x ∈ f a
⊢ ∃ v, v ∈ insert a s ∧ x ∈ f v

case insert.mp.inr
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hf : x ∈ Finset.sup s f
⊢ ∃ v, v ∈ insert a s ∧ x ∈ f v
case insert.mp
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hxi : x ∈ f a ∨ x ∈ Finset.sup s f
⊢ ∃ v, v ∈ insert a s ∧ x ∈ f v
cases' hxi with hf hf
case insert.mp.inl
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hf : x ∈ f a
⊢ a ∈ insert a s
case insert.mp.inl
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hf : x ∈ f a
⊢ ∃ v, v ∈ insert a s ∧ x ∈ f v
refine' ⟨a, _, hf⟩
no goals
case insert.mp.inl
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hf : x ∈ f a
⊢ a ∈ insert a s
simp only [true_or_iff, eq_self_iff_true, Finset.mem_insert]
case insert.mp.inr.intro.intro
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hf : x ∈ Finset.sup s f
v : α
hv : v ∈ s
hfv : x ∈ f v
⊢ ∃ v, v ∈ insert a s ∧ x ∈ f v
case insert.mp.inr
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hf : x ∈ Finset.sup s f
⊢ ∃ v, v ∈ insert a s ∧ x ∈ f v
rcases hxs.mp hf with ⟨v, hv, hfv⟩
case insert.mp.inr.intro.intro
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hf : x ∈ Finset.sup s f
v : α
hv : v ∈ s
hfv : x ∈ f v
⊢ v ∈ insert a s
case insert.mp.inr.intro.intro
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hf : x ∈ Finset.sup s f
v : α
hv : v ∈ s
hfv : x ∈ f v
⊢ ∃ v, v ∈ insert a s ∧ x ∈ f v
refine' ⟨v, _, hfv⟩
no goals
case insert.mp.inr.intro.intro
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
hf : x ∈ Finset.sup s f
v : α
hv : v ∈ s
hfv : x ∈ f v
⊢ v ∈ insert a s
simp only [hv, or_true_iff, Finset.mem_insert]
case insert.mpr.intro.intro
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
v : α
hv : v ∈ insert a s
hfv : x ∈ f v
⊢ x ∈ f a ∨ x ∈ Finset.sup s f
case insert.mpr
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
⊢ (∃ v, v ∈ insert a s ∧ x ∈ f v) → x ∈ f a ∨ x ∈ Finset.sup s f
rintro ⟨v, hv, hfv⟩
case insert.mpr.intro.intro
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
v : α
hv : v = a ∨ v ∈ s
hfv : x ∈ f v
⊢ x ∈ f a ∨ x ∈ Finset.sup s f
case insert.mpr.intro.intro
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
v : α
hv : v ∈ insert a s
hfv : x ∈ f v
⊢ x ∈ f a ∨ x ∈ Finset.sup s f
rw [Finset.mem_insert] at hv
case insert.mpr.intro.intro.inl
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
s : Finset α
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
v : α
hfv : x ∈ f v
has : ¬v ∈ s
⊢ x ∈ f v ∨ x ∈ Finset.sup s f

case insert.mpr.intro.intro.inr
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
v : α
hfv : x ∈ f v
hv : v ∈ s
⊢ x ∈ f a ∨ x ∈ Finset.sup s f
case insert.mpr.intro.intro
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
v : α
hv : v = a ∨ v ∈ s
hfv : x ∈ f v
⊢ x ∈ f a ∨ x ∈ Finset.sup s f
rcases hv with (rfl | hv)
no goals
case insert.mpr.intro.intro.inl
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
s : Finset α
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
v : α
hfv : x ∈ f v
has : ¬v ∈ s
⊢ x ∈ f v ∨ x ∈ Finset.sup s f
exact Or.inl hfv
no goals
case insert.mpr.intro.intro.inr
F : Type ?u.412533
α✝ : Type ?u.412536
β✝ : Type ?u.412539
γ : Type ?u.412542
ι : Type ?u.412545
κ : Type ?u.412548
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → Multiset β
x : β
a : α
s : Finset α
has : ¬a ∈ s
hxs : x ∈ Finset.sup s f ↔ ∃ v, v ∈ s ∧ x ∈ f v
v : α
hfv : x ∈ f v
hv : v ∈ s
⊢ x ∈ f a ∨ x ∈ Finset.sup s f
refine' Or.inr (hxs.mpr ⟨v, hv, hfv⟩)