equivalence of complements

Stream: general

[Yury G. Kudryashov]

The following definition works but it is slow.

import data.equiv.basic

open equiv

protected def compl {α β : Type*} {s : set α} {t : set β} [decidable_pred s] [decidable_pred t]
  (e₀ : s ≃ t) : {e : α ≃ β // ∀ x : s, e x = e₀ x} ≃ ((sᶜ : set α) ≃ (tᶜ : set β)) :=
{ to_fun := λ e, e.1.subtype_congr $ λ a, not_congr $
    begin
      rcases e with ⟨e, he⟩, dsimp,
      split; intro ha,
      { rw [← subtype.coe_mk a ha, he], exact subtype.coe_prop _ },
      { have := he (e₀.symm ⟨_, ha⟩),
        rw [e₀.apply_symm_apply, subtype.coe_mk] at this,
        rw [← e.injective this],
        exact subtype.coe_prop _ }
    end,
  inv_fun := λ e,
    ⟨(equiv.set.univ α).symm.trans $ (set.of_eq $ union_compl_self s).symm.trans $
      (equiv.set.union $ λ x, and_imp.2 absurd).trans $ (e₀.sum_congr e).trans $
      (equiv.set.union $ λ x, and_imp.2 absurd).symm.trans $ (set.of_eq $ union_compl_self t).trans
      (equiv.set.univ β), by { rintro ⟨x, hx⟩, simp [union_apply_left, *] }⟩,
  left_inv := λ ⟨e, he⟩, by { ext x, by_cases hx : x ∈ s, { simp [hx, union_apply_left, ← he] },
    { change x ∈ sᶜ at hx, dsimp, rw [union_apply_right],
      { simp [subtype_congr] }, { exact hx } } },
  right_inv := λ e, by { ext ⟨x, hx⟩, dsimp [subtype_congr], rw [union_apply_right],
    { simp, refl } } }

[Yury G. Kudryashov]

Any ideas how I can make it faster?

[Yury G. Kudryashov]

I didn't measure parse time but Emacs shows they busy indicator for a few seconds.

[Rob Lewis]

What commit are you on? This doesn't quite work for me, looks like set namespacing maybe? open set doesn't quite fix it.

[Chris Hughes]

import data.equiv.basic

open equiv set

@[simp] lemma set.sum_compl_symm_apply {α : Type*} {s : set α} [decidable_pred s] {x : s} :
(equiv.set.sum_compl s).symm x = sum.inl x :=
by cases x with x hx; exact set.sum_compl_symm_apply_of_mem hx

@[simp] lemma set.sum_compl_symm_apply_compl {α : Type*} {s : set α}
[decidable_pred s] {x : sᶜ} : (equiv.set.sum_compl s).symm x = sum.inr x :=
by cases x with x hx; exact set.sum_compl_symm_apply_of_not_mem hx

@[simp] lemma subtype_congr_apply {α : Sort} {β : Sort} {p : α → Prop} {q : β → Prop} (e : α ≃ β)
(h : ∀ (a : α), p a ↔ q (e a)) (x : {x // p x}) : e.subtype_congr h x = ⟨e x, (h _).1 x.2⟩ := rfl

protected def compl {α β : Type*} {s : set α} {t : set β} [decidable_pred s] [decidable_pred t]
(e₀ : s ≃ t) : {e : α ≃ β // ∀ x : s, e x = e₀ x} ≃ ((sᶜ : set α) ≃ (tᶜ : set β)) :=
{ to_fun := λ e, subtype_congr e
(λ a, not_congr $ iff.intro
(λ ha, by rw [← subtype.coe_mk a ha, e.prop ⟨a, ha⟩]; exact (e₀ ⟨a, ha⟩).prop)
(λ ha, calc a = (e : α ≃ β).symm (e a) : by simp only [symm_apply_apply, coe_fn_coe_base]
... = e₀.symm ⟨e a, ha⟩ : (e : α ≃ β).injective
(by { rw [e.prop (e₀.symm ⟨e a, ha⟩)],
simp only [apply_symm_apply, subtype.coe_mk] })
... ∈ s : (e₀.symm ⟨_, ha⟩).prop)),
inv_fun := λ e₁,
subtype.mk
(calc α ≃ s ⊕ (sᶜ : set α) : (set.sum_compl s).symm
... ≃ t ⊕ (tᶜ : set β) : equiv.sum_congr e₀ e₁
... ≃ β : set.sum_compl t)
(λ x, by simp only [sum.map_inl, trans_apply, sum_congr_apply,
set.sum_compl_apply_inl, set.sum_compl_symm_apply]),
left_inv := λ e,
begin
ext x,
by_cases hx : x ∈ s,
{ simp only [set.sum_compl_symm_apply_of_mem hx, ←e.prop ⟨x, hx⟩,
sum.map_inl, sum_congr_apply, trans_apply,
subtype.coe_mk, set.sum_compl_apply_inl] },
{ simp only [set.sum_compl_symm_apply_of_not_mem hx, sum.map_inr,
subtype_congr_apply, set.sum_compl_apply_inr, trans_apply,
sum_congr_apply, subtype.coe_mk] },
end,
right_inv := λ e, equiv.ext $ λ x, by simp only [sum.map_inr, subtype_congr_apply,
set.sum_compl_apply_inr, function.comp_app, sum_congr_apply, equiv.coe_trans,
subtype.coe_eta, subtype.coe_mk, set.sum_compl_symm_apply_compl] }

[Chris Hughes]

In the process of doing this I noticed a duplicate definition. equiv.sum_compl and equiv.set.sum_compl

[Yury G. Kudryashov]

Sorry, I've asked a question and fell asleep. Indeed, I forgot that I've added a couple of simp lemmas to make it compile.