α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | t = g a}
⊢ 0 < ↑↑μ {a | g a = t}
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
⊢ 0 < ↑↑μ {a | g a = t}
have uni : {a : α | t ≤ g a} = {a : α | t < g a} ∪ {a : α | t = g a} := by
  ext a
  simp only [mem_setOf, mem_union]
  apply le_iff_lt_or_eq
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
⊢ 0 < ↑↑μ {a | g a = t}
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | t = g a}
⊢ 0 < ↑↑μ {a | g a = t}
rw [show {a : α | t = g a} = {a : α | g a = t} by simp_rw [eq_comm]] at uni
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
disj : {a | t < g a} ∩ {a | g a = t} = ∅
⊢ 0 < ↑↑μ {a | g a = t}
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
⊢ 0 < ↑↑μ {a | g a = t}
have disj : {a : α | t < g a} ∩ {a : α | g a = t} = ∅ := by
  ext a
  simp only [mem_inter_iff, mem_setOf, mem_empty_iff_false, iff_false_iff, not_and]
  exact ne_of_gt
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
disj : {a | t < g a} ∩ {a | g a = t} = ∅
μ_add : ↑↑μ {a | t ≤ g a} = ↑↑μ {a | t < g a} + ↑↑μ {a | g a = t}
⊢ 0 < ↑↑μ {a | g a = t}
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
disj : {a | t < g a} ∩ {a | g a = t} = ∅
⊢ 0 < ↑↑μ {a | g a = t}
have μ_add : μ {a : α | t ≤ g a} = μ {a : α | t < g a} + μ {a : α | g a = t} := by
  rw [uni,
    measure_union (disjoint_iff_inter_eq_empty.mpr disj)
      (g_mble (Finite.measurableSet (finite_singleton t)))]
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
disj : {a | t < g a} ∩ {a | g a = t} = ∅
μ_add : ↑↑μ {a | t ≤ g a} = ↑↑μ {a | t < g a} + ↑↑μ {a | g a = t}
con : ¬0 < ↑↑μ {a | g a = t}
⊢ False
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
disj : {a | t < g a} ∩ {a | g a = t} = ∅
μ_add : ↑↑μ {a | t ≤ g a} = ↑↑μ {a | t < g a} + ↑↑μ {a | g a = t}
⊢ 0 < ↑↑μ {a | g a = t}
by_contra con
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
disj : {a | t < g a} ∩ {a | g a = t} = ∅
μ_add : ↑↑μ {a | t ≤ g a} = ↑↑μ {a | t < g a} + ↑↑μ {a | g a = t}
con : ↑↑μ {a | g a = t} = 0
⊢ False
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
disj : {a | t < g a} ∩ {a | g a = t} = ∅
μ_add : ↑↑μ {a | t ≤ g a} = ↑↑μ {a | t < g a} + ↑↑μ {a | g a = t}
con : ¬0 < ↑↑μ {a | g a = t}
⊢ False
rw [not_lt, nonpos_iff_eq_zero] at con
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
disj : {a | t < g a} ∩ {a | g a = t} = ∅
μ_add : ↑↑μ {a | t ≤ g a} = ↑↑μ {a | t < g a}
con : ↑↑μ {a | g a = t} = 0
⊢ False
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
disj : {a | t < g a} ∩ {a | g a = t} = ∅
μ_add : ↑↑μ {a | t ≤ g a} = ↑↑μ {a | t < g a} + ↑↑μ {a | g a = t}
con : ↑↑μ {a | g a = t} = 0
⊢ False
rw [con, add_zero] at μ_add
no goals
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
disj : {a | t < g a} ∩ {a | g a = t} = ∅
μ_add : ↑↑μ {a | t ≤ g a} = ↑↑μ {a | t < g a}
con : ↑↑μ {a | g a = t} = 0
⊢ False
exact ht μ_add
case h
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
a : α
⊢ a ∈ {a | t ≤ g a} ↔ a ∈ {a | t < g a} ∪ {a | t = g a}
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
⊢ {a | t ≤ g a} = {a | t < g a} ∪ {a | t = g a}
ext a
case h
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
a : α
⊢ t ≤ g a ↔ t < g a ∨ t = g a
case h
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
a : α
⊢ a ∈ {a | t ≤ g a} ↔ a ∈ {a | t < g a} ∪ {a | t = g a}
simp only [mem_setOf, mem_union]
no goals
case h
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
a : α
⊢ t ≤ g a ↔ t < g a ∨ t = g a
apply le_iff_lt_or_eq
no goals
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | t = g a}
⊢ {a | t = g a} = {a | g a = t}
simp_rw [eq_comm]
case h
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
a : α
⊢ a ∈ {a | t < g a} ∩ {a | g a = t} ↔ a ∈ ∅
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
⊢ {a | t < g a} ∩ {a | g a = t} = ∅
ext a
case h
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
a : α
⊢ t < g a → ¬g a = t
case h
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
a : α
⊢ a ∈ {a | t < g a} ∩ {a | g a = t} ↔ a ∈ ∅
simp only [mem_inter_iff, mem_setOf, mem_empty_iff_false, iff_false_iff, not_and]
no goals
case h
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
a : α
⊢ t < g a → ¬g a = t
exact ne_of_gt
no goals
α : Type u_2
inst✝⁵ : MeasurableSpace α
μ : MeasureTheory.Measure α
β : Type ?u.395934
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSingletonClass β
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : MeasurableSpace R
inst✝ : MeasurableSingletonClass R
g : α → R
g_mble : Measurable g
t : R
ht : ↑↑μ {a | t ≤ g a} ≠ ↑↑μ {a | t < g a}
uni : {a | t ≤ g a} = {a | t < g a} ∪ {a | g a = t}
disj : {a | t < g a} ∩ {a | g a = t} = ∅
⊢ ↑↑μ {a | t ≤ g a} = ↑↑μ {a | t < g a} + ↑↑μ {a | g a = t}
rw [uni,
  measure_union (disjoint_iff_inter_eq_empty.mpr disj)
    (g_mble (Finite.measurableSet (finite_singleton t)))]