## Stream: general

### Topic: missing instances?

#### Johan Commelin (Mar 07 2019 at 15:47):

Lean failed to find instances for functor finset and has_seq finset... But both shouldn't really be a problem right?
(I have no clue at all what has_seq is... so therefore I think finset ought to have such an instance :see_no_evil: :grinning: :upside_down:)

#### Johan Commelin (Mar 07 2019 at 15:50):

I want to take the pairwise product of all elements in two finsets. And a long time ago someone on Zulip suggested that ought to be written like this:

#### Johan Commelin (Mar 08 2019 at 07:35):

I tried rcases ht but rcases tactic failed: ht : quot.lift is not an inductive datatype.

#### Johan Commelin (Mar 08 2019 at 07:35):

Does this mean that I should not be using finsets?

#### Mario Carneiro (Mar 08 2019 at 07:37):

there are some lemmas to prove about what these mean

#### Mario Carneiro (Mar 08 2019 at 07:37):

it might be easier to just finset.image and finset.prod instead of this

#### Johan Commelin (Mar 08 2019 at 07:38):

Ok, let me try that

#### Johan Commelin (Mar 08 2019 at 07:44):

Hmmm, so what are the options I can use:

• T : finset A
• T : set A + [fintype T]
• T : set A + h : set.finite T
• [fintype T] + ι : T → A
• ...
I guess it is not obvious which one should be chosen, right?

#### Johan Commelin (Mar 08 2019 at 07:46):

In the end I need to talk about { t₁ * t₂ | t₁ ∈ T₁, t₂ ∈ T₂ }. Which choice has the best API for that?

#### Mario Carneiro (Mar 08 2019 at 07:55):

I think finset.prod.image has the most lemmas, if you care about finiteness (you can also just use a set and forget about finite)

#### Johan Commelin (Mar 08 2019 at 07:56):

But prod is taking the product over the whole finset.

#### Johan Commelin (Mar 08 2019 at 07:57):

I guess I'll just stick with sets

#### Mario Carneiro (Mar 08 2019 at 08:00):

finset.prod is the cartesian product of two finsets

#### Mario Carneiro (Mar 08 2019 at 08:00):

if you map (*) over that with image you get your desired finset

#### Mario Carneiro (Mar 08 2019 at 08:01):

or is it finset.product?

#### Johan Commelin (Mar 08 2019 at 08:01):

finset.prod : Π {α : Type u} {β : Type v} [_inst_1 : comm_monoid β], finset α → (α → β) → β
prod s f is the product of f x as x ranges over the elements of the finite set s.


#### Kenny Lau (Mar 08 2019 at 09:34):

local attribute [instance, priority 0] classical.dec
noncomputable instance : monad finset :=
{pure := @finset.singleton, bind := λ _ _, finset.bind}

example {α : Type u} [has_mul α] (T₁ T₂ : finset α) (t : α) (ht : t ∈ (*) <\$> T₁ <*> T₂) :
∃ t₁ ∈ T₁, ∃ t₂ ∈ T₂, t₁ * t₂ = t :=
let ⟨f, hf, hf2⟩ := finset.mem_bind.1 ht,
⟨t₁, h₁, hf⟩ := finset.mem_bind.1 hf,
⟨t₂, h₂, hf3⟩ := finset.mem_bind.1 hf2 in
⟨t₁, h₁, t₂, h₂, (finset.mem_singleton.1 hf3).symm ▸ (finset.mem_singleton.1 hf).symm ▸ rfl⟩


#### Johan Commelin (Mar 08 2019 at 09:35):

Thanks Kenny!

Last updated: May 08 2021 at 20:11 UTC