[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : MeasurableSpace M
inst✝² : SMul M α
inst✝¹ : MeasurableSMul M α
c : M
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
⊢ map (fun x => c • x) μ = μ
[PROOFSTEP]
ext1 s hs
[GOAL]
case h
G : Type u
M : Type v
α : Type w
s✝ : Set α
m : MeasurableSpace α
inst✝³ : MeasurableSpace M
inst✝² : SMul M α
inst✝¹ : MeasurableSMul M α
c : M
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑(map (fun x => c • x) μ) s = ↑↑μ s
[PROOFSTEP]
rw [map_apply (measurable_const_smul c) hs]
[GOAL]
case h
G : Type u
M : Type v
α : Type w
s✝ : Set α
m : MeasurableSpace α
inst✝³ : MeasurableSpace M
inst✝² : SMul M α
inst✝¹ : MeasurableSMul M α
c : M
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
s : Set α
hs : MeasurableSet s
⊢ ↑↑μ ((fun x x_1 => x • x_1) c ⁻¹' s) = ↑↑μ s
[PROOFSTEP]
exact SMulInvariantMeasure.measure_preimage_smul c hs
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
⊢ List.TFAE
    [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s, ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G), map (fun x => c • x) μ = μ, ∀ (c : G), MeasurePreserving fun x => c • x]
[PROOFSTEP]
tfae_have 1 ↔ 2
[GOAL]
case tfae_1_iff_2
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
⊢ SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
[PROOFSTEP]
exact ⟨fun h => h.1, fun h => ⟨h⟩⟩
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
⊢ List.TFAE
    [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s, ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G), map (fun x => c • x) μ = μ, ∀ (c : G), MeasurePreserving fun x => c • x]
[PROOFSTEP]
tfae_have 1 → 6
[GOAL]
case tfae_1_to_6
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
⊢ SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
[PROOFSTEP]
intro h c
[GOAL]
case tfae_1_to_6
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c✝ : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
h : SMulInvariantMeasure G α μ
c : G
⊢ map (fun x => c • x) μ = μ
[PROOFSTEP]
exact (measurePreserving_smul c μ).map_eq
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
⊢ List.TFAE
    [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s, ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G), map (fun x => c • x) μ = μ, ∀ (c : G), MeasurePreserving fun x => c • x]
[PROOFSTEP]
tfae_have 6 → 7
[GOAL]
case tfae_6_to_7
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
⊢ (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
[PROOFSTEP]
exact fun H c => ⟨measurable_const_smul c, H c⟩
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
⊢ List.TFAE
    [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s, ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G), map (fun x => c • x) μ = μ, ∀ (c : G), MeasurePreserving fun x => c • x]
[PROOFSTEP]
tfae_have 7 → 4
[GOAL]
case tfae_7_to_4
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
⊢ (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
[PROOFSTEP]
exact fun H c => (H c).measure_preimage_emb (measurableEmbedding_const_smul c)
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
⊢ List.TFAE
    [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s, ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G), map (fun x => c • x) μ = μ, ∀ (c : G), MeasurePreserving fun x => c • x]
[PROOFSTEP]
tfae_have 4 → 5
[GOAL]
case tfae_4_to_5
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
⊢ (∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s) → ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s
[PROOFSTEP]
exact fun H c s => by
  rw [← preimage_smul_inv]
  apply H
[GOAL]
G : Type u
M : Type v
α : Type w
s✝ : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c✝ : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
H : ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
c : G
s : Set α
⊢ ↑↑μ (c • s) = ↑↑μ s
[PROOFSTEP]
rw [← preimage_smul_inv]
[GOAL]
G : Type u
M : Type v
α : Type w
s✝ : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c✝ : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
H : ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
c : G
s : Set α
⊢ ↑↑μ ((fun x => c⁻¹ • x) ⁻¹' s) = ↑↑μ s
[PROOFSTEP]
apply H
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s) → ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s
⊢ List.TFAE
    [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s, ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G), map (fun x => c • x) μ = μ, ∀ (c : G), MeasurePreserving fun x => c • x]
[PROOFSTEP]
tfae_have 5 → 3
[GOAL]
case tfae_5_to_3
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s) → ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s
⊢ (∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s) → ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s
[PROOFSTEP]
exact fun H c s _ => H c s
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s) → ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s
tfae_5_to_3 :
  (∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s) → ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s
⊢ List.TFAE
    [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s, ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G), map (fun x => c • x) μ = μ, ∀ (c : G), MeasurePreserving fun x => c • x]
[PROOFSTEP]
tfae_have 3 → 2
[GOAL]
case tfae_3_to_2
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s) → ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s
tfae_5_to_3 :
  (∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s) → ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s
⊢ (∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s) →
    ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
[PROOFSTEP]
intro H c s hs
[GOAL]
case tfae_3_to_2
G : Type u
M : Type v
α : Type w
s✝ : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c✝ : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s) → ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s
tfae_5_to_3 :
  (∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s) → ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s
H : ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s
c : G
s : Set α
hs : MeasurableSet s
⊢ ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
[PROOFSTEP]
rw [preimage_smul]
[GOAL]
case tfae_3_to_2
G : Type u
M : Type v
α : Type w
s✝ : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c✝ : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s) → ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s
tfae_5_to_3 :
  (∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s) → ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s
H : ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s
c : G
s : Set α
hs : MeasurableSet s
⊢ ↑↑μ (c⁻¹ • s) = ↑↑μ s
[PROOFSTEP]
exact H c⁻¹ s hs
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
c : G
μ : Measure α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving fun x => c • x
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving fun x => c • x) → ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s) → ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s
tfae_5_to_3 :
  (∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s) → ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s
tfae_3_to_2 :
  (∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s) →
    ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s
⊢ List.TFAE
    [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G) (s : Set α), ↑↑μ ((fun x => c • x) ⁻¹' s) = ↑↑μ s, ∀ (c : G) (s : Set α), ↑↑μ (c • s) = ↑↑μ s,
      ∀ (c : G), map (fun x => c • x) μ = μ, ∀ (c : G), MeasurePreserving fun x => c • x]
[PROOFSTEP]
tfae_finish
[GOAL]
G : Type u
M : Type v
α : Type w
s✝ : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c✝ : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : NullMeasurableSet s
c : G
⊢ NullMeasurableSet (c • s)
[PROOFSTEP]
simpa only [← preimage_smul_inv] using hs.preimage (measurePreserving_smul _ _).quasiMeasurePreserving
[GOAL]
G : Type u
M : Type v
α : Type w
s✝ : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c✝ : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
h : ↑↑μ s = 0
c : G
⊢ ↑↑μ (c • s) = 0
[PROOFSTEP]
rwa [measure_smul]
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
c : G
μ : Measure α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousConstSMul G α
inst✝ : MulAction.IsMinimal G α
K U : Set α
hK : IsCompact K
hμK : ↑↑μ K ≠ 0
hU : IsOpen U
hne : Set.Nonempty U
t : Finset G
ht : K ⊆ ⋃ (g : G) (_ : g ∈ t), g • U
hμU : ↑↑μ U = 0
x✝¹ : G
x✝ : x✝¹ ∈ ↑t
⊢ ↑↑μ (x✝¹ • U) = 0
[PROOFSTEP]
rwa [measure_smul]
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
c : G
μ : Measure α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousConstSMul G α
inst✝ : MulAction.IsMinimal G α
K U : Set α
hU : IsOpen U
hne : Set.Nonempty U
hμU : ↑↑μ U ≠ ⊤
x : α
g : G
hg : g • x ∈ U
⊢ ↑↑μ ((fun x x_1 => x • x_1) g ⁻¹' U) ≠ ⊤
[PROOFSTEP]
rwa [measure_preimage_smul]
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSMul G α
c : G
μ : Measure α
inst✝⁴ : SMulInvariantMeasure G α μ
inst✝³ : TopologicalSpace α
inst✝² : ContinuousConstSMul G α
inst✝¹ : MulAction.IsMinimal G α
K U : Set α
inst✝ : Regular μ
hμ : μ ≠ 0
hU : IsOpen U
⊢ ↑↑μ U = 0 ↔ U = ∅
[PROOFSTEP]
rw [← not_iff_not, ← Ne.def, ← pos_iff_ne_zero, measure_pos_iff_nonempty_of_smulInvariant G hμ hU,
  nonempty_iff_ne_empty]
[GOAL]
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x y : G
hs : x • s =ᶠ[ae μ] s
hy : y ∈ Subgroup.zpowers x
⊢ y • s =ᶠ[ae μ] s
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp hy
[GOAL]
case intro
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
⊢ x ^ k • s =ᶠ[ae μ] s
[PROOFSTEP]
let e : α ≃ α := MulAction.toPermHom G α x
[GOAL]
case intro
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
⊢ x ^ k • s =ᶠ[ae μ] s
[PROOFSTEP]
have he : QuasiMeasurePreserving e μ μ := (measurePreserving_smul x μ).quasiMeasurePreserving
[GOAL]
case intro
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
he : QuasiMeasurePreserving ↑e
⊢ x ^ k • s =ᶠ[ae μ] s
[PROOFSTEP]
have he' : QuasiMeasurePreserving e.symm μ μ := (measurePreserving_smul x⁻¹ μ).quasiMeasurePreserving
[GOAL]
case intro
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
⊢ x ^ k • s =ᶠ[ae μ] s
[PROOFSTEP]
have h := he.image_zpow_ae_eq he' k hs
[GOAL]
case intro
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
h : ↑(e ^ k) '' s =ᶠ[ae μ] s
⊢ x ^ k • s =ᶠ[ae μ] s
[PROOFSTEP]
simp only [← MonoidHom.map_zpow] at h 
[GOAL]
case intro
G : Type u
M : Type v
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableSMul G α
c : G
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x : G
hs : x • s =ᶠ[ae μ] s
k : ℤ
hy : x ^ k ∈ Subgroup.zpowers x
e : α ≃ α := ↑(MulAction.toPermHom G α) x
he : QuasiMeasurePreserving ↑e
he' : QuasiMeasurePreserving ↑e.symm
h : (fun a => ↑(↑(MulAction.toPermHom G α) (x ^ k)) a) '' s =ᶠ[ae μ] s
⊢ x ^ k • s =ᶠ[ae μ] s
[PROOFSTEP]
simpa only [MulAction.toPermHom_apply, MulAction.toPerm_apply, image_smul] using h
[GOAL]
G✝ : Type u
M : Type v
α✝ : Type w
s✝ : Set α✝
m✝ : MeasurableSpace α✝
inst✝⁹ : Group G✝
inst✝⁸ : MulAction G✝ α✝
inst✝⁷ : MeasurableSpace G✝
inst✝⁶ : MeasurableSMul G✝ α✝
c : G✝
μ✝ : Measure α✝
inst✝⁵ : SMulInvariantMeasure G✝ α✝ μ✝
G : Type u
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : AddGroup G
inst✝³ : AddAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableVAdd G α
μ : Measure α
inst✝ : VAddInvariantMeasure G α μ
x y : G
hs : x +ᵥ s =ᶠ[ae μ] s
hy : y ∈ AddSubgroup.zmultiples x
⊢ y +ᵥ s =ᶠ[ae μ] s
[PROOFSTEP]
letI : MeasurableSpace (Multiplicative G) := (inferInstanceAs (MeasurableSpace G))
[GOAL]
G✝ : Type u
M : Type v
α✝ : Type w
s✝ : Set α✝
m✝ : MeasurableSpace α✝
inst✝⁹ : Group G✝
inst✝⁸ : MulAction G✝ α✝
inst✝⁷ : MeasurableSpace G✝
inst✝⁶ : MeasurableSMul G✝ α✝
c : G✝
μ✝ : Measure α✝
inst✝⁵ : SMulInvariantMeasure G✝ α✝ μ✝
G : Type u
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : AddGroup G
inst✝³ : AddAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableVAdd G α
μ : Measure α
inst✝ : VAddInvariantMeasure G α μ
x y : G
hs : x +ᵥ s =ᶠ[ae μ] s
hy : y ∈ AddSubgroup.zmultiples x
this : MeasurableSpace (Multiplicative G) := inferInstanceAs (MeasurableSpace G)
⊢ y +ᵥ s =ᶠ[ae μ] s
[PROOFSTEP]
letI : SMulInvariantMeasure (Multiplicative G) α μ :=
  ⟨fun g => VAddInvariantMeasure.measure_preimage_vadd (Multiplicative.toAdd g)⟩
[GOAL]
G✝ : Type u
M : Type v
α✝ : Type w
s✝ : Set α✝
m✝ : MeasurableSpace α✝
inst✝⁹ : Group G✝
inst✝⁸ : MulAction G✝ α✝
inst✝⁷ : MeasurableSpace G✝
inst✝⁶ : MeasurableSMul G✝ α✝
c : G✝
μ✝ : Measure α✝
inst✝⁵ : SMulInvariantMeasure G✝ α✝ μ✝
G : Type u
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : AddGroup G
inst✝³ : AddAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableVAdd G α
μ : Measure α
inst✝ : VAddInvariantMeasure G α μ
x y : G
hs : x +ᵥ s =ᶠ[ae μ] s
hy : y ∈ AddSubgroup.zmultiples x
this✝ : MeasurableSpace (Multiplicative G) := inferInstanceAs (MeasurableSpace G)
this : SMulInvariantMeasure (Multiplicative G) α μ :=
  { measure_preimage_smul := fun g => VAddInvariantMeasure.measure_preimage_vadd (↑Multiplicative.toAdd g) }
⊢ y +ᵥ s =ᶠ[ae μ] s
[PROOFSTEP]
letI : MeasurableSMul (Multiplicative G) α :=
  { measurable_const_smul := fun g => measurable_const_vadd (Multiplicative.toAdd g)
    measurable_smul_const := fun a =>
      @measurable_vadd_const (Multiplicative G) α (inferInstanceAs (VAdd G α)) _ _
        (inferInstanceAs (MeasurableVAdd G α)) a }
[GOAL]
G✝ : Type u
M : Type v
α✝ : Type w
s✝ : Set α✝
m✝ : MeasurableSpace α✝
inst✝⁹ : Group G✝
inst✝⁸ : MulAction G✝ α✝
inst✝⁷ : MeasurableSpace G✝
inst✝⁶ : MeasurableSMul G✝ α✝
c : G✝
μ✝ : Measure α✝
inst✝⁵ : SMulInvariantMeasure G✝ α✝ μ✝
G : Type u
α : Type w
s : Set α
m : MeasurableSpace α
inst✝⁴ : AddGroup G
inst✝³ : AddAction G α
inst✝² : MeasurableSpace G
inst✝¹ : MeasurableVAdd G α
μ : Measure α
inst✝ : VAddInvariantMeasure G α μ
x y : G
hs : x +ᵥ s =ᶠ[ae μ] s
hy : y ∈ AddSubgroup.zmultiples x
this✝¹ : MeasurableSpace (Multiplicative G) := inferInstanceAs (MeasurableSpace G)
this✝ : SMulInvariantMeasure (Multiplicative G) α μ :=
  { measure_preimage_smul := fun g => VAddInvariantMeasure.measure_preimage_vadd (↑Multiplicative.toAdd g) }
this : MeasurableSMul (Multiplicative G) α :=
  { measurable_const_smul := fun g => measurable_const_vadd (↑Multiplicative.toAdd g),
    measurable_smul_const := fun a => measurable_vadd_const a }
⊢ y +ᵥ s =ᶠ[ae μ] s
[PROOFSTEP]
exact @smul_ae_eq_self_of_mem_zpowers (Multiplicative G) α _ _ _ _ _ _ _ _ _ _ hs hy
