internlm/Lean-Github huggingface dataset:
Theorem: MulAction.stabilizer_subgroupOf_eq
Proof state before:
case h
α : Type u_2
G : Type u_1
H : Type ?u.1696
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
a : α
n : ↥N
⊢ n ∈ stabilizer (↥N) a ↔ n ∈ Subgroup.subgroupOf (stabilizer G a) N
Tactic:
simp only [Subgroup.mem_subgroupOf, mem_stabilizer_iff]
Proof state after:
case h
α : Type u_2
G : Type u_1
H : Type ?u.1696
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
a : α
n : ↥N
⊢ n • a = a ↔ ↑n • a = a
Theorem: MulAction.stabilizer_subgroupOf_eq
Proof state before:
case h
α : Type u_2
G : Type u_1
H : Type ?u.1696
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
a : α
n : ↥N
⊢ n • a = a ↔ ↑n • a = a
Tactic:
rfl
Proof state after:
no goals
Theorem: Subgroup.map_iff_mono_of_injective
Proof state before:
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ K ≤ K' ↔ map f K ≤ map f K'
Tactic:
constructor
Proof state after:
case mp
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ K ≤ K' → map f K ≤ map f K'

case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ map f K ≤ map f K' → K ≤ K'
Theorem: Subgroup.map_iff_mono_of_injective
Proof state before:
case mp
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ K ≤ K' → map f K ≤ map f K'

case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ map f K ≤ map f K' → K ≤ K'
Tactic:
exact Subgroup.map_mono
Proof state after:
case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ map f K ≤ map f K' → K ≤ K'
Theorem: Subgroup.map_iff_mono_of_injective
Proof state before:
case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ map f K ≤ map f K' → K ≤ K'
Tactic:
intro h
Proof state after:
case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
⊢ K ≤ K'
Theorem: Subgroup.map_iff_mono_of_injective
Proof state before:
case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
⊢ K ≤ K'
Tactic:
intro x hx
Proof state after:
case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
⊢ x ∈ K'
Theorem: Subgroup.map_iff_mono_of_injective
Proof state before:
case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
⊢ x ∈ K'
Tactic:
suffices f x ∈ Subgroup.map f K' by
  simp only [Subgroup.mem_map] at this
  obtain ⟨y, hy, hx⟩ := this
  rw [← hf hx]; exact hy
