-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.measure_norm_ge_lt_top {f : α → β} (hf : Integrable f μ) {ε : ℝ} (hε : 0 < ε) :
    μ { x | ε ≤ ‖f x‖ } < ∞

Proof state:
case refine_2.a
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ eLpNorm f 1 μ ^ ENNReal.toReal 1 < ⊤

Tactic:
simpa only [ENNReal.one_toReal, ENNReal.rpow_one] using
  (memLp_one_iff_integrable.2 hf).eLpNorm_lt_top

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ μ {x | ENNReal.ofReal ε ≤ ‖f x‖ₑ} < ⊤

Tactic:
refine (meas_ge_le_mul_pow_eLpNorm μ one_ne_zero ENNReal.one_ne_top hf.1 ?_).trans_lt ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ ENNReal.ofReal ε ≠ 0

case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ (ENNReal.ofReal ε)⁻¹ ^ ENNReal.toReal 1 * eLpNorm f 1 μ ^ ENNReal.toReal 1 < ⊤

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ μ {x | ε ≤ ‖f x‖} < ⊤

Tactic:
rw [show { x | ε ≤ ‖f x‖ } = { x | .ofReal ε ≤ ‖f x‖ₑ } by
    simp [ENNReal.ofReal, Real.toNNReal_le_iff_le_coe]]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ μ {x | ENNReal.ofReal ε ≤ ‖f x‖ₑ} < ⊤

Proof state:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ (ENNReal.ofReal ε)⁻¹ ^ ENNReal.toReal 1 * eLpNorm f 1 μ ^ ENNReal.toReal 1 < ⊤

Tactic:
apply ENNReal.mul_lt_top

Result:
case refine_2.a
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ (ENNReal.ofReal ε)⁻¹ ^ ENNReal.toReal 1 < ⊤

case refine_2.a
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ eLpNorm f 1 μ ^ ENNReal.toReal 1 < ⊤

Proof state:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ ENNReal.ofReal ε ≠ 0

Tactic:
simpa only [Ne, ENNReal.ofReal_eq_zero, not_le] using hε

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ {x | ε ≤ ‖f x‖} = {x | ENNReal.ofReal ε ≤ ‖f x‖ₑ}

Tactic:
simp [ENNReal.ofReal, Real.toNNReal_le_iff_le_coe]

Result:
no goals

Proof state:
case refine_2.a
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
ε : ℝ
hε : 0 < ε
⊢ (ENNReal.ofReal ε)⁻¹ ^ ENNReal.toReal 1 < ⊤

Tactic:
simpa only [ENNReal.one_toReal, ENNReal.rpow_one, ENNReal.inv_lt_top, ENNReal.ofReal_pos]
  using hε

Result:
no goals