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 : 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∞)
⊢ ∀
    (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:
4 → 5

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∞)
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 α
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c⁻¹ • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← preimage_smul_inv]

Premises used: Set.preimage_smul_inv
-- 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∞)
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∞) ((fun (x : α) ↦ c⁻¹ • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
apply 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∞)
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∞)
⊢ ∀
    (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
-- 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∞)
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∞)
⊢ ∀ (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
-- 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∞)
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∞)
⊢ ∀ (c : G) (s : Set α),
    MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
3

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∞)
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∞)
⊢ ∀
    (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:
5 → 3

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∞)
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∞)
⊢ ∀
    (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
-- 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∞)
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∞)
⊢ ∀ (c : G) (s : Set α),
    MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
3

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∞)
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∞)
⊢ ∀ (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 α
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∞)
⊢ ∀
    (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:
3 → 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 α
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
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (c⁻¹ • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ c • x) ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [preimage_smul]

Premises used: Set.preimage_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) μ = μ
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∞) (c⁻¹ • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
H c⁻¹ s hs

Premises used: Inv.inv
-- 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∞)
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∞) (c⁻¹ • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact H c⁻¹ s hs

Premises used: Inv.inv
-- 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∞)
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∞)
⊢ ∀
    (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