internlm/Lean-Github huggingface dataset:
Theorem: Equiv.Perm.isMaximalStab
Proof state before:
case inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard s = Set.ncard sᶜ
⊢ Subgroup.IsMaximal (stabilizer (Perm α) s)
Tactic:
exfalso
Proof state after:
case inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard s = Set.ncard sᶜ
⊢ False
Theorem: Equiv.Perm.isMaximalStab
Proof state before:
case inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard s = Set.ncard sᶜ
⊢ False
Tactic:
apply hα
Proof state after:
case inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard s = Set.ncard sᶜ
⊢ Fintype.card α = 2 * Set.ncard s
Theorem: Equiv.Perm.isMaximalStab
Proof state before:
case inr.inl
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard s = Set.ncard sᶜ
⊢ Fintype.card α = 2 * Set.ncard s
Tactic:
rw [← Nat.card_eq_fintype_card, ← Set.ncard_add_ncard_compl s, two_mul, ← hs]
Proof state after:
no goals
Theorem: Equiv.Perm.isMaximalStab
Proof state before:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty s
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (Perm α) s)
Tactic:
rw [← compl_compl s] at h0
Proof state after:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty sᶜᶜ
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (Perm α) s)
Theorem: Equiv.Perm.isMaximalStab
Proof state before:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty sᶜᶜ
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (Perm α) s)
Tactic:
rw [← stabilizer_compl]
Proof state after:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty sᶜᶜ
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (Perm α) sᶜ)
Theorem: Equiv.Perm.isMaximalStab
Proof state before:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty sᶜᶜ
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Subgroup.IsMaximal (stabilizer (Perm α) sᶜ)
Tactic:
apply Equiv.Perm.isMaximalStab' (sᶜ) h1 h0
Proof state after:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty sᶜᶜ
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Set.ncard sᶜ < Set.ncard sᶜᶜ
Theorem: Equiv.Perm.isMaximalStab
Proof state before:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty sᶜᶜ
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Set.ncard sᶜ < Set.ncard sᶜᶜ
Tactic:
rw [compl_compl]
Proof state after:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty sᶜᶜ
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Set.ncard sᶜ < Set.ncard s
Theorem: Equiv.Perm.isMaximalStab
Proof state before:
case inr.inr
α : Type u_1
inst✝³ : DecidableEq α
G : Type ?u.123924
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
s : Set α
h0 : Set.Nonempty sᶜᶜ
h1 : Set.Nonempty sᶜ
hα : Fintype.card α ≠ 2 * Set.ncard s
hs : Set.ncard sᶜ < Set.ncard s
⊢ Set.ncard sᶜ < Set.ncard s
Tactic:
exact hs
Proof state after:
no goals
Theorem: MulAction.Nat.Combination.stabilizer_eq
Proof state before:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
⊢ stabilizer G s = stabilizer G ↑↑s
Tactic:
ext g
Proof state after:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
g : G
⊢ g ∈ stabilizer G s ↔ g ∈ stabilizer G ↑↑s
Theorem: MulAction.Nat.Combination.stabilizer_eq
Proof state before:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
g : G
⊢ g ∈ stabilizer G s ↔ g ∈ stabilizer G ↑↑s
Tactic:
simp only [mem_stabilizer_iff]
Proof state after:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
g : G
⊢ g • s = s ↔ g • ↑↑s = ↑↑s
Theorem: MulAction.Nat.Combination.stabilizer_eq
Proof state before:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
g : G
⊢ g • s = s ↔ g • ↑↑s = ↑↑s
Tactic:
rw [← Subtype.coe_inj, ← Finset.coe_smul_finset]
Proof state after:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
g : G
⊢ ↑(g • s) = ↑s ↔ ↑(g • ↑s) = ↑↑s
Theorem: MulAction.Nat.Combination.stabilizer_eq
Proof state before:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
g : G
⊢ ↑(g • s) = ↑s ↔ ↑(g • ↑s) = ↑↑s
Tactic:
simp only [← Finset.coe_smul_finset, ← Finset.coe_inj]
Proof state after:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
g : G
⊢ ↑↑(g • s) = ↑↑s ↔ ↑(g • ↑s) = ↑↑s
Theorem: MulAction.Nat.Combination.stabilizer_eq
Proof state before:
case h
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : Fintype α
n : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : ↑(Nat.Combination α n)
g : G
⊢ ↑↑(g • s) = ↑↑s ↔ ↑(g • ↑s) = ↑↑s
Tactic:
simp only [Nat.combination_mulAction.coe_apply', Finset.coe_smul_finset]
Proof state after:
no goals
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α n)
Tactic:
cases' Nat.eq_or_lt_of_le h_one_le with h_one h_one_lt
Proof state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one : 1 = n
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α n)

