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 t : Set α
μ : Measure α
inst_3 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
ht : NullMeasurableSet t μ
hd : Pairwise.{u_1} (α := G) (AEDisjoint μ on fun (g : G) ↦ g • t ∩ s)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
calc
    μ t = ∑' g : G, μ (g • t ∩ s) := hs.measure_eq_tsum t
    _ = μ (⋃ g : G, g • t ∩ s) := Eq.symm <| measure_iUnion₀ hd fun _ =>
      (ht.smul _).inter hs.nullMeasurableSet
    _ ≤ μ s := measure_mono (iUnion_subset fun _ => inter_subset_right)

Premises used: Trans.trans, Set.iUnion_subset, MeasureTheory.measure_iUnion₀, MeasureTheory.NullMeasurableSet.inter, MeasureTheory.IsFundamentalDomain.nullMeasurableSet, MeasureTheory.NullMeasurableSet.smul, MeasureTheory.measure_mono, Eq.symm, MeasureTheory.IsFundamentalDomain.measure_eq_tsum, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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∞)
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∞)
⊢ ∃ x ∈ t, ∃ y ∈ t, ∃ (g : G), g ≠ 1 ∧ g • x = y

Tactic:
contrapose! ht
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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∞)

Tactic:
hs.measure_le_of_pairwise_disjoint htm (Pairwise.aedisjoint fun g₁ g₂ hne => ?_)

Premises used: MeasureTheory.IsFundamentalDomain.measure_le_of_pairwise_disjoint, Pairwise.aedisjoint
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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
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₂
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine hs.measure_le_of_pairwise_disjoint htm (Pairwise.aedisjoint fun g₁ g₂ hne => ?_)

Premises used: MeasureTheory.IsFundamentalDomain.measure_le_of_pairwise_disjoint, Pairwise.aedisjoint
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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)

Tactic:
(Disjoint.inf_left _ ?_).inf_right _

Premises used: Disjoint.inf_right, Disjoint.inf_left
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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₂
refine : Disjoint (g₁ • t) (g₂ • t)
⊢ Disjoint (g₁ • t ∩ s) (g₂ • t ∩ s)

Tactic:
refine (Disjoint.inf_left _ ?_).inf_right _

Premises used: Disjoint.inf_right, Disjoint.inf_left
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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₂
rw : ∀ ⦃a : α⦄, a ∈ g₁ • t → a ∉ g₂ • t
⊢ Disjoint (g₁ • t) (g₂ • t)

Tactic:
rw [Set.disjoint_left]

Premises used: Set.disjoint_left
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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

Tactic:
ht x hx y hy (g₂⁻¹ * g₁) (mt inv_mul_eq_one.1 hne.symm) ?_

Premises used: HMul.hMul, mt, Ne.symm, Inv.inv, Iff.mp, inv_mul_eq_one
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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
refine : (g₂⁻¹ * g₁) • x = y
⊢ False

Tactic:
refine ht x hx y hy (g₂⁻¹ * g₁) (mt inv_mul_eq_one.1 hne.symm) ?_

Premises used: HMul.hMul, mt, Ne.symm, Inv.inv, Iff.mp, inv_mul_eq_one
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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
rw₂ rw₃ : y = y
⊢ (g₂⁻¹ * g₁) • x = y

Tactic:
rw [mul_smul, ← hxy, inv_smul_smul]

Premises used: inv_smul_smul, SemigroupAction.mul_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 α
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 μ

Tactic:
le_antisymm (essSup_mono_measure' Measure.restrict_le_self) ?_

Premises used: le_antisymm, MeasureTheory.Measure.restrict_le_self, essSup_mono_measure'
-- 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 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
refine : essSup f μ ≤ essSup f (μ.restrict s)
⊢ essSup f (μ.restrict s) = essSup f μ

Tactic:
refine le_antisymm (essSup_mono_measure' Measure.restrict_le_self) ?_

Premises used: le_antisymm, MeasureTheory.Measure.restrict_le_self, essSup_mono_measure'
-- 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 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
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∞)})
⊢ essSup f μ ≤ essSup f (μ.restrict s)

Tactic:
rw [essSup_eq_sInf (μ.restrict s) f, essSup_eq_sInf μ f]

Premises used: essSup_eq_sInf, MeasureTheory.Measure.restrict
-- 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 : 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∞)})

Tactic:
sInf_le_sInf ?_

