-- Mathlib/GroupTheory/Perm/ClosureSwap.lean
theorem exists_smul_not_mem_of_subset_orbit_closure (S : Set G) (T : Set α) {a : α}
    (hS : ∀ g ∈ S, g⁻¹ ∈ S) (subset : T ⊆ orbit (closure S) a) (not_mem : a ∉ T)
    (nonempty : T.Nonempty) : ∃ σ ∈ S, ∃ a ∈ T, σ • a ∉ T

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
not_mem : a ∉ T
nonempty : T.Nonempty
key0 : ∀ σ ∈ S, ∀ a ∈ T, σ • a ∈ T
⊢ closure S ≤ stabilizer G T

Tactic:
refine (closure_le _).mpr fun σ hσ ↦ ?_

Result:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
not_mem : a ∉ T
nonempty : T.Nonempty
key0 : ∀ σ ∈ S, ∀ a ∈ T, σ • a ∈ T
σ : G
hσ : σ ∈ S
⊢ σ ∈ ↑(stabilizer G T)

Proof state:
case intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
nonempty : T.Nonempty
σ : ↥(closure S)
hb : (fun m => m • a) σ ∈ T
h : closure S ≤ stabilizer G T
⊢ a ∈ T

Tactic:
exact smul_mem_smul_set_iff.mp ((h σ.2).symm ▸ hb)

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
not_mem : a ∉ T
nonempty : T.Nonempty
key0 : ¬closure S ≤ stabilizer G T
⊢ ∃ σ ∈ S, ∃ a ∈ T, σ • a ∉ T

Tactic:
contrapose! key0

Result:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
not_mem : a ∉ T
nonempty : T.Nonempty
key0 : ∀ σ ∈ S, ∀ a ∈ T, σ • a ∈ T
⊢ closure S ≤ stabilizer G T

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
not_mem : a ∉ T
nonempty : T.Nonempty
⊢ ¬closure S ≤ stabilizer G T

Tactic:
have ⟨b, hb⟩ := nonempty

Result:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
not_mem : a ∉ T
nonempty : T.Nonempty
b : α
hb : b ∈ T
⊢ ¬closure S ≤ stabilizer G T

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
not_mem : a ∉ T
nonempty : T.Nonempty
key0 : ∀ σ ∈ S, ∀ a ∈ T, σ • a ∈ T
σ : G
hσ : σ ∈ S
⊢ σ ∈ ↑(stabilizer G T)

Tactic:
simp_rw [SetLike.mem_coe, mem_stabilizer_iff, Set.ext_iff, mem_smul_set_iff_inv_smul_mem]

Result:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
not_mem : a ∉ T
nonempty : T.Nonempty
key0 : ∀ σ ∈ S, ∀ a ∈ T, σ • a ∈ T
σ : G
hσ : σ ∈ S
⊢ ∀ (x : α), σ⁻¹ • x ∈ T ↔ x ∈ T

Proof state:
case intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
not_mem : a ∉ T
nonempty : T.Nonempty
σ : ↥(closure S)
hb : (fun m => m • a) σ ∈ T
⊢ ¬closure S ≤ stabilizer G T

Tactic:
contrapose! not_mem with h

Result:
case intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
nonempty : T.Nonempty
σ : ↥(closure S)
hb : (fun m => m • a) σ ∈ T
h : closure S ≤ stabilizer G T
⊢ a ∈ T

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
not_mem : a ∉ T
nonempty : T.Nonempty
⊢ ∃ σ ∈ S, ∃ a ∈ T, σ • a ∉ T

Tactic:
have key0 : ¬ closure S ≤ stabilizer G T := by
  have ⟨b, hb⟩ := nonempty
  obtain ⟨σ, rfl⟩ := subset hb
  contrapose! not_mem with h
  exact smul_mem_smul_set_iff.mp ((h σ.2).symm ▸ hb)

Result:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
not_mem : a ∉ T
nonempty : T.Nonempty
key0 : ¬closure S ≤ stabilizer G T
⊢ ∃ σ ∈ S, ∃ a ∈ T, σ • a ∉ T

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
not_mem : a ∉ T
nonempty : T.Nonempty
key0 : ∀ σ ∈ S, ∀ a ∈ T, σ • a ∈ T
σ : G
hσ : σ ∈ S
⊢ ∀ (x : α), σ⁻¹ • x ∈ T ↔ x ∈ T

Tactic:
exact fun a ↦ ⟨fun h ↦ smul_inv_smul σ a ▸ key0 σ hσ (σ⁻¹ • a) h, key0 σ⁻¹ (hS σ hσ) a⟩

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
not_mem : a ∉ T
nonempty : T.Nonempty
b : α
hb : b ∈ T
⊢ ¬closure S ≤ stabilizer G T

Tactic:
obtain ⟨σ, rfl⟩ := subset hb

Result:
case intro
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit (↥(closure S)) a
not_mem : a ∉ T
nonempty : T.Nonempty
σ : ↥(closure S)
hb : (fun m => m • a) σ ∈ T
⊢ ¬closure S ≤ stabilizer G T