α : Type u_1
β : Type ?u.22040
γ : Type ?u.22043
p : Pmf α
s t : Set α
x : MeasurableSpace α
hx : x ∈ Set.range fun i => OuterMeasure.caratheodory (↑p i • dirac i)
⊢ ⊤ ≤ x
α : Type u_1
β : Type ?u.22040
γ : Type ?u.22043
p : Pmf α
s t : Set α
⊢ OuterMeasure.caratheodory (toOuterMeasure p) = ⊤
refine' eq_top_iff.2 <| le_trans (le_sInf fun x hx => _) (le_sum_caratheodory _)
α : Type u_1
β : Type ?u.22040
γ : Type ?u.22043
p : Pmf α
s t : Set α
x : MeasurableSpace α
hx : x ∈ Set.range fun i => OuterMeasure.caratheodory (↑p i • dirac i)
y : α
hy : (fun i => OuterMeasure.caratheodory (↑p i • dirac i)) y = x
⊢ ⊤ ≤ x
α : Type u_1
β : Type ?u.22040
γ : Type ?u.22043
p : Pmf α
s t : Set α
x : MeasurableSpace α
hx : x ∈ Set.range fun i => OuterMeasure.caratheodory (↑p i • dirac i)
⊢ ⊤ ≤ x
have ⟨y, hy⟩ := hx
no goals
α : Type u_1
β : Type ?u.22040
γ : Type ?u.22043
p : Pmf α
s t : Set α
x : MeasurableSpace α
hx : x ∈ Set.range fun i => OuterMeasure.caratheodory (↑p i • dirac i)
y : α
hy : (fun i => OuterMeasure.caratheodory (↑p i • dirac i)) y = x
⊢ ⊤ ≤ x
exact
  ((le_of_eq (dirac_caratheodory y).symm).trans (le_smul_caratheodory _ _)).trans (le_of_eq hy)