Proof state after:
case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
⊢ f x ∈ map f K'
Theorem: Subgroup.map_iff_mono_of_injective
Proof state before:
case mpr
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
⊢ f x ∈ map f K'
Tactic:
apply h
Proof state after:
case mpr.a
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
⊢ f x ∈ map f K
Theorem: Subgroup.map_iff_mono_of_injective
Proof state before:
case mpr.a
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
⊢ f x ∈ map f K
Tactic:
rw [Subgroup.mem_map]
Proof state after:
case mpr.a
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
⊢ ∃ x_1 ∈ K, f x_1 = f x
Theorem: Subgroup.map_iff_mono_of_injective
Proof state before:
case mpr.a
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
⊢ ∃ x_1 ∈ K, f x_1 = f x
Tactic:
exact ⟨x, hx, rfl⟩
Proof state after:
no goals
Theorem: Subgroup.map_iff_mono_of_injective
Proof state before:
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
this : f x ∈ map f K'
⊢ x ∈ K'
Tactic:
simp only [Subgroup.mem_map] at this
Proof state after:
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
this : ∃ x_1 ∈ K', f x_1 = f x
⊢ x ∈ K'
Theorem: Subgroup.map_iff_mono_of_injective
Proof state before:
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx : x ∈ K
this : ∃ x_1 ∈ K', f x_1 = f x
⊢ x ∈ K'
Tactic:
obtain ⟨y, hy, hx⟩ := this
Proof state after:
case intro.intro
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx✝ : x ∈ K
y : G
hy : y ∈ K'
hx : f y = f x
⊢ x ∈ K'
Theorem: Subgroup.map_iff_mono_of_injective
Proof state before:
case intro.intro
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx✝ : x ∈ K
y : G
hy : y ∈ K'
hx : f y = f x
⊢ x ∈ K'
Tactic:
rw [← hf hx]
Proof state after:
case intro.intro
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx✝ : x ∈ K
y : G
hy : y ∈ K'
hx : f y = f x
⊢ y ∈ K'
Theorem: Subgroup.map_iff_mono_of_injective
Proof state before:
case intro.intro
α : Type ?u.3330
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
h : map f K ≤ map f K'
x : G
hx✝ : x ∈ K
y : G
hy : y ∈ K'
hx : f y = f x
⊢ y ∈ K'
Tactic:
exact hy
Proof state after:
no goals
Theorem: Subgroup.map_strict_mono_of_injective
Proof state before:
α : Type ?u.5373
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ K < K' ↔ map f K < map f K'
Tactic:
simp only [lt_iff_le_not_le]
Proof state after:
α : Type ?u.5373
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ K ≤ K' ∧ ¬K' ≤ K ↔ map f K ≤ map f K' ∧ ¬map f K' ≤ map f K
Theorem: Subgroup.map_strict_mono_of_injective
Proof state before:
α : Type ?u.5373
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ K ≤ K' ∧ ¬K' ≤ K ↔ map f K ≤ map f K' ∧ ¬map f K' ≤ map f K
Tactic:
simp_rw [← Subgroup.map_iff_mono_of_injective hf]
Proof state after:
no goals
Theorem: Subgroup.map_injective_of_injective
Proof state before:
α : Type ?u.7056
G : Type u_2
H : Type u_1
inst✝² : Group G
inst✝¹ : Group H
inst✝ : MulAction G α
N : Subgroup G
f : G →* H
K K' : Subgroup G
hf : Function.Injective ⇑f
⊢ map f K = map f K' ↔ K = K'
Tactic:
simp only [le_antisymm_iff, ← Subgroup.map_iff_mono_of_injective hf]
Proof state after:
no goals
Theorem: alternatingGroup.isPretransitive_ofFixingSubgroup
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ IsPretransitive ↥(fixingSubgroup (↥(alternatingGroup α)) s) ↥(SubMulAction.ofFixingSubgroup (↥(alternatingGroup α)) s)
Tactic:
rw [isPretransitive_iff_is_one_pretransitive]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ IsMultiplyPretransitive (↥(fixingSubgroup (↥(alternatingGroup α)) s))
    (↥(SubMulAction.ofFixingSubgroup (↥(alternatingGroup α)) s)) 1
Theorem: alternatingGroup.isPretransitive_ofFixingSubgroup
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ IsMultiplyPretransitive (↥(fixingSubgroup (↥(alternatingGroup α)) s))
    (↥(SubMulAction.ofFixingSubgroup (↥(alternatingGroup α)) s)) 1
Tactic:
apply remaining_transitivity'
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α ?n

case hmn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ 1 + Set.ncard s ≤ ?n

case hn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ ↑?n ≤ PartENat.card α

case n
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ ℕ
Theorem: alternatingGroup.isPretransitive_ofFixingSubgroup
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α ?n

case hmn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ 1 + Set.ncard s ≤ ?n

case hn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ ↑?n ≤ PartENat.card α

case n
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ ℕ
Tactic:
apply IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state after:
case hmn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ 1 + Set.ncard s ≤ Fintype.card α - 2

case hn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Theorem: alternatingGroup.isPretransitive_ofFixingSubgroup
Proof state before:
case hmn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ 1 + Set.ncard s ≤ Fintype.card α - 2
Tactic:
have h1' : 2 < Set.ncard (sᶜ : Set α) := by
  apply lt_of_le_of_lt _ hα
  rw [Nat.succ_le_iff, Set.one_lt_ncard_iff_nontrivial]
  exact h0
