quotient.fin_choice without choice.

quotient_fin_choice.lean

import data.fintype.basic

variables {ι : Type*} {α : ι → Type*} [S : Π i, setoid (α i)] {β : Sort*}
include S

def quotient.map_pi_pred (p : ι → Prop) (h : ∀ i, p i) :
  @quotient (Π i, p i → α i) pi_setoid → @quotient (Π i, α i) pi_setoid :=
quotient.map (λ f i, f i $ h i) (λ f g he i, he i $ h i)

def quotient.map_pi_pred₂ (p₁ p₂ : ι → Prop) (h : p₂ ≤ p₁) :
  @quotient (Π i, p₁ i → α i) pi_setoid → @quotient (Π i, p₂ i → α i) pi_setoid :=
quotient.map (λ f i hi, f i $ h i hi) (λ f g he i hi, he i $ h i hi)

def quotient.proj_pi (i) : @quotient (Π i, α i) pi_setoid → quotient (S i) :=
quotient.map (λ f, f i) (λ f g he, he i)

def quotient.proj_pi_pred (p : ι → Prop) (i) (hi : p i) :
  @quotient (Π i, p i → α i) pi_setoid → quotient (S i) :=
quotient.map (λ f, f i hi) (λ f g he, he i hi)

lemma quotient.proj_pi_map_pi_pred (p : ι → Prop) (h : ∀ i, p i)
  (f : @quotient (Π i, p i → α i) pi_setoid) (i) :
  (quotient.map_pi_pred p h f).proj_pi i = quotient.proj_pi_pred p i (h i) f :=
by { rcases f, refl }

lemma quotient.proj_pi_map_pi_pred₂ (p₁ p₂ : ι → Prop) (h : ∀ i, p₂ i → p₁ i)
  (f : @quotient (Π i, p₁ i → α i) pi_setoid) (i) (hi : p₂ i) :
  (quotient.map_pi_pred₂ p₁ p₂ h f).proj_pi_pred p₂ i hi = quotient.proj_pi_pred p₁ i (h i hi) f :=
by { rcases f, refl }

lemma quotient.pi_ext {f g : @quotient (Π i, α i) pi_setoid} (h : ∀ i, f.proj_pi i = g.proj_pi i) :
  f = g :=
begin
  rcases f, rcases g,
  apply quot.sound,
  exact λ i, quotient.exact (h i),
end

lemma quotient.pi_pred_ext (p : ι → Prop) {f g : @quotient (Π i, p i → α i) pi_setoid}
  (h : ∀ i hi, f.proj_pi_pred p i hi = g.proj_pi_pred p i hi) : f = g :=
begin
  rcases f, rcases g,
  apply quot.sound,
  exact λ i hi, quotient.exact (h i hi),
end

variable [decidable_eq ι]

lemma quotient.proj_pi_pred_fin_choice_aux (l) :
  ∀ (f : Π i ∈ l, quotient (S i)) i hi,
    quotient.proj_pi_pred (∈ l) i hi (quotient.fin_choice_aux l f) = f i hi :=
begin
  induction l with j l ih,
  { intros f i hi, exact hi.elim },
  intros f i hi,
  rw [quotient.fin_choice_aux],
  obtain ⟨a, ha⟩ := (f j $ list.mem_cons_self _ _).exists_rep,
  obtain ⟨g, hg⟩ := (quotient.fin_choice_aux l $ λ j h, f j $ list.mem_cons_of_mem _ h).exists_rep,
  rw [← ha, ← hg], dsimp [quotient.lift_on₂, quotient.proj_pi_pred, quotient.map_mk],
  split_ifs,
  { subst h, exact ha },
  specialize ih (λ k hk, f k $ list.mem_cons_of_mem _ hk)
    i ((list.eq_or_mem_of_mem_cons hi).resolve_left h),
  dsimp only at ih,
  rw [← ih, ← hg], refl,
end

namespace multiset

def quotient_choice [decidable_eq ι] {m : multiset ι}
  (f : Π i ∈ m, quotient (S i)) : @quotient (Π i ∈ m, α i) pi_setoid :=
begin
  let := equiv.subtype_quotient_equiv_quotient_subtype
    (λ l : list ι, ↑l = m) (λ s, s = m) (λ i, iff.rfl) (λ _ _, iff.rfl) ⟨m, rfl⟩,
  refine quotient.lift_on this (λ l, _) (λ l₁ l₂ h, _),
  { exact (quotient.fin_choice_aux ↑l $ 
      λ i hi, f i $ l.2 ▸ hi).map_pi_pred₂ _ _ (subset_of_le l.2.ge) },
  apply quotient.pi_pred_ext,
  intros i hi,
  simp_rw [quotient.proj_pi_map_pi_pred₂, quotient.proj_pi_pred_fin_choice_aux],
end

theorem quotient_choice_mk {m : multiset ι} (a : Π i ∈ m, α i) :
  quotient_choice (λ i h, ⟦a i h⟧) = ⟦a⟧ :=
begin
  dsimp [quotient_choice],
  induction m using quotient.ind,
  rw [equiv.subtype_quotient_equiv_quotient_subtype_mk],
  apply quotient.pi_pred_ext,
  intros i hi,
  dsimp, simp_rw [quotient.proj_pi_map_pi_pred₂, quotient.proj_pi_pred_fin_choice_aux],
  refl,
end

end multiset

variables [fintype ι] 

def quotient.fin_choice' (f : Π i, quotient (S i)) : @quotient (Π i, α i) pi_setoid :=
begin
  let := equiv.subtype_quotient_equiv_quotient_subtype (λ l : list ι, ∀ i, i ∈ l)
    (λ s : multiset ι, ∀ i, i ∈ s) (λ i, iff.rfl) (λ _ _, iff.rfl) ⟨_, finset.mem_univ⟩,
  refine quotient.lift_on this (λ l, quotient.map_pi_pred (∈ (l : list ι)) l.2 $ 
    quotient.fin_choice_aux l $ λ i _, f i) (λ l₁ l₂ h, _),
  dsimp only,
  refine quotient.pi_ext (λ i, _),
  simp_rw [quotient.proj_pi_map_pi_pred, quotient.proj_pi_pred_fin_choice_aux],
end

theorem quotient.fin_choice'_eq (f : Π i, α i) :
  quotient.fin_choice' (λ i, ⟦f i⟧) = ⟦f⟧ :=
begin
  dsimp [quotient.fin_choice'],
  obtain ⟨l, hl⟩ := (finset.univ.val : multiset ι).exists_rep,
  simp_rw ← hl,
  rw [equiv.subtype_quotient_equiv_quotient_subtype_mk],
  refine quotient.pi_ext (λ i, _),
  dsimp, simp_rw [quotient.proj_pi_map_pi_pred, quotient.proj_pi_pred_fin_choice_aux],
  refl,
end

def quotient_lift (f : (Π i, α i) → β)
  (h : ∀ (a b : Π i, α i), (∀ i, a i ≈ b i) → f a = f b)
  (q : Π i, quotient (S i)) : β :=
quotient.lift _ h (quotient.fin_choice' q)