internlm/Lean-Github huggingface dataset:
Theorem: Interval.mem_approx_iter_sqrt'
Proof state before:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
e : 2 ^ n = ↑(2 ^ n)
⊢ a = b ^ 2 ^ (-↑n)
Tactic:
rw [←hb, Real.rpow_neg (by norm_num), Real.rpow_natCast, e,
  Real.pow_rpow_inv_natCast a0 (pow_ne_zero _ (by norm_num))]
Proof state after:
no goals
Theorem: Interval.mem_approx_iter_sqrt'
Proof state before:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
⊢ 2 ^ n = ↑(2 ^ n)
Tactic:
norm_num
Proof state after:
no goals
Theorem: Interval.mem_approx_iter_sqrt'
Proof state before:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
e : 2 ^ n = ↑(2 ^ n)
⊢ 0 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Interval.mem_approx_iter_sqrt'
Proof state before:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
e : 2 ^ n = ↑(2 ^ n)
⊢ 2 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Box.approx_potential_small
Proof state before:
c' z' : ℂ
c4 : Complex.abs c' ≤ 4
z4 : Complex.abs z' ≤ 4
ss : Icc 0.216 1 ⊆ approx potential_small
⊢ ⋯.potential c' ↑z' ∈ approx potential_small
Tactic:
refine ss ⟨?_, ?_⟩
Proof state after:
case refine_1
c' z' : ℂ
c4 : Complex.abs c' ≤ 4
z4 : Complex.abs z' ≤ 4
ss : Icc 0.216 1 ⊆ approx potential_small
⊢ 0.216 ≤ ⋯.potential c' ↑z'

case refine_2
c' z' : ℂ
c4 : Complex.abs c' ≤ 4
z4 : Complex.abs z' ≤ 4
ss : Icc 0.216 1 ⊆ approx potential_small
⊢ ⋯.potential c' ↑z' ≤ 1
Theorem: Box.approx_potential_small
Proof state before:
c' z' : ℂ
c4 : Complex.abs c' ≤ 4
z4 : Complex.abs z' ≤ 4
⊢ Icc 0.216 1 ⊆ approx potential_small
Tactic:
rw [potential_small]
Proof state after:
c' z' : ℂ
c4 : Complex.abs c' ≤ 4
z4 : Complex.abs z' ≤ 4
⊢ Icc 0.216 1 ⊆ approx (0.216 ∪ 1)
Theorem: Box.approx_potential_small
Proof state before:
c' z' : ℂ
c4 : Complex.abs c' ≤ 4
z4 : Complex.abs z' ≤ 4
⊢ Icc 0.216 1 ⊆ approx (0.216 ∪ 1)
Tactic:
apply Icc_subset_approx
Proof state after:
case ax
c' z' : ℂ
c4 : Complex.abs c' ≤ 4
z4 : Complex.abs z' ≤ 4
⊢ 0.216 ∈ approx (0.216 ∪ 1)

case bx
c' z' : ℂ
c4 : Complex.abs c' ≤ 4
z4 : Complex.abs z' ≤ 4
⊢ 1 ∈ approx (0.216 ∪ 1)
Theorem: Box.approx_potential_small
Proof state before:
case ax
c' z' : ℂ
c4 : Complex.abs c' ≤ 4
z4 : Complex.abs z' ≤ 4
⊢ 0.216 ∈ approx (0.216 ∪ 1)
Tactic:
exact Interval.approx_union_left (Interval.approx_ofScientific _ _ _)
Proof state after:
no goals
Theorem: Box.approx_potential_small
Proof state before:
case bx
c' z' : ℂ
c4 : Complex.abs c' ≤ 4
z4 : Complex.abs z' ≤ 4
⊢ 1 ∈ approx (0.216 ∪ 1)
Tactic:
exact Interval.approx_union_right Interval.mem_approx_one
Proof state after:
no goals
Theorem: Box.approx_potential_small
Proof state before:
case refine_1
c' z' : ℂ
c4 : Complex.abs c' ≤ 4
z4 : Complex.abs z' ≤ 4
ss : Icc 0.216 1 ⊆ approx potential_small
⊢ 0.216 ≤ ⋯.potential c' ↑z'
Tactic:
exact le_potential c4 z4
Proof state after:
no goals
Theorem: Box.approx_potential_small
Proof state before:
case refine_2
c' z' : ℂ
c4 : Complex.abs c' ≤ 4
z4 : Complex.abs z' ≤ 4
ss : Icc 0.216 1 ⊆ approx potential_small
⊢ ⋯.potential c' ↑z' ≤ 1
Tactic:
apply Super.potential_le_one
Proof state after:
no goals
Theorem: Box.approx_potential_large
Proof state before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ ⋯.potential c' ↑z' ∈ approx z.potential_large
Tactic:
rw [potential_large]
Proof state after:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ ⋯.potential c' ↑z' ∈
    approx
      (let s := z.normSq;
      let log_s := s.log;
      (-log_s.div2).exp.grow (0.8095 * (log_s * -0.9635).exp).hi)
