set_option maxHeartbeats 1000 in
example (x : Nat) :
  ∃ (h : x = x)
      (h : x = x)
      (h : x = x)
      (h : x = x)
      (h : x = x)
      (h : x = x)
      (h : x = x)
      (h : x = x)
      (h : x = x)
      (h : x = x)
      (h : x = x)
      (h : x = x)
      (h : x = x), True := by
  simp only
  sorry