internlm/Lean-Github huggingface dataset:
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case inr.intro.h1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝¹ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (↥(alternatingGroup α)) sn = stabilizer ↥(alternatingGroup α) ↑s
⊢ Set.Nonempty (↑s)ᶜ
Tactic:
simp only [← Finset.coe_compl, Finset.coe_nonempty, ← Finset.card_compl_lt_iff_nonempty,
  compl_compl, hs]
Proof state after:
case inr.intro.h1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝¹ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (↥(alternatingGroup α)) sn = stabilizer ↥(alternatingGroup α) ↑s
⊢ n < Fintype.card α
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case inr.intro.h1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝¹ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (↥(alternatingGroup α)) sn = stabilizer ↥(alternatingGroup α) ↑s
⊢ n < Fintype.card α
Tactic:
exact hn
Proof state after:
no goals
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case inr.intro.hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝¹ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (↥(alternatingGroup α)) sn = stabilizer ↥(alternatingGroup α) ↑s
⊢ Fintype.card α ≠ 2 * Set.ncard ↑s
Tactic:
simp only [Set.ncard_coe_Finset, hs]
Proof state after:
case inr.intro.hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝¹ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (↥(alternatingGroup α)) sn = stabilizer ↥(alternatingGroup α) ↑s
⊢ Fintype.card α ≠ 2 * n
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case inr.intro.hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝¹ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (↥(alternatingGroup α)) sn = stabilizer ↥(alternatingGroup α) ↑s
⊢ Fintype.card α ≠ 2 * n
Tactic:
exact hα
Proof state after:
no goals
Theorem: MulAction.stabilizer_compl
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
⊢ stabilizer G sᶜ = stabilizer G s
Tactic:
have : ∀ s : Set α, stabilizer G s ≤ stabilizer G (sᶜ) :=
  by
  intro s g h
  rw [mem_stabilizer_iff, smul_compl_set, mem_stabilizer_iff.1 h]
Proof state after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
this : ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
⊢ stabilizer G sᶜ = stabilizer G s
Theorem: MulAction.stabilizer_compl
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
this : ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
⊢ stabilizer G sᶜ = stabilizer G s
Tactic:
refine' le_antisymm _ (this _)
Proof state after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
this : ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
⊢ stabilizer G sᶜ ≤ stabilizer G s
Theorem: MulAction.stabilizer_compl
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
this : ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
⊢ stabilizer G sᶜ ≤ stabilizer G s
Tactic:
convert this _
Proof state after:
case h.e'_4.h.e'_5
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
this : ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
⊢ s = sᶜᶜ
Theorem: MulAction.stabilizer_compl
Proof state before:
case h.e'_4.h.e'_5
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
this : ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
⊢ s = sᶜᶜ
Tactic:
exact (compl_compl _).symm
Proof state after:
no goals
Theorem: MulAction.stabilizer_compl
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
⊢ ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
Tactic:
intro s g h
Proof state after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s✝ s : Set α
g : G
h : g ∈ stabilizer G s
⊢ g ∈ stabilizer G sᶜ
Theorem: MulAction.stabilizer_compl
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s✝ s : Set α
g : G
h : g ∈ stabilizer G s
⊢ g ∈ stabilizer G sᶜ
Tactic:
rw [mem_stabilizer_iff, smul_compl_set, mem_stabilizer_iff.1 h]
Proof state after:
no goals
Theorem: MulAction.le_stabilizer_iff_smul_le
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ H ≤ stabilizer G s ↔ ∀ g ∈ H, g • s ⊆ s
Tactic:
constructor
Proof state after:
case mp
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ H ≤ stabilizer G s → ∀ g ∈ H, g • s ⊆ s

case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ (∀ g ∈ H, g • s ⊆ s) → H ≤ stabilizer G s
Theorem: MulAction.le_stabilizer_iff_smul_le
Proof state before:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ (∀ g ∈ H, g • s ⊆ s) → H ≤ stabilizer G s
Tactic:
intro hyp
Proof state after:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
⊢ H ≤ stabilizer G s
Theorem: MulAction.le_stabilizer_iff_smul_le
Proof state before:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
⊢ H ≤ stabilizer G s
Tactic:
intro g hg
Proof state after:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ g ∈ stabilizer G s
Theorem: MulAction.le_stabilizer_iff_smul_le
Proof state before:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ g ∈ stabilizer G s
Tactic:
rw [mem_stabilizer_iff]
Proof state after:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ g • s = s
Theorem: MulAction.le_stabilizer_iff_smul_le
Proof state before:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ g • s = s
Tactic:
apply subset_antisymm
Proof state after:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ g • s ⊆ s

case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ s ⊆ g • s
Theorem: MulAction.le_stabilizer_iff_smul_le
Proof state before:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ g • s ⊆ s

