Theorem: MulAction.Nat.Combination_isPreprimitive (Jordan/PermMaximal.lean)

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
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)

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
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)

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 α
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)

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
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)

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
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)

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
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)

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
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)

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]
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)

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]
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)

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]
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)

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 α)
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

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]
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)

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
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 α) α

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 α
State after:
no goals

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]
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 α

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
State after:
no goals

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
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

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]
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

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]
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

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 ↔ _
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

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 • s = s ↔ g • ↑s = ↑s
Tactic:
rw [← Finset.coe_smul_finset, ← Finset.coe_inj]
State after:
no goals

State before:
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
Tactic:
simp only [Finset.coe_nonempty, ← Finset.card_pos, hs]
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
⊢ 0 < n

State before:
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
⊢ 0 < n
Tactic:
apply lt_trans one_pos h_one_lt
State after:
no goals

State before:
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)ᶜ
Tactic:
simp only [← Finset.coe_compl, Finset.coe_nonempty,
  ← Finset.card_compl_lt_iff_nonempty, compl_compl, hs]
State after:
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
⊢ n < Fintype.card α

State before:
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
⊢ n < Fintype.card α
Tactic:
exact hn
State after:
no goals

State before:
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
Tactic:
simp only [Set.ncard_coe_Finset, ne_eq]
State after:
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 * s.card

State before:
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 * s.card
Tactic:
simp only [Finset.coe_sort_coe, Fintype.card_coe, hs]
State after:
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 * n

State before:
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 * n
Tactic:
exact hα
State after:
no goals