Theorem: C1_2_pos (Carleson/Carleson.lean)

State before:
a q : ℝ
hq : 1 < q
⊢ 0 < C1_2 a q
Tactic:
rw [C1_2]
State after:
a q : ℝ
hq : 1 < q
⊢ 0 < 2 ^ (450 * a ^ 3) / (q - 1) ^ 5

State before:
a q : ℝ
hq : 1 < q
⊢ 0 < 2 ^ (450 * a ^ 3) / (q - 1) ^ 5
Tactic:
apply div_pos
State after:
case ha
a q : ℝ
hq : 1 < q
⊢ 0 < 2 ^ (450 * a ^ 3)

case hb
a q : ℝ
hq : 1 < q
⊢ 0 < (q - 1) ^ 5

State before:
case ha
a q : ℝ
hq : 1 < q
⊢ 0 < 2 ^ (450 * a ^ 3)

case hb
a q : ℝ
hq : 1 < q
⊢ 0 < (q - 1) ^ 5
Tactic:
. apply Real.rpow_pos_of_pos
  norm_num
State after:
case hb
a q : ℝ
hq : 1 < q
⊢ 0 < (q - 1) ^ 5

State before:
case hb
a q : ℝ
hq : 1 < q
⊢ 0 < (q - 1) ^ 5
Tactic:
. apply pow_pos
  linarith [hq]
State after:
no goals

State before:
case ha
a q : ℝ
hq : 1 < q
⊢ 0 < 2 ^ (450 * a ^ 3)
Tactic:
apply Real.rpow_pos_of_pos
State after:
case ha.hx
a q : ℝ
hq : 1 < q
⊢ 0 < 2

State before:
case ha.hx
a q : ℝ
hq : 1 < q
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
case hb
a q : ℝ
hq : 1 < q
⊢ 0 < (q - 1) ^ 5
Tactic:
apply pow_pos
State after:
case hb.H
a q : ℝ
hq : 1 < q
⊢ 0 < q - 1

State before:
case hb.H
a q : ℝ
hq : 1 < q
⊢ 0 < q - 1
Tactic:
linarith [hq]
State after:
no goals