G : Type u_1
H : Type ?u.435204
α : Type u_2
β : Type ?u.435210
E : Type ?u.435213
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hs : IsFundamentalDomain G s
htm : NullMeasurableSet t
ht : ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → ∀ (g : G), g ≠ 1 → g • x ≠ y
⊢ ↑↑μ t ≤ ↑↑μ s
G : Type u_1
H : Type ?u.435204
α : Type u_2
β : Type ?u.435210
E : Type ?u.435213
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hs : IsFundamentalDomain G s
htm : NullMeasurableSet t
ht : ↑↑μ s < ↑↑μ t
⊢ ∃ x, x ∈ t ∧ ∃ y, y ∈ t ∧ ∃ g, g ≠ 1 ∧ g • x = y
contrapose! ht
G : Type u_1
H : Type ?u.435204
α : Type u_2
β : Type ?u.435210
E : Type ?u.435213
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
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 on fun g => g • t ∩ s) g₁ g₂
G : Type u_1
H : Type ?u.435204
α : Type u_2
β : Type ?u.435210
E : Type ?u.435213
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hs : IsFundamentalDomain G s
htm : NullMeasurableSet t
ht : ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → ∀ (g : G), g ≠ 1 → g • x ≠ y
⊢ ↑↑μ t ≤ ↑↑μ s
refine' hs.measure_le_of_pairwise_disjoint htm (Pairwise.aedisjoint fun g₁ g₂ hne => _)
G : Type u_1
H : Type ?u.435204
α : Type u_2
β : Type ?u.435210
E : Type ?u.435213
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
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)
G : Type u_1
H : Type ?u.435204
α : Type u_2
β : Type ?u.435210
E : Type ?u.435213
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
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 on fun g => g • t ∩ s) g₁ g₂
dsimp [Function.onFun]
G : Type u_1
H : Type ?u.435204
α : Type u_2
β : Type ?u.435210
E : Type ?u.435213
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
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)
G : Type u_1
H : Type ?u.435204
α : Type u_2
β : Type ?u.435210
E : Type ?u.435213
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
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)
refine' (Disjoint.inf_left _ _).inf_right _
G : Type u_1
H : Type ?u.435204
α : Type u_2
β : Type ?u.435210
E : Type ?u.435213
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
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₂
⊢ ∀ ⦃a : α⦄, a ∈ g₁ • t → ¬a ∈ g₂ • t
G : Type u_1
H : Type ?u.435204
α : Type u_2
β : Type ?u.435210
E : Type ?u.435213
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
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)
rw [Set.disjoint_left]
case intro.intro.intro.intro
G : Type u_1
H : Type ?u.435204
α : Type u_2
β : Type ?u.435210
E : Type ?u.435213
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
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
G : Type u_1
H : Type ?u.435204
α : Type u_2
β : Type ?u.435210
E : Type ?u.435213
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
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₂
⊢ ∀ ⦃a : α⦄, a ∈ g₁ • t → ¬a ∈ g₂ • t
rintro _ ⟨x, hx, rfl⟩ ⟨y, hy, hxy : g₂ • y = g₁ • x⟩
case intro.intro.intro.intro
G : Type u_1
H : Type ?u.435204
α : Type u_2
β : Type ?u.435210
E : Type ?u.435213
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
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
case intro.intro.intro.intro
G : Type u_1
H : Type ?u.435204
α : Type u_2
β : Type ?u.435210
E : Type ?u.435213
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
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
refine' ht x hx y hy (g₂⁻¹ * g₁) (mt inv_mul_eq_one.1 hne.symm) _
no goals
case intro.intro.intro.intro
G : Type u_1
H : Type ?u.435204
α : Type u_2
β : Type ?u.435210
E : Type ?u.435213
inst✝¹² : Group G
inst✝¹¹ : Group H
inst✝¹⁰ : MulAction G α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : MulAction H β
inst✝⁷ : MeasurableSpace β
inst✝⁶ : NormedAddCommGroup E
s t : Set α
μ : Measure α
inst✝⁵ : MeasurableSpace G
inst✝⁴ : MeasurableSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
ν : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
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
rw [mul_smul, ← hxy, inv_smul_smul]