awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 : a⁻¹ • x ∈ s
hxb : b⁻¹ • x ∈ s
⊢ False

Tactic:
hab (inv_injective <| (h_exists x).unique hxa hxb)

Premises used: ExistsUnique.unique, inv_injective
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 : a⁻¹ • x ∈ s
hxb : b⁻¹ • x ∈ s
⊢ False

Tactic:
exact hab (inv_injective <| (h_exists x).unique hxa hxb)

Premises used: ExistsUnique.unique, inv_injective
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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
rw : NullMeasurableSet ((fun (x : α) ↦ g⁻¹ • x) ⁻¹' s) μ
⊢ NullMeasurableSet (g • s) μ

Tactic:
rw [← inv_inv g, ← preimage_smul]

Premises used: Set.preimage_smul, inv_inv
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 ((fun (x : α) ↦ g⁻¹ • x) ⁻¹' s) μ

Tactic:
h_meas.preimage (h_qmp g⁻¹)

Premises used: MeasureTheory.NullMeasurableSet.preimage, Inv.inv
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 ((fun (x : α) ↦ g⁻¹ • x) ⁻¹' s) μ

Tactic:
exact h_meas.preimage (h_qmp g⁻¹)

Premises used: MeasureTheory.NullMeasurableSet.preimage, Inv.inv
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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) μ

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⁻¹)
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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) μ
rw : NullMeasurableSet (⋃ (g : G), g • s) μ
⊢ NullMeasurableSet {a : α | ∃ (g : G), g • a ∈ s} μ

Tactic:
rw [← iUnion_smul_eq_setOf_exists]

Premises used: Set.iUnion_smul_eq_setOf_exists
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 (⋃ (g : G), g • s) μ

Tactic:
.iUnion h_meas

Premises used: MeasureTheory.NullMeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 (⋃ (g : G), g • s) μ

Tactic:
exact .iUnion h_meas
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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} μ

Tactic:
have h_meas' : NullMeasurableSet {a | ∃ g : G, g • a ∈ s} μ := by
        rw [← iUnion_smul_eq_setOf_exists]; exact .iUnion h_meas
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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} μ
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (g : G), g • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ, ∃ (g : G), g • x ∈ s

Tactic:
rw [ae_iff_measure_eq h_meas', ← iUnion_smul_eq_setOf_exists]

Premises used: Set.iUnion_smul_eq_setOf_exists, MeasureTheory.ae_iff_measure_eq
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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∞)

Tactic:
le_antisymm (measure_mono <| subset_univ _) ?_

Premises used: Set.subset_univ, le_antisymm, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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} μ
refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (g : G), g • s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (g : G), g • s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
refine le_antisymm (measure_mono <| subset_univ _) ?_

Premises used: Set.subset_univ, le_antisymm, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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} μ
rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑' (i : G), (μ : (a : Set α) → ℝ≥0∞) (i • s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (g : G), g • s) : ℝ≥0∞)

Tactic:
rw [measure_iUnion₀ aedisjoint h_meas]

Premises used: MeasureTheory.measure_iUnion₀
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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} μ
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑' (i : G), (μ : (a : Set α) → ℝ≥0∞) (i • s) : ℝ≥0∞)

Tactic:
h_measure_univ_le
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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} μ
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑' (i : G), (μ : (a : Set α) → ℝ≥0∞) (i • s) : ℝ≥0∞)

Tactic:
exact h_measure_univ_le
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
h : IsFundamentalDomain G s μ
⊢ ⋃ (g : G), g • s =ᶠ[ae μ] univ

Tactic:
eventuallyEq_univ.2 <| h.ae_covers.mono fun _ ⟨g, hg⟩ =>
    mem_iUnion.2 ⟨g⁻¹, _, hg, inv_smul_smul _ _⟩

Premises used: Iff.mpr, iSup, Set.mem_iUnion, inv_smul_smul, _private.0.MeasureTheory.IsFundamentalDomain.iUnion_smul_ae_eq.match_1, Filter.Eventually.mono, Inv.inv, And.intro, Exists.intro, Filter.eventuallyEq_univ, HSMul.hSMul, MeasureTheory.IsFundamentalDomain.ae_covers
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
have hc := measure_univ_pos.mpr hμ
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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∞)
contrapose! :
  ∀ (hc : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
contrapose! hc
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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∞)
rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (g : G), g • s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← measure_congr h.iUnion_smul_ae_eq]

