Theorem: C_control_approximation_effect_eq (Carleson/Theorem1_1/Control_Approximation_Effect.lean)

State before:
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ C_control_approximation_effect ε * δ = δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹ * (2 / ε) ^ 2⁻¹ / Real.pi + Real.pi * δ
Tactic:
symm
State after:
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹ * (2 / ε) ^ 2⁻¹ / Real.pi + Real.pi * δ = C_control_approximation_effect ε * δ

State before:
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ δ * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹ * (2 / ε) ^ 2⁻¹ / Real.pi + Real.pi * δ = C_control_approximation_effect ε * δ
Tactic:
rw [C_control_approximation_effect, mul_comm, mul_div_right_comm, mul_comm δ, mul_assoc, mul_comm δ, ← mul_assoc, ← mul_assoc, ← add_mul]
State after:
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ ((2 / ε) ^ 2⁻¹ / Real.pi * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹ + Real.pi) * δ =
    (C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹ + Real.pi) * δ

State before:
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ ((2 / ε) ^ 2⁻¹ / Real.pi * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹ + Real.pi) * δ =
    (C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹ + Real.pi) * δ
Tactic:
congr 2
State after:
case e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ (2 / ε) ^ 2⁻¹ / Real.pi * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹ = C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹

State before:
case e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ (2 / ε) ^ 2⁻¹ / Real.pi * C1_2 4 2 * (4 * Real.pi) ^ 2⁻¹ = C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹
Tactic:
rw [mul_comm _ (C1_2 4 2), mul_assoc]
State after:
case e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ C1_2 4 2 * ((2 / ε) ^ 2⁻¹ / Real.pi * (4 * Real.pi) ^ 2⁻¹) = C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹

State before:
case e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ C1_2 4 2 * ((2 / ε) ^ 2⁻¹ / Real.pi * (4 * Real.pi) ^ 2⁻¹) = C1_2 4 2 * (8 / (Real.pi * ε)) ^ 2⁻¹
Tactic:
congr
State after:
case e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ (2 / ε) ^ 2⁻¹ / Real.pi * (4 * Real.pi) ^ 2⁻¹ = (8 / (Real.pi * ε)) ^ 2⁻¹

State before:
case e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ (2 / ε) ^ 2⁻¹ / Real.pi * (4 * Real.pi) ^ 2⁻¹ = (8 / (Real.pi * ε)) ^ 2⁻¹
Tactic:
rw [Real.div_rpow, Real.div_rpow _ (mul_nonneg _ _), Real.mul_rpow, Real.mul_rpow]
State after:
case e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 2 ^ 2⁻¹ / ε ^ 2⁻¹ / Real.pi * (4 ^ 2⁻¹ * Real.pi ^ 2⁻¹) = 8 ^ 2⁻¹ / (Real.pi ^ 2⁻¹ * ε ^ 2⁻¹)

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

State before:
case e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 2 ^ 2⁻¹ / ε ^ 2⁻¹ / Real.pi * (4 ^ 2⁻¹ * Real.pi ^ 2⁻¹) = 8 ^ 2⁻¹ / (Real.pi ^ 2⁻¹ * ε ^ 2⁻¹)

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Tactic:
ring_nf
State after:
case e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 2 ^ (1 / 2) * (ε ^ (1 / 2))⁻¹ * Real.pi⁻¹ * 4 ^ (1 / 2) * Real.pi ^ (1 / 2) =
    (ε ^ (1 / 2))⁻¹ * 8 ^ (1 / 2) * (Real.pi ^ (1 / 2))⁻¹

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

State before:
case e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 2 ^ (1 / 2) * (ε ^ (1 / 2))⁻¹ * Real.pi⁻¹ * 4 ^ (1 / 2) * Real.pi ^ (1 / 2) =
    (ε ^ (1 / 2))⁻¹ * 8 ^ (1 / 2) * (Real.pi ^ (1 / 2))⁻¹

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Tactic:
rw [mul_assoc, mul_comm (2 ^ _), mul_assoc, mul_assoc, mul_assoc, mul_comm (4 ^ _), ← mul_assoc Real.pi⁻¹,
    ← Real.rpow_neg_one Real.pi, ← Real.rpow_add, mul_comm (Real.pi ^ _), ← mul_assoc (2 ^ _), ← Real.mul_rpow]
State after:
case e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ (ε ^ (1 / 2))⁻¹ * ((2 * 4) ^ (1 / 2) * Real.pi ^ (-1 + 1 / 2)) =
    (ε ^ (1 / 2))⁻¹ * (8 ^ (1 / 2) * (Real.pi ^ (1 / 2))⁻¹)

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

State before:
case e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ (ε ^ (1 / 2))⁻¹ * ((2 * 4) ^ (1 / 2) * Real.pi ^ (-1 + 1 / 2)) =
    (ε ^ (1 / 2))⁻¹ * (8 ^ (1 / 2) * (Real.pi ^ (1 / 2))⁻¹)

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Tactic:
congr
State after:
case e_a.e_a.e_a.e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 2 * 4 = 8

case e_a.e_a.e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ Real.pi ^ (-1 + 1 / 2) = (Real.pi ^ (1 / 2))⁻¹

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

State before:
case e_a.e_a.e_a.e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 2 * 4 = 8

case e_a.e_a.e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ Real.pi ^ (-1 + 1 / 2) = (Real.pi ^ (1 / 2))⁻¹

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Tactic:
norm_num
State after:
case e_a.e_a.e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ Real.pi ^ (-1 + 1 / 2) = (Real.pi ^ (1 / 2))⁻¹

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

State before:
case e_a.e_a.e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ Real.pi ^ (-1 + 1 / 2) = (Real.pi ^ (1 / 2))⁻¹

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Tactic:
ring_nf
State after:
case e_a.e_a.e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ Real.pi ^ (-1 / 2) = (Real.pi ^ (1 / 2))⁻¹

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

State before:
case e_a.e_a.e_a.e_a.e_a
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ Real.pi ^ (-1 / 2) = (Real.pi ^ (1 / 2))⁻¹

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Tactic:
rw [neg_div, Real.rpow_neg]
State after:
case e_a.e_a.e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

State before:
case e_a.e_a.e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 < Real.pi

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 4

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 8

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ Real.pi

ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε

case e_a.e_a.e_a.hx
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ 2

case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Tactic:
all_goals linarith [Real.pi_pos]
State after:
no goals

State before:
case e_a.e_a.e_a.hy
ε δ : ℝ
ε_nonneg : 0 ≤ ε
⊢ 0 ≤ ε
Tactic:
linarith [Real.pi_pos]
State after:
no goals