awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (goal)
Goal:
M : Type uM
α : Type uα
β : Type uβ
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : SMul M α
inst_3 : SMul M β
inst_4 : MeasurableConstSMul M β
μ : Measure α
inst_5 : SMulInvariantMeasure M α μ
f : α → β
hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a
hf : Measurable f
m : M
S : Set β
hS : MeasurableSet S
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' (fun (x : β) ↦ m • x) ⁻¹' S) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ m • f x) ⁻¹' S) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ m • f x) ⁻¹' S) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ m • f x) ⁻¹' S) : ℝ≥0∞)
Tactic: rw [preimage_preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (goal)
Goal:
M : Type uM
α : Type uα
β : Type uβ
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : SMul M α
inst_3 : SMul M β
inst_4 : MeasurableConstSMul M β
μ : Measure α
inst_5 : SMulInvariantMeasure M α μ
f : α → β
hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a
hf : Measurable f
m : M
S : Set β
hS : MeasurableSet S
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ f (m • x)) ⁻¹' S) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ m • x) ⁻¹' f ⁻¹' S) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (HSMul.hSMul m ⁻¹' f ⁻¹' S) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ m • x) ⁻¹' f ⁻¹' S) : ℝ≥0∞)
Tactic: rw [← preimage_preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (goal)
Goal:
M : Type uM
α : Type uα
β : Type uβ
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : SMul M α
inst_3 : SMul M β
inst_4 : MeasurableConstSMul M β
μ : Measure α
inst_5 : SMulInvariantMeasure M α μ
f : α → β
hsmul : ∀ (m : M) (a : α), f (m • a) = m • f a
hf : Measurable f
m : M
S : Set β
hS : MeasurableSet S
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ m • x) ⁻¹' f ⁻¹' S) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' S) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' S) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' S) : ℝ≥0∞)
Tactic: rw [SMulInvariantMeasure.measure_preimage_smul m (hS.preimage hf)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (hypothesis)
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : MeasurableConstSMul G α
⊢ [SMulInvariantMeasure G α μ,
      ∀ (c : G) (s : Set α),
        MeasurableSet s →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ, ∀ (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ].TFAE
have tfae_1_iff_2 : SMulInvariantMeasure G α μ ↔
  ∀ (c : G) (s : Set α),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: tfae_have 1 ↔ 2 := ⟨fun h => h.1, fun h => ⟨h⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (hypothesis)
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : MeasurableConstSMul G α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔
    ∀ (c : G) (s : Set α),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ [SMulInvariantMeasure G α μ,
      ∀ (c : G) (s : Set α),
        MeasurableSet s →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ, ∀ (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ].TFAE
have tfae_1_to_6 : ∀ (a : SMulInvariantMeasure G α μ) (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ
Tactic: tfae_have 1 → 6 := fun h c => (measurePreserving_smul c μ).map_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (hypothesis)
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : MeasurableConstSMul G α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔
    ∀ (c : G) (s : Set α),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
tfae_1_to_6 : ∀ (a : SMulInvariantMeasure G α μ) (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ
⊢ [SMulInvariantMeasure G α μ,
      ∀ (c : G) (s : Set α),
        MeasurableSet s →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ, ∀ (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ].TFAE
have tfae_6_to_7 : ∀ (a : ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ) (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ
Tactic: tfae_have 6 → 7 := fun H c => ⟨measurable_const_smul c, H c⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (hypothesis)
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : MeasurableConstSMul G α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔
    ∀ (c : G) (s : Set α),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
tfae_1_to_6 : ∀ (a : SMulInvariantMeasure G α μ) (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ
tfae_6_to_7 :
  ∀ (a : ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ) (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ
⊢ [SMulInvariantMeasure G α μ,
      ∀ (c : G) (s : Set α),
        MeasurableSet s →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ, ∀ (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ].TFAE
have tfae_7_to_4 : ∀ (a : ∀ (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ) (c : G) (s : Set α),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: tfae_have 7 → 4 := fun H c => (H c).measure_preimage_emb (measurableEmbedding_const_smul c)
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (goal)
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : MeasurableConstSMul G α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔
    ∀ (c : G) (s : Set α),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
tfae_1_to_6 : ∀ (a : SMulInvariantMeasure G α μ) (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ
tfae_6_to_7 :
  ∀ (a : ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ) (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ
tfae_7_to_4 :
  ∀ (a : ∀ (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ) (c : G) (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
H :
  ∀ (c : G) (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c : G
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c⁻¹ • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← preimage_smul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (hypothesis)
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : MeasurableConstSMul G α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔
    ∀ (c : G) (s : Set α),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
tfae_1_to_6 : ∀ (a : SMulInvariantMeasure G α μ) (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ
tfae_6_to_7 :
  ∀ (a : ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ) (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ
tfae_7_to_4 :
  ∀ (a : ∀ (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ) (c : G) (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ [SMulInvariantMeasure G α μ,
      ∀ (c : G) (s : Set α),
        MeasurableSet s →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ, ∀ (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ].TFAE
have tfae_4_to_5 : ∀
  (a :
    ∀ (c : G) (s : Set α),
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
  (c : G) (s : Set α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: tfae_have 4 → 5
  | H, c, s => by
    rw [← preimage_smul_inv]
    apply H
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (hypothesis)
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : MeasurableConstSMul G α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔
    ∀ (c : G) (s : Set α),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
tfae_1_to_6 : ∀ (a : SMulInvariantMeasure G α μ) (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ
tfae_6_to_7 :
  ∀ (a : ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ) (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ
tfae_7_to_4 :
  ∀ (a : ∀ (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ) (c : G) (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
tfae_4_to_5 :
  ∀
    (a :
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (c : G) (s : Set α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ [SMulInvariantMeasure G α μ,
      ∀ (c : G) (s : Set α),
        MeasurableSet s →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ, ∀ (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ].TFAE
have tfae_5_to_3 : ∀
  (a :
    ∀ (c : G) (s : Set α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
  (c : G) (s : Set α),
  MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: tfae_have 5 → 3 := fun H c s _ => H c s
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (goal)
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : MeasurableConstSMul G α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔
    ∀ (c : G) (s : Set α),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
tfae_1_to_6 : ∀ (a : SMulInvariantMeasure G α μ) (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ
tfae_6_to_7 :
  ∀ (a : ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ) (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ
tfae_7_to_4 :
  ∀ (a : ∀ (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ) (c : G) (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
tfae_4_to_5 :
  ∀
    (a :
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (c : G) (s : Set α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
tfae_5_to_3 :
  ∀
    (a :
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (c : G) (s : Set α),
    MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
H :
  ∀ (c : G) (s : Set α),
    MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
c : G
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c⁻¹ • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [preimage_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (hypothesis)
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : MeasurableConstSMul G α
tfae_1_iff_2 :
  SMulInvariantMeasure G α μ ↔
    ∀ (c : G) (s : Set α),
      MeasurableSet s →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
tfae_1_to_6 : ∀ (a : SMulInvariantMeasure G α μ) (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ
tfae_6_to_7 :
  ∀ (a : ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ) (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ
tfae_7_to_4 :
  ∀ (a : ∀ (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ) (c : G) (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
tfae_4_to_5 :
  ∀
    (a :
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (c : G) (s : Set α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
tfae_5_to_3 :
  ∀
    (a :
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
    (c : G) (s : Set α),
    MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ [SMulInvariantMeasure G α μ,
      ∀ (c : G) (s : Set α),
        MeasurableSet s →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
            ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
          ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G) (s : Set α),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞),
      ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ, ∀ (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ].TFAE
have tfae_3_to_2 : ∀
  (a :
    ∀ (c : G) (s : Set α),
      MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))
  (c : G) (s : Set α),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: tfae_have 3 → 2
  | H, c, s, hs => by
    rw [preimage_smul]
    exact H c⁻¹ s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (goal)
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
inst_3 : TopologicalSpace α
inst_4 : ContinuousConstSMul G α
inst_5 : MulAction.IsMinimal G α
U : Set α
inst_6 : μ.Regular
hμ : μ ≠ 0
hU : IsOpen[inst_3] U
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ U = ∅
have rw : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ ¬U = ∅
Tactic: rw [← not_iff_not, ← Ne, ← pos_iff_ne_zero,
    measure_pos_iff_nonempty_of_smulInvariant G hμ hU, nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (goal)
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
inst_3 : TopologicalSpace α
inst_4 : ContinuousConstSMul G α
inst_5 : MulAction.IsMinimal G α
U : Set α
inst_6 : μ.Regular
hμ : μ ≠ 0
hU : IsOpen[inst_3] U
rw : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ ¬U = ∅
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ U = ∅
have rw₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ ¬U = ∅
Tactic: rw [← not_iff_not, ← Ne, ← pos_iff_ne_zero,
    measure_pos_iff_nonempty_of_smulInvariant G hμ hU, nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (goal)
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
inst_3 : TopologicalSpace α
inst_4 : ContinuousConstSMul G α
inst_5 : MulAction.IsMinimal G α
U : Set α
inst_6 : μ.Regular
hμ : μ ≠ 0
hU : IsOpen[inst_3] U
rw : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ ¬U = ∅
rw₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ ¬U = ∅
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ U = ∅
have rw₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ↔ ¬U = ∅
Tactic: rw [← not_iff_not, ← Ne, ← pos_iff_ne_zero,
    measure_pos_iff_nonempty_of_smulInvariant G hμ hU, nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (goal)
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
inst_3 : TopologicalSpace α
inst_4 : ContinuousConstSMul G α
inst_5 : MulAction.IsMinimal G α
U : Set α
inst_6 : μ.Regular
hμ : μ ≠ 0
hU : IsOpen[inst_3] U
rw : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ ¬U = ∅
rw₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ ¬U = ∅
rw₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ↔ ¬U = ∅
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ U = ∅
have rw₃ : U.Nonempty ↔ ¬U = ∅
Tactic: rw [← not_iff_not, ← Ne, ← pos_iff_ne_zero,
    measure_pos_iff_nonempty_of_smulInvariant G hμ hU, nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (goal)
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
inst_3 : TopologicalSpace α
inst_4 : ContinuousConstSMul G α
inst_5 : MulAction.IsMinimal G α
U : Set α
inst_6 : μ.Regular
hμ : μ ≠ 0
hU : IsOpen[inst_3] U
rw : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ ¬U = ∅
rw₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ ¬U = ∅
rw₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ↔ ¬U = ∅
rw₃ : U.Nonempty ↔ ¬U = ∅
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞) ↔ U = ∅
have rw₄ : U ≠ ∅ ↔ ¬U = ∅
Tactic: rw [← not_iff_not, ← Ne, ← pos_iff_ne_zero,
    measure_pos_iff_nonempty_of_smulInvariant G hμ hU, nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
⊢ closedBall x ε =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x ε
have inl : ∀ (hε : ε ≤ 0), closedBall x ε =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x ε
Tactic: rcases le_or_gt ε 0 with hε | hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
inl : ∀ (hε : ε ≤ 0), closedBall x ε =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x ε
⊢ closedBall x ε =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x ε
have inr : ∀ (hε : 0 < ε), closedBall x ε =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x ε
Tactic: rcases le_or_gt ε 0 with hε | hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ 2 * ε ≤ T
have linarith : T < 2 * ε → 2 * (ε - 0) + (T - 2 * ε) + (0 - T) = 0
Tactic: linarith [hT.out]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
linarith : T < 2 * ε → 2 * (ε - 0) + (T - 2 * ε) + (0 - T) = 0
⊢ 2 * ε ≤ T
have linarith₁ : T < 2 * ε → GT.gt (α := ℝ) 2 0
Tactic: linarith [hT.out]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ closedBall x ε =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x ε
have inl : 2 * ε ≤ 0
Tactic: rw [ball_eq_empty.mpr hε, ae_eq_empty, volume_closedBall,
      min_eq_right (by linarith [hT.out] : 2 * ε ≤ T), ENNReal.ofReal_eq_zero]