finset.fold of option.lift_or_get

Stream: Is there code for X?

[Eric Wieser]

Are there any lemmas to help me make progress on this goal?

import data.finset.fold

open finset

variables {α β : Type*} (s : finset β) (f : α → α → α) (g : α ≃ β) [is_associative α f] [is_commutative α f]

instance : is_associative β (equiv.arrow_congr g (equiv.arrow_congr g g) f) :=
⟨λ x y z, by simp [@is_associative.assoc _ f _ _ _ _]⟩

instance : is_commutative β (equiv.arrow_congr g (equiv.arrow_congr g g) f) :=
⟨λ x y, by {simp, rw [@is_commutative.comm _ f _ _ _]}⟩

example : (finset.fold (option.lift_or_get f)
            none (some ∘ g.symm) s).map g
        = (finset.fold (option.lift_or_get (equiv.arrow_congr g (equiv.arrow_congr g g) f))
            none some s) :=
begin
  simp,
  sorry
end

Should those is_associative and is_commutative instances be in mathlib?

[Eric Wieser]

I suppose a likely useful building block would be:

def option_congr (e : α ≃ β) : option α ≃ option β :=
{ to_fun := option.map e,
  inv_fun := option.map e.symm,
  left_inv := λ x, by cases x; simp,
  right_inv := λ x, by cases x; simp, }

does that exist?

[Yakov Pechersky]

Is there the automatic construction of a equiv of set.inj_on?

[Yury G. Kudryashov]

docs#equiv.set.image_of_inj_on

[Yury G. Kudryashov]

(open data/equiv/basic, search for inj_on)

[Eric Wieser]

@Yakov Pechersky, can you explain the link between your question and mine?

[Yakov Pechersky]

Since option.some is injective, you have that (handwavy notation) α ≃ option.some '' α, then transitively with β, then identify none with each other.

[Yakov Pechersky]

Which is what your explicit structure does. I was wondering if there was shorthand for it.