fin_oplus_fin_equiv_fin.lean

import logic.equiv.fin
import tactic.zify
import tactic.ring

def fin_oplus_fin_equiv_fin (n : ℕ) {m a : ℕ} (ham : a ≤ m) :
  fin m ⊕ fin n ≃ fin (m + n) :=
calc fin m ⊕ fin n ≃ fin (a + (m - a)) ⊕ fin n :
    equiv.sum_congr (fin.cast (by { zify [ham], ring})).to_equiv (equiv.refl _)
  ... ≃ (fin a ⊕ fin (m - a)) ⊕ fin n :
    equiv.sum_congr fin_sum_fin_equiv.symm (equiv.refl _)
  ... ≃ fin a ⊕ (fin (m - a) ⊕ fin n) : equiv.sum_assoc _ _ _
  ... ≃ fin a ⊕ (fin n ⊕ fin (m - a)) : equiv.sum_congr (equiv.refl _) (equiv.sum_comm _ _)
  ... ≃ fin a ⊕ fin (n + (m - a)) :
    equiv.sum_congr (equiv.refl _) fin_sum_fin_equiv
  ... ≃ fin (a + (n + (m - a))) : fin_sum_fin_equiv
  ... ≃ fin (m + n) : (fin.cast (by { zify [ham], ring })).to_equiv

lemma A {m n a : ℕ} (ham : a ≤ m) (i : fin m) (hi : (i : ℕ) < a) :
  fin_oplus_fin_equiv_fin n ham (sum.inl i) = fin.cast_le le_self_add i :=
begin
  apply fin.ext,
  simp [fin_oplus_fin_equiv_fin],
  have hx : fin_sum_fin_equiv.symm (fin.cast (_ : m = a + (m - a)) i) = sum.inl (i.cast_lt hi),
  { rw ←fin.cast_le_of_eq,
    swap, exact le_add_tsub,
    exact fin_sum_fin_equiv_symm_apply_cast_add (i.cast_lt hi) },
  rw hx,
  simp,
end

lemma B' {m n a : ℕ} (ham : a ≤ m) : n + a ≤ m + n :=
begin
  rw add_comm,
  apply add_le_add_right ham,
end

lemma B {m n a : ℕ} (ham : a ≤ m) (i : fin n) :
  fin_oplus_fin_equiv_fin n ham (sum.inr i) = fin.cast_le (B' ham) (fin.add_nat a i) :=
begin
  apply fin.ext,
  simp [fin_oplus_fin_equiv_fin],
  rw add_comm,
end

lemma C {m n a : ℕ} (ham : a ≤ m) (i : fin m) (hi : a ≤ (i : ℕ)) :
  fin_oplus_fin_equiv_fin n ham (sum.inl i) = fin.add_nat n i :=
begin
  apply fin.ext,
  simp [fin_oplus_fin_equiv_fin],
  have hi' : (i - a : ℕ) < m - a,
  { zify, apply int.sub_lt_sub_right,
    simp only [nat.cast_lt], exact i.2, },
  let i' : fin (m - a) := ⟨_, hi'⟩,
  have hx : fin_sum_fin_equiv.symm (fin.cast (_ : m = a + (m - a)) i) = sum.inr (i'),
  { rw ← fin_sum_fin_equiv_symm_apply_nat_add _,
    simp [fin.nat_add, fin.cast_le, fin.cast_lt, fin.cast],
    rw ←nat.add_sub_assoc hi,
    rw nat.add_sub_cancel_left },
  rw hx,
  simp,
  rw add_left_comm,
  rw ←nat.add_sub_assoc hi,rw nat.add_sub_cancel_left,
  rw add_comm,
end