case a
α : Type u_1
β : Type ?u.587542
γ : Type ?u.587545
δ : Type ?u.587548
ι : Type ?u.587551
R : Type ?u.587554
R' : Type ?u.587557
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
hs : MeasurableSet s
t : Set α
⊢ t ∈ ae (Measure.restrict μ s) ↔ t ∈ ae μ ⊓ 𝓟 s
α : Type u_1
β : Type ?u.587542
γ : Type ?u.587545
δ : Type ?u.587548
ι : Type ?u.587551
R : Type ?u.587554
R' : Type ?u.587557
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hs : MeasurableSet s
⊢ ae (Measure.restrict μ s) = ae μ ⊓ 𝓟 s
ext t
case a
α : Type u_1
β : Type ?u.587542
γ : Type ?u.587545
δ : Type ?u.587548
ι : Type ?u.587551
R : Type ?u.587554
R' : Type ?u.587557
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
hs : MeasurableSet s
t : Set α
⊢ ↑↑μ (tᶜ ∩ s) = 0 ↔ ↑↑μ {a | ¬a ∈ t ∧ a ∈ s} = 0
case a
α : Type u_1
β : Type ?u.587542
γ : Type ?u.587545
δ : Type ?u.587548
ι : Type ?u.587551
R : Type ?u.587554
R' : Type ?u.587557
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
hs : MeasurableSet s
t : Set α
⊢ t ∈ ae (Measure.restrict μ s) ↔ t ∈ ae μ ⊓ 𝓟 s
simp only [mem_inf_principal, mem_ae_iff, restrict_apply_eq_zero' hs, compl_setOf, not_imp,
  fun a => and_comm (a := a ∈ s) (b := ¬a ∈ t)]
no goals
case a
α : Type u_1
β : Type ?u.587542
γ : Type ?u.587545
δ : Type ?u.587548
ι : Type ?u.587551
R : Type ?u.587554
R' : Type ?u.587557
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
hs : MeasurableSet s
t : Set α
⊢ ↑↑μ (tᶜ ∩ s) = 0 ↔ ↑↑μ {a | ¬a ∈ t ∧ a ∈ s} = 0
rfl