awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u : Filter ι) F
g_1 h_1 : G
s : Set X
g h : G
⊢ (↑u : Filter ι).EventuallyLE (β := ℝ≥0∞)
    (fun (i : ι) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (g • s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞))
    fun (x : ι) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (h • s ∩ F x) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F x) : ℝ≥0∞) +
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((g⁻¹ • F x) ∆ (h⁻¹ • F x)) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F x) : ℝ≥0∞)
have h₁ : ∀ (i : ι) (hi : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) (0 : ℝ≥0∞)),
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (g • s ∩ F i) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) ≤
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (h • s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) +
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((g⁻¹ • F i) ∆ (h⁻¹ • F i)) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞)
Tactic: filter_upwards [hfoel.eventually_meas_ne_zero] with i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u : Filter ι) F
g_1 h_1 : G
s : Set X
g h : G
i : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (g • s ∩ F i) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) ≤
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (h • s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) +
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((g⁻¹ • F i) ∆ (h⁻¹ • F i)) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞)
have h₁ : HDiv.hDiv (β := ℝ≥0∞)
    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (g • s ∩ F i) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (h • s ∩ F i) : ℝ≥0∞))
    ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) ≤
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((g⁻¹ • F i) ∆ (h⁻¹ • F i)) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞)
Tactic: rw [← tsub_le_iff_left, ← ENNReal.sub_div <| fun _ _ ↦ hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
u : Ultrafilter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
hfoel : IsFoelner G μ (↑u : Filter ι) F
g_1 h_1 : G
s : Set X
g h : G
i : ι
hi : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HDiv.hDiv (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (g • s ∩ F i) : ℝ≥0∞)
        ((μ : (a : Set X) → ℝ≥0∞) (h • s ∩ F i) : ℝ≥0∞))
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞) ≤
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((g⁻¹ • F i) ∆ (h⁻¹ • F i)) : ℝ≥0∞)
      ((μ : (a : Set X) → ℝ≥0∞) (F i) : ℝ≥0∞)
have h₁ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (g • s ∩ F i) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (h • s ∩ F i) : ℝ≥0∞) ≤
  (μ : (a : Set X) → ℝ≥0∞) (s ∩ (g⁻¹ • F i) ∆ (h⁻¹ • F i))
Tactic: refine ENNReal.div_le_div_right (le_trans ?_ (measure_mono <| @inter_subset_right _ s _)) _
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
inst_4 : l.NeBot
hfoel : IsFoelner G μ l F
⊢ ∃ (m : Set X → ℝ≥0∞),
    m univ = 1 ∧
      (∀ (s t : Set X), MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t) ∧ ∀ (g : G) (s : Set X), m (g • s) = m s
have h : mean μ (Ultrafilter.of l) F univ = 1 ∧
  (∀ (s t : Set X),
      MeasurableSet t →
        Disjoint s t →
          mean μ (Ultrafilter.of l) F (s ∪ t) = mean μ (Ultrafilter.of l) F s + mean μ (Ultrafilter.of l) F t) ∧
    ∀ (g : G) (s : Set X), mean μ (Ultrafilter.of l) F (g • s) = mean μ (Ultrafilter.of l) F s
Tactic: use mean μ (Ultrafilter.of l) F
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
inst_4 : l.NeBot
hfoel : IsFoelner G μ l F
⊢ mean μ (Ultrafilter.of l) F univ = 1 ∧
    (∀ (s t : Set X),
        MeasurableSet t →
          Disjoint s t →
            mean μ (Ultrafilter.of l) F (s ∪ t) = mean μ (Ultrafilter.of l) F s + mean μ (Ultrafilter.of l) F t) ∧
      ∀ (g : G) (s : Set X), mean μ (Ultrafilter.of l) F (g • s) = mean μ (Ultrafilter.of l) F s