Theorem: Box.approx_potential_large
Proof state before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ ⋯.potential c' ↑z' ∈
    approx
      (let s := z.normSq;
      let log_s := s.log;
      (-log_s.div2).exp.grow (0.8095 * (log_s * -0.9635).exp).hi)
Tactic:
apply Interval.approx_grow (potential_approx 2 (le_trans (by norm_num) z6) cz)
Proof state after:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ (0.8095 * (z.normSq.log * -0.9635).exp).hi ≠ nan →
    potential_error 2 c' z' ≤ (0.8095 * (z.normSq.log * -0.9635).exp).hi.val

case zx
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ 1 / Complex.abs z' ∈ approx (-z.normSq.log.div2).exp
Theorem: Box.approx_potential_large
Proof state before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ 4 ≤ 6
Tactic:
norm_num
Proof state after:
no goals
Theorem: Box.approx_potential_large
Proof state before:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ (0.8095 * (z.normSq.log * -0.9635).exp).hi ≠ nan →
    potential_error 2 c' z' ≤ (0.8095 * (z.normSq.log * -0.9635).exp).hi.val
Tactic:
intro n
Proof state after:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : (0.8095 * (z.normSq.log * -0.9635).exp).hi ≠ nan
⊢ potential_error 2 c' z' ≤ (0.8095 * (z.normSq.log * -0.9635).exp).hi.val
Theorem: Box.approx_potential_large
Proof state before:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : (0.8095 * (z.normSq.log * -0.9635).exp).hi ≠ nan
⊢ potential_error 2 c' z' ≤ (0.8095 * (z.normSq.log * -0.9635).exp).hi.val
Tactic:
rw [Ne, Interval.hi_eq_nan] at n
Proof state after:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ potential_error 2 c' z' ≤ (0.8095 * (z.normSq.log * -0.9635).exp).hi.val
Theorem: Box.approx_potential_large
Proof state before:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ potential_error 2 c' z' ≤ (0.8095 * (z.normSq.log * -0.9635).exp).hi.val
Tactic:
refine le_trans (potential_error_le_of_z6 _ z6 cz) ?_
Proof state after:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ 0.8095 / Complex.abs z' ^ 1.927 ≤ (0.8095 * (z.normSq.log * -0.9635).exp).hi.val
Theorem: Box.approx_potential_large
Proof state before:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ 0.8095 / Complex.abs z' ^ 1.927 ≤ (0.8095 * (z.normSq.log * -0.9635).exp).hi.val
Tactic:
apply Interval.le_hi n
Proof state after:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ 0.8095 / Complex.abs z' ^ 1.927 ∈ approx (0.8095 * (z.normSq.log * -0.9635).exp)
Theorem: Box.approx_potential_large
Proof state before:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ 0.8095 / Complex.abs z' ^ 1.927 ∈ approx (0.8095 * (z.normSq.log * -0.9635).exp)
Tactic:
rw [div_eq_mul_inv, ←Real.rpow_neg (Complex.abs.nonneg _), Real.rpow_def_of_pos (by linarith)]
Proof state after:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ 0.8095 * ((Complex.abs z').log * -1.927).exp ∈ approx (0.8095 * (z.normSq.log * -0.9635).exp)
Theorem: Box.approx_potential_large
Proof state before:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ 0.8095 * ((Complex.abs z').log * -1.927).exp ∈ approx (0.8095 * (z.normSq.log * -0.9635).exp)
Tactic:
have e : Real.log (Complex.abs z') * -1.927 = Real.log (Complex.abs z' ^ 2) * -0.9635 := by
  rw [Real.log_pow, Nat.cast_two, mul_comm (2:ℝ), mul_assoc]; norm_num
Proof state after:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
e : (Complex.abs z').log * -1.927 = (Complex.abs z' ^ 2).log * -0.9635
⊢ 0.8095 * ((Complex.abs z').log * -1.927).exp ∈ approx (0.8095 * (z.normSq.log * -0.9635).exp)
Theorem: Box.approx_potential_large
Proof state before:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
e : (Complex.abs z').log * -1.927 = (Complex.abs z' ^ 2).log * -0.9635
⊢ 0.8095 * ((Complex.abs z').log * -1.927).exp ∈ approx (0.8095 * (z.normSq.log * -0.9635).exp)
Tactic:
rw [e]
Proof state after:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
e : (Complex.abs z').log * -1.927 = (Complex.abs z' ^ 2).log * -0.9635
⊢ 0.8095 * ((Complex.abs z' ^ 2).log * -0.9635).exp ∈ approx (0.8095 * (z.normSq.log * -0.9635).exp)
Theorem: Box.approx_potential_large
Proof state before:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
e : (Complex.abs z').log * -1.927 = (Complex.abs z' ^ 2).log * -0.9635
⊢ 0.8095 * ((Complex.abs z' ^ 2).log * -0.9635).exp ∈ approx (0.8095 * (z.normSq.log * -0.9635).exp)
Tactic:
mono
Proof state after:
no goals
Theorem: Box.approx_potential_large
Proof state before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ 0 < Complex.abs z'
Tactic:
linarith
Proof state after:
no goals
Theorem: Box.approx_potential_large
Proof state before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ (Complex.abs z').log * -1.927 = (Complex.abs z' ^ 2).log * -0.9635
Tactic:
rw [Real.log_pow, Nat.cast_two, mul_comm (2:ℝ), mul_assoc]
Proof state after:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ (Complex.abs z').log * -1.927 = (Complex.abs z').log * (2 * -0.9635)
Theorem: Box.approx_potential_large
Proof state before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ (Complex.abs z').log * -1.927 = (Complex.abs z').log * (2 * -0.9635)
Tactic:
norm_num
Proof state after:
no goals
Theorem: Box.approx_potential_large
Proof state before:
case zx
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ 1 / Complex.abs z' ∈ approx (-z.normSq.log.div2).exp
Tactic:
have e : 1 / Complex.abs z' = Real.exp (-(Real.log (Complex.abs z' ^ 2) / 2)) := by
  simp only [one_div, Real.log_pow, Nat.cast_ofNat, neg_mul, Real.rpow_neg zero_le_two,
    Real.rpow_one, ←mul_assoc, mul_comm _ (2:ℝ)⁻¹]
  rw [mul_div_cancel_left₀ _ two_ne_zero, Real.exp_neg, Real.exp_log (by linarith)]
Proof state after:
case zx
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
e : 1 / Complex.abs z' = (-((Complex.abs z' ^ 2).log / 2)).exp
⊢ 1 / Complex.abs z' ∈ approx (-z.normSq.log.div2).exp
Theorem: Box.approx_potential_large
Proof state before:
case zx
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
e : 1 / Complex.abs z' = (-((Complex.abs z' ^ 2).log / 2)).exp
⊢ 1 / Complex.abs z' ∈ approx (-z.normSq.log.div2).exp
Tactic:
rw [e]
Proof state after:
case zx
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
e : 1 / Complex.abs z' = (-((Complex.abs z' ^ 2).log / 2)).exp
⊢ (-((Complex.abs z' ^ 2).log / 2)).exp ∈ approx (-z.normSq.log.div2).exp
Theorem: Box.approx_potential_large
Proof state before:
case zx
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
e : 1 / Complex.abs z' = (-((Complex.abs z' ^ 2).log / 2)).exp
⊢ (-((Complex.abs z' ^ 2).log / 2)).exp ∈ approx (-z.normSq.log.div2).exp
Tactic:
mono
Proof state after:
no goals
Theorem: Box.approx_potential_large
Proof state before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ 1 / Complex.abs z' = (-((Complex.abs z' ^ 2).log / 2)).exp
Tactic:
simp only [one_div, Real.log_pow, Nat.cast_ofNat, neg_mul, Real.rpow_neg zero_le_two,
  Real.rpow_one, ←mul_assoc, mul_comm _ (2:ℝ)⁻¹]
