Theorem: ENNReal_rpow_ne_top (ForML/SchwartzLp.lean)

State before:
a : ENNReal
p : ℝ
hp : 0 < p
h : a ≠ ⊤
⊢ a ^ p ≠ ⊤
Tactic:
rw [← ENNReal.ofReal_toReal_eq_iff] at h
State after:
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ a ^ p ≠ ⊤

State before:
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ a ^ p ≠ ⊤
Tactic:
rw [← h]
State after:
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ ENNReal.ofReal (ENNReal.toReal a) ^ p ≠ ⊤

State before:
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ ENNReal.ofReal (ENNReal.toReal a) ^ p ≠ ⊤
Tactic:
simp
State after:
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ ENNReal.toReal a ≤ 0 → 0 ≤ p

State before:
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
⊢ ENNReal.toReal a ≤ 0 → 0 ≤ p
Tactic:
intros
State after:
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
a✝ : ENNReal.toReal a ≤ 0
⊢ 0 ≤ p

State before:
a : ENNReal
p : ℝ
hp : 0 < p
h : ENNReal.ofReal (ENNReal.toReal a) = a
a✝ : ENNReal.toReal a ≤ 0
⊢ 0 ≤ p
Tactic:
exact hp.le
State after:
no goals