dfinsupp_equiv.lean

import data.dfinsupp
import tactic

universes u v w

variables {ii : Type u} {jj : Type v} [decidable_eq ii] [decidable_eq jj]
variables (β : ii → jj → Type w) [Π i j, decidable_eq (β i j)]
variables [Π i j, has_zero (β i j)] 

def to_fun (x : Π₀ (ij : ii × jj), β ij.1 ij.2) : Π₀ i, Π₀ j, β i j :=
quotient.lift_on x 
  (λ x, ⟦dfinsupp.pre.mk 
    (λ i, show Π₀ j : jj, β i j, 
      from ⟦dfinsupp.pre.mk 
        (λ j, x.to_fun (i, j)) 
        (x.pre_support.map prod.snd)
        (λ j, (x.3 (i, j)).elim (λ h, or.inl (multiset.mem_map.2 ⟨(i, j), h, rfl⟩)) or.inr)⟧) 
    (x.pre_support.map prod.fst) 
    (λ i, or_iff_not_imp_left.2 $ λ h, dfinsupp.ext $ λ j, (x.3 (i, j)).resolve_left 
      (λ hij, h (multiset.mem_map.2 ⟨(i, j), hij, rfl⟩)))⟧) 
  (λ a b hab, dfinsupp.ext (λ i, dfinsupp.ext (λ j, hab _)))

def inv_fun (x : Π₀ i, Π₀ j, β i j) : Π₀ (ij : ii × jj), β ij.1 ij.2 :=
quotient.lift_on x 
  (λ x, ⟦dfinsupp.pre.mk (λ i : ii × jj, quotient.lift_on (x.1 i.1) 
      (λ x, x.1 i.2) 
      (λ a b hab, hab _)) 
    (x.pre_support.bind (λ i, (quotient.lift_on (x.1 i) 
      (λ x, ((x.pre_support.filter (λ j, x.1 j ≠ 0)).map (λ j, (i, j))).to_finset) 
      (λ a b hab, begin
          ext p,
          cases a, cases b,
          replace hab : a_to_fun = b_to_fun := funext hab,
          subst hab,
          cases p with p₁ p₂,
          simp [and_comm _ (_ = p₂), @and.left_comm _ (_ = p₂)],
          specialize b_zero p₂,
          specialize a_zero p₂,
          tauto,
      end)).1)) 
    (λ i, or_iff_not_imp_right.2 begin
      generalize hxi : x.1 i.1 = a,
      revert hxi,
      refine quotient.induction_on a (λ a hxi, _),
      assume h,
      have h₁ := (a.3 i.2).resolve_right h,
      have h₂ := (x.3 i.1).resolve_right (λ ha, begin
        rw [hxi] at ha,
        exact h ((quotient.exact ha) i.snd),
      end),
      simp only [exists_prop, ne.def, multiset.mem_bind],
      use i.fst,
      rw [hxi, quotient.lift_on_beta],
      simp only [multiset.mem_erase_dup, multiset.to_finset_val, 
        multiset.mem_map, multiset.mem_filter],
      exact ⟨h₂, i.2, ⟨h₁, h⟩, by cases i; refl⟩
    end)⟧) 
  (λ a b hab, dfinsupp.ext $ λ i, by unfold_coes; simp [hab i.1])

example : (Π₀ (ij : ii × jj), β ij.1 ij.2) ≃ Π₀ i, Π₀ j, β i j := 
{ to_fun := to_fun β,
  inv_fun := inv_fun β,
  left_inv := λ x, quotient.induction_on x (λ x, dfinsupp.ext (λ i, by cases i; refl)),
  right_inv := λ x, quotient.induction_on x (λ x, dfinsupp.ext (λ i, dfinsupp.ext (λ j,
    begin
      generalize hxi : x.1 i = a,
      revert hxi,
      refine quotient.induction_on a (λ a hxi, _),
      rw [to_fun, inv_fun],
      unfold_coes,
      simp,
      rw [hxi, quotient.lift_on_beta, quotient.lift_on_beta],
    end)))  }