Premises used: sInf_le_sInf
-- 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 : MeasurableConstSMul G α
inst_4 : SMulInvariantMeasure G α μ
inst_5 : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
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∞)}
⊢ 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:
refine sInf_le_sInf ?_

Premises used: sInf_le_sInf
-- 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 : 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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | a < f x} ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Measure.restrict_apply₀' hs.nullMeasurableSet] at ha

Premises used: MeasureTheory.IsFundamentalDomain.nullMeasurableSet, MeasureTheory.Measure.restrict_apply₀'
-- 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 : 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

Tactic:
measure_zero_of_invariant hs _ ?_ ha

Premises used: Set.Mem, setOf, MeasureTheory.IsFundamentalDomain.measure_zero_of_invariant
-- 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 : 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∞)
refine : ∀ (g : G), HSMul.hSMul (β := Set α) g {x : α | a < f x} = {x : α | a < f x}
⊢ Membership.mem (γ := Set ℝ≥0∞)
    {a : ℝ≥0∞ | Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | a < f x} : ℝ≥0∞) (0 : ℝ≥0∞)} a

Tactic:
refine measure_zero_of_invariant hs _ ?_ ha

Premises used: MeasureTheory.IsFundamentalDomain.measure_zero_of_invariant
-- 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 : 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
h : ∀ (x : α), x ∈ HSMul.hSMul (β := Set α) γ {x : α | a < f x} ↔ Membership.mem (γ := Set α) {x : α | a < f x} x
⊢ HSMul.hSMul (β := Set α) γ {x : α | a < f x} = {x : α | a < f x}

Tactic:
ext x
-- 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 : 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 : α
h : Membership.mem (γ := Set α) {x : α | a < f x} (γ⁻¹ • x) ↔ Membership.mem (γ := Set α) {x : α | a < f x} x
⊢ x ∈ HSMul.hSMul (β := Set α) γ {x : α | a < f x} ↔ Membership.mem (γ := Set α) {x : α | a < f x} x

Tactic:
rw [mem_smul_set_iff_inv_smul_mem]

Premises used: Set.mem_smul_set_iff_inv_smul_mem
-- 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 : 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 : α
⊢ Membership.mem (γ := Set α) {x : α | a < f x} (γ⁻¹ • x) ↔ Membership.mem (γ := Set α) {x : α | a < f x} x

Tactic:
simp only [mem_setOf_eq, hf γ⁻¹ x]

Premises used: Set.mem_setOf_eq, Inv.inv
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
x : α
⊢ x ∈ fundamentalFrontier G s ↔ x ∈ s ∧ ∃ (g : G), g ≠ 1 ∧ x ∈ g • s

Tactic:
simp [fundamentalFrontier]

Premises used: MeasureTheory.fundamentalFrontier
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
x : α
⊢ x ∈ fundamentalInterior G s ↔ x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s

Tactic:
simp [fundamentalInterior]

Premises used: MeasureTheory.fundamentalInterior
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
⊢ fundamentalFrontier G s ⊆ s

Tactic:
inter_subset_left

Premises used: Set.inter_subset_left, MeasureTheory.fundamentalFrontier
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
⊢ fundamentalInterior G s ⊆ s

Tactic:
diff_subset

Premises used: Set.diff_subset, MeasureTheory.fundamentalInterior
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
⊢ Disjoint (fundamentalInterior G s) (fundamentalFrontier G s)

Tactic:
disjoint_sdiff_self_left.mono_right inf_le_right

Premises used: inf_le_right, Disjoint.mono_right, disjoint_sdiff_self_left
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
⊢ fundamentalInterior G s ∪ fundamentalFrontier G s = s

Tactic:
diff_union_inter _ _

Premises used: MeasureTheory.fundamentalInterior, MeasureTheory.fundamentalFrontier, Set.diff_union_inter
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
⊢ fundamentalFrontier G s ∪ fundamentalInterior G s = s

Tactic:
inter_union_diff _ _

Premises used: MeasureTheory.fundamentalInterior, MeasureTheory.fundamentalFrontier, Set.inter_union_diff
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
⊢ s \ fundamentalInterior G s = fundamentalFrontier G s

Tactic:
sdiff_sdiff_right_self

Premises used: MeasureTheory.fundamentalInterior, MeasureTheory.fundamentalFrontier, sdiff_sdiff_right_self
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
⊢ s \ fundamentalFrontier G s = fundamentalInterior G s

