[GOAL]
α✝ β✝ : Type u
inst✝ : (P : Prop) → Decidable P
α β : Type ?u.384
⊢ Functor.mapConst = Functor.map ∘ const β
[PROOFSTEP]
simp only [Functor.mapConst, Functor.map]
[GOAL]
α✝ β✝ : Type u
inst✝ : (P : Prop) → Decidable P
α β γ : Type u_1
f : α → β → γ
s : Finset α
t : Finset β
⊢ image₂ f s t = Seq.seq (f <$> s) fun x => t
[PROOFSTEP]
ext
[GOAL]
case a
α✝ β✝ : Type u
inst✝ : (P : Prop) → Decidable P
α β γ : Type u_1
f : α → β → γ
s : Finset α
t : Finset β
a✝ : γ
⊢ a✝ ∈ image₂ f s t ↔ a✝ ∈ Seq.seq (f <$> s) fun x => t
[PROOFSTEP]
simp [mem_sup]
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
⊢ (SeqLeft.seqLeft s fun x => t) = Seq.seq (const β✝ <$> s) fun x => t
[PROOFSTEP]
rw [seq_def, fmap_def, seqLeft_def]
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
⊢ (if t = ∅ then ∅ else s) = sup (image (const β✝) s) fun f => image f t
[PROOFSTEP]
obtain rfl | ht := t.eq_empty_or_nonempty
[GOAL]
case inl
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
⊢ (if ∅ = ∅ then ∅ else s) = sup (image (const β✝) s) fun f => image f ∅
[PROOFSTEP]
simp_rw [image_empty, if_true]
[GOAL]
case inl
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
⊢ ∅ = sup (image (const β✝) s) fun f => ∅
[PROOFSTEP]
exact (sup_bot _).symm
[GOAL]
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
ht : Finset.Nonempty t
⊢ (if t = ∅ then ∅ else s) = sup (image (const β✝) s) fun f => image f t
[PROOFSTEP]
ext a
[GOAL]
case inr.a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
ht : Finset.Nonempty t
a : α✝
⊢ (a ∈ if t = ∅ then ∅ else s) ↔ a ∈ sup (image (const β✝) s) fun f => image f t
[PROOFSTEP]
rw [if_neg ht.ne_empty, mem_sup]
[GOAL]
case inr.a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
ht : Finset.Nonempty t
a : α✝
⊢ a ∈ s ↔ ∃ v, v ∈ image (const β✝) s ∧ a ∈ image v t
[PROOFSTEP]
refine' ⟨fun ha => ⟨const _ a, mem_image_of_mem _ ha, mem_image_const_self.2 ht⟩, _⟩
[GOAL]
case inr.a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
ht : Finset.Nonempty t
a : α✝
⊢ (∃ v, v ∈ image (const β✝) s ∧ a ∈ image v t) → a ∈ s
[PROOFSTEP]
rintro ⟨f, hf, ha⟩
[GOAL]
case inr.a.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
ht : Finset.Nonempty t
a : α✝
f : β✝ → α✝
hf : f ∈ image (const β✝) s
ha : a ∈ image f t
⊢ a ∈ s
[PROOFSTEP]
rw [mem_image] at hf ha 
[GOAL]
case inr.a.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
ht : Finset.Nonempty t
a : α✝
f : β✝ → α✝
hf : ∃ a, a ∈ s ∧ const β✝ a = f
ha : ∃ a_1, a_1 ∈ t ∧ f a_1 = a
⊢ a ∈ s
[PROOFSTEP]
obtain ⟨b, hb, rfl⟩ := hf
[GOAL]
case inr.a.intro.intro.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
ht : Finset.Nonempty t
a b : α✝
hb : b ∈ s
ha : ∃ a_1, a_1 ∈ t ∧ const β✝ b a_1 = a
⊢ a ∈ s
[PROOFSTEP]
obtain ⟨_, _, rfl⟩ := ha
[GOAL]
case inr.a.intro.intro.intro.intro.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
ht : Finset.Nonempty t
b : α✝
hb : b ∈ s
w✝ : β✝
left✝ : w✝ ∈ t
⊢ const β✝ b w✝ ∈ s
[PROOFSTEP]
exact hb
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
⊢ (SeqRight.seqRight s fun x => t) = Seq.seq (const α✝ id <$> s) fun x => t
[PROOFSTEP]
rw [seq_def, fmap_def, seqRight_def]
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
⊢ (if s = ∅ then ∅ else t) = sup (image (const α✝ id) s) fun f => image f t
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
t : Finset β✝
⊢ (if ∅ = ∅ then ∅ else t) = sup (image (const α✝ id) ∅) fun f => image f t
[PROOFSTEP]
rw [if_pos rfl, image_empty, sup_empty, bot_eq_empty]
[GOAL]
case inr
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
⊢ (if s = ∅ then ∅ else t) = sup (image (const α✝ id) s) fun f => image f t
[PROOFSTEP]
ext a
[GOAL]
case inr.a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
a : β✝
⊢ (a ∈ if s = ∅ then ∅ else t) ↔ a ∈ sup (image (const α✝ id) s) fun f => image f t
[PROOFSTEP]
rw [if_neg hs.ne_empty, mem_sup]
[GOAL]
case inr.a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
a : β✝
⊢ a ∈ t ↔ ∃ v, v ∈ image (const α✝ id) s ∧ a ∈ image v t
[PROOFSTEP]
refine' ⟨fun ha => ⟨id, mem_image_const_self.2 hs, by rwa [image_id]⟩, _⟩
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
a : β✝
ha : a ∈ t
⊢ a ∈ image id t
[PROOFSTEP]
rwa [image_id]
[GOAL]
case inr.a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
a : β✝
⊢ (∃ v, v ∈ image (const α✝ id) s ∧ a ∈ image v t) → a ∈ t
[PROOFSTEP]
rintro ⟨f, hf, ha⟩
[GOAL]
case inr.a.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
a : β✝
f : β✝ → β✝
hf : f ∈ image (const α✝ id) s
ha : a ∈ image f t
⊢ a ∈ t
[PROOFSTEP]
rw [mem_image] at hf ha 
[GOAL]
case inr.a.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
a : β✝
f : β✝ → β✝
hf : ∃ a, a ∈ s ∧ const α✝ id a = f
ha : ∃ a_1, a_1 ∈ t ∧ f a_1 = a
⊢ a ∈ t
[PROOFSTEP]
obtain ⟨b, hb, rfl⟩ := ha
[GOAL]
case inr.a.intro.intro.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
f : β✝ → β✝
hf : ∃ a, a ∈ s ∧ const α✝ id a = f
b : β✝
hb : b ∈ t
⊢ f b ∈ t
[PROOFSTEP]
obtain ⟨_, _, rfl⟩ := hf
[GOAL]
case inr.a.intro.intro.intro.intro.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
s : Finset α✝
t : Finset β✝
hs : Finset.Nonempty s
b : β✝
hb : b ∈ t
w✝ : α✝
left✝ : w✝ ∈ s
⊢ const α✝ id w✝ b ∈ t
[PROOFSTEP]
exact hb
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ : Type ?u.13031
f : α✝ → β✝
s : Finset α✝
⊢ (Seq.seq (pure f) fun x => s) = f <$> s
[PROOFSTEP]
simp only [pure_def, seq_def, sup_singleton, fmap_def]
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ γ✝ : Type ?u.13031
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
⊢ (Seq.seq u fun x => Seq.seq t fun x => s) = Seq.seq (Seq.seq (comp <$> u) fun x => t) fun x => s
[PROOFSTEP]
ext a
[GOAL]
case a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ γ✝ : Type ?u.13031
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ (a ∈ Seq.seq u fun x => Seq.seq t fun x => s) ↔ a ∈ Seq.seq (Seq.seq (comp <$> u) fun x => t) fun x => s
[PROOFSTEP]
simp_rw [seq_def, fmap_def]
[GOAL]
case a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ γ✝ : Type ?u.13031
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ (a ∈ sup u fun f => image f (sup t fun f => image f s)) ↔
    a ∈ sup (sup (image comp u) fun f => image f t) fun f => image f s
