-rw-r--r-- 1607 leangoppa-20230726/Goppadecoding/finset.lean raw
import Mathlib.Data.Finset.Basic

namespace Goppadecoding

section lemmas_finset

theorem erase_eq_filter_not_union_filter_erase {U: Type _} [DecidableEq U] {S: Finset U} {s: U} {p: U → Prop} [DecidablePred p]:
  s ∈ S.filter p → S.erase s = (S.filter (fun t ↦ ¬ p t)) ∪ ((S.filter p).erase s) :=
by
  simp only [Finset.mem_filter, not_and, and_imp]
  intro _ ps
  ext t
  by_cases pt: p t
  . simp only [Finset.mem_erase, ne_eq, Finset.mem_filter, not_and, Finset.mem_union, pt, not_true, and_false, and_true, false_or]
  . rename_i inst inst_1 a
    simp_all only [not_true, Finset.mem_erase, ne_eq, Finset.mem_filter, and_self, Finset.mem_union, not_false_eq_true, and_true, and_false, or_false, and_iff_right_iff_imp]
    intro a_1
    apply Aesop.BuiltinRules.not_intro
    intro a_2
    aesop_subst a_2
    simp_all only

theorem disjoint_filter_not_filter_erase {U: Type _} [DecidableEq U] {S: Finset U} {s: U} {p: U → Prop} [DecidablePred p]:
  Disjoint (S.filter p) ((S.filter (fun t ↦ ¬p t)).erase s) :=
by
  rw[disjoint_iff]
  ext t
  simp only [Finset.mem_filter, not_and, not_not, ge_iff_le, Finset.le_eq_subset, Finset.inf_eq_inter, Finset.mem_inter, Finset.mem_erase, ne_eq, Finset.bot_eq_empty, Finset.not_mem_empty, iff_false, and_imp]
  rename_i inst inst_1
  intro _ a_1 _ _
  simp_all only

theorem injon_filter {U: Type _} [DecidableEq U] {V: Type _} [DecidableEq V] (α: U → V) (S: Finset U) (p: U → Prop) [DecidablePred p]:
  Set.InjOn α S → Set.InjOn α (S.filter p) :=
by
  apply Set.InjOn.mono
  norm_cast
  exact Finset.filter_subset p S

end lemmas_finset