-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem pairwise_disjoint_fundamentalInterior :
    Pairwise (Disjoint on fun g : G => g • fundamentalInterior G s)

Proof state:
case intro.intro.intro.intro.refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : 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 : (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

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
⊢ Pairwise (Disjoint on fun g => g • fundamentalInterior G s)

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

Result:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
a b : G
hab : a ≠ b
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ (fun g => g • fundamentalInterior G s) a → a_1 ∉ (fun g => g • fundamentalInterior G s) b

Proof state:
case intro.intro.intro.intro
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : 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 : (fun x => b • x) y = (fun x => a • x) x
⊢ False

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

Result:
case intro.intro.intro.intro.refine_1
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : 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 : (fun x => b • x) y = (fun x => a • x) x
⊢ a⁻¹ * b ≠ 1

case intro.intro.intro.intro.refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : 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 : (fun x => b • x) y = (fun x => a • x) x
⊢ x ∈ (a⁻¹ * b) • s

Proof state:
case intro.intro.intro.intro.refine_1
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : 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 : (fun x => b • x) y = (fun x => a • x) x
⊢ a⁻¹ * b ≠ 1

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

Result:
no goals

Proof state:
case intro.intro.intro.intro
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
a b : G
hab : a ≠ b
x : α
hx : x ∈ fundamentalInterior G s
y : α
hy : y ∈ fundamentalInterior G s
hxy : (fun x => b • x) y = (fun x => a • x) x
⊢ False

Tactic:
rw [mem_fundamentalInterior] at hx hy

Result:
case intro.intro.intro.intro
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : 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 : (fun x => b • x) y = (fun x => a • x) x
⊢ False

Proof state:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
a b : G
hab : a ≠ b
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ (fun g => g • fundamentalInterior G s) a → a_1 ∉ (fun g => g • fundamentalInterior G s) b

Tactic:
rintro _ ⟨x, hx, rfl⟩ ⟨y, hy, hxy⟩

Result:
case intro.intro.intro.intro
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
a b : G
hab : a ≠ b
x : α
hx : x ∈ fundamentalInterior G s
y : α
hy : y ∈ fundamentalInterior G s
hxy : (fun x => b • x) y = (fun x => a • x) x
⊢ False