[PROOFSTEP]
simp only [exists_prop, mem_sup, mem_image]
[GOAL]
case a
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ γ✝ : Type ?u.13031
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ (∃ v, v ∈ u ∧ ∃ a_1, (∃ v, v ∈ t ∧ ∃ a, a ∈ s ∧ v a = a_1) ∧ v a_1 = a) ↔
    ∃ v, (∃ v_1, (∃ a, a ∈ u ∧ comp a = v_1) ∧ ∃ a, a ∈ t ∧ v_1 a = v) ∧ ∃ a_1, a_1 ∈ s ∧ v a_1 = a
[PROOFSTEP]
constructor
[GOAL]
case a.mp
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ γ✝ : Type ?u.13031
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ (∃ v, v ∈ u ∧ ∃ a_1, (∃ v, v ∈ t ∧ ∃ a, a ∈ s ∧ v a = a_1) ∧ v a_1 = a) →
    ∃ v, (∃ v_1, (∃ a, a ∈ u ∧ comp a = v_1) ∧ ∃ a, a ∈ t ∧ v_1 a = v) ∧ ∃ a_2, a_2 ∈ s ∧ v a_2 = a
[PROOFSTEP]
rintro ⟨g, hg, b, ⟨f, hf, a, ha, rfl⟩, rfl⟩
[GOAL]
case a.mp.intro.intro.intro.intro.intro.intro.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ γ✝ : Type ?u.13031
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
g : β✝ → γ✝
hg : g ∈ u
f : α✝ → β✝
hf : f ∈ t
a : α✝
ha : a ∈ s
⊢ ∃ v, (∃ v_1, (∃ a, a ∈ u ∧ comp a = v_1) ∧ ∃ a, a ∈ t ∧ v_1 a = v) ∧ ∃ a_1, a_1 ∈ s ∧ v a_1 = g (f a)
[PROOFSTEP]
exact ⟨g ∘ f, ⟨comp g, ⟨g, hg, rfl⟩, f, hf, rfl⟩, a, ha, rfl⟩
[GOAL]
case a.mpr
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ γ✝ : Type ?u.13031
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ (∃ v, (∃ v_1, (∃ a, a ∈ u ∧ comp a = v_1) ∧ ∃ a, a ∈ t ∧ v_1 a = v) ∧ ∃ a_1, a_1 ∈ s ∧ v a_1 = a) →
    ∃ v, v ∈ u ∧ ∃ a_2, (∃ v, v ∈ t ∧ ∃ a, a ∈ s ∧ v a = a_2) ∧ v a_2 = a
