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

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
⊢ ∀ a ∈ t, ∀ b ∈ t, ∃ g, g • a = b
Tactic:
intro a ha b hb
State after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ ∃ g, g • a = b

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ ∃ g, g • a = b
Tactic:
obtain ⟨g, hg, H⟩ := moves_in hα t a ha b hb
State after:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α
H : g • a = b
⊢ ∃ g, g • a = b

State before:
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α
H : g • a = b
⊢ ∃ g, g • a = b
Tactic:
use! g
State after:
case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α
H : g • a = b
⊢ g ∈ G

case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α
H : g • a = b
⊢ { val := g, property := ?property } • a = b

State before:
case property
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α
H : g • a = b
⊢ g ∈ G

case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α
H : g • a = b
⊢ { val := g, property := ?property } • a = b
Tactic:
exact hGt hg
State after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α
H : g • a = b
⊢ { val := g, property := ⋯ } • a = b

State before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Fintype.card α
G : Subgroup (Equiv.Perm α)
t : Set α
hGt : stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α ≤ G
a : α
ha : a ∈ t
b : α
hb : b ∈ t
g : Equiv.Perm α
hg : g ∈ stabilizer (Equiv.Perm α) t ⊓ alternatingGroup α
H : g • a = b
⊢ { val := g, property := ⋯ } • a = b
Tactic:
exact H
State after:
no goals