Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case h
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
μ' μ : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : IsFiniteMeasureOnCompacts μ'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst✝⁹] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst✝⁹, _] f
hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure[inst✝⁹] s)
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst✝⁹] t
t_comp : IsCompact t
st : s ⊆ t
A : μ' t - ν s ≤ μ' t - μ' s
B : μ' t = ν t
⊢ μ' s ≤ μ' t

pp: case h'
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
μ' μ : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : IsFiniteMeasureOnCompacts μ'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst✝⁹] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst✝⁹, _] f
hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure[inst✝⁹] s)
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst✝⁹] t
t_comp : IsCompact t
st : s ⊆ t
A : μ' t - ν s ≤ μ' t - μ' s
B : μ' t = ν t
⊢ μ' t ≠ ∞

pp: G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
μ' μ : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : IsFiniteMeasureOnCompacts μ'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst✝⁹] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst✝⁹, _] f
hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure[inst✝⁹] s)
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst✝⁹] t
t_comp : IsCompact t
st : s ⊆ t
A : ν t - ν s ≤ μ' (t \ s)
B : μ' t = ν t
⊢ μ' s ≠ ∞

pp: G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
μ' μ : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : IsFiniteMeasureOnCompacts μ'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst✝⁹] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst✝⁹, _] f
hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure[inst✝⁹] s)
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst✝⁹] t
t_comp : IsCompact t
st : s ⊆ t
A : ν (t \ s) ≤ μ' (t \ s)
B : μ' t = ν t
⊢ ν s ≠ ∞

Tactic:
· exact measure_mono st

Goal state after:
case h'
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
μ' μ : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : IsFiniteMeasureOnCompacts μ'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst✝⁹] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst✝⁹, _] f
hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure[inst✝⁹] s)
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst✝⁹] t
t_comp : IsCompact t
st : s ⊆ t
A : μ' t - ν s ≤ μ' t - μ' s
B : μ' t = ν t
⊢ μ' t ≠ ∞

G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
μ' μ : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : IsFiniteMeasureOnCompacts μ'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst✝⁹] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst✝⁹, _] f
hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure[inst✝⁹] s)
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst✝⁹] t
t_comp : IsCompact t
st : s ⊆ t
A : ν t - ν s ≤ μ' (t \ s)
B : μ' t = ν t
⊢ μ' s ≠ ∞

G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
inst✝⁴ : LocallyCompactSpace G
μ' μ : Measure G
inst✝³ : μ.IsHaarMeasure
inst✝² : IsFiniteMeasureOnCompacts μ'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : μ.InnerRegularCompactLTTop
s : Set G
hs : MeasurableSet s
h's : IsCompact (closure[inst✝⁹] s)
ν : Measure G := μ'.haarScalarFactor μ • μ
f : G → ℝ
f_cont : Continuous[inst✝⁹, _] f
hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure[inst✝⁹] s)
f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }
t : Set G := f ⁻¹' {1}
t_closed : IsClosed[inst✝⁹] t
t_comp : IsCompact t
st : s ⊆ t
A : ν (t \ s) ≤ μ' (t \ s)
B : μ' t = ν t
⊢ ν s ≠ ∞