Premises used: MeasureTheory.measure_congr, MeasureTheory.IsFundamentalDomain.iUnion_smul_ae_eq
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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∞)

Tactic:
le_trans (measure_iUnion_le _) ?_

Premises used: MeasureTheory.measure_iUnion_le, le_trans
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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∞)
refine : LE.le (α := ℝ≥0∞) (∑' (i : G), (μ : (a : Set α) → ℝ≥0∞) (i • s)) 0
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (g : G), g • s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine le_trans (measure_iUnion_le _) ?_

Premises used: MeasureTheory.measure_iUnion_le, le_trans
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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
simp_rw₂ : LE.le (α := ℝ≥0∞) 0 0
⊢ LE.le (α := ℝ≥0∞) (∑' (i : G), (μ : (a : Set α) → ℝ≥0∞) (i • s)) 0

Tactic:
simp_rw [measure_smul, hc, tsum_zero, le_refl]

Premises used: le_refl, tsum_zero, MeasureTheory.measure_smul
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
s : Set α
μ : Measure α
h : IsFundamentalDomain G s μ
ν : Measure α
hle : ν ≪ μ
⊢ IsFundamentalDomain G s ν

Tactic:
⟨h.1.mono_ac hle, hle h.2, h.aedisjoint.mono fun _ _ h => hle h⟩

Premises used: MeasureTheory.IsFundamentalDomain.mk, MeasureTheory.IsFundamentalDomain.nullMeasurableSet, MeasureTheory.IsFundamentalDomain.aedisjoint, MeasureTheory.NullMeasurableSet.mono_ac, MeasureTheory.IsFundamentalDomain.ae_covers, Pairwise.mono
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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
rwa : f (e g • x) ∈ s
rwa₁ rwa₂ rwa₃ rwa₄ : (fun (x : α) ↦ g • x) (f x) ∈ s
⊢ e g • x ∈ f ⁻¹' s

Tactic:
rwa [mem_preimage, hef g x]

Premises used: Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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
⊢ Bijective e

Tactic:
he
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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
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
⊢ (AEDisjoint ν on fun (g : H) ↦ g • f ⁻¹' s) a b

Tactic:
lift e to G ≃ H using he
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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
⊢ Ne.{u_1 + 1} (α := G) (((e.symm : (a : H) → G) a⁻¹)⁻¹ : G) (((e.symm : (a : H) → G) b⁻¹)⁻¹ : G)

Tactic:
simp [hab]
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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
⊢ 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]
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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 ν (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
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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) (x : β), f (HSMul.hSMul.{u_2, u_4, u_4} (α := H) ((e : (a : G) → H) g : H) x) = g • f x
this_1 : Ne.{u_1 + 1} (α := G) (((e.symm : (a : H) → G) a⁻¹)⁻¹ : G) (((e.symm : (a : H) → G) b⁻¹)⁻¹ : G)
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⁻¹)⁻¹)
⊢ (AEDisjoint ν on fun (g : H) ↦ g • f ⁻¹' s) a b

Tactic:
simpa only [onFun, ← preimage_smul_inv, preimage_preimage, ← hef, e.apply_symm_apply, inv_inv]
      using this

Premises used: Equiv.apply_symm_apply, Set.preimage_preimage, Function.onFun, Set.preimage_smul_inv, inv_inv
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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
rw : IsFundamentalDomain H ((⇑f.symm : (a : β) → α) ⁻¹' s) ν
⊢ IsFundamentalDomain H ((⇑f : (a : α) → β) '' s) ν

Tactic:
rw [f.image_eq_preimage_symm]

Premises used: Equiv.image_eq_preimage_symm
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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) ν

Tactic:
h.preimage_of_equiv hf e.symm.bijective fun g x => ?_

Premises used: Equiv.bijective, MeasureTheory.IsFundamentalDomain.preimage_of_equiv, Equiv.symm