Theorem: MeasureTheory.measureReal_iUnion_fintype_le (Carleson/ToMathlib/MeasureReal.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝ : Fintype β
f : β → Set α
⊢ μ.real (⋃ b, f b) ≤ ∑ p : β, μ.real (f p)
Tactic:
convert measureReal_biUnion_finset_le Finset.univ f
State after:
case h.e'_3.h.e'_4.h.e'_3.h
ι : Type u_1
α : Type u_2
β : Type u_3
x✝¹ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝ : Fintype β
f : β → Set α
x✝ : β
⊢ f x✝ = ⋃ (_ : x✝ ∈ Finset.univ), f x✝

State before:
case h.e'_3.h.e'_4.h.e'_3.h
ι : Type u_1
α : Type u_2
β : Type u_3
x✝¹ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
inst✝ : Fintype β
f : β → Set α
x✝ : β
⊢ f x✝ = ⋃ (_ : x✝ ∈ Finset.univ), f x✝
Tactic:
simp
State after:
no goals