[PROOFSTEP]
rintro ⟨c, ⟨_, ⟨g, hg, rfl⟩, f, hf, rfl⟩, a, ha, rfl⟩
[GOAL]
case a.mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulFunctor Finset := lawfulFunctor
α✝ β✝ γ✝ : Type ?u.13031
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
g : β✝ → γ✝
hg : g ∈ u
f : α✝ → β✝
hf : f ∈ t
a : α✝
ha : a ∈ s
⊢ ∃ v, v ∈ u ∧ ∃ a_1, (∃ v, v ∈ t ∧ ∃ a, a ∈ s ∧ v a = a_1) ∧ v a_1 = (g ∘ f) a
[PROOFSTEP]
exact ⟨g, hg, f a, ⟨f, hf, a, ha, rfl⟩, rfl⟩
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulApplicative Finset := lawfulApplicative
α✝ β✝ : Type ?u.21428
s : Finset α✝
t : Finset β✝
⊢ (Seq.seq (Prod.mk <$> s) fun x => t) = Seq.seq ((fun b a => (a, b)) <$> t) fun x => s
[PROOFSTEP]
simp_rw [seq_def, fmap_def, sup_image, sup_eq_biUnion]
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulApplicative Finset := lawfulApplicative
α✝ β✝ : Type ?u.21428
s : Finset α✝
t : Finset β✝
⊢ Finset.biUnion s ((fun f => image f t) ∘ Prod.mk) = Finset.biUnion t ((fun f => image f s) ∘ fun b a => (a, b))
[PROOFSTEP]
change (s.biUnion fun a => t.image fun b => (a, b)) = t.biUnion fun b => s.image fun a => (a, b)
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulApplicative Finset := lawfulApplicative
α✝ β✝ : Type ?u.21428
s : Finset α✝
t : Finset β✝
⊢ (Finset.biUnion s fun a => image (fun b => (a, b)) t) = Finset.biUnion t fun b => image (fun a => (a, b)) s
[PROOFSTEP]
trans s ×ˢ t <;> [rw [product_eq_biUnion]; rw [product_eq_biUnion_right]]
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulApplicative Finset := lawfulApplicative
α✝ β✝ : Type ?u.21428
s : Finset α✝
t : Finset β✝
⊢ (Finset.biUnion s fun a => image (fun b => (a, b)) t) = Finset.biUnion t fun b => image (fun a => (a, b)) s
[PROOFSTEP]
trans s ×ˢ t
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulApplicative Finset := lawfulApplicative
α✝ β✝ : Type ?u.23242
s : Finset α✝
t : Finset β✝
⊢ (Finset.biUnion s fun a => image (fun b => (a, b)) t) = s ×ˢ t
[PROOFSTEP]
rw [product_eq_biUnion]
[GOAL]
α β : Type u
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulApplicative Finset := lawfulApplicative
α✝ β✝ : Type ?u.23242
s : Finset α✝
t : Finset β✝
⊢ s ×ˢ t = Finset.biUnion t fun b => image (fun a => (a, b)) s
[PROOFSTEP]
rw [product_eq_biUnion_right]
[GOAL]
inst✝ : (P : Prop) → Decidable P
src✝ : LawfulApplicative Finset := lawfulApplicative
α✝ β✝ γ✝ : Type ?u.24298
s : Finset α✝
f : α✝ → Finset β✝
g : β✝ → Finset γ✝
⊢ s >>= f >>= g = s >>= fun x => f x >>= g
[PROOFSTEP]
simp only [bind, ← sup_biUnion, sup_eq_biUnion, biUnion_biUnion]
[GOAL]
α β γ : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : CommApplicative F
inst✝¹ : CommApplicative G
inst✝ : DecidableEq α
s : Finset α
⊢ traverse pure s = s
[PROOFSTEP]
rw [traverse, Multiset.id_traverse]
[GOAL]
α β γ : Type u
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : CommApplicative F
inst✝¹ : CommApplicative G
inst✝ : DecidableEq α
s : Finset α
⊢ Multiset.toFinset <$> s.val = s
[PROOFSTEP]
exact s.val_toFinset
[GOAL]
α β γ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : CommApplicative F
inst✝ : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
⊢ Functor.map h <$> traverse g s = traverse (Functor.map h ∘ g) s
[PROOFSTEP]
unfold traverse
[GOAL]
α β γ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : CommApplicative F
inst✝ : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
⊢ Functor.map h <$> Multiset.toFinset <$> Multiset.traverse g s.val =
    Multiset.toFinset <$> Multiset.traverse (Functor.map h ∘ g) s.val
[PROOFSTEP]
simp only [map_comp_coe, functor_norm]
[GOAL]
α β γ : Type u
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : CommApplicative F
inst✝ : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
⊢ (Multiset.toFinset ∘ Functor.map h) <$> Multiset.traverse g s.val =
    Multiset.toFinset <$> Multiset.traverse (Functor.map h ∘ g) s.val
[PROOFSTEP]
rw [LawfulFunctor.comp_map, Multiset.map_traverse]
