-- 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
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
⊢ [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_finish

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
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

Tactic:
tfae_have 3 → 2
| H, c, s, hs => by
  rw [preimage_smul]
  exact H c⁻¹ s hs

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
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
⊢ [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 α
⊢ [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 1 ↔ 2 := ⟨fun h => h.1, fun h => ⟨h⟩⟩

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
⊢ [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) μ = μ
⊢ [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 6 → 7 := fun H c => ⟨measurable_const_smul c, H 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) μ μ
⊢ [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