Theorem: MeasureTheory.measureReal_biUnion_finset_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 α
s : Finset β
f : β → Set α
⊢ μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
Tactic:
induction' s using Finset.induction_on with x s hx IH
State after:
case empty
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
f : β → Set α
⊢ μ.real (⋃ b ∈ ∅, f b) ≤ ∑ p ∈ ∅, μ.real (f p)

case insert
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
f : β → Set α
x : β
s : Finset β
hx : x ∉ s
IH : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
⊢ μ.real (⋃ b ∈ insert x s, f b) ≤ ∑ p ∈ insert x s, μ.real (f p)

State before:
case empty
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
f : β → Set α
⊢ μ.real (⋃ b ∈ ∅, f b) ≤ ∑ p ∈ ∅, μ.real (f p)
Tactic:
simp
State after:
no goals

State before:
case insert
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
f : β → Set α
x : β
s : Finset β
hx : x ∉ s
IH : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
⊢ μ.real (⋃ b ∈ insert x s, f b) ≤ ∑ p ∈ insert x s, μ.real (f p)
Tactic:
simp only [hx, Finset.mem_insert, iUnion_iUnion_eq_or_left, not_false_eq_true,
  Finset.sum_insert]
State after:
case insert
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
f : β → Set α
x : β
s : Finset β
hx : x ∉ s
IH : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
⊢ μ.real (f x ∪ ⋃ x ∈ s, f x) ≤ μ.real (f x) + ∑ p ∈ s, μ.real (f p)

State before:
case insert
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
f : β → Set α
x : β
s : Finset β
hx : x ∉ s
IH : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
⊢ μ.real (f x ∪ ⋃ x ∈ s, f x) ≤ μ.real (f x) + ∑ p ∈ s, μ.real (f p)
Tactic:
exact (measureReal_union_le _ _).trans (by gcongr)
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s✝ s₁ s₂ t : Set α
f : β → Set α
x : β
s : Finset β
hx : x ∉ s
IH : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
⊢ μ.real (f x) + μ.real (⋃ x ∈ s, f x) ≤ μ.real (f x) + ∑ p ∈ s, μ.real (f p)
Tactic:
gcongr
State after:
no goals