Theorem: Box.approx_potential_small (Ray/Render/Potential.lean)

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 ⟨?_, ?_⟩
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

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]
State after:
c' z' : ℂ
c4 : Complex.abs c' ≤ 4
z4 : Complex.abs z' ≤ 4
⊢ Icc 0.216 1 ⊆ approx (0.216 ∪ 1)

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
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)

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

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

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

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