α : Type u_2
β : Type u_1
γ : Type ?u.4498636
δ : Type ?u.4498639
ι : Type ?u.4498642
R : Type ?u.4498645
R' : Type ?u.4498648
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ ↑↑μ ((indicator s f ⁻¹' t)ᶜ) = 0 ↔ ↑↑(Measure.restrict μ s) ((f ⁻¹' t)ᶜ) = 0
α : Type u_2
β : Type u_1
γ : Type ?u.4498636
δ : Type ?u.4498639
ι : Type ?u.4498642
R : Type ?u.4498645
R' : Type ?u.4498648
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ t ∈ Filter.map (indicator s f) (ae μ) ↔ t ∈ Filter.map f (ae (Measure.restrict μ s))
simp_rw [mem_map, mem_ae_iff]
α : Type u_2
β : Type u_1
γ : Type ?u.4498636
δ : Type ?u.4498639
ι : Type ?u.4498642
R : Type ?u.4498645
R' : Type ?u.4498648
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ ↑↑μ ((f ⁻¹' t ∩ s ∪ 0 ⁻¹' t \ s)ᶜ) = 0 ↔ ↑↑μ ((f ⁻¹' t)ᶜ ∩ s) = 0
α : Type u_2
β : Type u_1
γ : Type ?u.4498636
δ : Type ?u.4498639
ι : Type ?u.4498642
R : Type ?u.4498645
R' : Type ?u.4498648
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ ↑↑μ ((indicator s f ⁻¹' t)ᶜ) = 0 ↔ ↑↑(Measure.restrict μ s) ((f ⁻¹' t)ᶜ) = 0
rw [Measure.restrict_apply' hs, Set.indicator_preimage, Set.ite]
α : Type u_2
β : Type u_1
γ : Type ?u.4498636
δ : Type ?u.4498639
ι : Type ?u.4498642
R : Type ?u.4498645
R' : Type ?u.4498648
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ ↑↑μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ (0 ⁻¹' t \ s)ᶜ) = 0 ↔ ↑↑μ ((f ⁻¹' t)ᶜ ∩ s) = 0
α : Type u_2
β : Type u_1
γ : Type ?u.4498636
δ : Type ?u.4498639
ι : Type ?u.4498642
R : Type ?u.4498645
R' : Type ?u.4498648
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ ↑↑μ ((f ⁻¹' t ∩ s ∪ 0 ⁻¹' t \ s)ᶜ) = 0 ↔ ↑↑μ ((f ⁻¹' t)ᶜ ∩ s) = 0
simp_rw [Set.compl_union, Set.compl_inter]
α : Type u_2
β : Type u_1
γ : Type ?u.4498636
δ : Type ?u.4498639
ι : Type ?u.4498642
R : Type ?u.4498645
R' : Type ?u.4498648
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ ↑↑μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun x => 0) ⁻¹' t \ s)ᶜ) = 0 ↔ ↑↑μ ((f ⁻¹' t)ᶜ ∩ s) = 0
α : Type u_2
β : Type u_1
γ : Type ?u.4498636
δ : Type ?u.4498639
ι : Type ?u.4498642
R : Type ?u.4498645
R' : Type ?u.4498648
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ ↑↑μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ (0 ⁻¹' t \ s)ᶜ) = 0 ↔ ↑↑μ ((f ⁻¹' t)ᶜ ∩ s) = 0
change μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun _ => (0 : β)) ⁻¹' t \ s)ᶜ) = 0 ↔ μ ((f ⁻¹' t)ᶜ ∩ s) = 0
α : Type u_2
β : Type u_1
γ : Type ?u.4498636
δ : Type ?u.4498639
ι : Type ?u.4498642
R : Type ?u.4498645
R' : Type ?u.4498648
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ ↑↑μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ s) = 0 ↔ ↑↑μ ((f ⁻¹' t)ᶜ ∩ s) = 0
α : Type u_2
β : Type u_1
γ : Type ?u.4498636
δ : Type ?u.4498639
ι : Type ?u.4498642
R : Type ?u.4498645
R' : Type ?u.4498648
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ ↑↑μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ ((fun x => 0) ⁻¹' t \ s)ᶜ) = 0 ↔ ↑↑μ ((f ⁻¹' t)ᶜ ∩ s) = 0
simp only [ht, ← Set.compl_eq_univ_diff, compl_compl, Set.compl_union, if_true,
  Set.preimage_const]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.4498636
δ : Type ?u.4498639
ι : Type ?u.4498642
R : Type ?u.4498645
R' : Type ?u.4498648
inst✝¹ : MeasurableSpace α
μ : MeasureTheory.Measure α
s t✝ : Set α
f : α → β
inst✝ : Zero β
t : Set β
ht : 0 ∈ t
hs : MeasurableSet s
⊢ ↑↑μ (((f ⁻¹' t)ᶜ ∪ sᶜ) ∩ s) = 0 ↔ ↑↑μ ((f ⁻¹' t)ᶜ ∩ s) = 0
simp_rw [Set.union_inter_distrib_right, Set.compl_inter_self s, Set.union_empty]