Theorem: Interval.mem_approx_iter_sqrt' (Ray/Render/Potential.lean)

State before:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
ax : a ^ 2 ^ n ∈ approx x
⊢ a ∈ approx (x.iter_sqrt n)
Tactic:
generalize hb : a^(2^n) = b at ax
State after:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
⊢ a ∈ approx (x.iter_sqrt n)

State before:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
⊢ a ∈ approx (x.iter_sqrt n)
Tactic:
have ab : a = b ^ (2 ^ (-n : ℝ) : ℝ) := by
  have e : (2:ℝ)^n = (2^n : ℕ) := by norm_num
  rw [←hb, Real.rpow_neg (by norm_num), Real.rpow_natCast, e,
    Real.pow_rpow_inv_natCast a0 (pow_ne_zero _ (by norm_num))]
State after:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
ab : a = b ^ 2 ^ (-↑n)
⊢ a ∈ approx (x.iter_sqrt n)

State before:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
ab : a = b ^ 2 ^ (-↑n)
⊢ a ∈ approx (x.iter_sqrt n)
Tactic:
rw [ab]
State after:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
ab : a = b ^ 2 ^ (-↑n)
⊢ b ^ 2 ^ (-↑n) ∈ approx (x.iter_sqrt n)

State before:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
ab : a = b ^ 2 ^ (-↑n)
⊢ b ^ 2 ^ (-↑n) ∈ approx (x.iter_sqrt n)
Tactic:
exact mem_approx_iter_sqrt ax
State after:
no goals

State before:
a : ℝ
x : Interval
n : ℕ
a0 : 0 ≤ a
b : ℝ
hb : a ^ 2 ^ n = b
ax : b ∈ approx x
⊢ a = b ^ 2 ^ (-↑n)
Tactic:
have e : (2:ℝ)^n = (2^n : ℕ) := by norm_num
State after:
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)

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))]
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals