-- Mathlib/MeasureTheory/Group/Action.lean
theorem smulInvariantMeasure_tfae :
    List.TFAE
      [SMulInvariantMeasure G α μ,
        ∀ (c : G) (s), MeasurableSet s → μ ((c • ·) ⁻¹' s) = μ s,
        ∀ (c : G) (s), MeasurableSet s → μ (c • s) = μ s,
        ∀ (c : G) (s), μ ((c • ·) ⁻¹' s) = μ s,
        ∀ (c : G) (s), μ (c • s) = μ s,
        ∀ c : G, Measure.map (c • ·) μ = μ,
        ∀ c : G, MeasurePreserving (c • ·) μ μ]

Proof state:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
μ : Measure α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
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), Measure.map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), Measure.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

Tactic:
exact H c⁻¹ s hs

Result:
no goals

Proof state:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
μ : Measure α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
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), Measure.map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), Measure.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

Tactic:
apply H

Result:
no goals

Proof state:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
μ : Measure α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
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), Measure.map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), Measure.map (fun x => c • x) μ = μ) → ∀ (c : G), MeasurePreserving (fun x => c • x) μ μ
⊢ [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), Measure.map (fun x => c • x) μ = μ,
      ∀ (c : G), MeasurePreserving (fun x => c • x) μ μ].TFAE

Tactic:
tfae_have 7 → 4 := fun H c => (H c).measure_preimage_emb (measurableEmbedding_const_smul c)

Result:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
μ : Measure α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
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), Measure.map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), Measure.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
⊢ [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), Measure.map (fun x => c • x) μ = μ,
      ∀ (c : G), MeasurePreserving (fun x => c • x) μ μ].TFAE

Proof state:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
μ : Measure α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
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), Measure.map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), Measure.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
⊢ [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), Measure.map (fun x => c • x) μ = μ,
      ∀ (c : G), MeasurePreserving (fun x => c • x) μ μ].TFAE

Tactic:
tfae_have 5 → 3 := fun H c s _ => H c s

Result:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝³ : Group G
inst✝² : MulAction G α
μ : Measure α
inst✝¹ : MeasurableSpace G
inst✝ : MeasurableSMul G α
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), Measure.map (fun x => c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), Measure.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
⊢ [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), Measure.map (fun x => c • x) μ = μ,
      ∀ (c : G), MeasurePreserving (fun x => c • x) μ μ].TFAE