case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ s ⊆ g • s
Tactic:
exact hyp g hg
Proof state after:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ s ⊆ g • s
Theorem: MulAction.le_stabilizer_iff_smul_le
Proof state before:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
⊢ s ⊆ g • s
Tactic:
intro x hx
Proof state after:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ x ∈ g • s
Theorem: MulAction.le_stabilizer_iff_smul_le
Proof state before:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ x ∈ g • s
Tactic:
use g⁻¹ • x
Proof state after:
case h
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ s ∧ (fun x => g • x) (g⁻¹ • x) = x
Theorem: MulAction.le_stabilizer_iff_smul_le
Proof state before:
case h
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ s ∧ (fun x => g • x) (g⁻¹ • x) = x
Tactic:
constructor
Proof state after:
case h.left
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ s

case h.right
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ (fun x => g • x) (g⁻¹ • x) = x
Theorem: MulAction.le_stabilizer_iff_smul_le
Proof state before:
case h.left
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ s

case h.right
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ (fun x => g • x) (g⁻¹ • x) = x
Tactic:
apply hyp g⁻¹ (inv_mem hg)
Proof state after:
case h.left.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ g⁻¹ • s

case h.right
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ (fun x => g • x) (g⁻¹ • x) = x
Theorem: MulAction.le_stabilizer_iff_smul_le
Proof state before:
case h.left.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ g⁻¹ • s

case h.right
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ (fun x => g • x) (g⁻¹ • x) = x
Tactic:
simp only [Set.smul_mem_smul_set_iff, hx]
Proof state after:
case h.right
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ (fun x => g • x) (g⁻¹ • x) = x
Theorem: MulAction.le_stabilizer_iff_smul_le
Proof state before:
case h.right
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ (fun x => g • x) (g⁻¹ • x) = x
Tactic:
simp only [smul_inv_smul]
Proof state after:
no goals
Theorem: MulAction.le_stabilizer_iff_smul_le
Proof state before:
case mp
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ H ≤ stabilizer G s → ∀ g ∈ H, g • s ⊆ s
Tactic:
intro hyp g hg
Proof state after:
case mp
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g • s ⊆ s
Theorem: MulAction.le_stabilizer_iff_smul_le
Proof state before:
case mp
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g • s ⊆ s
Tactic:
apply Eq.subset
Proof state after:
case mp.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g • s = s
Theorem: MulAction.le_stabilizer_iff_smul_le
Proof state before:
case mp.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g • s = s
Tactic:
rw [← mem_stabilizer_iff]
Proof state after:
case mp.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g ∈ stabilizer G s
Theorem: MulAction.le_stabilizer_iff_smul_le
Proof state before:
case mp.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : H ≤ stabilizer G s
g : G
hg : g ∈ H
⊢ g ∈ stabilizer G s
Tactic:
exact hyp hg
Proof state after:
no goals
Theorem: MulAction.mem_stabilizer_of_finite_iff_smul_le
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
⊢ g ∈ stabilizer G s ↔ g • s ⊆ s
Tactic:
haveI : Fintype s := Set.Finite.fintype hs
Proof state after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this : Fintype ↑s
⊢ g ∈ stabilizer G s ↔ g • s ⊆ s
Theorem: MulAction.mem_stabilizer_of_finite_iff_smul_le
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this : Fintype ↑s
⊢ g ∈ stabilizer G s ↔ g • s ⊆ s
Tactic:
haveI : Fintype (g • s : Set α) := Fintype.ofFinite _
Proof state after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g ∈ stabilizer G s ↔ g • s ⊆ s
Theorem: MulAction.mem_stabilizer_of_finite_iff_smul_le
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g ∈ stabilizer G s ↔ g • s ⊆ s
Tactic:
rw [mem_stabilizer_iff]
Proof state after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g • s = s ↔ g • s ⊆ s
Theorem: MulAction.mem_stabilizer_of_finite_iff_smul_le
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g • s = s ↔ g • s ⊆ s
Tactic:
constructor
Proof state after:
case mp
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g • s = s → g • s ⊆ s

case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g • s ⊆ s → g • s = s
Theorem: MulAction.mem_stabilizer_of_finite_iff_smul_le
Proof state before:
case mp
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g • s = s → g • s ⊆ s

case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g • s ⊆ s → g • s = s
Tactic:
exact Eq.subset
Proof state after:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g • s ⊆ s → g • s = s
Theorem: MulAction.mem_stabilizer_of_finite_iff_smul_le
Proof state before:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ g • s ⊆ s → g • s = s
Tactic:
rw [← Set.toFinset_inj, ← Set.toFinset_subset_toFinset]
Proof state after:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ Set.toFinset (g • s) ⊆ Set.toFinset s → Set.toFinset (g • s) = Set.toFinset s
Theorem: MulAction.mem_stabilizer_of_finite_iff_smul_le
Proof state before:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
⊢ Set.toFinset (g • s) ⊆ Set.toFinset s → Set.toFinset (g • s) = Set.toFinset s
Tactic:
intro h
Proof state after:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ Set.toFinset (g • s) = Set.toFinset s
Theorem: MulAction.mem_stabilizer_of_finite_iff_smul_le
Proof state before:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ Set.toFinset (g • s) = Set.toFinset s
Tactic:
apply Finset.eq_of_subset_of_card_le h
Proof state after:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ (Set.toFinset s).card ≤ (Set.toFinset (g • s)).card
Theorem: MulAction.mem_stabilizer_of_finite_iff_smul_le
Proof state before:
case mpr
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ (Set.toFinset s).card ≤ (Set.toFinset (g • s)).card
Tactic:
apply le_of_eq
Proof state after:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ (Set.toFinset s).card = (Set.toFinset (g • s)).card
Theorem: MulAction.mem_stabilizer_of_finite_iff_smul_le
Proof state before:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ (Set.toFinset s).card = (Set.toFinset (g • s)).card
Tactic:
suffices (g • s).toFinset = Finset.map ⟨_, MulAction.injective g⟩ hs.toFinset by
  rw [this, Finset.card_map, Set.toFinite_toFinset]