Proof state after:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ (Complex.abs z')⁻¹ = (-(2 * (Complex.abs z').log / 2)).exp
Theorem: Box.approx_potential_large
Proof state before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ (Complex.abs z')⁻¹ = (-(2 * (Complex.abs z').log / 2)).exp
Tactic:
rw [mul_div_cancel_left₀ _ two_ne_zero, Real.exp_neg, Real.exp_log (by linarith)]
Proof state after:
no goals
Theorem: Box.approx_potential_large
Proof state before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ 0 < Complex.abs z'
Tactic:
linarith
Proof state after:
no goals
Theorem: Box.mem_approx_potential
Proof state before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
⊢ ⋯.potential c' ↑z' ∈ approx (c.potential z n r).1
Tactic:
set s := superF 2
Proof state after:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
⊢ s.potential c' ↑z' ∈ approx (c.potential z n r).1
Theorem: Box.mem_approx_potential
Proof state before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
⊢ s.potential c' ↑z' ∈ approx (c.potential z n r).1
Tactic:
rw [Box.potential]
Proof state after:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := c.normSq.hi;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Theorem: Box.mem_approx_potential
Proof state before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := c.normSq.hi;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
generalize hcs : (normSq c).hi = cs
Proof state after:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := cs;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Theorem: Box.mem_approx_potential
Proof state before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := cs;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
generalize hi : iterate c z (cs.max 9) n = i
Proof state after:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := cs;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Theorem: Box.mem_approx_potential
Proof state before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := cs;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
by_cases csn : cs = nan
Proof state after:
case pos
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : cs = nan
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := cs;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1

case neg
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := cs;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Theorem: Box.mem_approx_potential
Proof state before:
case neg
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := cs;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
simp only [hi, Interval.hi_eq_nan, Floating.val_lt_val]
Proof state after:
case neg
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
⊢ s.potential c' ↑z' ∈
    approx
      (match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if i.z.normSq = nan ∨ 16.val < i.z.normSq.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1