awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s : Set α
c : G
rw rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [measure_smul]

Premises used: MeasureTheory.measure_smul
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s : Set α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
c : G
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
(measure_smul_eq_zero_iff _).2 h

Premises used: Iff.mpr, MeasureTheory.measure_smul_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
c : G
s : Set α
⊢ c • s ∈ ae μ ↔ s ∈ ae μ

Tactic:
simp only [mem_ae_iff, ← smul_set_compl, measure_smul_eq_zero_iff]

Premises used: MeasureTheory.measure_smul_eq_zero_iff, Set.smul_set_compl, MeasureTheory.mem_ae_iff
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
c : G
h : ∀ (s : Set α), s ∈ c • ae μ ↔ s ∈ ae μ
⊢ c • ae μ = ae μ

Tactic:
ext s
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
c : G
s : Set α
⊢ s ∈ c • ae μ ↔ s ∈ ae μ

Tactic:
simp only [mem_smul_filter, preimage_smul, smul_mem_ae]

Premises used: Set.preimage_smul, MeasureTheory.smul_mem_ae, Filter.mem_smul_filter
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
c : G
s : Set α
rw : EventuallyConst ((fun (x : α) ↦ c⁻¹ • x) ⁻¹' s) (ae μ) ↔ EventuallyConst s (ae μ)
rw₁ : EventuallyConst s (Filter.map (fun (x : α) ↦ c⁻¹ • x) (ae μ)) ↔ EventuallyConst s (ae μ)
rw₂ : EventuallyConst s (c⁻¹ • ae μ) ↔ EventuallyConst s (ae μ)
rw₃ rw₄ : EventuallyConst s (ae μ) ↔ EventuallyConst s (ae μ)
⊢ EventuallyConst (c • s) (ae μ) ↔ EventuallyConst s (ae μ)

Tactic:
rw [← preimage_smul_inv, eventuallyConst_preimage, Filter.map_smul, smul_ae]

Premises used: MeasureTheory.smul_ae, Set.preimage_smul_inv, Filter.eventuallyConst_preimage, Filter.map_smul
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ c • s ≤ᶠ[ae μ] c • t ↔ s ≤ᶠ[ae μ] t

Tactic:
simp only [ae_le_set, ← smul_set_sdiff, measure_smul_eq_zero_iff]

Premises used: MeasureTheory.measure_smul_eq_zero_iff, Set.smul_set_sdiff, MeasureTheory.ae_le_set
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ c • s =ᶠ[ae μ] c • t ↔ s =ᶠ[ae μ] t

Tactic:
simp only [Filter.eventuallyLE_antisymm_iff, smul_set_ae_le]

Premises used: Filter.eventuallyLE_antisymm_iff, MeasureTheory.smul_set_ae_le
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
M : Type v
α : Type w
m : MeasurableSpace α
inst : SMul M α
inst_1 : MeasurableConstSMul M α
c : M
μ : Measure α
inst_2 : SMulInvariantMeasure M α μ
h :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((Measure.map (fun (x : α) ↦ c • x) μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Measure.map (fun (x : α) ↦ c • x) μ = μ

Tactic:
ext1 s hs
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
M : Type v
α : Type w
m : MeasurableSpace α
inst : SMul M α
inst_1 : MeasurableConstSMul M α
c : M
μ : Measure α
inst_2 : SMulInvariantMeasure M α μ
s : Set α
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map (fun (x : α) ↦ c • x) μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [map_apply (measurable_const_smul c) hs]

Premises used: MeasureTheory.Measure.map_apply, MeasurableConstSMul.measurable_const_smul
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
M : Type v
α : Type w
m : MeasurableSpace α
inst : SMul M α
inst_1 : MeasurableConstSMul M α
c : M
μ : Measure α
inst_2 : SMulInvariantMeasure M α μ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
SMulInvariantMeasure.measure_preimage_smul c hs

Premises used: MeasureTheory.SMulInvariantMeasure.measure_preimage_smul
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
M : Type v
α : Type w
m : MeasurableSpace α
inst : SMul M α
inst_1 : MeasurableConstSMul M α
c : M
μ : Measure α
inst_2 : SMulInvariantMeasure M α μ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact SMulInvariantMeasure.measure_preimage_smul c hs

Premises used: MeasureTheory.SMulInvariantMeasure.measure_preimage_smul
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
M : Type v
α : Type w
m : MeasurableSpace α
inst : SMul M α
inst_1 : MeasurableConstSMul M α
c : M
μ : Measure α
inst_2 : SMulInvariantMeasure M α μ
⊢ Measure.map (fun (x : α) ↦ c • x) μ = μ

Tactic:
(measurePreserving_smul c μ).map_eq

Premises used: MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.measurePreserving_smul
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
α : Type w
f : α → α
x : MeasurableSpace α
μ : Measure α
hf : MeasurePreserving f μ μ
⊢ SMulInvariantMeasure (IterateMulAct f) α μ

Tactic:
⟨fun n _s hs ↦ (hf.iterate n.val).measure_preimage hs.nullMeasurableSet⟩

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.MeasurePreserving.iterate, MeasureTheory.SMulInvariantMeasure.mk, IterateMulAct.val, MeasureTheory.MeasurePreserving.measure_preimage
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
α : Type w
f : α → α
x : MeasurableSpace α
μ : Measure α
hf : Measurable f
⊢ SMulInvariantMeasure (IterateMulAct f) α μ ↔ MeasurePreserving f μ μ

Tactic:
⟨fun _ ↦
    have := hf.measurableSMul₂_iterateMulAct
    measurePreserving_smul (IterateMulAct.mk (f := f) 1) μ,
    MeasurePreserving.smulInvariantMeasure_iterateMulAct⟩

Premises used: MeasureTheory.MeasurePreserving.smulInvariantMeasure_iterateMulAct, IterateMulAct.mk, MeasureTheory.measurePreserving_smul, Iff.intro, OfNat.ofNat, Measurable.measurableSMul₂_iterateMulAct
-- Module: Mathlib.MeasureTheory.Group.Action
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
rw rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ m • f x) ⁻¹' S) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ m • f x) ⁻¹' S) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' (fun (x : β) ↦ m • x) ⁻¹' S) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ m • f x) ⁻¹' S) : ℝ≥0∞)

