case h
α : Type u_1
β : Type ?u.293388
γ : Type ?u.293391
δ : Type ?u.293394
ι : Type ?u.293397
R : Type ?u.293400
R' : Type ?u.293403
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
ht : NullMeasurableSet t
u : Set α
hu : MeasurableSet u
⊢ ↑↑(restrict μ (s ∩ t) + restrict μ (s \ t)) u = ↑↑(restrict μ s) u
α : Type u_1
β : Type ?u.293388
γ : Type ?u.293391
δ : Type ?u.293394
ι : Type ?u.293397
R : Type ?u.293400
R' : Type ?u.293403
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
ht : NullMeasurableSet t
⊢ restrict μ (s ∩ t) + restrict μ (s \ t) = restrict μ s
ext1 u hu
case h
α : Type u_1
β : Type ?u.293388
γ : Type ?u.293391
δ : Type ?u.293394
ι : Type ?u.293397
R : Type ?u.293400
R' : Type ?u.293403
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
ht : NullMeasurableSet t
u : Set α
hu : MeasurableSet u
⊢ ↑↑μ (u ∩ s ∩ t) + ↑↑μ (u ∩ s ∩ tᶜ) = ↑↑μ (u ∩ s)
case h
α : Type u_1
β : Type ?u.293388
γ : Type ?u.293391
δ : Type ?u.293394
ι : Type ?u.293397
R : Type ?u.293400
R' : Type ?u.293403
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
ht : NullMeasurableSet t
u : Set α
hu : MeasurableSet u
⊢ ↑↑(restrict μ (s ∩ t) + restrict μ (s \ t)) u = ↑↑(restrict μ s) u
simp only [add_apply, restrict_apply hu, ← inter_assoc, diff_eq]
no goals
case h
α : Type u_1
β : Type ?u.293388
γ : Type ?u.293391
δ : Type ?u.293394
ι : Type ?u.293397
R : Type ?u.293400
R' : Type ?u.293403
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t s : Set α
ht : NullMeasurableSet t
u : Set α
hu : MeasurableSet u
⊢ ↑↑μ (u ∩ s ∩ t) + ↑↑μ (u ∩ s ∩ tᶜ) = ↑↑μ (u ∩ s)
exact measure_inter_add_diff₀ (u ∩ s) ht