α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
⊢ ↑↑μ {a | ¬(f '' s) a = (f '' t) a} = 0
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : s =ᶠ[ae (comap f μ)] t
⊢ f '' s =ᶠ[ae μ] f '' t
rw [EventuallyEq, ae_iff] at hst⊢
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
⊢ ↑↑μ {a | ¬(f '' s) a = (f '' t) a} = 0
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
⊢ ↑↑μ {a | ¬(f '' s) a = (f '' t) a} = 0
have h_eq_α : { a : α | ¬s a = t a } = s \ t ∪ t \ s := by
  ext1 x
  simp only [eq_iff_iff, mem_setOf_eq, mem_union, mem_diff]
  tauto
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' s \ f '' t ∪ f '' t \ f '' s
⊢ ↑↑μ {a | ¬(f '' s) a = (f '' t) a} = 0
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
⊢ ↑↑μ {a | ¬(f '' s) a = (f '' t) a} = 0
have h_eq_β : { a : β | ¬(f '' s) a = (f '' t) a } = f '' s \ f '' t ∪ f '' t \ f '' s := by
  ext1 x
  simp only [eq_iff_iff, mem_setOf_eq, mem_union, mem_diff]
  tauto
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
⊢ ↑↑μ {a | ¬(f '' s) a = (f '' t) a} = 0
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' s \ f '' t ∪ f '' t \ f '' s
⊢ ↑↑μ {a | ¬(f '' s) a = (f '' t) a} = 0
rw [← Set.image_diff hfi, ← Set.image_diff hfi, ← Set.image_union] at h_eq_β
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
⊢ ↑↑μ (f '' (s \ t ∪ t \ s)) = 0
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
⊢ ↑↑μ {a | ¬(f '' s) a = (f '' t) a} = 0
rw [h_eq_β]
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) (s \ t ∪ t \ s) = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
⊢ ↑↑μ (f '' (s \ t ∪ t \ s)) = 0
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
⊢ ↑↑μ (f '' (s \ t ∪ t \ s)) = 0
rw [h_eq_α] at hst
no goals
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) (s \ t ∪ t \ s) = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
h_eq_β : {a | ¬(f '' s) a = (f '' t) a} = f '' (s \ t ∪ t \ s)
⊢ ↑↑μ (f '' (s \ t ∪ t \ s)) = 0
exact measure_image_eq_zero_of_comap_eq_zero f μ hfi hf hst
case h
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
x : α
⊢ x ∈ {a | ¬s a = t a} ↔ x ∈ s \ t ∪ t \ s
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
⊢ {a | ¬s a = t a} = s \ t ∪ t \ s
ext1 x
case h
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
x : α
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ ¬x ∈ t ∨ x ∈ t ∧ ¬x ∈ s
case h
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
x : α
⊢ x ∈ {a | ¬s a = t a} ↔ x ∈ s \ t ∪ t \ s
simp only [eq_iff_iff, mem_setOf_eq, mem_union, mem_diff]
no goals
case h
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
x : α
⊢ ¬(s x ↔ t x) ↔ x ∈ s ∧ ¬x ∈ t ∨ x ∈ t ∧ ¬x ∈ s
tauto
case h
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
x : β
⊢ x ∈ {a | ¬(f '' s) a = (f '' t) a} ↔ x ∈ f '' s \ f '' t ∪ f '' t \ f '' s
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
⊢ {a | ¬(f '' s) a = (f '' t) a} = f '' s \ f '' t ∪ f '' t \ f '' s
ext1 x
case h
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
x : β
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ ¬x ∈ f '' t ∨ x ∈ f '' t ∧ ¬x ∈ f '' s
case h
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
x : β
⊢ x ∈ {a | ¬(f '' s) a = (f '' t) a} ↔ x ∈ f '' s \ f '' t ∪ f '' t \ f '' s
simp only [eq_iff_iff, mem_setOf_eq, mem_union, mem_diff]
no goals
case h
α : Type u_2
β✝ : Type ?u.229583
γ : Type ?u.229586
δ : Type ?u.229589
ι : Type ?u.229592
R : Type ?u.229595
R' : Type ?u.229598
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β✝
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
β : Type u_1
inst✝ : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hfi : Injective f
hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s)
s t : Set α
hst : ↑↑(comap f μ) {a | ¬s a = t a} = 0
h_eq_α : {a | ¬s a = t a} = s \ t ∪ t \ s
x : β
⊢ ¬((f '' s) x ↔ (f '' t) x) ↔ x ∈ f '' s ∧ ¬x ∈ f '' t ∨ x ∈ f '' t ∧ ¬x ∈ f '' s
tauto