have h : mean μ (Ultrafilter.of l) F univ = 1
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
inst_4 : l.NeBot
hfoel : IsFoelner G μ l F
h : mean μ (Ultrafilter.of l) F univ = 1
⊢ mean μ (Ultrafilter.of l) F univ = 1 ∧
    (∀ (s t : Set X),
        MeasurableSet t →
          Disjoint s t →
            mean μ (Ultrafilter.of l) F (s ∪ t) = mean μ (Ultrafilter.of l) F s + mean μ (Ultrafilter.of l) F t) ∧
      ∀ (g : G) (s : Set X), mean μ (Ultrafilter.of l) F (g • s) = mean μ (Ultrafilter.of l) F s
have h₁ : ∀ (s t : Set X),
  MeasurableSet t →
    Disjoint s t → mean μ (Ultrafilter.of l) F (s ∪ t) = mean μ (Ultrafilter.of l) F s + mean μ (Ultrafilter.of l) F t
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FoelnerFilter (goal)
Goal:
G : Type u_1
X : Type u_2
inst : MeasurableSpace X
μ : Measure X
inst_1 : Group G
inst_2 : MulAction G X
ι : Type u_3
l : Filter ι
F : ι → Set X
inst_3 : SMulInvariantMeasure G X μ
inst_4 : l.NeBot
hfoel : IsFoelner G μ l F
h : mean μ (Ultrafilter.of l) F univ = 1
h₁ :
  ∀ (s t : Set X),
    MeasurableSet t →
      Disjoint s t → mean μ (Ultrafilter.of l) F (s ∪ t) = mean μ (Ultrafilter.of l) F s + mean μ (Ultrafilter.of l) F t
⊢ mean μ (Ultrafilter.of l) F univ = 1 ∧
    (∀ (s t : Set X),
        MeasurableSet t →
          Disjoint s t →
            mean μ (Ultrafilter.of l) F (s ∪ t) = mean μ (Ultrafilter.of l) F s + mean μ (Ultrafilter.of l) F t) ∧
      ∀ (g : G) (s : Set X), mean μ (Ultrafilter.of l) F (g • s) = mean μ (Ultrafilter.of l) F s
have h₂ : ∀ (g : G) (s : Set X), mean μ (Ultrafilter.of l) F (g • s) = mean μ (Ultrafilter.of l) F s
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (hypothesis)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
h_meas : NullMeasurableSet s μ
h_exists : ∀ (x : α), ∃! g : G, g • x ∈ s
a b : G
hab : a ≠ b
x : α
hxa : Membership.mem (γ := Set α) ((fun (g : G) ↦ g • s) a) x
hxb : Membership.mem (γ := Set α) ((fun (g : G) ↦ g • s) b) x
⊢ False
have hxa₁ : a⁻¹ • x ∈ s
Tactic: rw [mem_smul_set_iff_inv_smul_mem] at hxa hxb
Cleared hypotheses: hxa, hxb
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (hypothesis)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
h_meas : NullMeasurableSet s μ
h_exists : ∀ (x : α), ∃! g : G, g • x ∈ s
a b : G
hab : a ≠ b
x : α
hxa : Membership.mem (γ := Set α) ((fun (g : G) ↦ g • s) a) x
hxb : Membership.mem (γ := Set α) ((fun (g : G) ↦ g • s) b) x
hxa₁ : a⁻¹ • x ∈ s
⊢ False
have hxb₁ : b⁻¹ • x ∈ s
Tactic: rw [mem_smul_set_iff_inv_smul_mem] at hxa hxb
Cleared hypotheses: hxa, hxb
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
inst_3 : IsFiniteMeasure μ
inst_4 : Countable G
h_meas : NullMeasurableSet s μ
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
h_measure_univ_le :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • s) : ℝ≥0∞)
aedisjoint : Pairwise.{u_1} (α := G) (AEDisjoint μ on fun (g : G) ↦ g • s)
g : G
⊢ NullMeasurableSet (g • s) μ
have rw : NullMeasurableSet ((fun (x : α) ↦ g⁻¹ • x) ⁻¹' s) μ
Tactic: rw [← inv_inv g, ← preimage_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (hypothesis)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
inst_3 : IsFiniteMeasure μ
inst_4 : Countable G
h_meas : NullMeasurableSet s μ
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
h_measure_univ_le :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • s) : ℝ≥0∞)
aedisjoint : Pairwise.{u_1} (α := G) (AEDisjoint μ on fun (g : G) ↦ g • s)
⊢ ∀ᵐ (x : α) ∂μ, ∃ (g : G), g • x ∈ s
have h_meas₁ : ∀ (g : G), NullMeasurableSet (g • s) μ
Tactic: replace h_meas : ∀ g : G, NullMeasurableSet (g • s) μ := fun g => by
        rw [← inv_inv g, ← preimage_smul]; exact h_meas.preimage (h_qmp g⁻¹)
