awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AEStabilizer (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s t : Set α
h : s =ᶠ[ae μ] t
g : G
h₁ : g • s =ᶠ[ae μ] s ↔ Membership.mem (γ := Subgroup G) (aestabilizer G μ t) g
h₂ : g • s =ᶠ[ae μ] s ↔ g • t =ᶠ[ae μ] t
⊢ Membership.mem (γ := Subgroup G) (aestabilizer G μ s) g ↔ Membership.mem (γ := Subgroup G) (aestabilizer G μ t) g
have h₃ : g • s =ᶠ[ae μ] t ↔ g • t =ᶠ[ae μ] t
Tactic: rw [mem_aestabilizer, mem_aestabilizer, h.congr_right, ((smul_set_ae_eq g).2 h).congr_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AEStabilizer (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s t : Set α
h : s =ᶠ[ae μ] t
g : G
h₁ : g • s =ᶠ[ae μ] s ↔ Membership.mem (γ := Subgroup G) (aestabilizer G μ t) g
h₂ : g • s =ᶠ[ae μ] s ↔ g • t =ᶠ[ae μ] t
h₃ : g • s =ᶠ[ae μ] t ↔ g • t =ᶠ[ae μ] t
⊢ Membership.mem (γ := Subgroup G) (aestabilizer G μ s) g ↔ Membership.mem (γ := Subgroup G) (aestabilizer G μ t) g
have h₄ : g • t =ᶠ[ae μ] t ↔ g • t =ᶠ[ae μ] t
Tactic: rw [mem_aestabilizer, mem_aestabilizer, h.congr_right, ((smul_set_ae_eq g).2 h).congr_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AEStabilizer (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
⊢ Eq (α := Subgroup G) (aestabilizer G μ s) ⊤
have refine : ∀ (g : G), Membership.mem (γ := Subgroup G) ⊤ g → Membership.mem (γ := Subgroup G) (aestabilizer G μ s) g
Tactic: refine top_unique fun g _ ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AEStabilizer (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
g : G
h : Membership.mem (γ := Subgroup G) ⊤ g
⊢ Membership.mem (γ := Subgroup G) (aestabilizer G μ s) g
have x : s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
Tactic: cases eventuallyConst_set'.mp hs with
  | inl h => simp [aestabilizer_congr h]
  | inr h => simp [aestabilizer_congr h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AEStabilizer (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
x_1 : MeasurableSpace α
μ : Measure α
inst_2 : SMulInvariantMeasure G α μ
x y : G
s : Set α
hs : x • s =ᶠ[ae μ] s
hy : Membership.mem (γ := Subgroup G) (Subgroup.zpowers x) y
⊢ y • s =ᶠ[ae μ] s
have hs₁ : LE.le (α := Subgroup G) (Subgroup.zpowers x) (MulAction.aestabilizer G μ s)
Tactic: rw [← MulAction.mem_aestabilizer, ← Subgroup.zpowers_le] at hs
Cleared hypotheses: hs, hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (goal)
Goal:
G : Type u
α : Type w
m : MeasurableSpace α
inst : SMul G α
μ : Measure α
inst_1 : SMulInvariantMeasure G α μ
s : Set α
hs : NullMeasurableSet s μ
c : G
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' toMeasurable μ s) : ℝ≥0∞)
Tactic: rw [← measure_toMeasurable s,
    ← SMulInvariantMeasure.measure_preimage_smul c (measurableSet_toMeasurable μ 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 : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s ∩ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_inter, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s ∩ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ c • c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_inter, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s ∩ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ c • c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ (c * c⁻¹) • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_inter, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s ∩ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ c • c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ (c * c⁻¹) • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ HSMul.hSMul.{u, w, w} (α := G) 1 t) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_inter, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s ∩ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ c • c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ (c * c⁻¹) • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
rw₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ HSMul.hSMul.{u, w, w} (α := G) 1 t) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
have rw₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∩ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_inter, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s ∪ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_union, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s ∪ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ c • c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_union, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s ∪ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ c • c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ (c * c⁻¹) • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_union, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s ∪ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ c • c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ (c * c⁻¹) • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ HSMul.hSMul.{u, w, w} (α := G) 1 t) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_union, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s ∪ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ c • c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ (c * c⁻¹) • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
rw₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ HSMul.hSMul.{u, w, w} (α := G) 1 t) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
have rw₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∪ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_union, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s \ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_sdiff, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s \ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ c • c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_sdiff, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s \ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ c • c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ (c * c⁻¹) • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_sdiff, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s \ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ c • c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ (c * c⁻¹) • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ HSMul.hSMul.{u, w, w} (α := G) 1 t) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_sdiff, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • (s \ c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ c • c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ (c * c⁻¹) • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
rw₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ HSMul.hSMul.{u, w, w} (α := G) 1 t) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ c⁻¹ • t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
have rw₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s \ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_sdiff, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∆ (c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_symmDiff, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∆ (c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ (c • c⁻¹ • t)) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_symmDiff, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∆ (c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ (c • c⁻¹ • t)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ ((c * c⁻¹) • t)) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_symmDiff, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∆ (c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ (c • c⁻¹ • t)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ ((c * c⁻¹) • t)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ HSMul.hSMul.{u, w, w} (α := G) 1 t) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_symmDiff, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
c : G
s t : Set α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s ∆ (c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ (c • c⁻¹ • t)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ ((c * c⁻¹) • t)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
rw₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ HSMul.hSMul.{u, w, w} (α := G) 1 t) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ (c⁻¹ • t)) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
have rw₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((c • s) ∆ t) : ℝ≥0∞)
Tactic: rw [← measure_smul _ c, smul_set_symmDiff, smul_smul, mul_inv_cancel, one_smul]
-- 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 α μ
s : Set α
c : G
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [measure_smul]
-- 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 α μ
c : G
⊢ c • ae μ = ae μ
have h : ∀ (s : Set α), s ∈ c • ae μ ↔ s ∈ ae μ
Tactic: ext 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 : SMulInvariantMeasure G α μ
c : G
s : Set α
⊢ EventuallyConst (c • s) (ae μ) ↔ EventuallyConst s (ae μ)
have rw : EventuallyConst ((fun (x : α) ↦ c⁻¹ • x) ⁻¹' s) (ae μ) ↔ EventuallyConst s (ae μ)
Tactic: rw [← preimage_smul_inv, eventuallyConst_preimage, Filter.map_smul, smul_ae]
-- 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 α μ
c : G
s : Set α
rw : EventuallyConst ((fun (x : α) ↦ c⁻¹ • x) ⁻¹' s) (ae μ) ↔ EventuallyConst s (ae μ)
⊢ EventuallyConst (c • s) (ae μ) ↔ EventuallyConst s (ae μ)
have rw₁ : EventuallyConst s (Filter.map (fun (x : α) ↦ c⁻¹ • x) (ae μ)) ↔ EventuallyConst s (ae μ)
Tactic: rw [← preimage_smul_inv, eventuallyConst_preimage, Filter.map_smul, smul_ae]
-- 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 α μ
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 μ)
⊢ EventuallyConst (c • s) (ae μ) ↔ EventuallyConst s (ae μ)
have rw₂ : EventuallyConst s (c⁻¹ • ae μ) ↔ EventuallyConst s (ae μ)
Tactic: rw [← preimage_smul_inv, eventuallyConst_preimage, Filter.map_smul, smul_ae]
-- 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 α μ
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 μ)
⊢ EventuallyConst (c • s) (ae μ) ↔ EventuallyConst s (ae μ)
have rw₃ : EventuallyConst s (ae μ) ↔ EventuallyConst s (ae μ)
Tactic: rw [← preimage_smul_inv, eventuallyConst_preimage, Filter.map_smul, smul_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (goal)
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) μ = μ
have 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∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Action (goal)
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∞) (((Measure.map (fun (x : α) ↦ c • x) μ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [map_apply (measurable_const_smul c) hs]