Theorem: MeasureTheory.measure_diff_eq_top (Carleson/ToMathlib/MeasureReal.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
hs : μ s = ⊤
ht : μ t ≠ ⊤
⊢ μ (s \ t) = ⊤
Tactic:
contrapose! hs
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
ht : μ t ≠ ⊤
hs : μ (s \ t) ≠ ⊤
⊢ μ s ≠ ⊤

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
ht : μ t ≠ ⊤
hs : μ (s \ t) ≠ ⊤
⊢ μ s ≠ ⊤
Tactic:
apply ((measure_mono (subset_diff_union s t)).trans_lt _).ne
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
ht : μ t ≠ ⊤
hs : μ (s \ t) ≠ ⊤
⊢ μ (s \ t ∪ t) < ⊤

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
ht : μ t ≠ ⊤
hs : μ (s \ t) ≠ ⊤
⊢ μ (s \ t ∪ t) < ⊤
Tactic:
apply (measure_union_le _ _).trans_lt
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
ht : μ t ≠ ⊤
hs : μ (s \ t) ≠ ⊤
⊢ μ (s \ t) + μ t < ⊤

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t : Set α
ht : μ t ≠ ⊤
hs : μ (s \ t) ≠ ⊤
⊢ μ (s \ t) + μ t < ⊤
Tactic:
exact ENNReal.add_lt_top.2 ⟨hs.lt_top, ht.lt_top⟩
State after:
no goals