case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α n)
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α n)
Tactic:
have : Nontrivial α := by
  rw [← Fintype.one_lt_card_iff_nontrivial]
  exact lt_trans h_one_lt hn
Proof state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this : Nontrivial α
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α n)
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this : Nontrivial α
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α n)
Tactic:
haveI ht : IsPretransitive (Equiv.Perm α) (n.Combination α) :=
  n.Combination_isPretransitive α
Proof state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α n)
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α n)
Tactic:
have : Nontrivial (n.Combination α) :=
  n.Combination_nontrivial α (lt_trans (Nat.lt_succ_self 0) h_one_lt) hn
Proof state after:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α n)
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α n)
Tactic:
obtain ⟨sn : n.Combination α⟩ := this.to_nonempty
Proof state after:
case inr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α n)
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α n)
Tactic:
let s := sn.val
Proof state after:
case inr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α n)
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α n)
Tactic:
let hs : s.card = n := sn.prop
Proof state after:
case inr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α n)
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α n)
Tactic:
rw [← maximal_stabilizer_iff_preprimitive (Equiv.Perm α) sn]
Proof state after:
case inr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
⊢ Subgroup.IsMaximal (stabilizer (Equiv.Perm α) sn)
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
⊢ Subgroup.IsMaximal (stabilizer (Equiv.Perm α) sn)
Tactic:
have : stabilizer (Equiv.Perm α) sn =
    stabilizer (Equiv.Perm α) (s : Set α) := by
  ext g
  simp only [mem_stabilizer_iff]
  rw [← Subtype.coe_inj]
  change g • s = s ↔ _
  rw [← Finset.coe_smul_finset, ← Finset.coe_inj]
Proof state after:
case inr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ Subgroup.IsMaximal (stabilizer (Equiv.Perm α) sn)
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ Subgroup.IsMaximal (stabilizer (Equiv.Perm α) sn)
Tactic:
rw [this]
Proof state after:
case inr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ Subgroup.IsMaximal (stabilizer (Equiv.Perm α) ↑s)
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ Subgroup.IsMaximal (stabilizer (Equiv.Perm α) ↑s)
Tactic:
apply Equiv.Perm.isMaximalStab (s : Set α)
Proof state after:
case inr.intro.h0
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ Set.Nonempty ↑s

case inr.intro.h1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ Set.Nonempty (↑s)ᶜ

case inr.intro.hα
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝¹ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
⊢ Fintype.card α ≠ 2 * Set.ncard ↑s
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one : 1 = n
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α n)
Tactic:
rw [← h_one]
Proof state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one : 1 = n
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α 1)
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one : 1 = n
⊢ IsPreprimitive (Equiv.Perm α) ↑(Nat.Combination α 1)
Tactic:
apply isPreprimitive_of_surjective_map
  (Nat.bijective_toCombination_one_equivariant _ α).surjective
Proof state after:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one : 1 = n
⊢ IsPreprimitive (Equiv.Perm α) α
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one : 1 = n
⊢ IsPreprimitive (Equiv.Perm α) α
Tactic:
exact Equiv.Perm.isPreprimitive α
Proof state after:
no goals
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
⊢ Nontrivial α
Tactic:
rw [← Fintype.one_lt_card_iff_nontrivial]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
⊢ 1 < Fintype.card α
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
⊢ 1 < Fintype.card α
Tactic:
exact lt_trans h_one_lt hn
Proof state after:
no goals
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
⊢ stabilizer (Equiv.Perm α) sn = stabilizer (Equiv.Perm α) ↑s
Tactic:
ext g
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
g : Equiv.Perm α
⊢ g ∈ stabilizer (Equiv.Perm α) sn ↔ g ∈ stabilizer (Equiv.Perm α) ↑s
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
g : Equiv.Perm α
⊢ g ∈ stabilizer (Equiv.Perm α) sn ↔ g ∈ stabilizer (Equiv.Perm α) ↑s
Tactic:
simp only [mem_stabilizer_iff]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
g : Equiv.Perm α
⊢ g • sn = sn ↔ g • ↑s = ↑s
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
g : Equiv.Perm α
⊢ g • sn = sn ↔ g • ↑s = ↑s
Tactic:
rw [← Subtype.coe_inj]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
g : Equiv.Perm α
⊢ ↑(g • sn) = ↑sn ↔ g • ↑s = ↑s
Theorem: MulAction.Nat.Combination_isPreprimitive
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
g : Equiv.Perm α
⊢ ↑(g • sn) = ↑sn ↔ g • ↑s = ↑s
Tactic:
change g • s = s ↔ _
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
h_one_lt : 1 < n
this✝ : Nontrivial α
ht : IsPretransitive (Equiv.Perm α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
g : Equiv.Perm α
⊢ g • s = s ↔ g • ↑s = ↑s