case g
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
H✝ : Models arr m
k : ℕ
hk : k = n + 1
x : α
H : Agrees arr (fun x => x.rank) fun i => rank m ↑i
⊢ Agrees (Array.push arr { parent := n, value := x, rank := 0 }) (fun x => x.rank) fun i =>
    rank (UFModel.push m k (_ : n ≤ k)) ↑i
case g
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
H : Models arr m
k : ℕ
hk : k = n + 1
x : α
⊢ (Agrees arr (fun x => x.rank) fun i => rank m ↑i) →
    Agrees (Array.push arr { parent := n, value := x, rank := 0 }) (fun x => x.rank) fun i =>
      rank (UFModel.push m k (_ : n ≤ k)) ↑i
intro H
no goals
case g
α : Type u_1
arr : Array (UFNode α)
n : ℕ
m : UFModel n
H✝ : Models arr m
k : ℕ
hk : k = n + 1
x : α
H : Agrees arr (fun x => x.rank) fun i => rank m ↑i
⊢ Agrees (Array.push arr { parent := n, value := x, rank := 0 }) (fun x => x.rank) fun i =>
    rank (UFModel.push m k (_ : n ≤ k)) ↑i
refine H.push _ hk _ _ (fun i h ↦ ?_) (fun h ↦ ?_) <;>
simp [UFModel.push, h, lt_irrefl]