exact? takes unreasonably long

In the following program, exact? takes unreasonably long (4 minutes):

structure S where
  data : List Nat
  ne : data ≠ []
  p1 : data.head ne = 0
  p2 : data.getLast ne = 42
  p3 : data.length > 1

def S.tl (s : S) : S where
  data := if s.data[1]'s.p3 = 0 then s.data.tail else s.data
  ne := sorry
  p1 := sorry
  p2 := sorry
  p3 := sorry

theorem S.ind {motive : S → Prop}
    (step : ∀ s, motive s.tl → motive s)
    (base : ∀ s, s.data[1]'s.p3 ≠ 0 → motive s)
    (s : S) : motive s := by
  rcases s with ⟨data, ne, p1, p2, p3⟩
  let s' : S := ⟨data, ne, p1, p2, p3⟩
  induction data
  case nil => simp at ne
  case cons head tail hi =>
    by_cases h : s'.data[1]'s'.p3 = 0
    · refine step s' ?_
      show motive ⟨if _ then _ else _, _, _, _, _⟩
      simp only [if_pos h, s', List.tail_cons]
      exact? -- takes 4 minutes, and produces a broken proof
      /- this works: `exact hi _ _ _ _` -/
    · exact base s' h

When it eventually does finish, it returns this error:

error: found a proof, but the corresponding tactic failed:
  (expose_names; exact ((fun a =>
        hi
          (Eq.trans
              (ite_congr (Eq.refl ((head :: tail)[1] = 0)) (fun a => Eq.refl tail) fun a => Eq.refl (head :: tail))
              ((fun x_0 x_1 x_2 x_3 => (fun x_0 x_1 x_2 x_3 => if_pos h) x_0 x_1 x_2 x_3)
                (instDecidableEqNat (head :: tail)[1] 0) (List Nat) tail (head :: tail)) ▸
            tl._proof_1 s')
          (Eq.trans
              (ite_congr (Eq.refl ((head :: tail)[1] = 0)) (fun a => Eq.refl tail) fun a => Eq.refl (head :: tail))
              ((fun x_0 x_1 x_2 x_3 => (fun x_0 x_1 x_2 x_3 => if_pos h) x_0 x_1 x_2 x_3)
                (instDecidableEqNat (head :: tail)[1] 0) (List Nat) tail (head :: tail)) ▸
            tl._proof_2 s')
          (Eq.trans
              (ite_congr (Eq.refl ((head :: tail)[1] = 0)) (fun a => Eq.refl tail) fun a => Eq.refl (head :: tail))
              ((fun x_0 x_1 x_2 x_3 => (fun x_0 x_1 x_2 x_3 => if_pos h) x_0 x_1 x_2 x_3)
                (instDecidableEqNat (head :: tail)[1] 0) (List Nat) tail (head :: tail)) ▸
            tl._proof_3 s')
          (Eq.trans
              (ite_congr (Eq.refl ((head :: tail)[1] = 0)) (fun a => Eq.refl tail) fun a => Eq.refl (head :: tail))
              ((fun x_0 x_1 x_2 x_3 => (fun x_0 x_1 x_2 x_3 => if_pos h) x_0 x_1 x_2 x_3)
                (instDecidableEqNat (head :: tail)[1] 0) (List Nat) tail (head :: tail)) ▸
            tl._proof_4 s')) ∘
      motive)
    s')

Run the supplied Lean reproducer and focus on the exact? invocation after simp only [if_pos h, s', List.tail_cons]. Compare its behavior with the explicit exact hi _ _ _ _ proof and the reported generated term; done means exact? completes promptly and produces a valid proof without the tactic failure.