Cleared hypotheses: h_meas
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
inst_3 : IsFiniteMeasure μ
inst_4 : Countable G
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
h_measure_univ_le :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • s) : ℝ≥0∞)
aedisjoint : Pairwise.{u_1} (α := G) (AEDisjoint μ on fun (g : G) ↦ g • s)
h_meas : ∀ (g : G), NullMeasurableSet (g • s) μ
⊢ NullMeasurableSet {a : α | ∃ (g : G), g • a ∈ s} μ
have rw : NullMeasurableSet (⋃ (g : G), g • s) μ
Tactic: rw [← iUnion_smul_eq_setOf_exists]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (hypothesis)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
inst_3 : IsFiniteMeasure μ
inst_4 : Countable G
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
h_measure_univ_le :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • s) : ℝ≥0∞)
aedisjoint : Pairwise.{u_1} (α := G) (AEDisjoint μ on fun (g : G) ↦ g • s)
h_meas : ∀ (g : G), NullMeasurableSet (g • s) μ
⊢ ∀ᵐ (x : α) ∂μ, ∃ (g : G), g • x ∈ s
have h_meas' : NullMeasurableSet {a : α | ∃ (g : G), g • a ∈ s} μ
Tactic: have h_meas' : NullMeasurableSet {a | ∃ g : G, g • a ∈ s} μ := by
        rw [← iUnion_smul_eq_setOf_exists]; exact .iUnion h_meas
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
inst_3 : IsFiniteMeasure μ
inst_4 : Countable G
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
h_measure_univ_le :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • s) : ℝ≥0∞)
aedisjoint : Pairwise.{u_1} (α := G) (AEDisjoint μ on fun (g : G) ↦ g • s)
h_meas : ∀ (g : G), NullMeasurableSet (g • s) μ
h_meas' : NullMeasurableSet {a : α | ∃ (g : G), g • a ∈ s} μ
⊢ ∀ᵐ (x : α) ∂μ, ∃ (g : G), g • x ∈ s
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (g : G), g • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [ae_iff_measure_eq h_meas', ← iUnion_smul_eq_setOf_exists]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
inst_3 : IsFiniteMeasure μ
inst_4 : Countable G
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun (x : α) ↦ g • x) μ μ
h_measure_univ_le :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑' (g : G), (μ : (a : Set α) → ℝ≥0∞) (g • s) : ℝ≥0∞)
aedisjoint : Pairwise.{u_1} (α := G) (AEDisjoint μ on fun (g : G) ↦ g • s)
h_meas : ∀ (g : G), NullMeasurableSet (g • s) μ
h_meas' : NullMeasurableSet {a : α | ∃ (g : G), g • a ∈ s} μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (g : G), g • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (g : G), g • s) : ℝ≥0∞)
Tactic: refine le_antisymm (measure_mono <| subset_univ _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (hypothesis)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
inst_3 : Countable G
inst_4 : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have hc : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: have hc := measure_univ_pos.mpr hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
inst_3 : Countable G
inst_4 : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have contrapose! : ∀ (hc : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: contrapose! hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
inst_3 : Countable G
inst_4 : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (g : G), g • s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← measure_congr h.iUnion_smul_ae_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
inst_3 : Countable G
inst_4 : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (g : G), g • s) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine : LE.le (α := ℝ≥0∞) (∑' (i : G), (μ : (a : Set α) → ℝ≥0∞) (i • s)) 0
Tactic: refine le_trans (measure_iUnion_le _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
inst_3 : Countable G
inst_4 : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : G), (μ : (a : Set α) → ℝ≥0∞) (i • s)) 0
have simp_rw : LE.le (α := ℝ≥0∞) (∑' (i : G), (μ : (a : Set α) → ℝ≥0∞) s) 0
Tactic: simp_rw [measure_smul, hc, tsum_zero, le_refl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
inst_3 : Countable G
inst_4 : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw : LE.le (α := ℝ≥0∞) (∑' (i : G), (μ : (a : Set α) → ℝ≥0∞) s) 0
⊢ LE.le (α := ℝ≥0∞) (∑' (i : G), (μ : (a : Set α) → ℝ≥0∞) (i • s)) 0
have simp_rw₁ : LE.le (α := ℝ≥0∞) (∑' (i : G), 0) 0
Tactic: simp_rw [measure_smul, hc, tsum_zero, le_refl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
inst_3 : Countable G
inst_4 : SMulInvariantMeasure G α μ
hμ : μ ≠ 0
h : IsFundamentalDomain G s μ
hc : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw : LE.le (α := ℝ≥0∞) (∑' (i : G), (μ : (a : Set α) → ℝ≥0∞) s) 0
simp_rw₁ : LE.le (α := ℝ≥0∞) (∑' (i : G), 0) 0
⊢ LE.le (α := ℝ≥0∞) (∑' (i : G), (μ : (a : Set α) → ℝ≥0∞) (i • s)) 0
have simp_rw₂ : LE.le (α := ℝ≥0∞) 0 0
Tactic: simp_rw [measure_smul, hc, tsum_zero, le_refl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
inst_4 : MulAction H β
inst_5 : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : β → α
hf : QuasiMeasurePreserving f ν μ
e : G → H
he : Bijective e
hef : ∀ (g : G), Semiconj f (fun (x : β) ↦ e g • x) fun (x : α) ↦ g • x
x : β
h_1 : ∃ (g : G), g • f x ∈ s
g : G
hg : g • f x ∈ s
⊢ e g • x ∈ f ⁻¹' s
have rwa : f (e g • x) ∈ s
Tactic: rwa [mem_preimage, hef g x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
inst_4 : MulAction H β
inst_5 : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : β → α
hf : QuasiMeasurePreserving f ν μ
e : G → H
he : Bijective e
hef : ∀ (g : G), Semiconj f (fun (x : β) ↦ e g • x) fun (x : α) ↦ g • x
a b : H
hab : a ≠ b
⊢ (AEDisjoint ν on fun (g : H) ↦ g • f ⁻¹' s) a b
have lift : ∀ (e : G ≃ H)
  (hef :
    ∀ (g : G),
      Semiconj f (fun (x : β) ↦ HSMul.hSMul.{u_2, u_4, u_4} (α := H) ((e : (a : G) → H) g : H) x) fun (x : α) ↦ g • x),
  (AEDisjoint ν on fun (g : H) ↦ g • f ⁻¹' s) a b
Tactic: lift e to G ≃ H using he
Cleared hypotheses: e, he, hef
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (hypothesis)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
inst_4 : MulAction H β
inst_5 : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : β → α
hf : QuasiMeasurePreserving f ν μ
a b : H
hab : a ≠ b
e : G ≃ H
hef :
  ∀ (g : G),
    Semiconj f (fun (x : β) ↦ HSMul.hSMul.{u_2, u_4, u_4} (α := H) ((e : (a : G) → H) g : H) x) fun (x : α) ↦ g • x
⊢ (AEDisjoint ν on fun (g : H) ↦ g • f ⁻¹' s) a b
have this : Ne.{u_1 + 1} (α := G) (((e.symm : (a : H) → G) a⁻¹)⁻¹ : G) (((e.symm : (a : H) → G) b⁻¹)⁻¹ : G)
Tactic: have : (e.symm a⁻¹)⁻¹ ≠ (e.symm b⁻¹)⁻¹ := by simp [hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (hypothesis)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
inst_4 : MulAction H β
inst_5 : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : β → α
hf : QuasiMeasurePreserving f ν μ
a b : H
hab : a ≠ b
e : G ≃ H
hef :
  ∀ (g : G),
    Semiconj f (fun (x : β) ↦ HSMul.hSMul.{u_2, u_4, u_4} (α := H) ((e : (a : G) → H) g : H) x) fun (x : α) ↦ g • x
this : Ne.{u_1 + 1} (α := G) (((e.symm : (a : H) → G) a⁻¹)⁻¹ : G) (((e.symm : (a : H) → G) b⁻¹)⁻¹ : G)
⊢ (AEDisjoint ν on fun (g : H) ↦ g • f ⁻¹' s) a b
have this₁ : AEDisjoint ν (f ⁻¹' (fun (g : G) ↦ g • s) ((e.symm : (a : H) → G) a⁻¹)⁻¹)
  (f ⁻¹' (fun (g : G) ↦ g • s) ((e.symm : (a : H) → G) b⁻¹)⁻¹)
Tactic: have := (h.aedisjoint this).preimage hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
inst_4 : MulAction H β
inst_5 : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : α ≃ β
hf : QuasiMeasurePreserving (⇑f.symm : (a : β) → α) ν μ
e : H ≃ G
hef :
  ∀ (g : H),
    Semiconj (⇑f : (a : α) → β) (fun (x : α) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := G) ((e : (a : H) → G) g : G) x)
      fun (x : β) ↦ g • x
⊢ IsFundamentalDomain H ((⇑f : (a : α) → β) '' s) ν
have rw : IsFundamentalDomain H ((⇑f.symm : (a : β) → α) ⁻¹' s) ν
Tactic: rw [f.image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
inst_4 : MulAction H β
inst_5 : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : α ≃ β
hf : QuasiMeasurePreserving (⇑f.symm : (a : β) → α) ν μ
e : H ≃ G
hef :
  ∀ (g : H),
    Semiconj (⇑f : (a : α) → β) (fun (x : α) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := G) ((e : (a : H) → G) g : G) x)
      fun (x : β) ↦ g • x
⊢ IsFundamentalDomain H ((⇑f.symm : (a : β) → α) ⁻¹' s) ν
have refine : ∀ (g : G) (x : β),
  Eq.{u_3 + 1} (α := α)
    ((f.symm : (a : β) → α) ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_4, u_4} (α := H) ((e.symm : (a : G) → H) g : H) x) x) :
      α)
    ((fun (x : α) ↦ g • x) ((f.symm : (a : β) → α) x) : α)
Tactic: refine h.preimage_of_equiv hf e.symm.bijective fun g x => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
β : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
inst_4 : MulAction H β
inst_5 : MeasurableSpace β
s : Set α
μ : Measure α
ν : Measure β
h : IsFundamentalDomain G s μ
f : α ≃ β
hf : QuasiMeasurePreserving (⇑f.symm : (a : β) → α) ν μ
e : H ≃ G
hef :
  ∀ (g : H),
    Semiconj (⇑f : (a : α) → β) (fun (x : α) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := G) ((e : (a : H) → G) g : G) x)
      fun (x : β) ↦ g • x
g : G
x : β
⊢ Eq.{u_3 + 1} (α := α)
    ((f.symm : (a : β) → α) ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_4, u_4} (α := H) ((e.symm : (a : G) → H) g : H) x) x) :
      α)
    ((fun (x : α) ↦ g • x) ((f.symm : (a : β) → α) x) : α)
have rcases : ∀ (x : α),
  Eq.{u_3 + 1} (α := α)
    ((f.symm : (a : β) → α)
        ((fun (x : β) ↦ HSMul.hSMul.{u_2, u_4, u_4} (α := H) ((e.symm : (a : G) → H) g : H) x) ((f : (a : α) → β) x)) :
      α)
    ((fun (x : α) ↦ g • x) ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β)) : α)
Tactic: rcases f.surjective x with ⟨x, rfl⟩
Cleared hypotheses: x