-- 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.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 < ⊤ ∧ μ (⇑f ⁻¹' {y}) < ⊤
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
exact hf_eLpNorm.2

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
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
refine absurd ?_ hy_ne

Result:
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

Proof state:
case pos.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 : ‖y‖ₑ ^ p.toReal = 0 ∨ μ (⇑f ⁻¹' {y}) = 0
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
cases hf_eLpNorm with
| inl hf_eLpNorm =>
  refine absurd ?_ hy_ne
  simpa [hp_pos_real] using hf_eLpNorm
| inr hf_eLpNorm => simp [hf_eLpNorm]

Result:
no goals

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
hyf : y ∈ f.range
hf_eLpNorm : ‖y‖ₑ ^ p.toReal * μ (⇑f ⁻¹' {y}) < ⊤
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
rw [ENNReal.mul_lt_top_iff] at hf_eLpNorm

Result:
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
hyf : y ∈ f.range
hf_eLpNorm : ‖y‖ₑ ^ p.toReal < ⊤ ∧ μ (⇑f ⁻¹' {y}) < ⊤ ∨ ‖y‖ₑ ^ p.toReal = 0 ∨ μ (⇑f ⁻¹' {y}) = 0
⊢ μ (⇑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}) < ⊤
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
by_cases hyf : y ∈ f.range

Result:
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}) < ⊤

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
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
have hf_eLpNorm := MemLp.eLpNorm_lt_top hf

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 : eLpNorm (⇑f) p μ < ⊤
⊢ μ (⇑f ⁻¹' {y}) < ⊤

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 : α
⊢ x ∈ ⇑f ⁻¹' {y} ↔ x ∈ ∅

Tactic:
rw [Set.mem_preimage, Set.mem_singleton_iff, mem_empty_iff_false, iff_false]

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 : α
⊢ ¬f x = y

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 : α
hxy : f x = y
⊢ y ∈ f.range

Tactic:
rw [mem_range, Set.mem_range]

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_1, f y_1 = y

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 : α
hxy : f x = y
⊢ ∃ y_1, f y_1 = y

Tactic:
exact ⟨x, hxy⟩

Result:
no goals

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
hyf : y ∈ f.range
hf_eLpNorm : ‖y‖ₑ ^ p.toReal < ⊤ ∧ μ (⇑f ⁻¹' {y}) < ⊤ ∨ ‖y‖ₑ ^ p.toReal = 0 ∨ μ (⇑f ⁻¹' {y}) = 0
⊢ μ (⇑f ⁻¹' {y}) < ⊤

Tactic:
cases hf_eLpNorm with
| inl hf_eLpNorm => exact hf_eLpNorm.2
| inr hf_eLpNorm =>
  cases hf_eLpNorm with
  | inl hf_eLpNorm =>
    refine absurd ?_ hy_ne
    simpa [hp_pos_real] using hf_eLpNorm
  | inr hf_eLpNorm => simp [hf_eLpNorm]

Result:
no goals