awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in t, f x ∂μ)
have pos : ∀ (hfs : IntegrableOn f s μ), Eq.{u_5 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in t, f x ∂μ)
Tactic: by_cases hfs : IntegrableOn f s μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
pos : ∀ (hfs : IntegrableOn f s μ), Eq.{u_5 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in t, f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in t, f x ∂μ)
have neg : ∀ (hfs : ¬IntegrableOn f s μ), Eq.{u_5 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in t, f x ∂μ)
Tactic: by_cases hfs : IntegrableOn f s μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (hypothesis)
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : IntegrableOn f s μ
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in t, f x ∂μ)
have hft : IntegrableOn f t μ
Tactic: have hft : IntegrableOn f t μ := by rwa [ht.integrableOn_iff hs hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in t, f x ∂μ)
have x : Eq.{u_5 + 1} (α := E) (∑' (g : G), ∫ (x : α) in s ∩ g • t, f x ∂μ) (∑' (g : G), ∫ (x : α) in g • t ∩ s, f (g⁻¹ • x) ∂μ)
Tactic: calc
      ∫ x in s, f x ∂μ = ∑' g : G, ∫ x in s ∩ g • t, f x ∂μ := ht.setIntegral_eq_tsum hfs
      _ = ∑' g : G, ∫ x in g • t ∩ s, f (g⁻¹ • x) ∂μ := by simp only [hf, inter_comm]
      _ = ∫ x in t, f x ∂μ := (hs.setIntegral_eq_tsum' hft).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : ¬IntegrableOn f s μ
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in t, f x ∂μ)
have neg : ¬Integrable f (μ.restrict t)
Tactic: rw [integral_undef hfs, integral_undef]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
E : Type u_5
inst : Group G
inst_1 : MulAction G α
inst_2 : MeasurableSpace α
inst_3 : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
inst_6 : Countable G
inst_7 : NormedSpace ℝ E
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → E
hf : ∀ (g : G) (x : α), f (g • x) = f x
hfs : ¬IntegrableOn f s μ
⊢ ¬Integrable f (μ.restrict t)
have neg : ∀ (hfs : ¬IntegrableOn f t μ), ¬Integrable f (μ.restrict t)
Tactic: rwa [hs.integrableOn_iff ht hf] at hfs
Cleared hypotheses: hfs
-- 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 t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∃ x ∈ t, ∃ y ∈ t, ∃ (g : G), g ≠ 1 ∧ g • x = y
have contrapose! : ∀ (ht : ∀ (x : α) (_ : x ∈ t) (y : α) (_ : y ∈ t) (g : G) (_ : g ≠ 1), g • x ≠ y),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: contrapose! ht
Cleared hypotheses: ht
-- 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 t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ (x : α) (_ : x ∈ t) (y : α) (_ : y ∈ t) (g : G) (_ : g ≠ 1), g • x ≠ y
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have refine : ∀ (g₁ g₂ : G) (hne : g₁ ≠ g₂), onFun.{u_1 + 1, u_3 + 1, 1} (β := Set α) Disjoint (fun (g : G) ↦ g • t ∩ s) g₁ g₂
Tactic: refine hs.measure_le_of_pairwise_disjoint htm (Pairwise.aedisjoint fun g₁ g₂ hne => ?_)
-- 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 t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ (x : α) (_ : x ∈ t) (y : α) (_ : y ∈ t) (g : G) (_ : g ≠ 1), g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
⊢ Disjoint (g₁ • t ∩ s) (g₂ • t ∩ s)
have refine : Disjoint (g₁ • t) (g₂ • t)
Tactic: refine (Disjoint.inf_left _ ?_).inf_right _
-- 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 t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ (x : α) (_ : x ∈ t) (y : α) (_ : y ∈ t) (g : G) (_ : g ≠ 1), g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
⊢ Disjoint (g₁ • t) (g₂ • t)
have rw : ∀ ⦃a : α⦄, a ∈ g₁ • t → a ∉ g₂ • t
Tactic: rw [Set.disjoint_left]
-- 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 t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ (x : α) (_ : x ∈ t) (y : α) (_ : y ∈ t) (g : G) (_ : g ≠ 1), g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
x : α
hx : x ∈ t
y : α
hy : y ∈ t
hxy : g₂ • y = g₁ • x
⊢ False
have refine : (g₂⁻¹ * g₁) • x = y
Tactic: refine ht x hx y hy (g₂⁻¹ * g₁) (mt inv_mul_eq_one.1 hne.symm) ?_
-- 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 t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ (x : α) (_ : x ∈ t) (y : α) (_ : y ∈ t) (g : G) (_ : g ≠ 1), g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
x : α
hx : x ∈ t
y : α
hy : y ∈ t
hxy : g₂ • y = g₁ • x
⊢ (g₂⁻¹ * g₁) • x = y
have rw : g₂⁻¹ • g₁ • x = y
Tactic: rw [mul_smul, ← hxy, inv_smul_smul]
-- 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 t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ (x : α) (_ : x ∈ t) (y : α) (_ : y ∈ t) (g : G) (_ : g ≠ 1), g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
x : α
hx : x ∈ t
y : α
hy : y ∈ t
hxy : g₂ • y = g₁ • x
rw : g₂⁻¹ • g₁ • x = y
⊢ (g₂⁻¹ * g₁) • x = y
have rw₁ : g₂⁻¹ • g₂ • y = y
Tactic: rw [mul_smul, ← hxy, inv_smul_smul]
-- 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 t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ (x : α) (_ : x ∈ t) (y : α) (_ : y ∈ t) (g : G) (_ : g ≠ 1), g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
x : α
hx : x ∈ t
y : α
hy : y ∈ t
hxy : g₂ • y = g₁ • x
rw : g₂⁻¹ • g₁ • x = y
rw₁ : g₂⁻¹ • g₂ • y = y
⊢ (g₂⁻¹ * g₁) • x = y
have rw₂ : y = y
Tactic: rw [mul_smul, ← hxy, inv_smul_smul]
-- 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 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
⊢ essSup f (μ.restrict s) = essSup f μ
have refine : essSup f μ ≤ essSup f (μ.restrict s)
Tactic: refine le_antisymm (essSup_mono_measure' Measure.restrict_le_self) ?_
-- 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 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
⊢ essSup f μ ≤ essSup f (μ.restrict s)
have rw : LE.le (α := ℝ≥0∞) (sInf {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)})
  (sInf {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)})
