Theorem: Equiv.Perm.swap_mem_stabilizer (Jordan/PermMaximal.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ swap a b ∈ stabilizer (Perm α) s
Tactic:
suffices Equiv.swap a b • s ⊆ s by
  rw [mem_stabilizer_iff]
  apply Set.Subset.antisymm
  exact this
  exact Set.subset_set_smul_iff.mpr this
State after:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ swap a b • s ⊆ s

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
⊢ swap a b • s ⊆ s
Tactic:
rintro _ ⟨x, hx, rfl⟩
State after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
⊢ (fun x => swap a b • x) x ∈ s

State before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
⊢ (fun x => swap a b • x) x ∈ s
Tactic:
simp only [Equiv.Perm.smul_def]
State after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
⊢ (swap a b) x ∈ s

State before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
⊢ (swap a b) x ∈ s
Tactic:
cases' em (x = a) with hxa hxa'
State after:
case intro.intro.inl
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa : x = a
⊢ (swap a b) x ∈ s

case intro.intro.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
⊢ (swap a b) x ∈ s

State before:
case intro.intro.inl
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa : x = a
⊢ (swap a b) x ∈ s

case intro.intro.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
⊢ (swap a b) x ∈ s
Tactic:
rw [hxa, Equiv.swap_apply_left]
State after:
case intro.intro.inl
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa : x = a
⊢ b ∈ s

case intro.intro.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
⊢ (swap a b) x ∈ s

State before:
case intro.intro.inl
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa : x = a
⊢ b ∈ s

case intro.intro.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
⊢ (swap a b) x ∈ s
Tactic:
exact hb
State after:
case intro.intro.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
⊢ (swap a b) x ∈ s

State before:
case intro.intro.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
⊢ (swap a b) x ∈ s
Tactic:
cases' em (x = b) with hxb hxb'
State after:
case intro.intro.inr.inl
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb : x = b
⊢ (swap a b) x ∈ s

case intro.intro.inr.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb' : ¬x = b
⊢ (swap a b) x ∈ s

State before:
case intro.intro.inr.inl
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb : x = b
⊢ (swap a b) x ∈ s

case intro.intro.inr.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb' : ¬x = b
⊢ (swap a b) x ∈ s
Tactic:
rw [hxb, Equiv.swap_apply_right]
State after:
case intro.intro.inr.inl
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb : x = b
⊢ a ∈ s

case intro.intro.inr.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb' : ¬x = b
⊢ (swap a b) x ∈ s

State before:
case intro.intro.inr.inl
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb : x = b
⊢ a ∈ s

case intro.intro.inr.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb' : ¬x = b
⊢ (swap a b) x ∈ s
Tactic:
exact ha
State after:
case intro.intro.inr.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb' : ¬x = b
⊢ (swap a b) x ∈ s

State before:
case intro.intro.inr.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb' : ¬x = b
⊢ (swap a b) x ∈ s
Tactic:
rw [Equiv.swap_apply_of_ne_of_ne hxa' hxb']
State after:
case intro.intro.inr.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb' : ¬x = b
⊢ x ∈ s

State before:
case intro.intro.inr.inr
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
x : α
hx : x ∈ s
hxa' : ¬x = a
hxb' : ¬x = b
⊢ x ∈ s
Tactic:
exact hx
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ swap a b ∈ stabilizer (Perm α) s
Tactic:
rw [mem_stabilizer_iff]
State after:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ swap a b • s = s

State before:
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ swap a b • s = s
Tactic:
apply Set.Subset.antisymm
State after:
case h₁
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ swap a b • s ⊆ s

case h₂
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ s ⊆ swap a b • s

State before:
case h₁
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ swap a b • s ⊆ s

case h₂
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ s ⊆ swap a b • s
Tactic:
exact this
State after:
case h₂
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ s ⊆ swap a b • s

State before:
case h₂
α : Type u_1
inst✝² : DecidableEq α
G : Type ?u.11084
inst✝¹ : Group G
inst✝ : MulAction G α
a b : α
s : Set α
ha : a ∈ s
hb : b ∈ s
this : swap a b • s ⊆ s
⊢ s ⊆ swap a b • s
Tactic:
exact Set.subset_set_smul_iff.mpr this
State after:
no goals