Tactic:
rw [preimage_preimage]

Premises used: Set.preimage_preimage
-- Module: Mathlib.MeasureTheory.Group.Action
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 • f x) ⁻¹' S) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ f (m • x)) ⁻¹' S) : ℝ≥0∞)

Tactic:
simp_rw [hsmul]
-- Module: Mathlib.MeasureTheory.Group.Action
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
rw rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (HSMul.hSMul m ⁻¹' f ⁻¹' S) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ m • x) ⁻¹' f ⁻¹' S) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ f (m • x)) ⁻¹' S) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ m • x) ⁻¹' f ⁻¹' S) : ℝ≥0∞)

Tactic:
rw [← preimage_preimage]

Premises used: Set.preimage_preimage
-- Module: Mathlib.MeasureTheory.Group.Action
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
rw rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' S) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' S) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ m • x) ⁻¹' f ⁻¹' S) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' S) : ℝ≥0∞)

Tactic:
rw [SMulInvariantMeasure.measure_preimage_smul m (hS.preimage hf)]

Premises used: MeasurableSet.preimage, MeasureTheory.SMulInvariantMeasure.measure_preimage_smul
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
M_1 : Type v
α_1 : Type w
M : Type uM
N : Type uN
α : Type uα
β : Type uβ
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : SMul M α
inst_3 : SMul N α
inst_4 : SMulCommClass N M α
inst_5 : MeasurableConstSMul M α
inst_6 : MeasurableConstSMul N α
μ : Measure α
inst_7 : SMulInvariantMeasure M α μ
n : N
⊢ @SMulInvariantMeasure M α _ inst (Measure.map (fun (x : α) ↦ n • x) μ)

Tactic:
smulInvariantMeasure_map μ _ (smul_comm n) <| measurable_const_smul _

Premises used: MeasurableConstSMul.measurable_const_smul, MeasureTheory.smulInvariantMeasure_map, SMulCommClass.smul_comm
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : MeasurableConstSMul G α
⊢ SMulInvariantMeasure G α μ

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Group.Action
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : Group G
inst_1 : MulAction G α
μ : Measure α
inst_2 : MeasurableConstSMul G α
⊢ ∀ (c : G) (s : Set α),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Group.Action
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∞)

Tactic:
1 ↔ 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Group.Action
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∞)

Tactic:
tfae_have 1 ↔ 2 := ⟨fun h => h.1, fun h => ⟨h⟩⟩
-- Module: Mathlib.MeasureTheory.Group.Action
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 α μ

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Group.Action
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∞)
⊢ ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ

Tactic:
6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Group.Action
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∞)
⊢ ∀ (a : SMulInvariantMeasure G α μ) (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ

Tactic:
1 → 6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Group.Action
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∞)
⊢ ∀ (a : SMulInvariantMeasure G α μ) (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ

Tactic:
tfae_have 1 → 6 := fun h c => (measurePreserving_smul c μ).map_eq

Premises used: MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.measurePreserving_smul
-- Module: Mathlib.MeasureTheory.Group.Action
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) μ = μ
⊢ ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ

Tactic:
6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Group.Action
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) μ = μ
⊢ ∀ (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ

Tactic:
7

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Group.Action
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) μ = μ
⊢ ∀ (a : ∀ (c : G), Measure.map (fun (x : α) ↦ c • x) μ = μ) (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ

Tactic:
6 → 7

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Group.Action
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) μ = μ
⊢ ∀ (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⟩
-- Module: Mathlib.MeasureTheory.Group.Action
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) μ μ
⊢ ∀ (c : G), MeasurePreserving (fun (x : α) ↦ c • x) μ μ

Tactic:
7

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Group.Action
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) μ μ
⊢ ∀ (c : G) (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Group.Action
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) μ μ
⊢ ∀ (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:
7 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Group.Action
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) μ μ
⊢ ∀ (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)
-- Module: Mathlib.MeasureTheory.Group.Action
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∞)
⊢ ∀ (c : G) (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Group.Action
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∞)
⊢ ∀ (c : G) (s : Set α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false