Tactic: rw [essSup_eq_sInf (μ.restrict s) f, essSup_eq_sInf μ f]
-- 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 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
⊢ LE.le (α := ℝ≥0∞) (sInf {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)})
    (sInf {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)})
have refine : Subset (α := Set ℝ≥0∞)
  {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)}
  {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)}
Tactic: refine sInf_le_sInf ?_
-- 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 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
a : ℝ≥0∞
ha : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Membership.mem (γ := Set ℝ≥0∞)
    {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)} a
have ha₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | a < f x} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply₀' hs.nullMeasurableSet] at ha
Cleared hypotheses: ha
-- 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 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
a : ℝ≥0∞
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | a < f x} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Membership.mem (γ := Set ℝ≥0∞)
    {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)} a
have refine : ∀ (g : G), HSMul.hSMul (β := Set α) g {x : α | a < f x} = {x : α | a < f x}
Tactic: refine measure_zero_of_invariant hs _ ?_ ha
-- 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 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
a : ℝ≥0∞
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | a < f x} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
γ : G
⊢ HSMul.hSMul (β := Set α) γ {x : α | a < f x} = {x : α | a < f x}
have h : ∀ (x : α), x ∈ HSMul.hSMul (β := Set α) γ {x : α | a < f x} ↔ Membership.mem (γ := Set α) {x : α | a < f x} x
Tactic: ext x
-- 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 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
a : ℝ≥0∞
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | a < f x} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
γ : G
x : α
⊢ x ∈ HSMul.hSMul (β := Set α) γ {x : α | a < f x} ↔ Membership.mem (γ := Set α) {x : α | a < f x} x
have h : Membership.mem (γ := Set α) {x : α | a < f x} (γ⁻¹ • x) ↔ Membership.mem (γ := Set α) {x : α | a < f x} x
Tactic: rw [mem_smul_set_iff_inv_smul_mem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
inst_2 : Group H
inst_3 : MulAction H α
inst_4 : SMulCommClass H G α
g : H
⊢ fundamentalFrontier G (g • s) = g • fundamentalFrontier G s
have simp_rw : g • s ∩ ⋃ (g_1 : G), ⋃ (_ : g_1 ≠ 1), g_1 • g • s = g • (s ∩ ⋃ (g : G), ⋃ (_ : g ≠ 1), g • s)
Tactic: simp_rw [fundamentalFrontier, smul_set_inter, smul_set_iUnion, smul_comm g (_ : G) (_ : Set α)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
inst_2 : Group H
inst_3 : MulAction H α
inst_4 : SMulCommClass H G α
g : H
simp_rw : g • s ∩ ⋃ (g_1 : G), ⋃ (_ : g_1 ≠ 1), g_1 • g • s = g • (s ∩ ⋃ (g : G), ⋃ (_ : g ≠ 1), g • s)
⊢ fundamentalFrontier G (g • s) = g • fundamentalFrontier G s
have simp_rw₁ : g • s ∩ ⋃ (g_1 : G), ⋃ (_ : g_1 ≠ 1), g_1 • g • s = g • s ∩ HSMul.hSMul (β := Set α) g (⋃ (g : G), ⋃ (_ : g ≠ 1), g • s)
Tactic: simp_rw [fundamentalFrontier, smul_set_inter, smul_set_iUnion, smul_comm g (_ : G) (_ : Set α)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
inst_2 : Group H
inst_3 : MulAction H α
inst_4 : SMulCommClass H G α
g : H
simp_rw : g • s ∩ ⋃ (g_1 : G), ⋃ (_ : g_1 ≠ 1), g_1 • g • s = g • (s ∩ ⋃ (g : G), ⋃ (_ : g ≠ 1), g • s)
simp_rw₁ :
  g • s ∩ ⋃ (g_1 : G), ⋃ (_ : g_1 ≠ 1), g_1 • g • s =
    g • s ∩ HSMul.hSMul (β := Set α) g (⋃ (g : G), ⋃ (_ : g ≠ 1), g • s)
⊢ fundamentalFrontier G (g • s) = g • fundamentalFrontier G s
have simp_rw₂ : g • s ∩ ⋃ (g_1 : G), ⋃ (_ : g_1 ≠ 1), g_1 • g • s = g • s ∩ ⋃ (i : G), ⋃ (_ : i ≠ 1), g • i • s
Tactic: simp_rw [fundamentalFrontier, smul_set_inter, smul_set_iUnion, smul_comm g (_ : G) (_ : Set α)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
inst_2 : Group H
inst_3 : MulAction H α
inst_4 : SMulCommClass H G α
g : H
⊢ fundamentalInterior G (g • s) = g • fundamentalInterior G s
have simp_rw : g • s \ ⋃ (g_1 : G), ⋃ (_ : g_1 ≠ 1), g_1 • g • s = g • (s \ ⋃ (g : G), ⋃ (_ : g ≠ 1), g • s)
Tactic: simp_rw [fundamentalInterior, smul_set_sdiff, smul_set_iUnion, smul_comm g (_ : G) (_ : Set α)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
inst_2 : Group H
inst_3 : MulAction H α
inst_4 : SMulCommClass H G α
g : H
simp_rw : g • s \ ⋃ (g_1 : G), ⋃ (_ : g_1 ≠ 1), g_1 • g • s = g • (s \ ⋃ (g : G), ⋃ (_ : g ≠ 1), g • s)
⊢ fundamentalInterior G (g • s) = g • fundamentalInterior G s
have simp_rw₁ : g • s \ ⋃ (g_1 : G), ⋃ (_ : g_1 ≠ 1), g_1 • g • s = g • s \ HSMul.hSMul (β := Set α) g (⋃ (g : G), ⋃ (_ : g ≠ 1), g • s)
Tactic: simp_rw [fundamentalInterior, smul_set_sdiff, smul_set_iUnion, smul_comm g (_ : G) (_ : Set α)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
H : Type u_2
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
inst_2 : Group H
inst_3 : MulAction H α
inst_4 : SMulCommClass H G α
g : H
simp_rw : g • s \ ⋃ (g_1 : G), ⋃ (_ : g_1 ≠ 1), g_1 • g • s = g • (s \ ⋃ (g : G), ⋃ (_ : g ≠ 1), g • s)
simp_rw₁ :
  g • s \ ⋃ (g_1 : G), ⋃ (_ : g_1 ≠ 1), g_1 • g • s =
    g • s \ HSMul.hSMul (β := Set α) g (⋃ (g : G), ⋃ (_ : g ≠ 1), g • s)
⊢ fundamentalInterior G (g • s) = g • fundamentalInterior G s
have simp_rw₂ : g • s \ ⋃ (g_1 : G), ⋃ (_ : g_1 ≠ 1), g_1 • g • s = g • s \ ⋃ (i : G), ⋃ (_ : i ≠ 1), g • i • s
Tactic: simp_rw [fundamentalInterior, smul_set_sdiff, smul_set_iUnion, smul_comm g (_ : G) (_ : Set α)]
-- 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 α
s : Set α
⊢ Pairwise.{u_1} (α := G) (onFun.{u_1 + 1, u_3 + 1, 1} (β := Set α) Disjoint fun (g : G) ↦ g • fundamentalInterior G s)
have refine : ∀ (a b : G) (hab : a ≠ b) ⦃a_1 : α⦄,
  Membership.mem (γ := Set α) ((fun (g : G) ↦ g • fundamentalInterior G s) a) a_1 →
    a_1 ∉ (fun (g : G) ↦ g • fundamentalInterior G s) b
Tactic: refine fun a b hab => disjoint_left.2 ?_
-- 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 α
s : Set α
a b : G
hab : a ≠ b
x : α
hx : x ∈ fundamentalInterior G s
y : α
hy : y ∈ fundamentalInterior G s
hxy : Eq.{u_3 + 1} (α := α) ((fun (x : α) ↦ b • x) y) ((fun (x : α) ↦ a • x) x)
⊢ False
have rw : ∀ (hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s) (y : α) (hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s)
  (hxy : Eq.{u_3 + 1} (α := α) ((fun (x : α) ↦ b • x) y) ((fun (x : α) ↦ a • x) x)), False
Tactic: rw [mem_fundamentalInterior] at hx hy
Cleared hypotheses: hx, y, hy, hxy
-- 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 α
s : Set α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s
hxy : Eq.{u_3 + 1} (α := α) ((fun (x : α) ↦ b • x) y) ((fun (x : α) ↦ a • x) x)
⊢ False
have refine_1 : a⁻¹ * b ≠ 1
Tactic: refine hx.2 (a⁻¹ * b) ?_ ?_
-- 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 α
s : Set α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s
hxy : Eq.{u_3 + 1} (α := α) ((fun (x : α) ↦ b • x) y) ((fun (x : α) ↦ a • x) x)
refine_1 : a⁻¹ * b ≠ 1
⊢ False
have refine_2 : x ∈ (a⁻¹ * b) • s
Tactic: refine hx.2 (a⁻¹ * b) ?_ ?_
-- 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 α
s : Set α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s
hxy : Eq.{u_3 + 1} (α := α) ((fun (x : α) ↦ b • x) y) ((fun (x : α) ↦ a • x) x)
⊢ a⁻¹ * b ≠ 1
have refine_1 : ¬a⁻¹ * b = 1
Tactic: rwa [Ne, inv_mul_eq_iff_eq_mul, mul_one, eq_comm]
-- 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 α
s : Set α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s
hxy : Eq.{u_3 + 1} (α := α) ((fun (x : α) ↦ b • x) y) ((fun (x : α) ↦ a • x) x)
refine_1 : ¬a⁻¹ * b = 1
⊢ a⁻¹ * b ≠ 1
have refine_1₁ : ¬b = a * 1
Tactic: rwa [Ne, inv_mul_eq_iff_eq_mul, mul_one, eq_comm]
-- 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 α
s : Set α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s
hxy : Eq.{u_3 + 1} (α := α) ((fun (x : α) ↦ b • x) y) ((fun (x : α) ↦ a • x) x)
refine_1 : ¬a⁻¹ * b = 1
refine_1₁ : ¬b = a * 1
⊢ a⁻¹ * b ≠ 1
have refine_1₂ : ¬b = a
Tactic: rwa [Ne, inv_mul_eq_iff_eq_mul, mul_one, eq_comm]
-- 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 α
s : Set α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s
hxy : Eq.{u_3 + 1} (α := α) ((fun (x : α) ↦ b • x) y) ((fun (x : α) ↦ a • x) x)
refine_1 : ¬a⁻¹ * b = 1
refine_1₁ : ¬b = a * 1
refine_1₂ : ¬b = a
⊢ a⁻¹ * b ≠ 1
have refine_1₃ : ¬a = b
Tactic: rwa [Ne, inv_mul_eq_iff_eq_mul, mul_one, eq_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Countable G
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
⊢ ∀ᵐ (x : α) ∂μ, ∃ (g : G), g • x ∈ fundamentalInterior G s
have simp_rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : G), i⁻¹ • fundamentalInterior G s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [ae_iff, not_exists, ← mem_inv_smul_set_iff, setOf_forall, ← compl_setOf,
      setOf_mem_eq, ← compl_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.FundamentalDomain (goal)
Goal:
G : Type u_1
α : Type u_3
inst : Countable G
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst_4 : MeasurableConstSMul G α
inst_5 : SMulInvariantMeasure G α μ
⊢ Subset.{u_3} (α := Set α) ((⋃ (g : G), g⁻¹ • s) \ ⋃ (g : G), g⁻¹ • fundamentalFrontier G s)
    (⋃ (g : G), g⁻¹ • fundamentalInterior G s)
have simp_rw : Subset.{u_3} (α := Set α) (⋃ (g : G), g⁻¹ • s) (⋃ (g : G), g⁻¹ • s)
Tactic: simp_rw [diff_subset_iff, ← iUnion_union_distrib, ← smul_set_union (α := G) (β := α),
        fundamentalFrontier_union_fundamentalInterior]