Proof state after:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ Set.toFinset (g • s) = Finset.map { toFun := fun x => g • x, inj' := ⋯ } (Set.Finite.toFinset hs)
Theorem: MulAction.mem_stabilizer_of_finite_iff_smul_le
Proof state before:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ Set.toFinset (g • s) = Finset.map { toFun := fun x => g • x, inj' := ⋯ } (Set.Finite.toFinset hs)
Tactic:
rw [← Finset.coe_inj]
Proof state after:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ ↑(Set.toFinset (g • s)) = ↑(Finset.map { toFun := fun x => g • x, inj' := ⋯ } (Set.Finite.toFinset hs))
Theorem: MulAction.mem_stabilizer_of_finite_iff_smul_le
Proof state before:
case mpr.a
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝ : Fintype ↑s
this : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
⊢ ↑(Set.toFinset (g • s)) = ↑(Finset.map { toFun := fun x => g • x, inj' := ⋯ } (Set.Finite.toFinset hs))
Tactic:
simp only [Set.coe_toFinset, Set.toFinite_toFinset, Finset.coe_map, Function.Embedding.coeFn_mk, Set.image_smul]
Proof state after:
no goals
Theorem: MulAction.mem_stabilizer_of_finite_iff_smul_le
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
this✝¹ : Fintype ↑s
this✝ : Fintype ↑(g • s)
h : Set.toFinset (g • s) ⊆ Set.toFinset s
this : Set.toFinset (g • s) = Finset.map { toFun := fun x => g • x, inj' := ⋯ } (Set.Finite.toFinset hs)
⊢ (Set.toFinset s).card = (Set.toFinset (g • s)).card
Tactic:
rw [this, Finset.card_map, Set.toFinite_toFinset]
Proof state after:
no goals
Theorem: MulAction.mem_stabilizer_of_finite_iff_le_smul
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
⊢ g ∈ stabilizer G s ↔ s ⊆ g • s
Tactic:
rw [← @inv_mem_iff, mem_stabilizer_of_finite_iff_smul_le G s hs]
Proof state after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
⊢ g⁻¹ • s ⊆ s ↔ s ⊆ g • s
Theorem: MulAction.mem_stabilizer_of_finite_iff_le_smul
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
hs : Set.Finite s
g : G
⊢ g⁻¹ • s ⊆ s ↔ s ⊆ g • s
Tactic:
exact Set.subset_set_smul_iff.symm
Proof state after:
no goals
Theorem: MulAction.fixingSubgroup_le_stabilizer
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
⊢ fixingSubgroup G s ≤ stabilizer G s
Tactic:
intro k hk
Proof state after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : k ∈ fixingSubgroup G s
⊢ k ∈ stabilizer G s
Theorem: MulAction.fixingSubgroup_le_stabilizer
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : k ∈ fixingSubgroup G s
⊢ k ∈ stabilizer G s
Tactic:
rw [mem_fixingSubgroup_iff] at hk
Proof state after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ k ∈ stabilizer G s
Theorem: MulAction.fixingSubgroup_le_stabilizer
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ k ∈ stabilizer G s
Tactic:
rw [mem_stabilizer_iff]
Proof state after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ k • s = s
Theorem: MulAction.fixingSubgroup_le_stabilizer
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ k • s = s
Tactic:
change (fun x => k • x) '' s = s
Proof state after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ (fun x => k • x) '' s = s
Theorem: MulAction.fixingSubgroup_le_stabilizer
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ (fun x => k • x) '' s = s
Tactic:
conv_rhs => rw [← Set.image_id s]
Proof state after:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ (fun x => k • x) '' s = id '' s
Theorem: MulAction.fixingSubgroup_le_stabilizer
Proof state before:
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ (fun x => k • x) '' s = id '' s
Tactic:
apply Set.image_congr
Proof state after:
case h
G : Type u_2
inst✝¹ : Group G
α : Type u_1
inst✝ : MulAction G α
s : Set α
k : G
hk : ∀ y ∈ s, k • y = y
⊢ ∀ a ∈ s, k • a = id a