Computation with explicit subsets of a finite set in Lean 3. Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/How.20to.20show.20a.20set.20is.20an.20.CF.83-algebra

compute_finite_sigma_algebra.lean

import measure_theory.measurable_space_def

lemma Sup_mem_of_sup_mem {α} [complete_lattice α] (m : multiset α) (p : set α)
  (h : ∀ s ∈ m.powerset, multiset.sup s ∈ p)
  (f : ℕ → α) (hf : ∀ i, f i ∈ m) : (⨆ i, f i) ∈ p :=
begin
  classical,
  have hff : (set.range f).finite,
  { apply m.to_finset.finite_to_set.subset,
    rintro _ ⟨i, rfl⟩, rw [finset.mem_coe, multiset.mem_to_finset], exact hf i },
  change p (Sup _),
  rw [← hff.coe_to_finset, ← finset.sup_id_eq_Sup, finset.sup_def, multiset.map_id],
  apply h,
  rw [multiset.mem_powerset, finset.val_le_iff_val_subset],
  intros a ha, obtain ⟨i, rfl⟩ := hff.mem_to_finset.1 ha, exact hf i,
end

lemma list.sublists'_map {α β} (l : list α) (f : α → β) :
  (l.map f).sublists' = l.sublists'.map (list.map f) :=
begin
  induction l with hd tl ih, { refl },
  { simpa only [list.map_cons, list.sublists'_cons, list.map_append, ih, list.map_map] },
end

lemma multiset.powerset_map {α β} (s : multiset α) (f : α → β) :
  (s.map f).powerset = s.powerset.map (multiset.map f) :=
begin
  rw ← s.coe_to_list,
  simpa only [multiset.powerset_coe', multiset.coe_map, list.sublists'_map, list.map_map],
end

lemma multiset.sup_map_finset_coe {α} [decidable_eq α] (s : multiset (finset α)) :
  (s.map coe : multiset (set α)).sup = s.sup :=
begin
  induction s using multiset.induction with a s ih, { refl },
  { simpa only [multiset.sup_cons, multiset.map_cons, finset.sup_eq_union, finset.coe_union, ih] },
end

lemma Sup_mem_of_map_sup_mem {α} [decidable_eq α] (m : multiset $ finset α) (p : set (set α))
  (h : ∀ s ∈ m.powerset, ↑(multiset.sup s) ∈ p)
  (f : ℕ → set α) (hf : ∀ i, f i ∈ m.map (coe : finset α → set α)) : (⨆ i, f i) ∈ p :=
begin
  refine Sup_mem_of_sup_mem _ p (λ _ hs, _) _ hf,
  rw [multiset.powerset_map, multiset.mem_map] at hs,
  obtain ⟨s, hs, rfl⟩ := hs,
  rw multiset.sup_map_finset_coe,
  exact h s hs,
end

local notation `f4` := finset (fin 4)

lemma mysig_aux :
  ({{0,1}, {2,3}, {0,1,2,3}, ∅} : set $ set $ fin 4) =
  {x | x = ({0,1}:f4) ∨ x = ({2,3}:f4) ∨ x = ({0,1,2,3}:f4) ∨ x = (∅:f4)} :=
by congr; { ext, exact (or_false _).symm }

set_option profiler true
/- elaboration of mysig took 3.02s -/
def mysig : measurable_space (fin 4) :=
{ measurable_set' := (∈ ({{0,1}, {2,3}, {0,1,2,3}, ∅} : set $ set $ fin 4)),
  measurable_set_empty := or.inr (or.inr $ or.inr rfl),
  measurable_set_compl := begin
    simp_rw [mysig_aux, set.mem_set_of],
    rintro _ (rfl|rfl|rfl|rfl),
    all_goals { rw ← finset.coe_compl, simp only [finset.coe_inj], dec_trivial },
  end,
  measurable_set_Union := λ f hf, begin
    rw mysig_aux at hf ⊢,
    fapply Sup_mem_of_map_sup_mem,
    { exact {{0,1}, {2,3}, {0,1,2,3}, ∅} },
    { simp_rw set.mem_set_of,
      rintro _ (h|h|h|h|h|h|h|h|h|h|h|h|h|h|h|h|⟨⟨⟩⟩),
      all_goals { subst h, simp only [finset.coe_inj], dec_trivial } },
    { exact λ i, (hf i).imp id (or.imp id $ or.imp id (or_false _).2) },
  end }