refine Tuple.bubble_sort_induction hd (fun (g : Weight n d) i j hij₁ hij₂ hwg ↦ ?_)
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
⊢ w ≤ sorted w'
n d : ℕ
inst✝ : NeZero d
w w' : Weight n d
hw : Monotone w
hd : w ≤ w'
g : Weight n d
i j : Fin (Nat.succ n)
hij₁ : i < j
hij₂ : g j < g i
hwg : w ≤ g
⊢ w ≤ g ∘ ⇑(Equiv.swap i j)