Proof state after:
case hmn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
h1' : 2 < Set.ncard sᶜ
⊢ 1 + Set.ncard s ≤ Fintype.card α - 2
Theorem: alternatingGroup.isPretransitive_ofFixingSubgroup
Proof state before:
case hmn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
h1' : 2 < Set.ncard sᶜ
⊢ 1 + Set.ncard s ≤ Fintype.card α - 2
Tactic:
rw [add_comm, ← Nat.card_eq_fintype_card, ← Set.ncard_add_ncard_compl s,
  Nat.add_sub_assoc (le_of_lt h1'), add_le_add_iff_left]
Proof state after:
case hmn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
h1' : 2 < Set.ncard sᶜ
⊢ 1 ≤ Set.ncard sᶜ - 2
Theorem: alternatingGroup.isPretransitive_ofFixingSubgroup
Proof state before:
case hmn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
h1' : 2 < Set.ncard sᶜ
⊢ 1 ≤ Set.ncard sᶜ - 2
Tactic:
apply Nat.le_sub_of_add_le
Proof state after:
case hmn.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
h1' : 2 < Set.ncard sᶜ
⊢ 1 + 2 ≤ Set.ncard sᶜ
Theorem: alternatingGroup.isPretransitive_ofFixingSubgroup
Proof state before:
case hmn.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
h1' : 2 < Set.ncard sᶜ
⊢ 1 + 2 ≤ Set.ncard sᶜ
Tactic:
exact h1'
Proof state after:
no goals
Theorem: alternatingGroup.isPretransitive_ofFixingSubgroup
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ 2 < Set.ncard sᶜ
Tactic:
apply lt_of_le_of_lt _ hα
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ 2 ≤ Set.ncard s
Theorem: alternatingGroup.isPretransitive_ofFixingSubgroup
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ 2 ≤ Set.ncard s
Tactic:
rw [Nat.succ_le_iff, Set.one_lt_ncard_iff_nontrivial]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ Set.Nontrivial s
Theorem: alternatingGroup.isPretransitive_ofFixingSubgroup
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ Set.Nontrivial s
Tactic:
exact h0
Proof state after:
no goals
Theorem: alternatingGroup.isPretransitive_ofFixingSubgroup
Proof state before:
case hn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ ↑(Fintype.card α - 2) ≤ PartENat.card α
Tactic:
rw [PartENat.card_eq_coe_fintype_card]
Proof state after:
case hn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ ↑(Fintype.card α - 2) ≤ ↑(Fintype.card α)
Theorem: alternatingGroup.isPretransitive_ofFixingSubgroup
Proof state before:
case hn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : Set.Nontrivial s
hα : Set.ncard s < Set.ncard sᶜ
⊢ ↑(Fintype.card α - 2) ≤ ↑(Fintype.card α)
Tactic:
simp only [Nat.cast_le, tsub_le_iff_right, le_add_iff_nonneg_right, zero_le]
Proof state after:
no goals
Theorem: alternatingGroup.stabilizer_ne_top'
Proof 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
Proof state after:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hsc : Set.Nontrivial sᶜ
a : α
ha : a ∈ s
⊢ stabilizer (↥(alternatingGroup α)) s ≠ ⊤
Theorem: alternatingGroup.stabilizer_ne_top'
Proof 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
Proof 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 ≠ ⊤
Theorem: alternatingGroup.stabilizer_ne_top'
Proof 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
Proof 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 ≠ ⊤
Theorem: alternatingGroup.stabilizer_ne_top'
Proof 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
Proof 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 ≠ ⊤
Theorem: alternatingGroup.stabilizer_ne_top'
Proof 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
Proof 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 ≠ ⊤
Theorem: alternatingGroup.stabilizer_ne_top'
Proof 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
Proof 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
Theorem: alternatingGroup.stabilizer_ne_top'
Proof 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
Proof 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
Theorem: alternatingGroup.stabilizer_ne_top'
Proof 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
Proof 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
Theorem: alternatingGroup.stabilizer_ne_top'
Proof 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
Proof 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
Theorem: alternatingGroup.stabilizer_ne_top'
Proof 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]
Proof 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
Theorem: alternatingGroup.stabilizer_ne_top'
Proof 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
Proof 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
Theorem: alternatingGroup.stabilizer_ne_top'
Proof 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]
Proof 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