α : Type u_1
β : Type ?u.144519
γ : Type ?u.144522
δ : Type ?u.144525
ι : Type ?u.144528
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
⊢ ↑↑μ
      (if h : ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s then Exists.choose h
      else
        if h' : ∃ t x, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t ∩ u) = ↑↑μ (s ∩ u) then
          Exists.choose h'
        else Exists.choose (_ : ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = ↑↑μ s)) =
    ↑↑μ s
α : Type u_1
β : Type ?u.144519
γ : Type ?u.144522
δ : Type ?u.144525
ι : Type ?u.144528
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
⊢ ↑↑μ (toMeasurable μ s) = ↑↑μ s
rw [toMeasurable_def]
case inl
α : Type u_1
β : Type ?u.144519
γ : Type ?u.144522
δ : Type ?u.144525
ι : Type ?u.144528
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
hs : ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
⊢ ↑↑μ (Exists.choose hs) = ↑↑μ s

case inr.inl
α : Type u_1
β : Type ?u.144519
γ : Type ?u.144522
δ : Type ?u.144525
ι : Type ?u.144528
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
hs : ¬∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ∃ t x, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t ∩ u) = ↑↑μ (s ∩ u)
⊢ ↑↑μ (Exists.choose h's) = ↑↑μ s

case inr.inr
α : Type u_1
β : Type ?u.144519
γ : Type ?u.144522
δ : Type ?u.144525
ι : Type ?u.144528
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
hs : ¬∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ¬∃ t x, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t ∩ u) = ↑↑μ (s ∩ u)
⊢ ↑↑μ (Exists.choose (_ : ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = ↑↑μ s)) = ↑↑μ s
α : Type u_1
β : Type ?u.144519
γ : Type ?u.144522
δ : Type ?u.144525
ι : Type ?u.144528
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
⊢ ↑↑μ
      (if h : ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s then Exists.choose h
      else
        if h' : ∃ t x, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t ∩ u) = ↑↑μ (s ∩ u) then
          Exists.choose h'
        else Exists.choose (_ : ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = ↑↑μ s)) =
    ↑↑μ s
split_ifs with hs h's
no goals
case inl
α : Type u_1
β : Type ?u.144519
γ : Type ?u.144522
δ : Type ?u.144525
ι : Type ?u.144528
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
hs : ∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
⊢ ↑↑μ (Exists.choose hs) = ↑↑μ s
exact measure_congr hs.choose_spec.snd.2
no goals
case inr.inl
α : Type u_1
β : Type ?u.144519
γ : Type ?u.144522
δ : Type ?u.144525
ι : Type ?u.144528
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
hs : ¬∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ∃ t x, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t ∩ u) = ↑↑μ (s ∩ u)
⊢ ↑↑μ (Exists.choose h's) = ↑↑μ s
simpa only [inter_univ] using h's.choose_spec.snd.2 univ MeasurableSet.univ
no goals
case inr.inr
α : Type u_1
β : Type ?u.144519
γ : Type ?u.144522
δ : Type ?u.144525
ι : Type ?u.144528
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s✝ s₁ s₂ t s : Set α
hs : ¬∃ t x, MeasurableSet t ∧ t =ᵐ[μ] s
h's : ¬∃ t x, MeasurableSet t ∧ ∀ (u : Set α), MeasurableSet u → ↑↑μ (t ∩ u) = ↑↑μ (s ∩ u)
⊢ ↑↑μ (Exists.choose (_ : ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑↑μ t = ↑↑μ s)) = ↑↑μ s
exact (exists_measurable_superset μ s).choose_spec.2.2