-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem measure_preimage_lt_top_of_memLp (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ∞) (f : α →ₛ E)
    (hf : MemLp f p μ) (y : E) (hy_ne : y ≠ 0) : μ (f ⁻¹' {y}) < ∞

Proof state:
case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : ∀ a ∈ f.range, ‖a‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {a}) < ⊤
hyf : y ∈ f.range
⊢ μ (⇑f ⁻¹' {y}) < ⊤

case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : ∀ a ∈ f.range, ‖a‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {a}) < ⊤
hyf : y ∉ f.range
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
swap

Result:
case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : ∀ a ∈ f.range, ‖a‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {a}) < ⊤
hyf : y ∉ f.range
⊢ μ (⇑f ⁻¹' {y}) < ⊤

case pos
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : ∀ a ∈ f.range, ‖a‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {a}) < ⊤
hyf : y ∈ f.range
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Proof state:
case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : ∀ a ∈ f.range, ‖a‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {a}) < ⊤
hyf : y ∉ f.range
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
suffices h_empty : f ⁻¹' {y} = ∅ by
  rw [h_empty, measure_empty]; exact ENNReal.coe_lt_top

Result:
case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : ∀ a ∈ f.range, ‖a‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {a}) < ⊤
hyf : y ∉ f.range
⊢ ⇑f ⁻¹' {y} = ∅

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : ∀ a ∈ f.range, ‖a‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {a}) < ⊤
hyf : y ∉ f.range
h_empty : ⇑f ⁻¹' {y} = ∅
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
rw [h_empty, measure_empty]

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : ∀ a ∈ f.range, ‖a‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {a}) < ⊤
hyf : y ∉ f.range
h_empty : ⇑f ⁻¹' {y} = ∅
⊢ 0 < ⊤

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : ∀ a ∈ f.range, ‖a‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {a}) < ⊤
hyf : y ∉ f.range
h_empty : ⇑f ⁻¹' {y} = ∅
⊢ 0 < ⊤

Tactic:
exact ENNReal.coe_lt_top

Result:
no goals

Proof state:
case neg.h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : ∀ a ∈ f.range, ‖a‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {a}) < ⊤
hyf : y ∉ f.range
x : α
⊢ ¬f x = y

Tactic:
refine fun hxy => hyf ?_

Result:
case neg.h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : ∀ a ∈ f.range, ‖a‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {a}) < ⊤
hyf : y ∉ f.range
x : α
hxy : f x = y
⊢ y ∈ f.range

Proof state:
case pos.inr.inr
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hyf : y ∈ f.range
hf_eLpNorm : μ (⇑f ⁻¹' {y}) = 0
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
simp [hf_eLpNorm]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : eLpNorm (⇑f) p μ < ⊤
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
rw [eLpNorm_eq_eLpNorm' hp_pos hp_ne_top, f.eLpNorm'_eq, one_div,
  ← @ENNReal.lt_rpow_inv_iff _ _ p.toReal⁻¹ (by simp [hp_pos_real]),
  @ENNReal.top_rpow_of_pos p.toReal⁻¹⁻¹ (by simp [hp_pos_real]),
  ENNReal.sum_lt_top] at hf_eLpNorm

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : ∀ a ∈ f.range, ‖a‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {a}) < ⊤
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Proof state:
case neg
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : ∀ a ∈ f.range, ‖a‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {a}) < ⊤
hyf : y ∉ f.range
⊢ ⇑f ⁻¹' {y} = ∅

Tactic:
ext1 x

Result:
case neg.h
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : ∀ a ∈ f.range, ‖a‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {a}) < ⊤
hyf : y ∉ f.range
x : α
⊢ x ∈ ⇑f ⁻¹' {y} ↔ x ∈ ∅

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : ∑ y ∈ f.range, ‖y‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {y}) < ⊤ ^ p.toReal⁻¹⁻¹
⊢ 0 < p.toReal⁻¹⁻¹

Tactic:
simp [hp_pos_real]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
have hp_pos_real : 0 < p.toReal := ENNReal.toReal_pos hp_pos hp_ne_top

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hf_eLpNorm : (∑ y ∈ f.range, ‖y‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {y})) ^ p.toReal⁻¹ < ⊤
⊢ 0 < p.toReal⁻¹

Tactic:
simp [hp_pos_real]

Result:
no goals

Proof state:
case pos.inr.inl
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
hp_pos : p ≠ 0
hp_ne_top : p ≠ ⊤
f : α →ₛ E
hf : MemLp (⇑f) p μ
y : E
hy_ne : y ≠ 0
hp_pos_real : 0 < p.toReal
hyf : y ∈ f.range
hf_eLpNorm : ‖y‖ₑ ^ p.toReal = 0
⊢ y = 0

Tactic:
simpa [hp_pos_real] using hf_eLpNorm

Result:
no goals