Tactic:
diff_self_inter

Premises used: Set.diff_self_inter, MeasureTheory.fundamentalInterior, MeasureTheory.fundamentalFrontier
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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)
simp_rw₂ : g • s ∩ ⋃ (g_1 : G), ⋃ (_ : g_1 ≠ 1), g_1 • g • s = g • s ∩ ⋃ (i : G), ⋃ (_ : i ≠ 1), g • i • s
⊢ fundamentalFrontier G (g • s) = g • fundamentalFrontier G s

Tactic:
simp_rw [fundamentalFrontier, smul_set_inter, smul_set_iUnion, smul_comm g (_ : G) (_ : Set α)]

Premises used: Set.smul_set_inter, MeasureTheory.fundamentalFrontier, Set.smul_set_iUnion, SMulCommClass.smul_comm
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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)
simp_rw₂ : g • s \ ⋃ (g_1 : G), ⋃ (_ : g_1 ≠ 1), g_1 • g • s = g • s \ ⋃ (i : G), ⋃ (_ : i ≠ 1), g • i • s
⊢ fundamentalInterior G (g • s) = g • fundamentalInterior G s

Tactic:
simp_rw [fundamentalInterior, smul_set_sdiff, smul_set_iUnion, smul_comm g (_ : G) (_ : Set α)]

Premises used: MeasureTheory.fundamentalInterior, Set.smul_set_sdiff, Set.smul_set_iUnion, SMulCommClass.smul_comm
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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)

Tactic:
fun a b hab => disjoint_left.2 ?_

Premises used: Iff.mpr, Set.disjoint_left, Pairwise
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
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
⊢ Pairwise.{u_1} (α := G) (onFun.{u_1 + 1, u_3 + 1, 1} (β := Set α) Disjoint fun (g : G) ↦ g • fundamentalInterior G s)

Tactic:
refine fun a b hab => disjoint_left.2 ?_

Premises used: Iff.mpr, Set.disjoint_left
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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)
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
⊢ False

Tactic:
rw [mem_fundamentalInterior] at hx hy

Premises used: MeasureTheory.mem_fundamentalInterior
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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

Tactic:
hx.2 (a⁻¹ * b) ?_ ?_

Premises used: HMul.hMul, Inv.inv, And.right
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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_2 : x ∈ (a⁻¹ * b) • s
⊢ False

Tactic:
refine hx.2 (a⁻¹ * b) ?_ ?_

Premises used: HMul.hMul, Inv.inv, And.right
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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
refine_1₃ refine_1₄ refine_1₅ refine_1₆ : ¬a = b
⊢ a⁻¹ * b ≠ 1

Tactic:
rwa [Ne, inv_mul_eq_iff_eq_mul, mul_one, eq_comm]

Premises used: Ne, eq_comm, mul_one, inv_mul_eq_iff_eq_mul
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
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)
⊢ x ∈ (a⁻¹ * b) • s

Tactic:
simpa [mul_smul, ← hxy, mem_inv_smul_set_iff] using hy.1

Premises used: Set.mem_inv_smul_set_iff, And.left, SemigroupAction.mul_smul
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
inst_2 : Countable G
inst_3 : MeasurableSpace α
inst_4 : MeasurableConstSMul G α
μ : Measure α
inst_5 : SMulInvariantMeasure G α μ
hs : NullMeasurableSet s μ
⊢ NullMeasurableSet (fundamentalFrontier G s) μ

Tactic:
hs.inter <| .iUnion fun _ => .iUnion fun _ => hs.smul _

Premises used: MeasureTheory.fundamentalFrontier, MeasureTheory.NullMeasurableSet.inter, MeasureTheory.NullMeasurableSet.smul, MeasureTheory.NullMeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Group.FundamentalDomain
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
s : Set α
inst_2 : Countable G
inst_3 : MeasurableSpace α
inst_4 : MeasurableConstSMul G α
μ : Measure α
inst_5 : SMulInvariantMeasure G α μ
hs : NullMeasurableSet s μ
⊢ NullMeasurableSet (fundamentalInterior G s) μ

Tactic:
hs.diff <| .iUnion fun _ => .iUnion fun _ => hs.smul _

Premises used: MeasureTheory.fundamentalInterior, MeasureTheory.NullMeasurableSet.smul, MeasureTheory.NullMeasurableSet.iUnion, MeasureTheory.NullMeasurableSet.diff