polyrith debug output

Stream: mathlib4

[Heather Macbeth]

@Mario Carneiro I have an issue with polyrith apparently giving debug output. I know you looked into a similar issue before but maybe the fix wasn't targeted quite right -- can you look again?

import Mathlib.Tactic.Polyrith
import Mathlib.Tactic.Set

open Classical

noncomputable def F : ℤ × ℤ × ℤ → ℤ × ℤ × ℤ :=
fun ⟨x, y, z⟩ ↦
if h1 : ∃ k : ℤ, x = k then
  (x + 2 * z, z, h1.choose)
else
  sorry

/-
(hyp`h - ((4 * var1) * hyp`hk))
(«term_-_» `h "-" («term_*_» («term_*_» (num "4") "*" `z) "*" `hk))
-/
example {x y z w : ℤ} (h : x ^ 2 + 4 * y * z = w) :
    (F (x, y, z)).1 ^ 2 + 4 * (F (x, y, z)).2.1 * (F (x, y, z)).2.2 = w := by
  dsimp [F]
  split
  next h1 =>
    set k := h1.choose
    have hk : y = x + z + k := sorry
    polyrith
  sorry

[Mario Carneiro]

!4#2091