G : Type u_1
H : Type ?u.515944
α : Type u_2
β : Type ?u.515950
E : Type ?u.515953
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x : α
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
G : Type u_1
H : Type ?u.515944
α : Type u_2
β : Type ?u.515950
E : Type ?u.515953
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x : α
⊢ Pairwise (Disjoint on fun g => g • fundamentalInterior G s)
refine' fun a b hab => disjoint_left.2 _
case intro.intro.intro.intro
G : Type u_1
H : Type ?u.515944
α : Type u_2
β : Type ?u.515950
E : Type ?u.515953
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x✝ : α
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
G : Type u_1
H : Type ?u.515944
α : Type u_2
β : Type ?u.515950
E : Type ?u.515953
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x : α
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
rintro _ ⟨x, hx, rfl⟩ ⟨y, hy, hxy⟩
case intro.intro.intro.intro
G : Type u_1
H : Type ?u.515944
α : Type u_2
β : Type ?u.515950
E : Type ?u.515953
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x✝ : α
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
case intro.intro.intro.intro
G : Type u_1
H : Type ?u.515944
α : Type u_2
β : Type ?u.515950
E : Type ?u.515953
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x✝ : α
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
rw [mem_fundamentalInterior] at hx hy
case intro.intro.intro.intro.refine'_1
G : Type u_1
H : Type ?u.515944
α : Type u_2
β : Type ?u.515950
E : Type ?u.515953
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x✝ : α
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
H : Type ?u.515944
α : Type u_2
β : Type ?u.515950
E : Type ?u.515953
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x✝ : α
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
case intro.intro.intro.intro
G : Type u_1
H : Type ?u.515944
α : Type u_2
β : Type ?u.515950
E : Type ?u.515953
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x✝ : α
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
refine' hx.2 (a⁻¹ * b) _ _
case intro.intro.intro.intro.refine'_2
G : Type u_1
H : Type ?u.515944
α : Type u_2
β : Type ?u.515950
E : Type ?u.515953
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x✝ : α
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
case intro.intro.intro.intro.refine'_1
G : Type u_1
H : Type ?u.515944
α : Type u_2
β : Type ?u.515950
E : Type ?u.515953
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x✝ : α
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
H : Type ?u.515944
α : Type u_2
β : Type ?u.515950
E : Type ?u.515953
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x✝ : α
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
rwa [Ne.def, inv_mul_eq_iff_eq_mul, mul_one, eq_comm]
no goals
case intro.intro.intro.intro.refine'_2
G : Type u_1
H : Type ?u.515944
α : Type u_2
β : Type ?u.515950
E : Type ?u.515953
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x✝ : α
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
simpa [mul_smul, ← hxy, mem_inv_smul_set_iff] using hy.1