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

State before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
⊢ ∀ a ∈ t, ∀ b ∈ t, ∃ g, g • a = b
Tactic:
intro a ha b hb
State after:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ ∃ g, g • a = b

State before:
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ ∃ g, g • a = b
Tactic:
use ⟨Equiv.swap a b, ?_⟩
State after:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ { val := swap a b, property := ?w } • a = b

case w
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ swap a b ∈ G

State before:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ { val := swap a b, property := ?w } • a = b
Tactic:
change Equiv.swap a b • a = b
State after:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ swap a b • a = b

State before:
case h
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ swap a b • a = b
Tactic:
simp only [Equiv.Perm.smul_def, Equiv.swap_apply_left]
State after:
no goals

State before:
case w
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ swap a b ∈ G
Tactic:
apply le_of_lt hGt
State after:
case w.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ swap a b ∈ stabilizer (Perm α) t

State before:
case w.a
α : Type u_1
inst✝³ : DecidableEq α
G✝ : Type ?u.17243
inst✝² : Group G✝
inst✝¹ : MulAction G✝ α
inst✝ : Fintype α
G : Subgroup (Perm α)
t : Set α
hGt : stabilizer (Perm α) t < G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ swap a b ∈ stabilizer (Perm α) t
Tactic:
apply swap_mem_stabilizer ha hb
State after:
no goals