-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem exists_ne_one_smul_eq (hs : IsFundamentalDomain G s μ) (htm : NullMeasurableSet t μ)
    (ht : μ s < μ t) : ∃ x ∈ t, ∃ y ∈ t, ∃ g, g ≠ (1 : G) ∧ g • x = y

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y
⊢ μ t ≤ μ s

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

Result:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
⊢ (Disjoint on fun g => g • t ∩ s) g₁ g₂

Proof state:
case intro.intro.intro.intro
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ 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

Tactic:
rw [mul_smul, ← hxy, inv_smul_smul]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
⊢ ∀ ⦃a : α⦄, a ∈ g₁ • t → a ∉ g₂ • t

Tactic:
rintro _ ⟨x, hx, rfl⟩ ⟨y, hy, hxy : g₂ • y = g₁ • x⟩

Result:
case intro.intro.intro.intro
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ 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

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
⊢ (Disjoint on fun g => g • t ∩ s) g₁ g₂

Tactic:
dsimp [Function.onFun]

Result:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
⊢ Disjoint (g₁ • t ∩ s) (g₂ • t ∩ s)

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
⊢ Disjoint (g₁ • t ∩ s) (g₂ • t ∩ s)

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

Result:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
⊢ Disjoint (g₁ • t) (g₂ • t)

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
⊢ Disjoint (g₁ • t) (g₂ • t)

Tactic:
rw [Set.disjoint_left]

Result:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y
g₁ g₂ : G
hne : g₁ ≠ g₂
⊢ ∀ ⦃a : α⦄, a ∈ g₁ • t → a ∉ g₂ • t

Proof state:
case intro.intro.intro.intro
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ 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:
refine ht x hx y hy (g₂⁻¹ * g₁) (mt inv_mul_eq_one.1 hne.symm) ?_

Result:
case intro.intro.intro.intro
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ 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

Proof state:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : μ s < μ t
⊢ ∃ x ∈ t, ∃ y ∈ t, ∃ g, g ≠ 1 ∧ g • x = y

Tactic:
contrapose! ht

Result:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
htm : NullMeasurableSet t μ
ht : ∀ x ∈ t, ∀ y ∈ t, ∀ (g : G), g ≠ 1 → g • x ≠ y
⊢ μ t ≤ μ s