Need help with ugly proof involving Fin and calc

Stream: new members

[Alex Mobius]

Having trouble with a proof, the lowdown is this:

1. I have (a.push v).size = a.size + 1, but the former is inside of Fin types in my expressions, and I don't know how to perform the substitution "globally" (rw at * just masks hypotheses with new ones, but the goal still refers to the old ones), thus I'm unable to use Fin.le_val_last, and am forced to go to the succ projection for the proof.
2. calc seems to be very unhappy about inequalities involving Fin and Nat, which is how I've arrived at the wart in L60.
   (Apologies for the larger example, really don't know how to minify further while preserving the problem at hand)

import Mathlib.Order.Fin.Basic
import Mathlib.Logic.Equiv.Defs
import Mathlib.Logic.Lemmas
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Nodup

structure Labels (T: Type u) [DecidableEq T] where
  data: Array T
  nodup: data.toList.Nodup

variable {T: Type u} [DecidableEq T]

instance: Membership T (Labels T) where
  mem := (Membership.mem ·.data ·)

instance (v: T) (l: Labels T): Decidable (v ∈ l) := Array.instDecidableMemOfDecidableEq v l.data

namespace Labels

variable (l: Labels T)

@[reducible] def size := l.data.size

abbrev Idx := Fin (l.size)

def find v (h: v ∈ l): l.Idx :=
  let x := l.data.idxOf v
  have sm: x < l.size := Array.idxOf_lt_length h
  ⟨ x, sm ⟩

def add v (h: v ∉ l): Σ (l: Labels T), l.Idx :=
  let data' := l.data.push v
  have nodup': data'.toList.Nodup := by
    unfold data'
    rw [Array.push_toList]
    simp [List.nodup_middle, List.nodup_cons]
    exact ⟨ h, l.nodup ⟩
  let l' := {data:=data', nodup:=nodup'}
  have : l.data.size < data'.size := by
    unfold data'
    rw [Array.size_push]
    apply Nat.lt_add_one
  let x: Labels.Idx l' := ⟨ l.data.size, this ⟩
  ⟨ l', x ⟩

theorem add_argmax: l.add v h = ⟨ l', x ⟩ -> ∀ u (h: u ∈ l'), l'.find u h ≤ x := by
  intro added
  simp [add] at added
  intro u h
  let x' := l'.find u h
  change x' ≤ x
  obtain ⟨ rfl, xeq ⟩ := added
  have xeq := xeq.eq
  let size' := (l.data.push v).size
  have sizeplus1: size' = l.data.size + 1 := Array.size_push _ _
  rw [←Fin.succ_le_succ_iff, Fin.le_iff_val_le_val]
  apply Fin.val_eq_of_eq at xeq
  calc
    x'.succ.val ≤ size' := by
      have vl := Fin.le_last x'.succ
      rw [Fin.le_iff_val_le_val] at vl
      exact vl
    size' = l.data.size + 1 := sizeplus1
    l.data.size + 1 = x.succ.val := Nat.succ_inj.mpr xeq