case refine'_1
α : Type u_1
β : Type ?u.33782
γ : Type ?u.33785
δ : Type ?u.33788
ι : Type ?u.33791
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : ↑↑μ (s ∪ t) < ⊤
⊢ ↑↑μ s < ⊤

case refine'_2
α : Type u_1
β : Type ?u.33782
γ : Type ?u.33785
δ : Type ?u.33788
ι : Type ?u.33791
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : ↑↑μ (s ∪ t) < ⊤
⊢ ↑↑μ t < ⊤
α : Type u_1
β : Type ?u.33782
γ : Type ?u.33785
δ : Type ?u.33788
ι : Type ?u.33791
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
⊢ ↑↑μ (s ∪ t) < ⊤ ↔ ↑↑μ s < ⊤ ∧ ↑↑μ t < ⊤
refine' ⟨fun h => ⟨_, _⟩, fun h => measure_union_lt_top h.1 h.2⟩
no goals
case refine'_1
α : Type u_1
β : Type ?u.33782
γ : Type ?u.33785
δ : Type ?u.33788
ι : Type ?u.33791
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : ↑↑μ (s ∪ t) < ⊤
⊢ ↑↑μ s < ⊤
exact (measure_mono (Set.subset_union_left s t)).trans_lt h
no goals
case refine'_2
α : Type u_1
β : Type ?u.33782
γ : Type ?u.33785
δ : Type ?u.33788
ι : Type ?u.33791
inst✝ : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
h : ↑↑μ (s ∪ t) < ⊤
⊢ ↑↑μ t < ⊤
exact (measure_mono (Set.subset_union_right s t)).trans_lt h