n=7 representative hole pattern (1,3) is infeasible

import Mathlib.Data.Real.Sqrt
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.NormNum

theorem CirclePackingConstants.n7_pattern_13_infeasible
 (x0 y0 x1 y1 x2 y2 x3 y3 x4 y4 x5 y5 x6 y6 : ℝ)
 (hx0L : (0:ℝ) ≤ x0)
 (hx0U : x0 ≤ (1000:ℝ))
 (hy0L : (0:ℝ) ≤ y0)
 (hy0U : y0 ≤ (1000:ℝ))
 (hx1L : (2000:ℝ) ≤ x1)
 (hx1U : x1 ≤ (3000:ℝ))
 (hy1L : (0:ℝ) ≤ y1)
 (hy1U : y1 ≤ (1000:ℝ))
 (hx2L : (1000:ℝ) ≤ x2)
 (hx2U : x2 ≤ (2000:ℝ))
 (hy2L : (1000:ℝ) ≤ y2)
 (hy2U : y2 ≤ (2000:ℝ))
 (hx3L : (2000:ℝ) ≤ x3)
 (hx3U : x3 ≤ (3000:ℝ))
 (hy3L : (1000:ℝ) ≤ y3)
 (hy3U : y3 ≤ (2000:ℝ))
 (hx4L : (0:ℝ) ≤ x4)
 (hx4U : x4 ≤ (1000:ℝ))
 (hy4L : (2000:ℝ) ≤ y4)
 (hy4U : y4 ≤ (3000:ℝ))
 (hx5L : (1000:ℝ) ≤ x5)
 (hx5U : x5 ≤ (2000:ℝ))
 (hy5L : (2000:ℝ) ≤ y5)
 (hy5U : y5 ≤ (3000:ℝ))
 (hx6L : (2000:ℝ) ≤ x6)
 (hx6U : x6 ≤ (3000:ℝ))
 (hy6L : (2000:ℝ) ≤ y6)
 (hy6U : y6 ≤ (3000:ℝ))
  (hT01 : (2584683:ℝ) < (x0-x1)^2+(y0-y1)^2)
  (hT02 : (2584683:ℝ) < (x0-x2)^2+(y0-y2)^2)
  (hT03 : (2584683:ℝ) < (x0-x3)^2+(y0-y3)^2)
  (hT04 : (2584683:ℝ) < (x0-x4)^2+(y0-y4)^2)
  (hT05 : (2584683:ℝ) < (x0-x5)^2+(y0-y5)^2)
  (hT06 : (2584683:ℝ) < (x0-x6)^2+(y0-y6)^2)
  (hT12 : (2584683:ℝ) < (x1-x2)^2+(y1-y2)^2)
  (hT13 : (2584683:ℝ) < (x1-x3)^2+(y1-y3)^2)
  (hT14 : (2584683:ℝ) < (x1-x4)^2+(y1-y4)^2)
  (hT15 : (2584683:ℝ) < (x1-x5)^2+(y1-y5)^2)
  (hT16 : (2584683:ℝ) < (x1-x6)^2+(y1-y6)^2)
  (hT23 : (2584683:ℝ) < (x2-x3)^2+(y2-y3)^2)
  (hT24 : (2584683:ℝ) < (x2-x4)^2+(y2-y4)^2)
  (hT25 : (2584683:ℝ) < (x2-x5)^2+(y2-y5)^2)
  (hT26 : (2584683:ℝ) < (x2-x6)^2+(y2-y6)^2)
  (hT34 : (2584683:ℝ) < (x3-x4)^2+(y3-y4)^2)
  (hT35 : (2584683:ℝ) < (x3-x5)^2+(y3-y5)^2)
  (hT36 : (2584683:ℝ) < (x3-x6)^2+(y3-y6)^2)
  (hT45 : (2584683:ℝ) < (x4-x5)^2+(y4-y5)^2)
  (hT46 : (2584683:ℝ) < (x4-x6)^2+(y4-y6)^2)
  (hT56 : (2584683:ℝ) < (x5-x6)^2+(y5-y6)^2)
 (hSep56 : (4-2*Real.sqrt 3)^2 < ((x5-x6)/3000)^2 + ((y5-y6)/3000)^2)
 (hSep36 : (4-2*Real.sqrt 3)^2 < ((x3-x6)/3000)^2 + ((y3-y6)/3000)^2)
 (hSep52 : (4-2*Real.sqrt 3)^2 < ((x5-x2)/3000)^2 + ((y5-y2)/3000)^2)
 (hSep32 : (4-2*Real.sqrt 3)^2 < ((x3-x2)/3000)^2 + ((y3-y2)/3000)^2)
 (hSep54 : (4-2*Real.sqrt 3)^2 < ((x5-x4)/3000)^2 + ((y5-y4)/3000)^2)
 (hSep24 : (4-2*Real.sqrt 3)^2 < ((x2-x4)/3000)^2 + ((y2-y4)/3000)^2)
 (hSep31 : (4-2*Real.sqrt 3)^2 < ((x3-x1)/3000)^2 + ((y3-y1)/3000)^2)
 (hSep21 : (4-2*Real.sqrt 3)^2 < ((x2-x1)/3000)^2 + ((y2-y1)/3000)^2)
 : False  := by sorry