Theorem: alternatingGroup.stabilizer_ne_top' (Jordan/AlternatingMaximal.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : Set.Nonempty s
hsc : Set.Nontrivial sᶜ
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤
Tactic:
obtain ⟨a, ha⟩ := hs
State after:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
a : α
ha : a ∈ s
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤

State before:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
a : α
ha : a ∈ s
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤
Tactic:
obtain ⟨b, hb, c, hc, hbc⟩ := hsc
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
c : α
hc : c ∈ sᶜ
hbc : b ≠ c
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤
Tactic:
rw [Set.mem_compl_iff] at hb hc
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤
Tactic:
have hac : a ≠ c := by intro h; apply hc; rw [← h]; exact ha
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤
Tactic:
have hab : a ≠ b := by intro h; apply hb; rw [← h]; exact ha
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤
Tactic:
intro h
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
⊢ False

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
⊢ False
Tactic:
apply hc
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
⊢ c ∈ s

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
⊢ c ∈ s
Tactic:
let g := Equiv.swap a b * Equiv.swap a c
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
⊢ c ∈ s

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
⊢ c ∈ s
Tactic:
have hg : g ∈ alternatingGroup α :=
  by
  rw [Equiv.Perm.mem_alternatingGroup]
  apply Equiv.Perm.IsThreeCycle.sign
  apply Equiv.Perm.isThreeCycle_swap_mul_swap_same hab hac hbc
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
⊢ c ∈ s

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
⊢ c ∈ s
Tactic:
suffices g • s = s by
  rw [← this]
  use a
  constructor; exact ha
  dsimp [g]
  rw [Equiv.swap_apply_left]
  rw [Equiv.swap_apply_of_ne_of_ne hac.symm hbc.symm]
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
⊢ g • s = s

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
⊢ g • s = s
Tactic:
change (⟨g, hg⟩ : alternatingGroup α) • s = s
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
⊢ { val := g, property := hg } • s = s

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
⊢ { val := g, property := hg } • s = s
Tactic:
rw [← MulAction.mem_stabilizer_iff]
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
⊢ { val := g, property := hg } ∈ stabilizer (↥(alternatingGroup α)) s

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
⊢ { val := g, property := hg } ∈ stabilizer (↥(alternatingGroup α)) s
Tactic:
erw [h]
State after:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
⊢ { val := g, property := hg } ∈ ⊤

State before:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
⊢ { val := g, property := hg } ∈ ⊤
Tactic:
apply Subgroup.mem_top
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
⊢ a ≠ c
Tactic:
intro h
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
h : a = c
⊢ False

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
h : a = c
⊢ False
Tactic:
apply hc
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
h : a = c
⊢ c ∈ s

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
h : a = c
⊢ c ∈ s
Tactic:
rw [← h]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
h : a = c
⊢ a ∈ s

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
h : a = c
⊢ a ∈ s
Tactic:
exact ha
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
⊢ a ≠ b
Tactic:
intro h
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
h : a = b
⊢ False

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
h : a = b
⊢ False
Tactic:
apply hb
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
h : a = b
⊢ b ∈ s

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
h : a = b
⊢ b ∈ s
Tactic:
rw [← h]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
h : a = b
⊢ a ∈ s

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
h : a = b
⊢ a ∈ s
Tactic:
exact ha
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
⊢ g ∈ alternatingGroup α
Tactic:
rw [Equiv.Perm.mem_alternatingGroup]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
⊢ Equiv.Perm.sign g = 1

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
⊢ Equiv.Perm.sign g = 1
Tactic:
apply Equiv.Perm.IsThreeCycle.sign
State after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
⊢ Equiv.Perm.IsThreeCycle g

State before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
⊢ Equiv.Perm.IsThreeCycle g
Tactic:
apply Equiv.Perm.isThreeCycle_swap_mul_swap_same hab hac hbc
State after:
no goals

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ c ∈ s
Tactic:
rw [← this]
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ c ∈ g • s

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ c ∈ g • s
Tactic:
use a
State after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ a ∈ s ∧ (fun x => g • x) a = c

State before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ a ∈ s ∧ (fun x => g • x) a = c
Tactic:
constructor
State after:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ a ∈ s

case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ (fun x => g • x) a = c

State before:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ a ∈ s

case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ (fun x => g • x) a = c
Tactic:
exact ha
State after:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ (fun x => g • x) a = c

State before:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ (fun x => g • x) a = c
Tactic:
dsimp [g]
State after:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ (Equiv.swap a b) ((Equiv.swap a c) a) = c

State before:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ (Equiv.swap a b) ((Equiv.swap a c) a) = c
Tactic:
rw [Equiv.swap_apply_left]
State after:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ (Equiv.swap a b) c = c

State before:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
c : α
hc : c ∉ s
hbc : b ≠ c
hac : a ≠ c
hab : a ≠ b
h : stabilizer (↥(alternatingGroup α)) s = ⊤
g : Equiv.Perm α := Equiv.swap a b * Equiv.swap a c
hg : g ∈ alternatingGroup α
this : g • s = s
⊢ (Equiv.swap a b) c = c
Tactic:
rw [Equiv.swap_apply_of_ne_of_ne hac.symm hbc.symm]
State after:
no goals