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

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : autoParam (μ s₂ ≠ ⊤) _auto✝
h₂ : autoParam (μ t₂ ≠ ⊤) _auto✝
⊢ μ.real (s₁ ∪ t₁) = μ.real (s₂ ∪ t₂)
Tactic:
simp [measureReal_def]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : autoParam (μ s₂ ≠ ⊤) _auto✝
h₂ : autoParam (μ t₂ ≠ ⊤) _auto✝
⊢ (μ (s₁ ∪ t₁)).toReal = (μ (s₂ ∪ t₂)).toReal

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : autoParam (μ s₂ ≠ ⊤) _auto✝
h₂ : autoParam (μ t₂ ≠ ⊤) _auto✝
⊢ (μ (s₁ ∪ t₁)).toReal = (μ (s₂ ∪ t₂)).toReal
Tactic:
rw [measure_union_congr_of_subset hs _ ht]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : autoParam (μ s₂ ≠ ⊤) _auto✝
h₂ : autoParam (μ t₂ ≠ ⊤) _auto✝
⊢ μ t₂ ≤ μ t₁

ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : autoParam (μ s₂ ≠ ⊤) _auto✝
h₂ : autoParam (μ t₂ ≠ ⊤) _auto✝
⊢ μ s₂ ≤ μ s₁

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : autoParam (μ s₂ ≠ ⊤) _auto✝
h₂ : autoParam (μ t₂ ≠ ⊤) _auto✝
⊢ μ t₂ ≤ μ t₁
Tactic:
exact (ENNReal.toReal_le_toReal h₂ (measure_ne_top_of_subset ht h₂)).1 htμ
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s s₁ s₂ t t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : autoParam (μ s₂ ≠ ⊤) _auto✝
h₂ : autoParam (μ t₂ ≠ ⊤) _auto✝
⊢ μ s₂ ≤ μ s₁
Tactic:
exact (ENNReal.toReal_le_toReal h₁ (measure_ne_top_of_subset hs h₁)).1 hsμ
State after:
no goals