[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
nodup✝¹ : Nodup s
t : Multiset α
nodup✝ : Nodup t
h : { val := s, nodup := nodup✝¹ }.val = { val := t, nodup := nodup✝ }.val
⊢ { val := s, nodup := nodup✝¹ } = { val := t, nodup := nodup✝ }
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
nodup✝¹ nodup✝ : Nodup s
⊢ { val := s, nodup := nodup✝¹ } = { val := s, nodup := nodup✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ IsRefl (Finset α) fun x x_1 => x ≤ x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ IsTrans (Finset α) fun x x_1 => x ≤ x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ IsAntisymm (Finset α) fun x x_1 => x ≤ x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ IsIrrefl (Finset α) fun x x_1 => x < x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ IsTrans (Finset α) fun x x_1 => x < x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ IsAsymm (Finset α) fun x x_1 => x < x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
⊢ ¬s ⊆ t ↔ ∃ x, x ∈ s ∧ ¬x ∈ t
[PROOFSTEP]
simp only [← coe_subset, Set.not_subset, mem_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t s₁ s₂ : Finset α
⊢ ↑s₁ ⊂ ↑s₂ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁
[PROOFSTEP]
simp only [Set.ssubset_def, Finset.coe_subset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
l : List α
⊢ ¬∃ a, a ∈ Quotient.mk (List.isSetoid α) []
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
l✝ : List α
a : α
l : List α
⊢ a ∈ Quotient.mk (List.isSetoid α) (a :: l)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
a : α
⊢ ¬a ∈ ∅
[PROOFSTEP]
simp only [mem_def, empty_val, not_mem_zero, not_false_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s : Finset α
⊢ s = ∅ → ∀ (x : α), ¬x ∈ s
[PROOFSTEP]
rintro rfl x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
x : α
⊢ ¬x ∈ ∅
[PROOFSTEP]
apply not_mem_empty
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
⊢ ∀ (x : α), x ∈ ↑∅ ↔ x ∈ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s : Finset α
⊢ ↑s = ∅ ↔ s = ∅
[PROOFSTEP]
rw [← coe_empty, coe_inj]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s : Finset α
⊢ IsEmpty { x // x ∈ s } ↔ s = ∅
[PROOFSTEP]
simpa using @Set.isEmpty_coe_sort α s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b a : α
s : Finset α
⊢ s.val = {a} ↔ s = {a}
[PROOFSTEP]
rw [← val_inj]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b a : α
s : Finset α
⊢ s.val = {a} ↔ s.val = {a}.val
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
a✝ b a : α
⊢ ↑{a} = {a}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
a✝ b a x✝ : α
⊢ x✝ ∈ ↑{a} ↔ x✝ ∈ {a}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
⊢ ↑s = {a} ↔ s = {a}
[PROOFSTEP]
rw [← coe_singleton, coe_inj]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
⊢ s = {a} ↔ a ∈ s ∧ ∀ (x : α), x ∈ s → x = a
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
⊢ s = {a} → a ∈ s ∧ ∀ (x : α), x ∈ s → x = a
[PROOFSTEP]
intro t
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
⊢ (a ∈ s ∧ ∀ (x : α), x ∈ s → x = a) → s = {a}
[PROOFSTEP]
intro t
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
t : s = {a}
⊢ a ∈ s ∧ ∀ (x : α), x ∈ s → x = a
[PROOFSTEP]
rw [t]
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
t : s = {a}
⊢ a ∈ {a} ∧ ∀ (x : α), x ∈ {a} → x = a
[PROOFSTEP]
exact ⟨Finset.mem_singleton_self _, fun _ => Finset.mem_singleton.1⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
t : a ∈ s ∧ ∀ (x : α), x ∈ s → x = a
⊢ s = {a}
[PROOFSTEP]
ext
[GOAL]
case mpr.a
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝¹ b : α
s : Finset α
a : α
t : a ∈ s ∧ ∀ (x : α), x ∈ s → x = a
a✝ : α
⊢ a✝ ∈ s ↔ a✝ ∈ {a}
[PROOFSTEP]
rw [Finset.mem_singleton]
[GOAL]
case mpr.a
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝¹ b : α
s : Finset α
a : α
t : a ∈ s ∧ ∀ (x : α), x ∈ s → x = a
a✝ : α
⊢ a✝ ∈ s ↔ a✝ = a
[PROOFSTEP]
exact ⟨t.right _, fun r => r.symm ▸ t.left⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
⊢ s = {a} ↔ Finset.Nonempty s ∧ ∀ (x : α), x ∈ s → x = a
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
⊢ s = {a} → Finset.Nonempty s ∧ ∀ (x : α), x ∈ s → x = a
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
a✝ b a : α
⊢ Finset.Nonempty {a} ∧ ∀ (x : α), x ∈ {a} → x = a
[PROOFSTEP]
simp
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
⊢ (Finset.Nonempty s ∧ ∀ (x : α), x ∈ s → x = a) → s = {a}
[PROOFSTEP]
rintro ⟨hne, h_uniq⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
hne : Finset.Nonempty s
h_uniq : ∀ (x : α), x ∈ s → x = a
⊢ s = {a}
[PROOFSTEP]
rw [eq_singleton_iff_unique_mem]
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
hne : Finset.Nonempty s
h_uniq : ∀ (x : α), x ∈ s → x = a
⊢ a ∈ s ∧ ∀ (x : α), x ∈ s → x = a
[PROOFSTEP]
refine' ⟨_, h_uniq⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
hne : Finset.Nonempty s
h_uniq : ∀ (x : α), x ∈ s → x = a
⊢ a ∈ s
[PROOFSTEP]
rw [← h_uniq hne.choose hne.choose_spec]
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
hne : Finset.Nonempty s
h_uniq : ∀ (x : α), x ∈ s → x = a
⊢ Exists.choose hne ∈ s
[PROOFSTEP]
exact hne.choose_spec
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a b : α
inst✝ : Unique α
s : Finset α
⊢ Finset.Nonempty s ↔ s = {default}
[PROOFSTEP]
simp [eq_singleton_iff_nonempty_unique_mem]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a b : α
s : Finset α
⊢ (∃ a, s = {a}) ↔ ∃! a, a ∈ s
[PROOFSTEP]
simp only [eq_singleton_iff_unique_mem, ExistsUnique]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b : α
s : Set α
a : α
⊢ ↑{a} ⊆ s ↔ a ∈ s
[PROOFSTEP]
rw [coe_singleton, Set.singleton_subset_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
⊢ s ⊆ {a} ↔ s = ∅ ∨ s = {a}
[PROOFSTEP]
rw [← coe_subset, coe_singleton, Set.subset_singleton_iff_eq, coe_eq_empty, coe_eq_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
a b : α
⊢ {a} ⊆ {b} ↔ a = b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
a✝ b : α
s : Finset α
a : α
⊢ s ⊂ {a} ↔ s = ∅
[PROOFSTEP]
rw [← coe_ssubset, coe_singleton, Set.ssubset_singleton_iff, coe_eq_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
a b : α
ha : a ∈ s
⊢ s = {a} ∨ Set.Nontrivial ↑s
[PROOFSTEP]
rw [← coe_eq_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
a b : α
ha : a ∈ s
⊢ ↑s = {a} ∨ Set.Nontrivial ↑s
[PROOFSTEP]
exact Set.eq_singleton_or_nontrivial ha
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
a b : α
h : ¬a ∈ s
p : α → Prop
⊢ (∀ (x : α), x ∈ cons a s h → p x) ↔ p a ∧ ∀ (x : α), x ∈ s → p x
[PROOFSTEP]
simp only [mem_cons, or_imp, forall_and, forall_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
a b : α
m : Multiset α
hm : Nodup m
⊢ Finset.Nonempty { val := m, nodup := hm } ↔ m ≠ 0
[PROOFSTEP]
induction m using Multiset.induction_on
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
a b : α
hm : Nodup 0
⊢ Finset.Nonempty { val := 0, nodup := hm } ↔ 0 ≠ 0
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
a b a✝¹ : α
s✝ : Multiset α
a✝ : ∀ {hm : Nodup s✝}, Finset.Nonempty { val := s✝, nodup := hm } ↔ s✝ ≠ 0
hm : Nodup (a✝¹ ::ₘ s✝)
⊢ Finset.Nonempty { val := a✝¹ ::ₘ s✝, nodup := hm } ↔ a✝¹ ::ₘ s✝ ≠ 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t : Finset α
a✝ b a : α
s : Finset α
h : ¬a ∈ s
⊢ ↑(cons a s h) = insert a ↑s
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ t : Finset α
a✝ b a : α
s : Finset α
h : ¬a ∈ s
x✝ : α
⊢ x✝ ∈ ↑(cons a s h) ↔ x✝ ∈ insert a ↑s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
a b : α
hs : ¬a ∈ s
ht : ¬a ∈ t
⊢ cons a s hs ⊆ cons a t ht ↔ s ⊆ t
[PROOFSTEP]
rwa [← coe_subset, coe_cons, coe_cons, Set.insert_subset_insert_iff, coe_subset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
a b : α
⊢ s ⊂ t ↔ ∃ a h, cons a s h ⊆ t
[PROOFSTEP]
refine' ⟨fun h => _, fun ⟨a, ha, h⟩ => ssubset_of_ssubset_of_subset (ssubset_cons _) h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
a b : α
h : s ⊂ t
⊢ ∃ a h, cons a s h ⊆ t
[PROOFSTEP]
obtain ⟨a, hs, ht⟩ := not_subset.1 h.2
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s t : Finset α
a✝ b : α
h : s ⊂ t
a : α
hs : a ∈ t
ht : ¬a ∈ s
⊢ ∃ a h, cons a s h ⊆ t
[PROOFSTEP]
exact ⟨a, ht, cons_subset.2 ⟨hs, h.subset⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s t u : Finset α
a b : α
⊢ _root_.Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → ¬a ∈ s
[PROOFSTEP]
rw [_root_.disjoint_comm, disjoint_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s t u : Finset α
a b : α
⊢ _root_.Disjoint s t ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b
[PROOFSTEP]
simp only [disjoint_left, imp_not_comm, forall_eq']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s t u : Finset α
a b x✝ : α
⊢ ¬(x✝ ∈ s → ¬x✝ ∈ t) ↔ x✝ ∈ s ∧ x✝ ∈ t
[PROOFSTEP]
rw [not_imp, not_not]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s t u : Finset α
a b : α
⊢ _root_.Disjoint {a} s ↔ ¬a ∈ s
[PROOFSTEP]
simp only [disjoint_left, mem_singleton, forall_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s t u : Finset α
a b : α
⊢ _root_.Disjoint {a} {b} ↔ a ≠ b
[PROOFSTEP]
rw [disjoint_singleton_left, mem_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
s t u : Finset α
a b : α
⊢ _root_.Disjoint ↑s ↑t ↔ _root_.Disjoint s t
[PROOFSTEP]
simp only [Finset.disjoint_left, Set.disjoint_left, mem_coe]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
s t : Finset α
h : _root_.Disjoint s t
a : α
⊢ a ∈ disjUnion s t h ↔ a ∈ s ∨ a ∈ t
[PROOFSTEP]
rcases s with ⟨⟨s⟩⟩
[GOAL]
case mk.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
t : Finset α
a : α
val✝ : Multiset α
s : List α
nodup✝ : Nodup (Quot.mk Setoid.r s)
h : _root_.Disjoint { val := Quot.mk Setoid.r s, nodup := nodup✝ } t
⊢ a ∈ disjUnion { val := Quot.mk Setoid.r s, nodup := nodup✝ } t h ↔
    a ∈ { val := Quot.mk Setoid.r s, nodup := nodup✝ } ∨ a ∈ t
[PROOFSTEP]
rcases t with ⟨⟨t⟩⟩
[GOAL]
case mk.mk.mk.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
a : α
val✝¹ : Multiset α
s : List α
nodup✝¹ : Nodup (Quot.mk Setoid.r s)
val✝ : Multiset α
t : List α
nodup✝ : Nodup (Quot.mk Setoid.r t)
h : _root_.Disjoint { val := Quot.mk Setoid.r s, nodup := nodup✝¹ } { val := Quot.mk Setoid.r t, nodup := nodup✝ }
⊢ a ∈ disjUnion { val := Quot.mk Setoid.r s, nodup := nodup✝¹ } { val := Quot.mk Setoid.r t, nodup := nodup✝ } h ↔
    a ∈ { val := Quot.mk Setoid.r s, nodup := nodup✝¹ } ∨ a ∈ { val := Quot.mk Setoid.r t, nodup := nodup✝ }
[PROOFSTEP]
apply List.mem_append
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
a : α
h : _root_.Disjoint s {a}
⊢ disjUnion s {a} h = cons a s (_ : ¬a ∈ s)
[PROOFSTEP]
rw [disjUnion_comm, singleton_disjUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
⊢ (insert a s).val = dedup (a ::ₘ s.val)
[PROOFSTEP]
rw [dedup_cons, dedup_eq_self]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
⊢ (insert a s).val = ndinsert a s.val
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
h : ¬a ∈ s
⊢ (insert a s).val = a ::ₘ s.val
[PROOFSTEP]
rw [insert_val, ndinsert_of_not_mem h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝¹ b a✝ : α
s : Finset α
h : ¬a✝ ∈ s
a : α
⊢ a ∈ cons a✝ s h ↔ a ∈ insert a✝ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
x : α
⊢ x ∈ ↑(insert a s) ↔ x ∈ insert a ↑s
[PROOFSTEP]
simp only [mem_coe, mem_insert, Set.mem_insert_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a b : α
s : Finset α
x y : α
⊢ x ∈ insert y s ↔ x ∈ insert y ↑s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a✝ b a : α
⊢ insert a ∅ = {a}
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a✝¹ b a a✝ : α
⊢ a✝ ∈ insert a ∅ ↔ a✝ ∈ {a}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b✝ a b : α
s : Finset α
x : α
⊢ x ∈ insert a (insert b s) ↔ x ∈ insert b (insert a s)
[PROOFSTEP]
simp only [mem_insert, or_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a✝ b✝ a b : α
⊢ ↑{a, b} = {a, b}
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a✝ b✝ a b x✝ : α
⊢ x✝ ∈ ↑{a, b} ↔ x✝ ∈ {a, b}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b✝ : α
s : Finset α
a b : α
⊢ ↑s = {a, b} ↔ s = {a, b}
[PROOFSTEP]
rw [← coe_pair, coe_inj]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
x : α
⊢ x ∈ insert a (insert a s) ↔ x ∈ insert a s
[PROOFSTEP]
simp only [mem_insert, ← or_assoc, or_self_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b : α
s t : Finset α
a : α
h : ¬a ∈ s
⊢ s ≠ insert a t
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b : α
s t : Finset α
a : α
h : s = insert a t
⊢ a ∈ s
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t
[PROOFSTEP]
simp only [subset_iff, mem_insert, forall_eq, or_imp, forall_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ s ⊂ t ↔ ∃ a x, insert a s ⊆ t
[PROOFSTEP]
exact_mod_cast @Set.ssubset_iff_insert α s t
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a b : α✝
α : Type u_4
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
s : Multiset α
nd : Nodup s
⊢ p { val := s, nodup := nd }
[PROOFSTEP]
induction s using Multiset.induction with
| empty => exact empty
| @cons a s IH =>
  cases' nodup_cons.1 nd with m nd'
  rw [← (eq_of_veq _ : Finset.cons a ⟨s, _⟩ m = ⟨a ::ₘ s, nd⟩)]
  · exact cons m (IH nd')
  · rw [cons_val]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a b : α✝
α : Type u_4
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
s : Multiset α
nd : Nodup s
⊢ p { val := s, nodup := nd }
[PROOFSTEP]
induction s using Multiset.induction with
| empty => exact empty
| @cons a s IH =>
  cases' nodup_cons.1 nd with m nd'
  rw [← (eq_of_veq _ : Finset.cons a ⟨s, _⟩ m = ⟨a ::ₘ s, nd⟩)]
  · exact cons m (IH nd')
  · rw [cons_val]
[GOAL]
case empty
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s t u v : Finset α✝
a b : α✝
α : Type u_4
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
nd : Nodup 0
⊢ p { val := 0, nodup := nd }
[PROOFSTEP]

| empty => exact empty
[GOAL]
case empty
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s t u v : Finset α✝
a b : α✝
α : Type u_4
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
nd : Nodup 0
⊢ p { val := 0, nodup := nd }
[PROOFSTEP]
exact empty
[GOAL]
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a✝ b : α✝
α : Type u_4
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : Nodup s), p { val := s, nodup := nd }
nd : Nodup (a ::ₘ s)
⊢ p { val := a ::ₘ s, nodup := nd }
[PROOFSTEP]

| @cons a s IH =>
  cases' nodup_cons.1 nd with m nd'
  rw [← (eq_of_veq _ : Finset.cons a ⟨s, _⟩ m = ⟨a ::ₘ s, nd⟩)]
  · exact cons m (IH nd')
  · rw [cons_val]
[GOAL]
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a✝ b : α✝
α : Type u_4
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : Nodup s), p { val := s, nodup := nd }
nd : Nodup (a ::ₘ s)
⊢ p { val := a ::ₘ s, nodup := nd }
[PROOFSTEP]
cases' nodup_cons.1 nd with m nd'
[GOAL]
case cons.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a✝ b : α✝
α : Type u_4
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : Nodup s), p { val := s, nodup := nd }
nd : Nodup (a ::ₘ s)
m : ¬a ∈ s
nd' : Nodup s
⊢ p { val := a ::ₘ s, nodup := nd }
[PROOFSTEP]
rw [← (eq_of_veq _ : Finset.cons a ⟨s, _⟩ m = ⟨a ::ₘ s, nd⟩)]
[GOAL]
case cons.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a✝ b : α✝
α : Type u_4
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : Nodup s), p { val := s, nodup := nd }
nd : Nodup (a ::ₘ s)
m : ¬a ∈ s
nd' : Nodup s
⊢ p (Finset.cons a { val := s, nodup := ?m.116533 } m)
[PROOFSTEP]
exact cons m (IH nd')
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a✝ b : α✝
α : Type u_4
p : Finset α → Prop
empty : p ∅
cons : ∀ ⦃a : α⦄ {s : Finset α} (h : ¬a ∈ s), p s → p (Finset.cons a s h)
a : α
s : Multiset α
IH : ∀ (nd : Nodup s), p { val := s, nodup := nd }
nd : Nodup (a ::ₘ s)
m : ¬a ∈ s
nd' : Nodup s
⊢ (Finset.cons a { val := s, nodup := nd' } m).val = { val := a ::ₘ s, nodup := nd }.val
[PROOFSTEP]
rw [cons_val]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a b : α✝
α : Type u_4
p : (s : Finset α) → Finset.Nonempty s → Prop
h₀ : ∀ (a : α), p {a} (_ : Finset.Nonempty {a})
h₁ :
  ∀ ⦃a : α⦄ (s : Finset α) (h : ¬a ∈ s) (hs : Finset.Nonempty s),
    p s hs → p (cons a s h) (_ : Finset.Nonempty (cons a s h))
s : Finset α
hs : Finset.Nonempty s
⊢ p s hs
[PROOFSTEP]
induction' s using Finset.cons_induction with a t ha h
[GOAL]
case empty
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a b : α✝
α : Type u_4
p : (s : Finset α) → Finset.Nonempty s → Prop
h₀ : ∀ (a : α), p {a} (_ : Finset.Nonempty {a})
h₁ :
  ∀ ⦃a : α⦄ (s : Finset α) (h : ¬a ∈ s) (hs : Finset.Nonempty s),
    p s hs → p (cons a s h) (_ : Finset.Nonempty (cons a s h))
s : Finset α
hs✝ : Finset.Nonempty s
hs : Finset.Nonempty ∅
⊢ p ∅ hs
[PROOFSTEP]
exact (not_nonempty_empty hs).elim
[GOAL]
case cons
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ t✝ u v : Finset α✝
a✝ b : α✝
α : Type u_4
p : (s : Finset α) → Finset.Nonempty s → Prop
h₀ : ∀ (a : α), p {a} (_ : Finset.Nonempty {a})
h₁ :
  ∀ ⦃a : α⦄ (s : Finset α) (h : ¬a ∈ s) (hs : Finset.Nonempty s),
    p s hs → p (cons a s h) (_ : Finset.Nonempty (cons a s h))
s : Finset α
hs✝ : Finset.Nonempty s
a : α
t : Finset α
ha : ¬a ∈ t
h : ∀ (hs : Finset.Nonempty t), p t hs
hs : Finset.Nonempty (cons a t ha)
⊢ p (cons a t ha) hs
[PROOFSTEP]
obtain rfl | ht := t.eq_empty_or_nonempty
[GOAL]
case cons.inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ t u v : Finset α✝
a✝ b : α✝
α : Type u_4
p : (s : Finset α) → Finset.Nonempty s → Prop
h₀ : ∀ (a : α), p {a} (_ : Finset.Nonempty {a})
h₁ :
  ∀ ⦃a : α⦄ (s : Finset α) (h : ¬a ∈ s) (hs : Finset.Nonempty s),
    p s hs → p (cons a s h) (_ : Finset.Nonempty (cons a s h))
s : Finset α
hs✝ : Finset.Nonempty s
a : α
ha : ¬a ∈ ∅
h : ∀ (hs : Finset.Nonempty ∅), p ∅ hs
hs : Finset.Nonempty (cons a ∅ ha)
⊢ p (cons a ∅ ha) hs
[PROOFSTEP]
exact h₀ a
[GOAL]
case cons.inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ t✝ u v : Finset α✝
a✝ b : α✝
α : Type u_4
p : (s : Finset α) → Finset.Nonempty s → Prop
h₀ : ∀ (a : α), p {a} (_ : Finset.Nonempty {a})
h₁ :
  ∀ ⦃a : α⦄ (s : Finset α) (h : ¬a ∈ s) (hs : Finset.Nonempty s),
    p s hs → p (cons a s h) (_ : Finset.Nonempty (cons a s h))
s : Finset α
hs✝ : Finset.Nonempty s
a : α
t : Finset α
ha : ¬a ∈ t
h : ∀ (hs : Finset.Nonempty t), p t hs
hs : Finset.Nonempty (cons a t ha)
ht : Finset.Nonempty t
⊢ p (cons a t ha) hs
[PROOFSTEP]
exact h₁ t ha ht (h ht)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ u v : Finset α
a b : α
t : Finset α
x : α
h : ¬x ∈ t
⊢ { i // i ∈ insert x t } ≃ Option { i // i ∈ t }
[PROOFSTEP]
refine'
  { toFun := fun y => if h : ↑y = x then none else some ⟨y, (mem_insert.mp y.2).resolve_left h⟩
    invFun := fun y => (y.elim ⟨x, mem_insert_self _ _⟩) fun z => ⟨z, mem_insert_of_mem z.2⟩ .. }
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ u v : Finset α
a b : α
t : Finset α
x : α
h : ¬x ∈ t
⊢ LeftInverse
    (fun y =>
      Option.elim y { val := x, property := (_ : x ∈ insert x t) } fun z =>
        { val := ↑z, property := (_ : ↑z ∈ insert x t) })
    fun y => if h : ↑y = x then none else some { val := ↑y, property := (_ : ↑y ∈ t) }
[PROOFSTEP]
intro y
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ u v : Finset α
a b : α
t : Finset α
x : α
h : ¬x ∈ t
y : { i // i ∈ insert x t }
⊢ (fun y =>
        Option.elim y { val := x, property := (_ : x ∈ insert x t) } fun z =>
          { val := ↑z, property := (_ : ↑z ∈ insert x t) })
      ((fun y => if h : ↑y = x then none else some { val := ↑y, property := (_ : ↑y ∈ t) }) y) =
    y
[PROOFSTEP]
by_cases h : ↑y = x
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ u v : Finset α
a b : α
t : Finset α
x : α
h✝ : ¬x ∈ t
y : { i // i ∈ insert x t }
h : ↑y = x
⊢ (fun y =>
        Option.elim y { val := x, property := (_ : x ∈ insert x t) } fun z =>
          { val := ↑z, property := (_ : ↑z ∈ insert x t) })
      ((fun y => if h : ↑y = x then none else some { val := ↑y, property := (_ : ↑y ∈ t) }) y) =
    y
[PROOFSTEP]
simp only [Subtype.ext_iff, h, Option.elim, dif_pos, Subtype.coe_mk]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ u v : Finset α
a b : α
t : Finset α
x : α
h✝ : ¬x ∈ t
y : { i // i ∈ insert x t }
h : ¬↑y = x
⊢ (fun y =>
        Option.elim y { val := x, property := (_ : x ∈ insert x t) } fun z =>
          { val := ↑z, property := (_ : ↑z ∈ insert x t) })
      ((fun y => if h : ↑y = x then none else some { val := ↑y, property := (_ : ↑y ∈ t) }) y) =
    y
[PROOFSTEP]
simp only [h, Option.elim, dif_neg, not_false_iff, Subtype.coe_eta, Subtype.coe_mk]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ u v : Finset α
a b : α
t : Finset α
x : α
h : ¬x ∈ t
⊢ Function.RightInverse
    (fun y =>
      Option.elim y { val := x, property := (_ : x ∈ insert x t) } fun z =>
        { val := ↑z, property := (_ : ↑z ∈ insert x t) })
    fun y => if h : ↑y = x then none else some { val := ↑y, property := (_ : ↑y ∈ t) }
[PROOFSTEP]
rintro (_ | y)
[GOAL]
case refine'_2.none
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ u v : Finset α
a b : α
t : Finset α
x : α
h : ¬x ∈ t
⊢ (fun y => if h : ↑y = x then none else some { val := ↑y, property := (_ : ↑y ∈ t) })
      ((fun y =>
          Option.elim y { val := x, property := (_ : x ∈ insert x t) } fun z =>
            { val := ↑z, property := (_ : ↑z ∈ insert x t) })
        none) =
    none
[PROOFSTEP]
simp only [Option.elim, dif_pos]
[GOAL]
case refine'_2.some
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ u v : Finset α
a b : α
t : Finset α
x : α
h : ¬x ∈ t
y : { i // i ∈ t }
⊢ (fun y => if h : ↑y = x then none else some { val := ↑y, property := (_ : ↑y ∈ t) })
      ((fun y =>
          Option.elim y { val := x, property := (_ : x ∈ insert x t) } fun z =>
            { val := ↑z, property := (_ : ↑z ∈ insert x t) })
        (some y)) =
    some y
[PROOFSTEP]
have : ↑y ≠ x := by
  rintro ⟨⟩
  exact h y.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ u v : Finset α
a b : α
t : Finset α
x : α
h : ¬x ∈ t
y : { i // i ∈ t }
⊢ ↑y ≠ x
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ u v : Finset α
a b : α
t : Finset α
y : { i // i ∈ t }
h : ¬↑y ∈ t
⊢ False
[PROOFSTEP]
exact h y.2
[GOAL]
case refine'_2.some
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ u v : Finset α
a b : α
t : Finset α
x : α
h : ¬x ∈ t
y : { i // i ∈ t }
this : ↑y ≠ x
⊢ (fun y => if h : ↑y = x then none else some { val := ↑y, property := (_ : ↑y ∈ t) })
      ((fun y =>
          Option.elim y { val := x, property := (_ : x ∈ insert x t) } fun z =>
            { val := ↑z, property := (_ : ↑z ∈ insert x t) })
        (some y)) =
    some y
[PROOFSTEP]
simp only [this, Option.elim, Subtype.eta, dif_neg, not_false_iff, Subtype.coe_mk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ _root_.Disjoint (insert a s) t ↔ ¬a ∈ t ∧ _root_.Disjoint s t
[PROOFSTEP]
simp only [disjoint_left, mem_insert, or_imp, forall_and, forall_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ _root_.Disjoint (insert a t) s ↔ ¬a ∈ s ∧ _root_.Disjoint s t
[PROOFSTEP]
rw [disjoint_insert_left, _root_.disjoint_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a✝ b : α
s t : Finset α
h : _root_.Disjoint s t
a : α
⊢ a ∈ disjUnion s t h ↔ a ∈ s ∪ t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁ s₂ t t₁ t₂ u v : Finset α
a b : α
⊢ ¬a ∈ s ∪ t ↔ ¬a ∈ s ∧ ¬a ∈ t
[PROOFSTEP]
rw [mem_union, not_or]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u✝ v : Finset α
a b : α
s t u : Finset α
x✝ : α
⊢ x✝ ∈ s ∪ (t ∪ u) ↔ x✝ ∈ t ∪ (s ∪ u)
[PROOFSTEP]
simp only [mem_union, or_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u✝ v : Finset α
a b : α
s t u : Finset α
x : α
⊢ x ∈ s ∪ t ∪ u ↔ x ∈ s ∪ u ∪ t
[PROOFSTEP]
simp only [mem_union, or_assoc, @or_comm (x ∈ t)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t t₁ t₂ u v : Finset α
a b : α
s : Finset α
x : α
⊢ x ∈ s ∨ x ∈ ∅ ↔ x ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t t₁ t₂ u v : Finset α
a b : α
s : Finset α
x : α
⊢ x ∈ ∅ ∨ x ∈ s ↔ x ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a✝ b a : α
s t : Finset α
⊢ insert a s ∪ t = insert a (s ∪ t)
[PROOFSTEP]
simp only [insert_eq, union_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a✝ b a : α
s t : Finset α
⊢ s ∪ insert a t = insert a (s ∪ t)
[PROOFSTEP]
simp only [insert_eq, union_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a✝ b a : α
s t : Finset α
⊢ insert a (s ∪ t) = insert a s ∪ insert a t
[PROOFSTEP]
simp only [insert_union, union_insert, insert_idem]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a b : α
s t : Finset α
⊢ s = s ∪ t ↔ t ⊆ s
[PROOFSTEP]
rw [← union_eq_left_iff_subset, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a b : α
s t : Finset α
⊢ s = t ∪ s ↔ t ⊆ s
[PROOFSTEP]
rw [← union_eq_right_iff_subset, eq_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁ s₂ t t₁ t₂ u v : Finset α
a b : α
⊢ _root_.Disjoint (s ∪ t) u ↔ _root_.Disjoint s u ∧ _root_.Disjoint t u
[PROOFSTEP]
simp only [disjoint_left, mem_union, or_imp, forall_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁ s₂ t t₁ t₂ u v : Finset α
a b : α
⊢ _root_.Disjoint s (t ∪ u) ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
[PROOFSTEP]
simp only [disjoint_right, mem_union, or_imp, forall_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁ s₂ t t₁ t₂ u v : Finset α
a b : α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
⊢ ∀ (a b : Finset α), P a b
[PROOFSTEP]
intro a b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁ s₂ t t₁ t₂ u v : Finset α
a✝ b✝ : α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a b : Finset α
⊢ P a b
[PROOFSTEP]
refine' Finset.induction_on b empty_right fun x s _xs hi => symm _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t t₁ t₂ u v : Finset α
a✝ b✝ : α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a b : Finset α
x : α
s : Finset α
_xs : ¬x ∈ s
hi : P a s
⊢ P (insert x s) a
[PROOFSTEP]
rw [Finset.insert_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t t₁ t₂ u v : Finset α
a✝ b✝ : α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a b : Finset α
x : α
s : Finset α
_xs : ¬x ∈ s
hi : P a s
⊢ P ({x} ∪ s) a
[PROOFSTEP]
apply union_of _ (symm hi)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t t₁ t₂ u v : Finset α
a✝ b✝ : α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a b : Finset α
x : α
s : Finset α
_xs : ¬x ∈ s
hi : P a s
⊢ P {x} a
[PROOFSTEP]
refine' Finset.induction_on a empty_right fun a t _ta hi => symm _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a✝¹ b✝ : α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a✝ b : Finset α
x : α
s : Finset α
_xs : ¬x ∈ s
hi✝ : P a✝ s
a : α
t : Finset α
_ta : ¬a ∈ t
hi : P {x} t
⊢ P (insert a t) {x}
[PROOFSTEP]
rw [Finset.insert_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a✝¹ b✝ : α
P : Finset α → Finset α → Prop
symm : ∀ {a b : Finset α}, P a b → P b a
empty_right : ∀ {a : Finset α}, P a ∅
singletons : ∀ {a b : α}, P {a} {b}
union_of : ∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c
a✝ b : Finset α
x : α
s : Finset α
_xs : ¬x ∈ s
hi✝ : P a✝ s
a : α
t : Finset α
_ta : ¬a ∈ t
hi : P {x} t
⊢ P ({a} ∪ t) {x}
[PROOFSTEP]
exact union_of singletons (symm hi)
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_4
ι : Type u_5
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
hs : ↑s ⊆ ⋃ (i : ι), f i
⊢ ∃ i, ↑s ⊆ f i
[PROOFSTEP]
classical
revert hs
refine' s.induction_on _ _
· refine' fun _ => ⟨hn.some, _⟩
  simp only [coe_empty, Set.empty_subset]
· intro b t _hbt htc hbtc
  obtain ⟨i : ι, hti : (t : Set α) ⊆ f i⟩ := htc (Set.Subset.trans (t.subset_insert b) hbtc)
  obtain ⟨j, hbj⟩ : ∃ j, b ∈ f j := by simpa [Set.mem_iUnion₂] using hbtc (t.mem_insert_self b)
  rcases h j i with ⟨k, hk, hk'⟩
  use k
  rw [coe_insert, Set.insert_subset_iff]
  exact ⟨hk hbj, _root_.trans hti hk'⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_4
ι : Type u_5
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
hs : ↑s ⊆ ⋃ (i : ι), f i
⊢ ∃ i, ↑s ⊆ f i
[PROOFSTEP]
revert hs
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_4
ι : Type u_5
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
⊢ ↑s ⊆ ⋃ (i : ι), f i → ∃ i, ↑s ⊆ f i
[PROOFSTEP]
refine' s.induction_on _ _
[GOAL]
case refine'_1
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_4
ι : Type u_5
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
⊢ ↑∅ ⊆ ⋃ (i : ι), f i → ∃ i, ↑∅ ⊆ f i
[PROOFSTEP]
refine' fun _ => ⟨hn.some, _⟩
[GOAL]
case refine'_1
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_4
ι : Type u_5
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
x✝ : ↑∅ ⊆ ⋃ (i : ι), f i
⊢ ↑∅ ⊆ f (Nonempty.some hn)
[PROOFSTEP]
simp only [coe_empty, Set.empty_subset]
[GOAL]
case refine'_2
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_4
ι : Type u_5
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s → (↑s ⊆ ⋃ (i : ι), f i → ∃ i, ↑s ⊆ f i) → ↑(insert a s) ⊆ ⋃ (i : ι), f i → ∃ i, ↑(insert a s) ⊆ f i
[PROOFSTEP]
intro b t _hbt htc hbtc
[GOAL]
case refine'_2
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_4
ι : Type u_5
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : ↑t ⊆ ⋃ (i : ι), f i → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
⊢ ∃ i, ↑(insert b t) ⊆ f i
[PROOFSTEP]
obtain ⟨i : ι, hti : (t : Set α) ⊆ f i⟩ := htc (Set.Subset.trans (t.subset_insert b) hbtc)
[GOAL]
case refine'_2.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_4
ι : Type u_5
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : ↑t ⊆ ⋃ (i : ι), f i → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
i : ι
hti : ↑t ⊆ f i
⊢ ∃ i, ↑(insert b t) ⊆ f i
[PROOFSTEP]
obtain ⟨j, hbj⟩ : ∃ j, b ∈ f j := by simpa [Set.mem_iUnion₂] using hbtc (t.mem_insert_self b)
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_4
ι : Type u_5
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : ↑t ⊆ ⋃ (i : ι), f i → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
i : ι
hti : ↑t ⊆ f i
⊢ ∃ j, b ∈ f j
[PROOFSTEP]
simpa [Set.mem_iUnion₂] using hbtc (t.mem_insert_self b)
[GOAL]
case refine'_2.intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_4
ι : Type u_5
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : ↑t ⊆ ⋃ (i : ι), f i → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
i : ι
hti : ↑t ⊆ f i
j : ι
hbj : b ∈ f j
⊢ ∃ i, ↑(insert b t) ⊆ f i
[PROOFSTEP]
rcases h j i with ⟨k, hk, hk'⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_4
ι : Type u_5
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : ↑t ⊆ ⋃ (i : ι), f i → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
i : ι
hti : ↑t ⊆ f i
j : ι
hbj : b ∈ f j
k : ι
hk : f j ⊆ f k
hk' : f i ⊆ f k
⊢ ∃ i, ↑(insert b t) ⊆ f i
[PROOFSTEP]
use k
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_4
ι : Type u_5
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : ↑t ⊆ ⋃ (i : ι), f i → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
i : ι
hti : ↑t ⊆ f i
j : ι
hbj : b ∈ f j
k : ι
hk : f j ⊆ f k
hk' : f i ⊆ f k
⊢ ↑(insert b t) ⊆ f k
[PROOFSTEP]
rw [coe_insert, Set.insert_subset_iff]
[GOAL]
case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α✝
a b✝ : α✝
α : Type u_4
ι : Type u_5
hn : Nonempty ι
f : ι → Set α
h : Directed (fun x x_1 => x ⊆ x_1) f
s : Finset α
b : α
t : Finset α
_hbt : ¬b ∈ t
htc : ↑t ⊆ ⋃ (i : ι), f i → ∃ i, ↑t ⊆ f i
hbtc : ↑(insert b t) ⊆ ⋃ (i : ι), f i
i : ι
hti : ↑t ⊆ f i
j : ι
hbj : b ∈ f j
k : ι
hk : f j ⊆ f k
hk' : f i ⊆ f k
⊢ b ∈ f k ∧ ↑t ⊆ f k
[PROOFSTEP]
exact ⟨hk hbj, _root_.trans hti hk'⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_4
ι : Type u_5
f : ι → Set α
c : Set ι
hn : Set.Nonempty c
hc : DirectedOn (fun i j => f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ (i : ι) (_ : i ∈ c), f i
⊢ ∃ i, i ∈ c ∧ ↑s ⊆ f i
[PROOFSTEP]
rw [Set.biUnion_eq_iUnion] at hs 
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_4
ι : Type u_5
f : ι → Set α
c : Set ι
hn : Set.Nonempty c
hc : DirectedOn (fun i j => f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ (x : ↑c), f ↑x
⊢ ∃ i, i ∈ c ∧ ↑s ⊆ f i
[PROOFSTEP]
haveI := hn.coe_sort
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_4
ι : Type u_5
f : ι → Set α
c : Set ι
hn : Set.Nonempty c
hc : DirectedOn (fun i j => f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ (x : ↑c), f ↑x
this : Nonempty ↑c
⊢ ∃ i, i ∈ c ∧ ↑s ⊆ f i
[PROOFSTEP]
obtain ⟨⟨i, hic⟩, hi⟩ := (directed_comp.2 hc.directed_val).exists_mem_subset_of_finset_subset_biUnion hs
[GOAL]
case intro.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α✝
s✝ s₁ s₂ t t₁ t₂ u v : Finset α✝
a b : α✝
α : Type u_4
ι : Type u_5
f : ι → Set α
c : Set ι
hn : Set.Nonempty c
hc : DirectedOn (fun i j => f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ (x : ↑c), f ↑x
this : Nonempty ↑c
i : ι
hic : i ∈ c
hi : ↑s ⊆ ((fun j => f j) ∘ Subtype.val) { val := i, property := hic }
⊢ ∃ i, i ∈ c ∧ ↑s ⊆ f i
[PROOFSTEP]
exact ⟨i, hic, hi⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u✝ v : Finset α
a b : α
s₁ s₂ u : Finset α
⊢ s₁ ⊆ s₂ → s₁ ⊆ u → s₁ ⊆ s₂ ∩ u
[PROOFSTEP]
simp (config := { contextual := true }) [subset_iff, mem_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a b : α
s t : Finset α
⊢ (s ∪ t) ∩ s = s
[PROOFSTEP]
rw [← coe_inj, coe_inter, coe_union, Set.union_inter_cancel_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a b : α
s t : Finset α
⊢ (s ∪ t) ∩ t = t
[PROOFSTEP]
rw [← coe_inj, coe_inter, coe_union, Set.union_inter_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a b : α
s₁ s₂ : Finset α
x✝ : α
⊢ x✝ ∈ s₁ ∩ s₂ ↔ x✝ ∈ s₂ ∩ s₁
[PROOFSTEP]
simp only [mem_inter, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a b : α
s₁ s₂ s₃ : Finset α
x✝ : α
⊢ x✝ ∈ s₁ ∩ s₂ ∩ s₃ ↔ x✝ ∈ s₁ ∩ (s₂ ∩ s₃)
[PROOFSTEP]
simp only [mem_inter, and_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a b : α
s₁ s₂ s₃ : Finset α
x✝ : α
⊢ x✝ ∈ s₁ ∩ (s₂ ∩ s₃) ↔ x✝ ∈ s₂ ∩ (s₁ ∩ s₃)
[PROOFSTEP]
simp only [mem_inter, and_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a b : α
s₁ s₂ s₃ : Finset α
x✝ : α
⊢ x✝ ∈ s₁ ∩ s₂ ∩ s₃ ↔ x✝ ∈ s₁ ∩ s₃ ∩ s₂
[PROOFSTEP]
simp only [mem_inter, and_right_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t t₁ t₂ u v : Finset α
a b : α
s : Finset α
x✝ : α
⊢ x✝ ∈ s ∧ x✝ ∈ ∅ ↔ x✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t t₁ t₂ u v : Finset α
a b : α
s : Finset α
x✝ : α
⊢ x✝ ∈ ∅ ∧ x✝ ∈ s ↔ x✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a b : α
s t : Finset α
⊢ s ∩ (t ∪ s) = s
[PROOFSTEP]
rw [inter_comm, union_inter_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a✝ b : α
s₁ s₂ : Finset α
a : α
h : a ∈ s₂
x : α
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ insert a (s₁ ∩ s₂)
[PROOFSTEP]
have : x = a ∨ x ∈ s₂ ↔ x ∈ s₂ := or_iff_right_of_imp <| by rintro rfl; exact h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a✝ b : α
s₁ s₂ : Finset α
a : α
h : a ∈ s₂
x : α
⊢ x = a → x ∈ s₂
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a b : α
s₁ s₂ : Finset α
x : α
h : x ∈ s₂
⊢ x ∈ s₂
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a✝ b : α
s₁ s₂ : Finset α
a : α
h : a ∈ s₂
x : α
this : x = a ∨ x ∈ s₂ ↔ x ∈ s₂
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ insert a (s₁ ∩ s₂)
[PROOFSTEP]
simp only [mem_inter, mem_insert, or_and_left, this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a✝ b : α
s₁ s₂ : Finset α
a : α
h : a ∈ s₁
⊢ s₁ ∩ insert a s₂ = insert a (s₁ ∩ s₂)
[PROOFSTEP]
rw [inter_comm, insert_inter_of_mem h, inter_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a✝ b : α
s₁ s₂ : Finset α
a : α
h : ¬a ∈ s₂
x : α
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ s₁ ∩ s₂
[PROOFSTEP]
have : ¬(x = a ∧ x ∈ s₂) := by rintro ⟨rfl, H⟩; exact h H
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a✝ b : α
s₁ s₂ : Finset α
a : α
h : ¬a ∈ s₂
x : α
⊢ ¬(x = a ∧ x ∈ s₂)
[PROOFSTEP]
rintro ⟨rfl, H⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a b : α
s₁ s₂ : Finset α
x : α
H : x ∈ s₂
h : ¬x ∈ s₂
⊢ False
[PROOFSTEP]
exact h H
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a✝ b : α
s₁ s₂ : Finset α
a : α
h : ¬a ∈ s₂
x : α
this : ¬(x = a ∧ x ∈ s₂)
⊢ x ∈ insert a s₁ ∩ s₂ ↔ x ∈ s₁ ∩ s₂
[PROOFSTEP]
simp only [mem_inter, mem_insert, or_and_right, this, false_or_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁✝ s₂✝ t t₁ t₂ u v : Finset α
a✝ b : α
s₁ s₂ : Finset α
a : α
h : ¬a ∈ s₁
⊢ s₁ ∩ insert a s₂ = s₁ ∩ s₂
[PROOFSTEP]
rw [inter_comm, insert_inter_of_not_mem h, inter_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t t₁ t₂ u v : Finset α
a✝ b a : α
s : Finset α
H : a ∈ s
⊢ insert a ∅ ∩ s = insert a ∅
[PROOFSTEP]
rw [insert_inter_of_mem H, empty_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t t₁ t₂ u v : Finset α
a✝ b a : α
s : Finset α
H : ¬a ∈ s
⊢ ∀ (x : α), ¬x ∈ {a} ∩ s
[PROOFSTEP]
simp only [mem_inter, mem_singleton]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t t₁ t₂ u v : Finset α
a✝ b a : α
s : Finset α
H : ¬a ∈ s
⊢ ∀ (x : α), ¬(x = a ∧ x ∈ s)
[PROOFSTEP]
rintro x ⟨rfl, h⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t t₁ t₂ u v : Finset α
a b : α
s : Finset α
x : α
h : x ∈ s
H : ¬x ∈ s
⊢ False
[PROOFSTEP]
exact H h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t t₁ t₂ u v : Finset α
a✝ b a : α
s : Finset α
h : a ∈ s
⊢ s ∩ {a} = {a}
[PROOFSTEP]
rw [inter_comm, singleton_inter_of_mem h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t t₁ t₂ u v : Finset α
a✝ b a : α
s : Finset α
h : ¬a ∈ s
⊢ s ∩ {a} = ∅
[PROOFSTEP]
rw [inter_comm, singleton_inter_of_not_mem h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a b : α
x y s t : Finset α
h : x ⊆ y
h' : s ⊆ t
⊢ x ∩ s ⊆ y ∩ t
[PROOFSTEP]
intro a a_in
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a✝ b : α
x y s t : Finset α
h : x ⊆ y
h' : s ⊆ t
a : α
a_in : a ∈ x ∩ s
⊢ a ∈ y ∩ t
[PROOFSTEP]
rw [Finset.mem_inter] at a_in ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a✝ b : α
x y s t : Finset α
h : x ⊆ y
h' : s ⊆ t
a : α
a_in : a ∈ x ∧ a ∈ s
⊢ a ∈ y ∧ a ∈ t
[PROOFSTEP]
exact ⟨h a_in.1, h' a_in.2⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁ s₂ t t₁ t₂ u v : Finset α
a✝ b✝ : α
a b c : Finset α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
[PROOFSTEP]
simp (config := { contextual := true }) only [sup_eq_union, inf_eq_inter, le_eq_subset, subset_iff, mem_inter,
  mem_union, and_imp, or_imp, true_or_iff, imp_true_iff, true_and_iff, or_true_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s s₁ s₂ t t₁ t₂ u v : Finset α
a b : α
⊢ (∃ a, a ∈ s ∧ a ∈ t) ↔ Finset.Nonempty (s ∩ t)
[PROOFSTEP]
simp [Finset.Nonempty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a b : α
s t : Finset α
⊢ _root_.Disjoint s t ∨ Finset.Nonempty (s ∩ t)
[PROOFSTEP]
rw [← not_disjoint_iff_nonempty_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a b : α
s t : Finset α
⊢ _root_.Disjoint s t ∨ ¬_root_.Disjoint s t
[PROOFSTEP]
exact em _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ IsDirected (Finset α) fun x x_1 => x ≤ x_1
[PROOFSTEP]
classical infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ IsDirected (Finset α) fun x x_1 => x ≤ x_1
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a✝ b a : α
⊢ erase {a} a = ∅
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a✝ b a x : α
⊢ x ∈ erase {a} a ↔ x ∈ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ a ≠ b → a ∈ s → a ∈ erase s b
[PROOFSTEP]
simp only [mem_erase]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ a ≠ b → a ∈ s → a ≠ b ∧ a ∈ s
[PROOFSTEP]
exact And.intro
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
hs : b ∈ s
hsa : ¬b ∈ erase s a
⊢ b = a
[PROOFSTEP]
rw [mem_erase, not_and] at hsa 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
hs : b ∈ s
hsa : b ≠ a → ¬b ∈ s
⊢ b = a
[PROOFSTEP]
exact not_imp_not.mp hsa hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b : α
s : Finset α
a x : α
⊢ x ∈ erase (insert a s) a ↔ x ∈ erase s a
[PROOFSTEP]
simp (config := { contextual := true }) only [mem_erase, mem_insert, and_congr_right_iff, false_or_iff, iff_self_iff,
  imp_true_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
h : ¬a ∈ s
⊢ erase (insert a s) a = s
[PROOFSTEP]
rw [erase_insert_eq_erase, erase_eq_of_not_mem h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b✝ a b : α
s : Finset α
h : a ≠ b
x : α
⊢ x ∈ erase (insert a s) b ↔ x ∈ insert a (erase s b)
[PROOFSTEP]
have : x ≠ b ∧ x = a ↔ x = a := and_iff_right_of_imp fun hx => hx.symm ▸ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b✝ a b : α
s : Finset α
h : a ≠ b
x : α
this : x ≠ b ∧ x = a ↔ x = a
⊢ x ∈ erase (insert a s) b ↔ x ∈ insert a (erase s b)
[PROOFSTEP]
simp only [mem_erase, mem_insert, and_or_left, this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b✝ a b : α
s : Finset α
ha : ¬a ∈ s
hb : a ≠ b
⊢ erase (cons a s ha) b = cons a (erase s b) (_ : a ∈ erase s b → False)
[PROOFSTEP]
simp only [cons_eq_insert, erase_insert_of_ne hb]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
h : a ∈ s
x : α
⊢ x ∈ insert a (erase s a) ↔ x ∈ s
[PROOFSTEP]
simp only [mem_insert, mem_erase, or_and_left, dec_em, true_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
h : a ∈ s
x : α
⊢ x = a ∨ x ∈ s ↔ x ∈ s
[PROOFSTEP]
apply or_iff_right_of_imp
[GOAL]
case ha
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
h : a ∈ s
x : α
⊢ x = a → x ∈ s
[PROOFSTEP]
rintro rfl
[GOAL]
case ha
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a b : α
s : Finset α
x : α
h : x ∈ s
⊢ x ∈ s
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
x✝ : α
⊢ x✝ ≠ a ∧ x✝ ∈ s ↔ x✝ ∈ ↑s \ {a}
[PROOFSTEP]
rw [and_comm, Set.mem_diff, Set.mem_singleton_iff, mem_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a b : α
s t : Finset α
⊢ s ⊂ t ↔ ∃ a, a ∈ t ∧ s ⊆ erase t a
[PROOFSTEP]
refine' ⟨fun h => _, fun ⟨a, ha, h⟩ => ssubset_of_subset_of_ssubset h <| erase_ssubset ha⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a b : α
s t : Finset α
h : s ⊂ t
⊢ ∃ a, a ∈ t ∧ s ⊆ erase t a
[PROOFSTEP]
obtain ⟨a, ht, hs⟩ := not_subset.1 h.2
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b : α
s t : Finset α
h : s ⊂ t
a : α
ht : a ∈ t
hs : ¬a ∈ s
⊢ ∃ a, a ∈ t ∧ s ⊆ erase t a
[PROOFSTEP]
exact ⟨a, ht, subset_erase.2 ⟨h.1, hs⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b : α
s : Finset α
a : α
h : ¬a ∈ s
⊢ erase (cons a s h) a = s
[PROOFSTEP]
rw [cons_eq_insert, erase_insert_eq_erase, erase_eq_of_not_mem h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
⊢ erase (erase s a) a = erase s a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b✝ a b : α
s : Finset α
⊢ erase (erase s a) b = erase (erase s b) a
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b✝ a b : α
s : Finset α
x : α
⊢ x ∈ erase (erase s a) b ↔ x ∈ erase (erase s b) a
[PROOFSTEP]
simp only [mem_erase, ← and_assoc]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b✝ a b : α
s : Finset α
x : α
⊢ (x ≠ b ∧ x ≠ a) ∧ x ∈ s ↔ (x ≠ a ∧ x ≠ b) ∧ x ∈ s
[PROOFSTEP]
rw [@and_comm (x ≠ a)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b a : α
s t : Finset α
⊢ s ⊆ insert a t ↔ erase s a ⊆ t
[PROOFSTEP]
simp only [subset_iff, or_iff_not_imp_left, mem_erase, mem_insert, and_imp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b a : α
s t : Finset α
⊢ (∀ ⦃x : α⦄, x ∈ s → ¬x = a → x ∈ t) ↔ ∀ ⦃x : α⦄, x ≠ a → x ∈ s → x ∈ t
[PROOFSTEP]
exact forall_congr' fun x => forall_swap
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
h : ¬a ∈ s
⊢ s ⊆ insert a t ↔ s ⊆ t
[PROOFSTEP]
rw [subset_insert_iff, erase_eq_of_not_mem h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
h : a ∈ t
⊢ erase s a ⊆ t ↔ s ⊆ t
[PROOFSTEP]
rw [← subset_insert_iff, insert_eq_of_mem h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a b x y : α
s : Finset α
hx : x ∈ s
⊢ erase s x = erase s y ↔ x = y
[PROOFSTEP]
refine ⟨fun h => eq_of_mem_of_not_mem_erase hx ?_, congr_arg _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a b x y : α
s : Finset α
hx : x ∈ s
h : erase s x = erase s y
⊢ ¬x ∈ erase s y
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a b x y : α
s : Finset α
hx : x ∈ s
h : erase s x = erase s y
⊢ ¬x ∈ erase s x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b a : α
s : Finset α
hs : s ∈ {s | a ∈ s}
t : Finset α
ht : t ∈ {s | a ∈ s}
h : erase s a = (fun s => erase s a) t
⊢ s = t
[PROOFSTEP]
rw [← insert_erase hs, ← insert_erase ht, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
s₁ s₂ : Finset α
⊢ ∀ (x : α), ¬x ∈ s₁ ∩ (s₂ \ s₁)
[PROOFSTEP]
simp only [mem_inter, mem_sdiff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
s₁ s₂ : Finset α
⊢ ∀ (x : α), ¬(x ∈ s₁ ∧ x ∈ s₂ ∧ ¬x ∈ s₁)
[PROOFSTEP]
rintro x ⟨h, _, hn⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
s₁ s₂ : Finset α
x : α
h : x ∈ s₁
left✝ : x ∈ s₂
hn : ¬x ∈ s₁
⊢ False
[PROOFSTEP]
exact hn h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
x y : Finset α
⊢ x ⊓ y ⊔ x \ y = x
[PROOFSTEP]
simp only [ext_iff, mem_union, mem_sdiff, inf_eq_inter, sup_eq_union, mem_inter, ← and_or_left, em, and_true,
  implies_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
x y : Finset α
⊢ x ⊓ y ⊓ x \ y = ⊥
[PROOFSTEP]
simp only [ext_iff, inter_sdiff_self, inter_empty, inter_assoc, false_iff_iff, inf_eq_inter, not_mem_empty,
  bot_eq_empty, not_false_iff, implies_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
h : a ∈ t
⊢ ¬a ∈ s \ t
[PROOFSTEP]
simp only [mem_sdiff, h, not_true, not_false_iff, and_false_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
h : ¬a ∈ s
⊢ ¬a ∈ s \ t
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u✝ v : Finset α
a b : α
s t u : Finset α
⊢ s ∩ (t \ u) = (s ∩ t) \ u
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u✝ v : Finset α
a b : α
s t u : Finset α
x : α
⊢ x ∈ s ∩ (t \ u) ↔ x ∈ (s ∩ t) \ u
[PROOFSTEP]
simp [and_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ s ∪ t \ s = t ∪ s \ t
[PROOFSTEP]
simp [union_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a b : α
s t : Finset α
x : α
h : ¬x ∈ t
⊢ insert x s \ t = insert x (s \ t)
[PROOFSTEP]
rw [← coe_inj, coe_insert, coe_sdiff, coe_sdiff, coe_insert]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a b : α
s t : Finset α
x : α
h : ¬x ∈ t
⊢ insert x ↑s \ ↑t = insert x (↑s \ ↑t)
[PROOFSTEP]
exact Set.insert_diff_of_not_mem _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a b : α
s : Finset α
x : α
h : x ∈ t
⊢ insert x s \ t = s \ t
[PROOFSTEP]
rw [← coe_inj, coe_sdiff, coe_sdiff, coe_insert]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a b : α
s : Finset α
x : α
h : x ∈ t
⊢ insert x ↑s \ ↑t = ↑s \ ↑t
[PROOFSTEP]
exact Set.insert_diff_of_mem _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ u v : Finset α
a b x : α
h : ¬x ∈ s
t : Finset α
⊢ s \ insert x t = s \ t
[PROOFSTEP]
refine' Subset.antisymm (sdiff_subset_sdiff (Subset.refl _) (subset_insert _ _)) fun y hy => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ u v : Finset α
a b x : α
h : ¬x ∈ s
t : Finset α
y : α
hy : y ∈ s \ t
⊢ y ∈ s \ insert x t
[PROOFSTEP]
simp only [mem_sdiff, mem_insert, not_or] at hy ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ u v : Finset α
a b x : α
h : ¬x ∈ s
t : Finset α
y : α
hy : y ∈ s ∧ ¬y ∈ t
⊢ y ∈ s ∧ ¬y = x ∧ ¬y ∈ t
[PROOFSTEP]
exact ⟨hy.1, fun hxy => h <| hxy ▸ hy.1, hy.2⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b a : α
s : Finset α
⊢ s \ {a} = erase s a
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝¹ b a : α
s : Finset α
a✝ : α
⊢ a✝ ∈ s \ {a} ↔ a✝ ∈ erase s a
[PROOFSTEP]
rw [mem_erase, mem_sdiff, mem_singleton, and_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
⊢ _root_.Disjoint (erase s a) t ↔ _root_.Disjoint s (erase t a)
[PROOFSTEP]
simp_rw [erase_eq, disjoint_sdiff_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
ha : ¬a ∈ t
hst : _root_.Disjoint (erase s a) t
⊢ _root_.Disjoint s t
[PROOFSTEP]
rw [← erase_insert ha, ← disjoint_erase_comm, disjoint_insert_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
ha : ¬a ∈ t
hst : _root_.Disjoint (erase s a) t
⊢ ¬a ∈ erase s a ∧ _root_.Disjoint (erase s a) t
[PROOFSTEP]
exact ⟨not_mem_erase _ _, hst⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
ha : ¬a ∈ s
hst : _root_.Disjoint s (erase t a)
⊢ _root_.Disjoint s t
[PROOFSTEP]
rw [← erase_insert ha, disjoint_erase_comm, disjoint_insert_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
ha : ¬a ∈ s
hst : _root_.Disjoint s (erase t a)
⊢ ¬a ∈ erase t a ∧ _root_.Disjoint s (erase t a)
[PROOFSTEP]
exact ⟨not_mem_erase _ _, hst⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b a : α
s t : Finset α
⊢ s ∩ erase t a = erase (s ∩ t) a
[PROOFSTEP]
simp only [erase_eq, inter_sdiff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b a : α
s t : Finset α
⊢ erase s a ∩ t = erase (s ∩ t) a
[PROOFSTEP]
simpa only [inter_comm t] using inter_erase a t s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b : α
s t : Finset α
a : α
⊢ erase s a \ t = erase (s \ t) a
[PROOFSTEP]
simp_rw [erase_eq, sdiff_right_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b : α
s t : Finset α
a : α
⊢ insert a s ∪ t = s ∪ insert a t
[PROOFSTEP]
rw [insert_union, union_insert]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b : α
s t : Finset α
a : α
⊢ erase s a ∩ t = s ∩ erase t a
[PROOFSTEP]
rw [erase_inter, inter_erase]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b : α
s t : Finset α
a : α
⊢ erase (s ∪ t) a = erase s a ∪ erase t a
[PROOFSTEP]
simp_rw [erase_eq, union_sdiff_distrib]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b : α
s t : Finset α
a : α
⊢ insert a (s ∩ t) = insert a s ∩ insert a t
[PROOFSTEP]
simp_rw [insert_eq, union_distrib_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a✝ b : α
s t : Finset α
a : α
⊢ erase (s \ t) a = erase s a \ erase t a
[PROOFSTEP]
simp_rw [erase_eq, sdiff_sdiff, sup_sdiff_eq_sup le_rfl, sup_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a b : α
ha : a ∈ t
s : Finset α
⊢ erase s a ∪ t = s ∪ t
[PROOFSTEP]
rw [← insert_erase (mem_union_right s ha), erase_union_distrib, ← union_insert, insert_erase ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t✝ u v : Finset α
a b : α
ha : a ∈ s
t : Finset α
⊢ s ∪ erase t a = s ∪ t
[PROOFSTEP]
rw [← insert_erase (mem_union_left t ha), erase_union_distrib, ← insert_union, insert_erase ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
ha : ¬a ∈ s
⊢ _root_.Disjoint {a} s
[PROOFSTEP]
simp [ha]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
hts : t ⊆ s
ha : a ∈ t
⊢ s \ t ∪ erase t a = erase s a
[PROOFSTEP]
simp_rw [erase_eq, sdiff_union_sdiff_cancel hts (singleton_subset_iff.2 ha)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a b : α
s t : Finset α
x : α
⊢ s \ insert x t = erase (s \ t) x
[PROOFSTEP]
simp_rw [← sdiff_singleton_eq_erase, insert_eq, sdiff_sdiff_left', sdiff_union_distrib, inter_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ u v : Finset α
a b : α
s t : Finset α
x : α
hxs : x ∈ s
hxt : ¬x ∈ t
⊢ insert x (s \ insert x t) = s \ t
[PROOFSTEP]
rw [sdiff_insert, insert_erase (mem_sdiff.mpr ⟨hxs, hxt⟩)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
h : a ∈ s
⊢ s \ erase t a = insert a (s \ t)
[PROOFSTEP]
rw [← sdiff_singleton_eq_erase, sdiff_sdiff_eq_sdiff_union (singleton_subset_iff.2 h), insert_eq, union_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t u v : Finset α
a b : α
ha : a ∈ s
⊢ s \ erase s a = {a}
[PROOFSTEP]
rw [sdiff_erase ha, sdiff_self, insert_emptyc_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t u v : Finset α
a✝ b : α
s : Finset α
a : α
⊢ erase s a = ∅ ↔ s = ∅ ∨ s = {a}
[PROOFSTEP]
rw [← sdiff_singleton_eq_erase, sdiff_eq_empty_iff_subset, subset_singleton_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
a b : α
⊢ a ∈ s ∆ t ↔ a ∈ s ∧ ¬a ∈ t ∨ a ∈ t ∧ ¬a ∈ s
[PROOFSTEP]
simp_rw [symmDiff, sup_eq_union, mem_union, mem_sdiff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Finset α
a b x : α
⊢ x ∈ ↑(s ∆ t) ↔ x ∈ ↑s ∆ ↑t
[PROOFSTEP]
simp [mem_symmDiff, Set.mem_symmDiff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SizeOf α
x : α
s : Finset α
hx : x ∈ s
⊢ sizeOf x < sizeOf s
[PROOFSTEP]
cases s
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : Nodup val✝
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ sizeOf x < sizeOf { val := val✝, nodup := nodup✝ }
[PROOFSTEP]
dsimp [SizeOf.sizeOf, SizeOf.sizeOf, Multiset.sizeOf]
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : Nodup val✝
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ sizeOf x < 1 + Quot.liftOn val✝ (fun m => List._sizeOf_1 m) (_ : ∀ (x x_1 : List α), x ~ x_1 → sizeOf x = sizeOf x_1)
[PROOFSTEP]
rw [add_comm]
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : Nodup val✝
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ sizeOf x < Quot.liftOn val✝ (fun m => List._sizeOf_1 m) (_ : ∀ (x x_1 : List α), x ~ x_1 → sizeOf x = sizeOf x_1) + 1
[PROOFSTEP]
refine' lt_trans _ (Nat.lt_succ_self _)
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SizeOf α
x : α
val✝ : Multiset α
nodup✝ : Nodup val✝
hx : x ∈ { val := val✝, nodup := nodup✝ }
⊢ sizeOf x < Quot.liftOn val✝ (fun m => List._sizeOf_1 m) (_ : ∀ (x x_1 : List α), x ~ x_1 → sizeOf x = sizeOf x_1)
[PROOFSTEP]
exact Multiset.sizeOf_lt_sizeOf_of_mem hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
⊢ Finset.Nonempty (attach s) ↔ Finset.Nonempty s
[PROOFSTEP]
simp [Finset.Nonempty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
⊢ attach s = ∅ ↔ s = ∅
[PROOFSTEP]
simp [eq_empty_iff_forall_not_mem]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ piecewise (insert j s) f g j = f j
[PROOFSTEP]
simp [piecewise]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ ∅)
⊢ piecewise ∅ f g = g
[PROOFSTEP]
ext i
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝ : (i : α) → Decidable (i ∈ ∅)
i : α
⊢ piecewise ∅ f g i = g i
[PROOFSTEP]
simp [piecewise]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : (j : α) → Decidable (j ∈ ↑s)
⊢ Set.piecewise (↑s) f g = piecewise s f g
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : (j : α) → Decidable (j ∈ ↑s)
x✝ : α
⊢ Set.piecewise (↑s) f g x✝ = piecewise s f g x✝
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
i : α
hi : i ∈ s
⊢ piecewise s f g i = f i
[PROOFSTEP]
simp [piecewise, hi]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
i : α
hi : ¬i ∈ s
⊢ piecewise s f g i = g i
[PROOFSTEP]
simp [piecewise, hi]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
i j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
h : i ≠ j
⊢ piecewise (insert j s) f g i = piecewise s f g i
[PROOFSTEP]
simp [piecewise, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ piecewise (insert j s) f g = update (piecewise s f g) j (f j)
[PROOFSTEP]
classical simp only [← piecewise_coe, coe_insert, ← Set.piecewise_insert]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ piecewise (insert j s) f g = update (piecewise s f g) j (f j)
[PROOFSTEP]
simp only [← piecewise_coe, coe_insert, ← Set.piecewise_insert]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
⊢ Set.piecewise (↑(insert j s)) f g = Set.piecewise (insert j ↑s) f g
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
x✝ : α
⊢ Set.piecewise (↑(insert j s)) f g x✝ = Set.piecewise (insert j ↑s) f g x✝
[PROOFSTEP]
congr
[GOAL]
case h.e_s
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝² : (j : α) → Decidable (j ∈ s)
inst✝¹ : DecidableEq α
j : α
inst✝ : (i : α) → Decidable (i ∈ insert j s)
x✝ : α
⊢ ↑(insert j s) = insert j ↑s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
i : α
p : δ i → Prop
hf : p (f i)
hg : p (g i)
⊢ p (piecewise s f g i)
[PROOFSTEP]
by_cases hi : i ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
i : α
p : δ i → Prop
hf : p (f i)
hg : p (g i)
hi : i ∈ s
⊢ p (piecewise s f g i)
[PROOFSTEP]
simpa [hi]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
i : α
p : δ i → Prop
hf : p (f i)
hg : p (g i)
hi : ¬i ∈ s
⊢ p (piecewise s f g i)
[PROOFSTEP]
simpa [hi]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ✝ : α → Sort u_4
s : Finset α
f✝ g✝ : (i : α) → δ✝ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_5
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ Set.pi t t'
hg : g ∈ Set.pi t t'
⊢ piecewise s f g ∈ Set.pi t t'
[PROOFSTEP]
classical
rw [← piecewise_coe]
exact Set.piecewise_mem_pi (↑s) hf hg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ✝ : α → Sort u_4
s : Finset α
f✝ g✝ : (i : α) → δ✝ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_5
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ Set.pi t t'
hg : g ∈ Set.pi t t'
⊢ piecewise s f g ∈ Set.pi t t'
[PROOFSTEP]
rw [← piecewise_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ✝ : α → Sort u_4
s : Finset α
f✝ g✝ : (i : α) → δ✝ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_5
t : Set α
t' : (i : α) → Set (δ i)
f g : (i : α) → δ i
hf : f ∈ Set.pi t t'
hg : g ∈ Set.pi t t'
⊢ Set.piecewise (↑s) f g ∈ Set.pi t t'
[PROOFSTEP]
exact Set.piecewise_mem_pi (↑s) hf hg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
⊢ piecewise {i} f g = update g i (f i)
[PROOFSTEP]
rw [← insert_emptyc_eq, piecewise_insert, piecewise_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
v : δ i
⊢ update (piecewise s f g) i v = piecewise s (update f i v) (update g i v)
[PROOFSTEP]
ext j
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
v : δ i
j : α
⊢ update (piecewise s f g) i v j = piecewise s (update f i v) (update g i v) j
[PROOFSTEP]
rcases em (j = i) with (rfl | hj)
[GOAL]
case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
j : α
v : δ j
⊢ update (piecewise s f g) j v j = piecewise s (update f j v) (update g j v) j
[PROOFSTEP]
by_cases hs : j ∈ s
[GOAL]
case h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
v : δ i
j : α
hj : ¬j = i
⊢ update (piecewise s f g) i v j = piecewise s (update f i v) (update g i v) j
[PROOFSTEP]
by_cases hs : j ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
j : α
v : δ j
hs : j ∈ s
⊢ update (piecewise s f g) j v j = piecewise s (update f j v) (update g j v) j
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
j : α
v : δ j
hs : ¬j ∈ s
⊢ update (piecewise s f g) j v j = piecewise s (update f j v) (update g j v) j
[PROOFSTEP]
simp [*]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
v : δ i
j : α
hj : ¬j = i
hs : j ∈ s
⊢ update (piecewise s f g) i v j = piecewise s (update f i v) (update g i v) j
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
v : δ i
j : α
hj : ¬j = i
hs : ¬j ∈ s
⊢ update (piecewise s f g) i v j = piecewise s (update f i v) (update g i v) j
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
hi : i ∈ s
v : δ i
⊢ update (piecewise s f g) i v = piecewise s (update f i v) g
[PROOFSTEP]
rw [update_piecewise]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
hi : i ∈ s
v : δ i
⊢ piecewise s (update f i v) (update g i v) = piecewise s (update f i v) g
[PROOFSTEP]
refine' s.piecewise_congr (fun _ _ => rfl) fun j hj => update_noteq _ _ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
hi : i ∈ s
v : δ i
j : α
hj : ¬j ∈ s
⊢ j ≠ i
[PROOFSTEP]
exact fun h => hj (h.symm ▸ hi)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
hi : ¬i ∈ s
v : δ i
⊢ update (piecewise s f g) i v = piecewise s f (update g i v)
[PROOFSTEP]
rw [update_piecewise]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
hi : ¬i ∈ s
v : δ i
⊢ piecewise s (update f i v) (update g i v) = piecewise s f (update g i v)
[PROOFSTEP]
refine' s.piecewise_congr (fun j hj => update_noteq _ _ _) fun _ _ => rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : α → Sort u_4
s : Finset α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : DecidableEq α
i : α
hi : ¬i ∈ s
v : δ i
j : α
hj : j ∈ s
⊢ j ≠ i
[PROOFSTEP]
exact fun h => hi (h ▸ hj)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ✝ : α → Sort u_4
s : Finset α
f✝ g✝ : (i : α) → δ✝ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_5
inst✝ : (i : α) → Preorder (δ i)
f g f' g' : (i : α) → δ i
Hf : ∀ (x : α), x ∈ s → f x ≤ f' x
Hg : ∀ (x : α), ¬x ∈ s → g x ≤ g' x
x : α
⊢ piecewise s f g x ≤ piecewise s f' g' x
[PROOFSTEP]
by_cases hx : x ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
δ✝ : α → Sort u_4
s : Finset α
f✝ g✝ : (i : α) → δ✝ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_5
inst✝ : (i : α) → Preorder (δ i)
f g f' g' : (i : α) → δ i
Hf : ∀ (x : α), x ∈ s → f x ≤ f' x
Hg : ∀ (x : α), ¬x ∈ s → g x ≤ g' x
x : α
hx : x ∈ s
⊢ piecewise s f g x ≤ piecewise s f' g' x
[PROOFSTEP]
simp [hx, *]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
δ✝ : α → Sort u_4
s : Finset α
f✝ g✝ : (i : α) → δ✝ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
δ : α → Type u_5
inst✝ : (i : α) → Preorder (δ i)
f g f' g' : (i : α) → δ i
Hf : ∀ (x : α), x ∈ s → f x ≤ f' x
Hg : ∀ (x : α), ¬x ∈ s → g x ≤ g' x
x : α
hx : ¬x ∈ s
⊢ piecewise s f g x ≤ piecewise s f' g' x
[PROOFSTEP]
simp [hx, *]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
inst✝ : DecidableEq α
s t : Finset α
⊢ Decidable (s ⊂ t)
[PROOFSTEP]
rw [ssubset_iff_subset_ne]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
inst✝ : DecidableEq α
s t : Finset α
⊢ Decidable (s ⊆ t ∧ s ≠ t)
[PROOFSTEP]
have h₁ : Decidable (s ⊆ t) := decidableSubsetFinset
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
inst✝ : DecidableEq α
s t : Finset α
h₁ : Decidable (s ⊆ t)
⊢ Decidable (s ⊆ t ∧ s ≠ t)
[PROOFSTEP]
have h₂ : Decidable (s ≠ t) := instDecidableNot
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ : Finset α
inst✝ : DecidableEq α
s t : Finset α
h₁ : Decidable (s ⊆ t)
h₂ : Decidable (s ≠ t)
⊢ Decidable (s ⊆ t ∧ s ≠ t)
[PROOFSTEP]
exact instDecidableAnd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
p : α → Prop
_hp : (a : α) → Decidable (p a)
⊢ (∃ a x, p a) ↔ ∃ a, a ∈ s ∧ p a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
a : α
⊢ a ∈ filter q (filter p s) ↔ a ∈ filter (fun a => p a ∧ q a) s
[PROOFSTEP]
simp only [mem_filter, and_assoc, Bool.decide_and, Bool.decide_coe, Bool.and_eq_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ filter (fun x => True) s = s
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
a✝ : α
⊢ a✝ ∈ filter (fun x => True) s ↔ a✝ ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
a : α
⊢ a ∈ filter (fun x => False) s ↔ a ∈ ∅
[PROOFSTEP]
simp [mem_filter, and_false_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ filter p s = s ↔ ∀ (x : α), x ∈ s → p x
[PROOFSTEP]
simp [Finset.ext_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
h : ∀ (x : α), x ∈ s → ¬p x
⊢ ∀ (x : α), ¬x ∈ filter p s
[PROOFSTEP]
simpa only [eq_empty_iff_forall_not_mem, mem_filter, not_and] using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ filter p s = ∅ ↔ ∀ (x : α), x ∈ s → ¬p x
[PROOFSTEP]
refine' ⟨_, filter_false_of_mem⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ filter p s = ∅ → ∀ (x : α), x ∈ s → ¬p x
[PROOFSTEP]
intro hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
hs : filter p s = ∅
⊢ ∀ (x : α), x ∈ s → ¬p x
[PROOFSTEP]
injection hs with hs'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
hs' : Multiset.filter p s.val = 0
⊢ ∀ (x : α), x ∈ s → ¬p x
[PROOFSTEP]
rwa [filter_eq_nil] at hs' 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Finset α
⊢ Finset.Nonempty (filter p s) ↔ ∃ a, a ∈ s ∧ p a
[PROOFSTEP]
simp [nonempty_iff_ne_empty, Ne.def, filter_eq_empty_iff, not_not, not_forall]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
⊢ filter p {a} = if p a then {a} else ∅
[PROOFSTEP]
classical
ext x
simp
split_ifs with h <;> by_cases h' : x = a <;> simp [h, h']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
⊢ filter p {a} = if p a then {a} else ∅
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a x : α
⊢ x ∈ filter p {a} ↔ x ∈ if p a then {a} else ∅
[PROOFSTEP]
simp
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a x : α
⊢ x = a ∧ p x ↔ x ∈ if p a then {a} else ∅
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a x : α
h : p a
⊢ x = a ∧ p x ↔ x ∈ {a}
[PROOFSTEP]
by_cases h' : x = a
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a x : α
h : ¬p a
⊢ x = a ∧ p x ↔ x ∈ ∅
[PROOFSTEP]
by_cases h' : x = a
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a x : α
h : p a
h' : x = a
⊢ x = a ∧ p x ↔ x ∈ {a}
[PROOFSTEP]
simp [h, h']
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a x : α
h : p a
h' : ¬x = a
⊢ x = a ∧ p x ↔ x ∈ {a}
[PROOFSTEP]
simp [h, h']
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a x : α
h : ¬p a
h' : x = a
⊢ x = a ∧ p x ↔ x ∈ ∅
[PROOFSTEP]
simp [h, h']
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a x : α
h : ¬p a
h' : ¬x = a
⊢ x = a ∧ p x ↔ x ∈ ∅
[PROOFSTEP]
simp [h, h']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ q✝ : α → Prop
inst✝³ : DecidablePred p✝
inst✝² : DecidablePred q✝
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ _root_.Disjoint (filter p s) (filter q s) ↔ ∀ (x : α), x ∈ s → p x → ¬q x
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ q✝ : α → Prop
inst✝³ : DecidablePred p✝
inst✝² : DecidablePred q✝
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ _root_.Disjoint (filter p s) (filter q s) → ∀ (x : α), x ∈ s → p x → ¬q x
[PROOFSTEP]
simp (config := { contextual := true }) [disjoint_left]
[GOAL]
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ q✝ : α → Prop
inst✝³ : DecidablePred p✝
inst✝² : DecidablePred q✝
s : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ (∀ (x : α), x ∈ s → p x → ¬q x) → _root_.Disjoint (filter p s) (filter q s)
[PROOFSTEP]
simp (config := { contextual := true }) [disjoint_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ q✝ : α → Prop
inst✝³ : DecidablePred p✝
inst✝² : DecidablePred q✝
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : _root_.Disjoint p q
⊢ _root_.Disjoint (filter p s) (filter q t)
[PROOFSTEP]
simp_rw [disjoint_left, mem_filter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ q✝ : α → Prop
inst✝³ : DecidablePred p✝
inst✝² : DecidablePred q✝
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : _root_.Disjoint p q
⊢ ∀ ⦃a : α⦄, a ∈ s ∧ p a → ¬(a ∈ t ∧ q a)
[PROOFSTEP]
rintro a ⟨_, hp⟩ ⟨_, hq⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ q✝ : α → Prop
inst✝³ : DecidablePred p✝
inst✝² : DecidablePred q✝
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : _root_.Disjoint p q
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False
[PROOFSTEP]
rw [Pi.disjoint_iff] at h 
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ q✝ : α → Prop
inst✝³ : DecidablePred p✝
inst✝² : DecidablePred q✝
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (i : α), _root_.Disjoint (p i) (q i)
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False
[PROOFSTEP]
simpa [hp, hq] using h a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
⊢ _root_.Disjoint (if p a then {a} else ∅) (filter p s)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
h✝ : p a
⊢ _root_.Disjoint {a} (filter p s)
[PROOFSTEP]
rw [disjoint_singleton_left]
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
h✝ : p a
⊢ ¬a ∈ filter p s
[PROOFSTEP]
exact mem_filter.not.mpr <| mt And.left ha
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
h✝ : ¬p a
⊢ _root_.Disjoint ∅ (filter p s)
[PROOFSTEP]
exact disjoint_empty_left _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
⊢ filter p (cons a s ha) =
    disjUnion (if p a then {a} else ∅) (filter p s) (_ : _root_.Disjoint (if p a then {a} else ∅) (filter p s))
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
h : p a
⊢ filter p (cons a s ha) = disjUnion {a} (filter p s) (_ : _root_.Disjoint {a} (filter p s))
[PROOFSTEP]
rw [filter_cons_of_pos _ _ _ ha h, singleton_disjUnion]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
a : α
s : Finset α
ha : ¬a ∈ s
h : ¬p a
⊢ filter p (cons a s ha) = disjUnion ∅ (filter p s) (_ : _root_.Disjoint ∅ (filter p s))
[PROOFSTEP]
rw [filter_cons_of_neg _ _ _ ha h, empty_disjUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x✝ : α
⊢ x✝ ∈ filter p (s₁ ∪ s₂) ↔ x✝ ∈ filter p s₁ ∪ filter p s₂
[PROOFSTEP]
simp only [mem_filter, mem_union, or_and_right]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
x : α
⊢ x ∈ filter p s ∪ filter q s ↔ x ∈ filter (fun x => p x ∨ q x) s
[PROOFSTEP]
simp [mem_filter, mem_union, ← and_or_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
s t : Finset α
inst✝ : (i : α) → Decidable (i ∈ t)
i : α
⊢ i ∈ filter (fun i => i ∈ t) s ↔ i ∈ s ∩ t
[PROOFSTEP]
simp [mem_filter, mem_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s t : Finset α
⊢ filter p (s ∩ t) = filter p s ∩ filter p t
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ a✝ ∈ filter p (s ∩ t) ↔ a✝ ∈ filter p s ∩ filter p t
[PROOFSTEP]
simp [mem_filter, mem_inter, and_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s t : Finset α
⊢ filter p s ∩ t = filter p (s ∩ t)
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ a✝ ∈ filter p s ∩ t ↔ a✝ ∈ filter p (s ∩ t)
[PROOFSTEP]
simp only [mem_inter, mem_filter, and_right_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s t : Finset α
⊢ s ∩ filter p t = filter p (s ∩ t)
[PROOFSTEP]
rw [inter_comm, filter_inter, inter_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ filter p (insert a s) = if p a then insert a (filter p s) else filter p s
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
⊢ x ∈ filter p (insert a s) ↔ x ∈ if p a then insert a (filter p s) else filter p s
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
h : p a
⊢ x ∈ filter p (insert a s) ↔ x ∈ insert a (filter p s)
[PROOFSTEP]
by_cases h' : x = a
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
h : ¬p a
⊢ x ∈ filter p (insert a s) ↔ x ∈ filter p s
[PROOFSTEP]
by_cases h' : x = a
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
h : p a
h' : x = a
⊢ x ∈ filter p (insert a s) ↔ x ∈ insert a (filter p s)
[PROOFSTEP]
simp [h, h']
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
h : p a
h' : ¬x = a
⊢ x ∈ filter p (insert a s) ↔ x ∈ insert a (filter p s)
[PROOFSTEP]
simp [h, h']
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
h : ¬p a
h' : x = a
⊢ x ∈ filter p (insert a s) ↔ x ∈ filter p s
[PROOFSTEP]
simp [h, h']
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
h : ¬p a
h' : ¬x = a
⊢ x ∈ filter p (insert a s) ↔ x ∈ filter p s
[PROOFSTEP]
simp [h, h']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ filter p (erase s a) = erase (filter p s) a
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
⊢ x ∈ filter p (erase s a) ↔ x ∈ erase (filter p s) a
[PROOFSTEP]
simp only [and_assoc, mem_filter, iff_self_iff, mem_erase]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
x✝ : α
⊢ x✝ ∈ filter (fun a => p a ∨ q a) s ↔ x✝ ∈ filter p s ∪ filter q s
[PROOFSTEP]
simp [mem_filter, mem_union, and_or_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
x✝ : α
⊢ x✝ ∈ filter (fun a => p a ∧ q a) s ↔ x✝ ∈ filter p s ∩ filter q s
[PROOFSTEP]
simp [mem_filter, mem_inter, and_comm, and_left_comm, and_self_iff, and_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ a ∈ filter (fun a => ¬p a) s ↔ a ∈ s \ filter p s
[PROOFSTEP]
simp only [Bool.decide_coe, Bool.not_eq_true', mem_filter, and_comm, mem_sdiff, not_and_or, Bool.not_eq_true,
  and_or_left, and_not_self, or_false]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x✝ : α
⊢ x✝ ∈ s₁ \ s₂ ↔ x✝ ∈ filter (fun x => ¬x ∈ s₂) s₁
[PROOFSTEP]
simp [mem_sdiff, mem_filter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s₁ s₂ : Finset α
⊢ s₁ \ s₂ = s₁ ↔ s₁ ∩ s₂ ⊆ ∅
[PROOFSTEP]
simp [Subset.antisymm_iff, disjoint_iff_inter_eq_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ∃ s₁ s₂, s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁
[PROOFSTEP]
classical
refine' ⟨s.filter (· ∈ t₁), s.filter (· ∉ t₁), _, _, _⟩
· simp [filter_union_right, em]
· intro x
  simp
· intro x
  simp
  intro hx hx₂
  refine' ⟨Or.resolve_left (h hx) hx₂, hx₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ∃ s₁ s₂, s₁ ∪ s₂ = s ∧ ↑s₁ ⊆ t₁ ∧ ↑s₂ ⊆ t₂ \ t₁
[PROOFSTEP]
refine' ⟨s.filter (· ∈ t₁), s.filter (· ∉ t₁), _, _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ filter (fun x => x ∈ t₁) s ∪ filter (fun x => ¬x ∈ t₁) s = s
[PROOFSTEP]
simp [filter_union_right, em]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x => x ∈ t₁) s) ⊆ t₁
[PROOFSTEP]
intro x
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ ↑(filter (fun x => x ∈ t₁) s) → x ∈ t₁
[PROOFSTEP]
simp
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x => ¬x ∈ t₁) s) ⊆ t₂ \ t₁
[PROOFSTEP]
intro x
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ ↑(filter (fun x => ¬x ∈ t₁) s) → x ∈ t₂ \ t₁
[PROOFSTEP]
simp
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
⊢ x ∈ s → ¬x ∈ t₁ → x ∈ t₂ ∧ ¬x ∈ t₁
[PROOFSTEP]
intro hx hx₂
[GOAL]
case refine'_3
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
x : α
hx : x ∈ s
hx₂ : ¬x ∈ t₁
⊢ x ∈ t₂ ∧ ¬x ∈ t₁
[PROOFSTEP]
refine' ⟨Or.resolve_left (h hx) hx₂, hx₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
⊢ filter (Eq b) s = if b ∈ s then {b} else ∅
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
⊢ filter (Eq b) s = {b}
[PROOFSTEP]
ext
[GOAL]
case pos.a
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
a✝ : β
⊢ a✝ ∈ filter (Eq b) s ↔ a✝ ∈ {b}
[PROOFSTEP]
simp only [mem_filter, mem_singleton, decide_eq_true_eq]
[GOAL]
case pos.a
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
a✝ : β
⊢ a✝ ∈ s ∧ b = a✝ ↔ a✝ = b
[PROOFSTEP]
refine ⟨fun h => h.2.symm, ?_⟩
[GOAL]
case pos.a
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : b ∈ s
a✝ : β
⊢ a✝ = b → a✝ ∈ s ∧ b = a✝
[PROOFSTEP]
rintro rfl
[GOAL]
case pos.a
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
a✝ : β
h : a✝ ∈ s
⊢ a✝ ∈ s ∧ a✝ = a✝
[PROOFSTEP]
exact ⟨h, rfl⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : ¬b ∈ s
⊢ filter (Eq b) s = ∅
[PROOFSTEP]
ext
[GOAL]
case neg.a
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : ¬b ∈ s
a✝ : β
⊢ a✝ ∈ filter (Eq b) s ↔ a✝ ∈ ∅
[PROOFSTEP]
simp only [mem_filter, not_and, iff_false_iff, not_mem_empty, decide_eq_true_eq]
[GOAL]
case neg.a
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : ¬b ∈ s
a✝ : β
⊢ a✝ ∈ s → ¬b = a✝
[PROOFSTEP]
rintro m rfl
[GOAL]
case neg.a
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
h : ¬b ∈ s
m : b ∈ s
⊢ False
[PROOFSTEP]
exact h m
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b x✝¹ : β
x✝ : x✝¹ ∈ s
⊢ x✝¹ = b ↔ b = x✝¹
[PROOFSTEP]
simp_rw [@eq_comm _ b]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b : β
⊢ filter (fun a => b ≠ a) s = erase s b
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b a✝ : β
⊢ a✝ ∈ filter (fun a => b ≠ a) s ↔ a✝ ∈ erase s b
[PROOFSTEP]
simp only [mem_filter, mem_erase, Ne.def, decide_not, Bool.not_eq_true', decide_eq_false_iff_not]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b a✝ : β
⊢ a✝ ∈ s ∧ ¬b = a✝ ↔ ¬a✝ = b ∧ a✝ ∈ s
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝³ : DecidablePred p
inst✝² : DecidablePred q
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset β
b x✝¹ : β
x✝ : x✝¹ ∈ s
⊢ x✝¹ ≠ b ↔ b ≠ x✝¹
[PROOFSTEP]
simp_rw [@ne_comm _ b]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : DecidableEq α
s t : Finset α
⊢ filter p s ∩ filter (fun a => ¬p a) t = ∅
[PROOFSTEP]
simpa using (disjoint_filter_filter_neg s t p).eq_bot
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n m l : ℕ
⊢ range n = ∅ ↔ n = 0
[PROOFSTEP]
rw [← not_nonempty_iff_eq_empty, nonempty_range_iff, not_not]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ m✝ l n m : ℕ
⊢ filter (fun x => x = m) (range n) = if m < n then {m} else ∅
[PROOFSTEP]
convert filter_eq (range n) m using 2
[GOAL]
case h.e'_2.h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ m✝ l n m : ℕ
⊢ (fun x => x = m) = Eq m
[PROOFSTEP]
ext
[GOAL]
case h.e'_2.h.e'_2.h.a
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ m✝ l n m x✝ : ℕ
⊢ x✝ = m ↔ m = x✝
[PROOFSTEP]
rw [eq_comm]
[GOAL]
case h.e'_3.h₁.a
α : Type u_1
β : Type u_2
γ : Type u_3
n✝ m✝ l n m : ℕ
⊢ m < n ↔ m ∈ range n
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
⊢ (∃ x, x ∈ ∅ ∧ p x) ↔ False
[PROOFSTEP]
simp only [not_mem_empty, false_and_iff, exists_false]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s : Finset α
p : α → Prop
⊢ (∃ x, x ∈ insert a s ∧ p x) ↔ p a ∨ ∃ x, x ∈ s ∧ p x
[PROOFSTEP]
simp only [mem_insert, or_and_right, exists_or, exists_eq_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
a : α
s : Finset α
p : α → Prop
⊢ (∀ (x : α), x ∈ insert a s → p x) ↔ p a ∧ ∀ (x : α), x ∈ s → p x
[PROOFSTEP]
simp only [mem_insert, or_imp, forall_and, forall_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
k j : ℕ
⊢ ¬j + k ∈ range k
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
k : ℕ
j : { n // ¬n ∈ range k }
⊢ (fun j => { val := j + k, property := (_ : ¬j + k ∈ range k) }) ((fun i => ↑i - k) j) = j
[PROOFSTEP]
rw [Subtype.ext_iff_val]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
k : ℕ
j : { n // ¬n ∈ range k }
⊢ ↑((fun j => { val := j + k, property := (_ : ¬j + k ∈ range k) }) ((fun i => ↑i - k) j)) = ↑j
[PROOFSTEP]
apply tsub_add_cancel_of_le
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
k : ℕ
j : { n // ¬n ∈ range k }
⊢ k ≤ ↑j
[PROOFSTEP]
simpa using j.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
k j : ℕ
⊢ ¬j + k ∈ range k
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t l l' : Multiset α
hl : Nodup l
hl' : Nodup l'
h : toFinset l = toFinset l'
⊢ l = l'
[PROOFSTEP]
simpa [← toFinset_eq hl, ← toFinset_eq hl'] using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ toFinset {a} = {a}
[PROOFSTEP]
rw [← cons_zero, toFinset_cons, toFinset_zero, IsLawfulSingleton.insert_emptyc_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ s t : Multiset α
⊢ ∀ (a : α), a ∈ toFinset (s + t) ↔ a ∈ toFinset s ∪ toFinset t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t s : Multiset α
h : 0 ≠ 0
⊢ toFinset (0 • s) = toFinset s
[PROOFSTEP]
contradiction
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
⊢ toFinset ((n + 1) • s) = toFinset s
[PROOFSTEP]
by_cases h : n = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : n = 0
⊢ toFinset ((n + 1) • s) = toFinset s
[PROOFSTEP]
rw [h, zero_add, one_nsmul]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t s : Multiset α
n : ℕ
x✝ : n + 1 ≠ 0
h : ¬n = 0
⊢ toFinset ((n + 1) • s) = toFinset s
[PROOFSTEP]
rw [add_nsmul, toFinset_add, one_nsmul, toFinset_nsmul s n h, Finset.union_idempotent]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ s t : Multiset α
⊢ ∀ (a : α), a ∈ toFinset (s ∩ t) ↔ a ∈ toFinset s ∩ toFinset t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ s t : Multiset α
⊢ toFinset (s ∪ t) = toFinset s ∪ toFinset t
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s✝ t✝ s t : Multiset α
a✝ : α
⊢ a✝ ∈ toFinset (s ∪ t) ↔ a✝ ∈ toFinset s ∪ toFinset t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Multiset α
⊢ Finset.Nonempty (toFinset s) ↔ s ≠ 0
[PROOFSTEP]
simp only [toFinset_eq_empty, Ne.def, Finset.nonempty_iff_ne_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Multiset α
⊢ toFinset s ⊆ toFinset t ↔ s ⊆ t
[PROOFSTEP]
simp only [Finset.subset_iff, Multiset.subset_iff, Multiset.mem_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Multiset α
⊢ toFinset s ⊂ toFinset t ↔ s ⊂ t
[PROOFSTEP]
simp_rw [Finset.ssubset_def, toFinset_subset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ⊆ t ∧ ¬t ⊆ s ↔ s ⊂ t
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t m : Multiset α
⊢ toFinset (dedup m) = toFinset m
[PROOFSTEP]
simp_rw [toFinset, dedup_idempotent]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq α
s t : Multiset α
inst✝ : DecidableEq β
m : Multiset α
f : α → Multiset β
⊢ toFinset (bind (dedup m) f) = toFinset (bind m f)
[PROOFSTEP]
simp_rw [toFinset, dedup_bind_dedup]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Multiset α
⊢ IsWellFounded (Multiset β) fun x x_1 => x ⊂ x_1
[PROOFSTEP]
classical exact Subrelation.isWellFounded (InvImage _ toFinset) toFinset_ssubset.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Multiset α
⊢ IsWellFounded (Multiset β) fun x x_1 => x ⊂ x_1
[PROOFSTEP]
exact Subrelation.isWellFounded (InvImage _ toFinset) toFinset_ssubset.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
⊢ toFinset s.val = s
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
a✝ : α
⊢ a✝ ∈ toFinset s.val ↔ a✝ ∈ s
[PROOFSTEP]
rw [Multiset.mem_toFinset, ← mem_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l l' : List α
a : α
n : Nodup l
⊢ Multiset.Nodup ↑l
[PROOFSTEP]
rwa [Multiset.coe_nodup]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l l' : List α
a : α
⊢ (toFinset (a :: l)).val = (insert a (toFinset l)).val
[PROOFSTEP]
by_cases h : a ∈ l
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l l' : List α
a : α
h : a ∈ l
⊢ (toFinset (a :: l)).val = (insert a (toFinset l)).val
[PROOFSTEP]
simp [Finset.insert_val', Multiset.dedup_cons, h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l l' : List α
a : α
h : ¬a ∈ l
⊢ (toFinset (a :: l)).val = (insert a (toFinset l)).val
[PROOFSTEP]
simp [Finset.insert_val', Multiset.dedup_cons, h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l l' : List α
a : α
⊢ Set.SurjOn toFinset {l | Nodup l} Set.univ
[PROOFSTEP]
rintro ⟨⟨l⟩, hl⟩ _
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l✝ l' : List α
a : α
val✝ : Multiset α
l : List α
hl : Multiset.Nodup (Quot.mk Setoid.r l)
a✝ : { val := Quot.mk Setoid.r l, nodup := hl } ∈ Set.univ
⊢ { val := Quot.mk Setoid.r l, nodup := hl } ∈ toFinset '' {l | Nodup l}
[PROOFSTEP]
exact ⟨l, hl, (toFinset_eq hl).symm⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l l' : List α
a : α
⊢ toFinset l = toFinset l' ↔ dedup l ~ dedup l'
[PROOFSTEP]
simp [Finset.ext_iff, perm_ext (nodup_dedup _) (nodup_dedup _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l l' : List α
a✝ : α
a b : List α
⊢ toFinset a = toFinset b ↔ ∀ (x : α), x ∈ a ↔ x ∈ b
[PROOFSTEP]
simp only [Finset.ext_iff, mem_toFinset]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l l' : List α
a : α
hl : Nodup l
hl' : Nodup l'
h : toFinset l = toFinset l'
⊢ l ~ l'
[PROOFSTEP]
rw [← Multiset.coe_eq_coe]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l l' : List α
a : α
hl : Nodup l
hl' : Nodup l'
h : toFinset l = toFinset l'
⊢ ↑l = ↑l'
[PROOFSTEP]
exact Multiset.Nodup.toFinset_inj hl hl' h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l l' : List α
a : α
⊢ toFinset (l ++ l') = toFinset l ∪ toFinset l'
[PROOFSTEP]
induction' l with hd tl hl
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l l' : List α
a : α
⊢ toFinset ([] ++ l') = toFinset [] ∪ toFinset l'
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l l' : List α
a hd : α
tl : List α
hl : toFinset (tl ++ l') = toFinset tl ∪ toFinset l'
⊢ toFinset (hd :: tl ++ l') = toFinset (hd :: tl) ∪ toFinset l'
[PROOFSTEP]
simp [hl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l l' : List α
a : α
n : ℕ
hn : n ≠ 0
⊢ toFinset (replicate n a) = {a}
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l l' : List α
a : α
n : ℕ
hn : n ≠ 0
x : α
⊢ x ∈ toFinset (replicate n a) ↔ x ∈ {a}
[PROOFSTEP]
simp [hn, List.mem_replicate]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l✝ l'✝ : List α
a : α
l l' : List α
⊢ toFinset (l ∪ l') = toFinset l ∪ toFinset l'
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l✝ l'✝ : List α
a : α
l l' : List α
a✝ : α
⊢ a✝ ∈ toFinset (l ∪ l') ↔ a✝ ∈ toFinset l ∪ toFinset l'
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l✝ l'✝ : List α
a : α
l l' : List α
⊢ toFinset (l ∩ l') = toFinset l ∩ toFinset l'
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l✝ l'✝ : List α
a : α
l l' : List α
a✝ : α
⊢ a✝ ∈ toFinset (l ∩ l') ↔ a✝ ∈ toFinset l ∩ toFinset l'
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l✝ l' : List α
a : α
l : List α
⊢ toFinset l = ∅ ↔ l = []
[PROOFSTEP]
cases l
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l l' : List α
a : α
⊢ toFinset [] = ∅ ↔ [] = []
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l l' : List α
a head✝ : α
tail✝ : List α
⊢ toFinset (head✝ :: tail✝) = ∅ ↔ head✝ :: tail✝ = []
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
l✝ l' : List α
a : α
l : List α
⊢ Finset.Nonempty (toFinset l) ↔ l ≠ []
[PROOFSTEP]
simp [Finset.nonempty_iff_ne_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
⊢ List.Nodup (toList s)
[PROOFSTEP]
rw [toList, ← Multiset.coe_nodup, Multiset.coe_toList]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
⊢ Nodup s.val
[PROOFSTEP]
exact s.nodup
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
⊢ List.toFinset (toList s) = s
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s : Finset α
a✝ : α
⊢ a✝ ∈ List.toFinset (toList s) ↔ a✝ ∈ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s : Finset α
⊢ toList s = [a] ↔ s = {a}
[PROOFSTEP]
rw [toList, Multiset.toList_eq_singleton_iff, val_eq_singleton_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s : Finset α
h : ¬a ∈ s
⊢ List.Nodup (a :: toList s)
[PROOFSTEP]
simp [h, nodup_toList s]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
s : Finset α
h : ¬a ∈ s
x : α
⊢ x ∈ toList (cons a s h) ↔ x ∈ a :: toList s
[PROOFSTEP]
simp only [List.mem_cons, Finset.mem_toList, Finset.mem_cons]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t✝ t₁ t₂ t : α → Finset β
⊢ Set.PairwiseDisjoint (↑∅) t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
b : β
h : Set.PairwiseDisjoint (↑s) t
⊢ b ∈ disjiUnion s t h ↔ ∃ a, a ∈ s ∧ b ∈ t a
[PROOFSTEP]
simp only [mem_def, disjiUnion_val, mem_bind, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
h : Set.PairwiseDisjoint (↑s) t
⊢ ↑(disjiUnion s t h) = ⋃ (x : α) (_ : x ∈ ↑s), ↑(t x)
[PROOFSTEP]
simp [Set.ext_iff, mem_disjiUnion, Set.mem_iUnion, iff_self_iff, mem_coe, imp_true_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : Set.PairwiseDisjoint (↑s) f
h2 : Set.PairwiseDisjoint (↑(disjiUnion s f h1)) g
a : { x // x ∈ s }
x✝¹ : a ∈ ↑(attach s)
b : { x // x ∈ s }
x✝ : b ∈ ↑(attach s)
hab : a ≠ b
x : γ
hxa :
  x ∈
    (fun a =>
        disjiUnion (f ↑a) g (_ : ∀ (b : β), b ∈ ↑(f ↑a) → ∀ (c : β), c ∈ ↑(f ↑a) → b ≠ c → (_root_.Disjoint on g) b c))
      a
hxb :
  x ∈
    (fun a =>
        disjiUnion (f ↑a) g (_ : ∀ (b : β), b ∈ ↑(f ↑a) → ∀ (c : β), c ∈ ↑(f ↑a) → b ≠ c → (_root_.Disjoint on g) b c))
      b
⊢ False
[PROOFSTEP]
obtain ⟨xa, hfa, hga⟩ := mem_disjiUnion.mp hxa
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : Set.PairwiseDisjoint (↑s) f
h2 : Set.PairwiseDisjoint (↑(disjiUnion s f h1)) g
a : { x // x ∈ s }
x✝¹ : a ∈ ↑(attach s)
b : { x // x ∈ s }
x✝ : b ∈ ↑(attach s)
hab : a ≠ b
x : γ
hxa :
  x ∈
    (fun a =>
        disjiUnion (f ↑a) g (_ : ∀ (b : β), b ∈ ↑(f ↑a) → ∀ (c : β), c ∈ ↑(f ↑a) → b ≠ c → (_root_.Disjoint on g) b c))
      a
hxb :
  x ∈
    (fun a =>
        disjiUnion (f ↑a) g (_ : ∀ (b : β), b ∈ ↑(f ↑a) → ∀ (c : β), c ∈ ↑(f ↑a) → b ≠ c → (_root_.Disjoint on g) b c))
      b
xa : β
hfa : xa ∈ f ↑a
hga : x ∈ g xa
⊢ False
[PROOFSTEP]
obtain ⟨xb, hfb, hgb⟩ := mem_disjiUnion.mp hxb
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : Set.PairwiseDisjoint (↑s) f
h2 : Set.PairwiseDisjoint (↑(disjiUnion s f h1)) g
a : { x // x ∈ s }
x✝¹ : a ∈ ↑(attach s)
b : { x // x ∈ s }
x✝ : b ∈ ↑(attach s)
hab : a ≠ b
x : γ
hxa :
  x ∈
    (fun a =>
        disjiUnion (f ↑a) g (_ : ∀ (b : β), b ∈ ↑(f ↑a) → ∀ (c : β), c ∈ ↑(f ↑a) → b ≠ c → (_root_.Disjoint on g) b c))
      a
hxb :
  x ∈
    (fun a =>
        disjiUnion (f ↑a) g (_ : ∀ (b : β), b ∈ ↑(f ↑a) → ∀ (c : β), c ∈ ↑(f ↑a) → b ≠ c → (_root_.Disjoint on g) b c))
      b
xa : β
hfa : xa ∈ f ↑a
hga : x ∈ g xa
xb : β
hfb : xb ∈ f ↑b
hgb : x ∈ g xb
⊢ False
[PROOFSTEP]
refine' disjoint_left.mp (h2 (mem_disjiUnion.mpr ⟨_, a.prop, hfa⟩) (mem_disjiUnion.mpr ⟨_, b.prop, hfb⟩) _) hga hgb
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : Set.PairwiseDisjoint (↑s) f
h2 : Set.PairwiseDisjoint (↑(disjiUnion s f h1)) g
a : { x // x ∈ s }
x✝¹ : a ∈ ↑(attach s)
b : { x // x ∈ s }
x✝ : b ∈ ↑(attach s)
hab : a ≠ b
x : γ
hxa :
  x ∈
    (fun a =>
        disjiUnion (f ↑a) g (_ : ∀ (b : β), b ∈ ↑(f ↑a) → ∀ (c : β), c ∈ ↑(f ↑a) → b ≠ c → (_root_.Disjoint on g) b c))
      a
hxb :
  x ∈
    (fun a =>
        disjiUnion (f ↑a) g (_ : ∀ (b : β), b ∈ ↑(f ↑a) → ∀ (c : β), c ∈ ↑(f ↑a) → b ≠ c → (_root_.Disjoint on g) b c))
      b
xa : β
hfa : xa ∈ f ↑a
hga : x ∈ g xa
xb : β
hfb : xb ∈ f ↑b
hgb : x ∈ g xb
⊢ xa ≠ xb
[PROOFSTEP]
rintro rfl
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
g : β → Finset γ
h1 : Set.PairwiseDisjoint (↑s) f
h2 : Set.PairwiseDisjoint (↑(disjiUnion s f h1)) g
a : { x // x ∈ s }
x✝¹ : a ∈ ↑(attach s)
b : { x // x ∈ s }
x✝ : b ∈ ↑(attach s)
hab : a ≠ b
x : γ
hxa :
  x ∈
    (fun a =>
        disjiUnion (f ↑a) g (_ : ∀ (b : β), b ∈ ↑(f ↑a) → ∀ (c : β), c ∈ ↑(f ↑a) → b ≠ c → (_root_.Disjoint on g) b c))
      a
hxb :
  x ∈
    (fun a =>
        disjiUnion (f ↑a) g (_ : ∀ (b : β), b ∈ ↑(f ↑a) → ∀ (c : β), c ∈ ↑(f ↑a) → b ≠ c → (_root_.Disjoint on g) b c))
      b
xa : β
hfa : xa ∈ f ↑a
hga : x ∈ g xa
hfb : xa ∈ f ↑b
hgb : x ∈ g xa
⊢ False
[PROOFSTEP]
exact disjoint_left.mp (h1 a.prop b.prop <| Subtype.coe_injective.ne hab) hfa hfb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
h : ∀ (x : α), x ∈ s → f x ∈ t
x' : β
hx : x' ∈ ↑t
y' : β
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ (_root_.Disjoint on fun a => filter (fun c => f c = a) s) x' y'
[PROOFSTEP]
simp_rw [disjoint_left, mem_filter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
h : ∀ (x : α), x ∈ s → f x ∈ t
x' : β
hx : x' ∈ ↑t
y' : β
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ ∀ ⦃a : α⦄, a ∈ s ∧ f a = x' → ¬(a ∈ s ∧ f a = y')
[PROOFSTEP]
rintro i ⟨_, rfl⟩ ⟨_, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
h : ∀ (x : α), x ∈ s → f x ∈ t
i : α
left✝¹ : i ∈ s
hx : f i ∈ ↑t
left✝ : i ∈ s
hy : f i ∈ ↑t
hne : f i ≠ f i
⊢ False
[PROOFSTEP]
exact hne rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
h : ∀ (x : α), x ∈ s → f x ∈ t
b : α
⊢ b ∈
      disjiUnion t (fun a => filter (fun c => f c = a) s)
        (_ :
          ∀ (x' : β),
            x' ∈ ↑t → ∀ (y' : β), y' ∈ ↑t → x' ≠ y' → (_root_.Disjoint on fun a => filter (fun c => f c = a) s) x' y') ↔
    b ∈ s
[PROOFSTEP]
simpa using h b
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
b : β
⊢ b ∈ Finset.biUnion s t ↔ ∃ a, a ∈ s ∧ b ∈ t a
[PROOFSTEP]
simp only [mem_def, biUnion_val, mem_dedup, mem_bind, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
⊢ ↑(Finset.biUnion s t) = ⋃ (x : α) (_ : x ∈ ↑s), ↑(t x)
[PROOFSTEP]
simp [Set.ext_iff, mem_biUnion, Set.mem_iUnion, iff_self_iff, mem_coe, imp_true_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
inst✝ : DecidableEq α
a : α
x : β
⊢ x ∈ Finset.biUnion (insert a s) t ↔ x ∈ t a ∪ Finset.biUnion s t
[PROOFSTEP]
simp only [mem_biUnion, exists_prop, mem_union, mem_insert, or_and_right, exists_or, exists_eq_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
hs : s₁ = s₂
ht : ∀ (a : α), a ∈ s₁ → t₁ a = t₂ a
x : β
⊢ x ∈ Finset.biUnion s₁ t₁ ↔ x ∈ Finset.biUnion s₂ t₂
[PROOFSTEP]
simp_rw [mem_biUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
hs : s₁ = s₂
ht : ∀ (a : α), a ∈ s₁ → t₁ a = t₂ a
x : β
⊢ (∃ a, a ∈ s₁ ∧ x ∈ t₁ a) ↔ ∃ a, a ∈ s₂ ∧ x ∈ t₂ a
[PROOFSTEP]
apply exists_congr
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
hs : s₁ = s₂
ht : ∀ (a : α), a ∈ s₁ → t₁ a = t₂ a
x : β
⊢ ∀ (a : α), a ∈ s₁ ∧ x ∈ t₁ a ↔ a ∈ s₂ ∧ x ∈ t₂ a
[PROOFSTEP]
simp (config := { contextual := true }) only [hs, and_congr_right_iff, ht, implies_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s' : Finset β
⊢ Finset.biUnion s t ⊆ s' ↔ ∀ (x : α), x ∈ s → t x ⊆ s'
[PROOFSTEP]
simp only [subset_iff, mem_biUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s' : Finset β
⊢ (∀ ⦃x : β⦄, (∃ a, a ∈ s ∧ x ∈ t a) → x ∈ s') ↔ ∀ (x : α), x ∈ s → ∀ ⦃x_1 : β⦄, x_1 ∈ t x → x_1 ∈ s'
[PROOFSTEP]
exact ⟨fun H a ha b hb => H ⟨a, ha, hb⟩, fun H b ⟨a, ha, hb⟩ => H a ha hb⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
a : α
⊢ Finset.biUnion {a} t = t a
[PROOFSTEP]
classical rw [← insert_emptyc_eq, biUnion_insert, biUnion_empty, union_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
a : α
⊢ Finset.biUnion {a} t = t a
[PROOFSTEP]
rw [← insert_emptyc_eq, biUnion_insert, biUnion_empty, union_empty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
t : Finset β
⊢ Finset.biUnion s f ∩ t = Finset.biUnion s fun x => f x ∩ t
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
t : Finset β
x : β
⊢ x ∈ Finset.biUnion s f ∩ t ↔ x ∈ Finset.biUnion s fun x => f x ∩ t
[PROOFSTEP]
simp only [mem_biUnion, mem_inter]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
t : Finset β
x : β
⊢ (∃ a, a ∈ s ∧ x ∈ f a) ∧ x ∈ t ↔ ∃ a, a ∈ s ∧ x ∈ f a ∧ x ∈ t
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
t : Finset β
s : Finset α
f : α → Finset β
⊢ t ∩ Finset.biUnion s f = Finset.biUnion s fun x => t ∩ f x
[PROOFSTEP]
rw [inter_comm, biUnion_inter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
t : Finset β
s : Finset α
f : α → Finset β
⊢ (Finset.biUnion s fun x => f x ∩ t) = Finset.biUnion s fun x => t ∩ f x
[PROOFSTEP]
simp [inter_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
⊢ Finset.biUnion (Finset.biUnion s f) g = Finset.biUnion s fun a => Finset.biUnion (f a) g
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
a✝ : γ
⊢ a✝ ∈ Finset.biUnion (Finset.biUnion s f) g ↔ a✝ ∈ Finset.biUnion s fun a => Finset.biUnion (f a) g
[PROOFSTEP]
simp only [Finset.mem_biUnion, exists_prop]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
a✝ : γ
⊢ (∃ a, (∃ a_1, a_1 ∈ s ∧ a ∈ f a_1) ∧ a✝ ∈ g a) ↔ ∃ a, a ∈ s ∧ ∃ a_1, a_1 ∈ f a ∧ a✝ ∈ g a_1
[PROOFSTEP]
simp_rw [← exists_and_right, ← exists_and_left, and_assoc]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
inst✝ : DecidableEq γ
s : Finset α
f : α → Finset β
g : β → Finset γ
a✝ : γ
⊢ (∃ a x, x ∈ s ∧ a ∈ f x ∧ a✝ ∈ g a) ↔ ∃ a x, a ∈ s ∧ x ∈ f a ∧ a✝ ∈ g x
[PROOFSTEP]
rw [exists_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
inst✝ : DecidableEq α
s : Multiset α
t : α → Multiset β
x : β
⊢ x ∈ toFinset (Multiset.bind s t) ↔ x ∈ Finset.biUnion (toFinset s) fun a => toFinset (t a)
[PROOFSTEP]
simp only [Multiset.mem_toFinset, mem_biUnion, Multiset.mem_bind, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
h : ∀ (a : α), a ∈ s → t₁ a ⊆ t₂ a
⊢ Finset.biUnion s t₁ ⊆ Finset.biUnion s t₂
[PROOFSTEP]
have : ∀ b a, a ∈ s → b ∈ t₁ a → ∃ a : α, a ∈ s ∧ b ∈ t₂ a := fun b a ha hb => ⟨a, ha, Finset.mem_of_subset (h a ha) hb⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
h : ∀ (a : α), a ∈ s → t₁ a ⊆ t₂ a
this : ∀ (b : β) (a : α), a ∈ s → b ∈ t₁ a → ∃ a, a ∈ s ∧ b ∈ t₂ a
⊢ Finset.biUnion s t₁ ⊆ Finset.biUnion s t₂
[PROOFSTEP]
simpa only [subset_iff, mem_biUnion, exists_imp, and_imp, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t✝ t₁ t₂ t : α → Finset β
h : s₁ ⊆ s₂
⊢ Finset.biUnion s₁ t ⊆ Finset.biUnion s₂ t
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t✝ t₁ t₂ t : α → Finset β
h : s₁ ⊆ s₂
x : β
⊢ x ∈ Finset.biUnion s₁ t → x ∈ Finset.biUnion s₂ t
[PROOFSTEP]
simp only [and_imp, mem_biUnion, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t✝ t₁ t₂ t : α → Finset β
h : s₁ ⊆ s₂
x : β
⊢ (∃ a, a ∈ s₁ ∧ x ∈ t a) → ∃ a, a ∈ s₂ ∧ x ∈ t a
[PROOFSTEP]
exact Exists.imp fun a ha => ⟨h ha.1, ha.2⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
inst✝ : DecidableEq α
x : α
⊢ x ∈ Finset.biUnion s singleton ↔ x ∈ s
[PROOFSTEP]
simp only [mem_biUnion, mem_singleton, exists_prop, exists_eq_right']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
⊢ filter p (Finset.biUnion s f) = Finset.biUnion s fun a => filter p (f a)
[PROOFSTEP]
ext b
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ b ∈ filter p (Finset.biUnion s f) ↔ b ∈ Finset.biUnion s fun a => filter p (f a)
[PROOFSTEP]
simp only [mem_biUnion, exists_prop, mem_filter]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a, a ∈ s ∧ b ∈ f a) ∧ p b ↔ ∃ a, a ∈ s ∧ b ∈ f a ∧ p b
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a, a ∈ s ∧ b ∈ f a) ∧ p b → ∃ a, a ∈ s ∧ b ∈ f a ∧ p b
[PROOFSTEP]
rintro ⟨⟨a, ha, hba⟩, hb⟩
[GOAL]
case a.mp.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
hb : p b
a : α
ha : a ∈ s
hba : b ∈ f a
⊢ ∃ a, a ∈ s ∧ b ∈ f a ∧ p b
[PROOFSTEP]
exact ⟨a, ha, hba, hb⟩
[GOAL]
case a.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a, a ∈ s ∧ b ∈ f a ∧ p b) → (∃ a, a ∈ s ∧ b ∈ f a) ∧ p b
[PROOFSTEP]
rintro ⟨a, ha, hba, hb⟩
[GOAL]
case a.mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
a : α
ha : a ∈ s
hba : b ∈ f a
hb : p b
⊢ (∃ a, a ∈ s ∧ b ∈ f a) ∧ p b
[PROOFSTEP]
exact ⟨⟨a, ha, hba⟩, hb⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
inst✝ : DecidableEq α
s : Finset α
t : Finset β
f : α → β
h : ∀ (x : α), x ∈ s → f x ∈ t
⊢ (Finset.biUnion t fun a => filter (fun c => f c = a) s) = s
[PROOFSTEP]
simpa only [disjiUnion_eq_biUnion] using disjiUnion_filter_eq_of_maps_to h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ f : α → Finset β
s : Finset α
b : β
⊢ erase (Finset.biUnion s f) b = Finset.biUnion s fun x => erase (f x) b
[PROOFSTEP]
ext a
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ f : α → Finset β
s : Finset α
b a : β
⊢ a ∈ erase (Finset.biUnion s f) b ↔ a ∈ Finset.biUnion s fun x => erase (f x) b
[PROOFSTEP]
simp [Finset.mem_biUnion, iff_self_iff, exists_and_left, Finset.mem_erase]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t t₁ t₂ f : α → Finset β
s : Finset α
b a : β
⊢ (¬a = b ∧ ∃ a_1, a_1 ∈ s ∧ a ∈ f a_1) ↔ ∃ a_1, a_1 ∈ s ∧ ¬a = b ∧ a ∈ f a_1
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
⊢ Finset.Nonempty (Finset.biUnion s t) ↔ ∃ x, x ∈ s ∧ Finset.Nonempty (t x)
[PROOFSTEP]
simp only [Finset.Nonempty, mem_biUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
⊢ (∃ x a, a ∈ s ∧ x ∈ t a) ↔ ∃ x, x ∈ s ∧ ∃ x_1, x_1 ∈ t x
[PROOFSTEP]
rw [exists_swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
⊢ (∃ y x, y ∈ s ∧ x ∈ t y) ↔ ∃ x, x ∈ s ∧ ∃ x_1, x_1 ∈ t x
[PROOFSTEP]
simp [exists_and_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
t : Finset β
⊢ _root_.Disjoint (Finset.biUnion s f) t ↔ ∀ (i : α), i ∈ s → _root_.Disjoint (f i) t
[PROOFSTEP]
classical
refine' s.induction _ _
· simp only [forall_mem_empty_iff, biUnion_empty, disjoint_empty_left]
· intro i s his ih
  simp only [disjoint_union_left, biUnion_insert, his, forall_mem_insert, ih]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
t : Finset β
⊢ _root_.Disjoint (Finset.biUnion s f) t ↔ ∀ (i : α), i ∈ s → _root_.Disjoint (f i) t
[PROOFSTEP]
refine' s.induction _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
t : Finset β
⊢ _root_.Disjoint (Finset.biUnion ∅ f) t ↔ ∀ (i : α), i ∈ ∅ → _root_.Disjoint (f i) t
[PROOFSTEP]
simp only [forall_mem_empty_iff, biUnion_empty, disjoint_empty_left]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset α
f : α → Finset β
t : Finset β
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    ¬a ∈ s →
      (_root_.Disjoint (Finset.biUnion s f) t ↔ ∀ (i : α), i ∈ s → _root_.Disjoint (f i) t) →
        (_root_.Disjoint (Finset.biUnion (insert a s) f) t ↔ ∀ (i : α), i ∈ insert a s → _root_.Disjoint (f i) t)
[PROOFSTEP]
intro i s his ih
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s✝¹ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s✝ : Finset α
f : α → Finset β
t : Finset β
i : α
s : Finset α
his : ¬i ∈ s
ih : _root_.Disjoint (Finset.biUnion s f) t ↔ ∀ (i : α), i ∈ s → _root_.Disjoint (f i) t
⊢ _root_.Disjoint (Finset.biUnion (insert i s) f) t ↔ ∀ (i_1 : α), i_1 ∈ insert i s → _root_.Disjoint (f i_1) t
[PROOFSTEP]
simp only [disjoint_union_left, biUnion_insert, his, forall_mem_insert, ih]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq β
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
s : Finset β
t : Finset α
f : α → Finset β
⊢ _root_.Disjoint s (Finset.biUnion t f) ↔ ∀ (i : α), i ∈ t → _root_.Disjoint s (f i)
[PROOFSTEP]
simpa only [_root_.disjoint_comm] using disjoint_biUnion_left t f s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
a : α
ha : ¬a ∈ s
r : β → β → Prop
f : α → β
⊢ _root_.Pairwise (r on fun a_1 => f ↑a_1) ↔
    _root_.Pairwise (r on fun a => f ↑a) ∧ ∀ (b : α), b ∈ s → r (f a) (f b) ∧ r (f b) (f a)
[PROOFSTEP]
simp only [pairwise_subtype_iff_pairwise_finset', Finset.coe_cons, Set.pairwise_insert, Finset.mem_coe,
  and_congr_right_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
a : α
ha : ¬a ∈ s
r : β → β → Prop
f : α → β
⊢ Set.Pairwise (↑s) (r on f) →
    ((∀ (b : α), b ∈ s → a ≠ b → (r on f) a b ∧ (r on f) b a) ↔ ∀ (b : α), b ∈ s → r (f a) (f b) ∧ r (f b) (f a))
[PROOFSTEP]
exact fun _ =>
  ⟨fun h b hb =>
    h b hb <| by
      rintro rfl
      contradiction,
    fun h b hb _ => h b hb⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
a : α
ha : ¬a ∈ s
r : β → β → Prop
f : α → β
x✝ : Set.Pairwise (↑s) (r on f)
h : ∀ (b : α), b ∈ s → a ≠ b → (r on f) a b ∧ (r on f) b a
b : α
hb : b ∈ s
⊢ a ≠ b
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
a : α
ha : ¬a ∈ s
r : β → β → Prop
f : α → β
x✝ : Set.Pairwise (↑s) (r on f)
h : ∀ (b : α), b ∈ s → a ≠ b → (r on f) a b ∧ (r on f) b a
hb : a ∈ s
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
x : α
⊢ Option.elim' default val ((fun x => if h : x = default then none else some { val := x, property := h }) x) = x
[PROOFSTEP]
dsimp only
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
x : α
⊢ Option.elim' default val (if h : x = default then none else some { val := x, property := h }) = x
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
x : α
h✝ : x = default
⊢ Option.elim' default val none = x
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
x : α
h✝ : ¬x = default
⊢ Option.elim' default val (some { val := x, property := h✝ }) = x
[PROOFSTEP]
simp [*]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
⊢ Function.RightInverse (Option.elim' default val) fun x =>
    if h : x = default then none else some { val := x, property := h }
[PROOFSTEP]
rintro (_ | ⟨x, h⟩)
[GOAL]
case none
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
⊢ (fun x => if h : x = default then none else some { val := x, property := h }) (Option.elim' default val none) = none
[PROOFSTEP]
simp
[GOAL]
case some.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
x : α
h : x ≠ default
⊢ (fun x => if h : x = default then none else some { val := x, property := h })
      (Option.elim' default val (some { val := x, property := h })) =
    some { val := x, property := h }
[PROOFSTEP]
dsimp only
[GOAL]
case some.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
x : α
h : x ≠ default
⊢ (if h : Option.elim' default val (some { val := x, property := h }) = default then none
    else some { val := Option.elim' default val (some { val := x, property := h }), property := h }) =
    some { val := x, property := h }
[PROOFSTEP]
split_ifs with hi
[GOAL]
case pos
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
x : α
h : x ≠ default
hi : Option.elim' default val (some { val := x, property := h }) = default
⊢ False
[PROOFSTEP]
simp [h] at hi 
[GOAL]
case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
α : Type u
inst✝¹ : Inhabited α
inst✝ : DecidableEq α
x : α
h : x ≠ default
hi : ¬Option.elim' default val (some { val := x, property := h }) = default
⊢ some { val := Option.elim' default val (some { val := x, property := h }), property := hi } =
    some { val := x, property := h }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
m1 m2 : Multiset α
⊢ _root_.Disjoint (toFinset m1) (toFinset m2) ↔ Disjoint m1 m2
[PROOFSTEP]
rw [Finset.disjoint_iff_ne]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
m1 m2 : Multiset α
⊢ (∀ (a : α), a ∈ toFinset m1 → ∀ (b : α), b ∈ toFinset m2 → a ≠ b) ↔ Disjoint m1 m2
[PROOFSTEP]
refine' ⟨fun h a ha1 ha2 => _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
m1 m2 : Multiset α
h : ∀ (a : α), a ∈ toFinset m1 → ∀ (b : α), b ∈ toFinset m2 → a ≠ b
a : α
ha1 : a ∈ m1
ha2 : a ∈ m2
⊢ False
[PROOFSTEP]
rw [← Multiset.mem_toFinset] at ha1 ha2 
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
m1 m2 : Multiset α
h : ∀ (a : α), a ∈ toFinset m1 → ∀ (b : α), b ∈ toFinset m2 → a ≠ b
a : α
ha1✝ : a ∈ m1
ha1 : a ∈ toFinset m1
ha2✝ : a ∈ m2
ha2 : a ∈ toFinset m2
⊢ False
[PROOFSTEP]
exact h _ ha1 _ ha2 rfl
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
m1 m2 : Multiset α
⊢ Disjoint m1 m2 → ∀ (a : α), a ∈ toFinset m1 → ∀ (b : α), b ∈ toFinset m2 → a ≠ b
[PROOFSTEP]
rintro h a ha b hb rfl
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
m1 m2 : Multiset α
h : Disjoint m1 m2
a : α
ha : a ∈ toFinset m1
hb : a ∈ toFinset m2
⊢ False
[PROOFSTEP]
rw [Multiset.mem_toFinset] at ha hb 
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
m1 m2 : Multiset α
h : Disjoint m1 m2
a : α
ha : a ∈ m1
hb : a ∈ m2
⊢ False
[PROOFSTEP]
exact h ha hb
