awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : Finite α
this_2 : Fintype α
this_3 : IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
rw : IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
⊢ IsPreprimitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)

Tactic:
rw [← isCoatom_stabilizer_iff_preprimitive _ s]

Premises used: MulAction.isCoatom_stabilizer_iff_preprimitive
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : Finite α
this_2 : Fintype α
this_3 : IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
rw : IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) (↑s : Set α))
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)

Tactic:
rw [stabilizer_coe]

Premises used: Set.powersetCard.stabilizer_coe
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : Finite α
this_2 : Fintype α
this_3 : IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
hs_nonempty : (↑s : Set α).Nonempty
hsc_nonempty : (↑s : Set α)ᶜ.Nonempty
hα₁ : Nat.card α ≠ 2 * (↑s : Set α).ncard
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) (↑s : Set α))

Tactic:
apply isCoatom_stabilizer

Premises used: Equiv.Perm.isCoatom_stabilizer
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : Finite α
this_2 : Fintype α
this_3 : IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
hs_nonempty hs_nonempty₁ hs_nonempty₂ hs_nonempty₃ : 1 ≤ n
⊢ (↑s : Set α).Nonempty

Tactic:
rwa [powersetCard.coe_nonempty_iff]

Premises used: Set.powersetCard.coe_nonempty_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : Finite α
this_2 : Fintype α
this_3 : IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
hsc_nonempty : ¬n = Nat.card α
⊢ (↑s : Set α)ᶜ.Nonempty

Tactic:
rw [nonempty_compl, ne_eq, eq_univ_iff_ncard, ncard_eq]

Premises used: ne_eq, Set.eq_univ_iff_ncard, Set.powersetCard.ncard_eq, Set.nonempty_compl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : Finite α
this_2 : Fintype α
this_3 : IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
⊢ ¬n = Nat.card α

Tactic:
hn.ne

Premises used: LT.lt.ne
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : Finite α
this_2 : Fintype α
this_3 : IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
⊢ ¬n = Nat.card α

Tactic:
exact hn.ne

Premises used: LT.lt.ne
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : Finite α
this_2 : Fintype α
this_3 : IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
hα₁ hα₂ hα₃ hα₄ : Nat.card α ≠ 2 * n
⊢ Nat.card α ≠ 2 * (↑s : Set α).ncard

Tactic:
rwa [ncard_eq]

Premises used: Set.powersetCard.ncard_eq
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
inr :
  ∀
    (this :
      ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α)
        (hn : 2 * n ≤ Nat.card α), IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2))
    (hn : Nat.card α < 2 * n), IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
wlog! :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)

Tactic:
wlog! hn : 2 * n ≤ Nat.card α

Premises used: Nat.card
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
apply : 2 * (Nat.card α - n) ≤ Nat.card α
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)

Tactic:
apply this hα
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
⊢ 2 * (Nat.card α - n) ≤ Nat.card α

Tactic:
grind
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)

Tactic:
have : IsPretransitive (alternatingGroup α) (powersetCard α (Nat.card α - n)) := by
      apply this hα
      grind
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this_1 :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)
pos : ∀ (hn' : n ≤ Nat.card α), IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
neg : ∀ (hn' : ¬n ≤ Nat.card α), IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)

Tactic:
by_cases hn' : n ≤ Nat.card α

Premises used: Nat.card
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this_1 :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)
hn' : n ≤ Nat.card α
apply : n + (Nat.card α - n) = Fintype.card α
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)

Tactic:
apply IsPretransitive.of_surjective_map
        (mulActionHom_compl_bijective (alternatingGroup α) α _).surjective this

Premises used: Membership.mem, Subtype, Set.powersetCard.mulActionHom_compl_bijective, Function.Bijective.surjective, MulAction.IsPretransitive.of_surjective_map, alternatingGroup
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this_1 :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)
hn' : n ≤ Nat.card α
⊢ n + (Nat.card α - n) = Fintype.card α

Tactic:
aesop
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this_1 :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
this_2 : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)
hn' : ¬n ≤ Nat.card α
this : Subsingleton.{u_2 + 1} (↑(powersetCard α n) : Type u_2)
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this_1 :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)
hn' : ¬n ≤ Nat.card α
neg : Subsingleton.{u_2 + 1} (↑(powersetCard α n) : Type u_2)
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)

Tactic:
suffices Subsingleton (powersetCard α n) by infer_instance
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this_1 :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)
hn' : ¬n ≤ Nat.card α
⊢ Nat.card α < n

Tactic:
rw [not_le] at hn'

Premises used: not_le
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this_1 :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)
hn' : Nat.card α < n
neg : LE.le (α := ℕ) 0 1
⊢ Subsingleton.{u_2 + 1} (↑(powersetCard α n) : Type u_2)

Tactic:
rw [← Finite.card_le_one_iff_subsingleton, powersetCard.card,
        Nat.choose_eq_zero_iff.mpr hn']

Premises used: Iff.mpr, Nat.choose_eq_zero_iff, Finite.card_le_one_iff_subsingleton, Set.powersetCard.card
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this_1 :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)
hn' : Nat.card α < n
⊢ LE.le (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α_1 : Type u_2
n_1 : ℕ
inst : DecidableEq α_1
α : Type u_2
n : ℕ
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
h : IsMultiplyPretransitive (↥(alternatingGroup α)) α n
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)

Tactic:
apply isPretransitive_of_isMultiplyPretransitive

Premises used: Set.powersetCard.isPretransitive_of_isMultiplyPretransitive
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α_1 : Type u_2
n_1 : ℕ
inst : DecidableEq α_1
α : Type u_2
n : ℕ
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
h : ∀ (hn : HMul.hMul (α := ℕ) 2 0 ≤ Nat.card α), IsMultiplyPretransitive (↥(alternatingGroup α)) α 0
h₁ : ∀ (hn0 : n ≠ 0), IsMultiplyPretransitive (↥(alternatingGroup α)) α n
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n

Tactic:
rcases eq_or_ne n 0 with rfl | hn0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α_1 : Type u_2
n : ℕ
inst : DecidableEq α_1
α : Type u_2
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : HMul.hMul (α := ℕ) 2 0 ≤ Nat.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 0

Tactic:
infer_instance
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α_1 : Type u_2
n_1 : ℕ
inst : DecidableEq α_1
α : Type u_2
n : ℕ
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
h :
  ∀ (hn : HMul.hMul (α := ℕ) 2 1 ≤ Nat.card α) (hn0 : Ne (α := ℕ) 1 0),
    IsMultiplyPretransitive (↥(alternatingGroup α)) α 1
h₁ : ∀ (hn1 : n ≠ 1), IsMultiplyPretransitive (↥(alternatingGroup α)) α n
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n

Tactic:
rcases eq_or_ne n 1 with rfl | hn1

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α_1 : Type u_2
n : ℕ
inst : DecidableEq α_1
α : Type u_2
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : HMul.hMul (α := ℕ) 2 1 ≤ Nat.card α
hn0 : Ne (α := ℕ) 1 0
h : IsPretransitive (↥(alternatingGroup α)) α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 1

Tactic:
rw [is_one_pretransitive_iff]

Premises used: MulAction.is_one_pretransitive_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α_1 : Type u_2
n : ℕ
inst : DecidableEq α_1
α : Type u_2
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : HMul.hMul (α := ℕ) 2 1 ≤ Nat.card α
hn0 : Ne (α := ℕ) 1 0
⊢ IsPretransitive (↥(alternatingGroup α)) α

Tactic:
alternatingGroup.isPretransitive_of_three_le_card α hα

Premises used: alternatingGroup.isPretransitive_of_three_le_card
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α_1 : Type u_2
n : ℕ
inst : DecidableEq α_1
α : Type u_2
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : HMul.hMul (α := ℕ) 2 1 ≤ Nat.card α
hn0 : Ne (α := ℕ) 1 0
⊢ IsPretransitive (↥(alternatingGroup α)) α

Tactic:
exact alternatingGroup.isPretransitive_of_three_le_card α hα

Premises used: alternatingGroup.isPretransitive_of_three_le_card
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α_1 : Type u_2
n_1 : ℕ
inst : DecidableEq α_1
α : Type u_2
n : ℕ
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)

Tactic:
have := alternatingGroup.isMultiplyPretransitive α
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α_1 : Type u_2
n_1 : ℕ
inst : DecidableEq α_1
α : Type u_2
n : ℕ
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
hn1 : n ≠ 1
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
h : n ≤ Nat.card α - 2
h₁ : Nat.card α - 2 ≤ Nat.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n

Tactic:
apply isMultiplyPretransitive_of_le (n := Nat.card α - 2)

Premises used: MulAction.isMultiplyPretransitive_of_le
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α_1 : Type u_2
n_1 : ℕ
inst : DecidableEq α_1
α : Type u_2
n : ℕ
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
hn1 : n ≠ 1
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
⊢ n ≤ Nat.card α - 2

Tactic:
grind
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α_1 : Type u_2
n_1 : ℕ
inst : DecidableEq α_1
α : Type u_2
n : ℕ
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
hn1 : n ≠ 1
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
⊢ Nat.card α - 2 ≤ Nat.card α

Tactic:
grind
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)

Tactic:
have : IsPretransitive (alternatingGroup α) (powersetCard α n) :=
    isPretransitive_alternatingGroup (le_trans h_three_le hn.le)
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
⊢ 0 < n

Tactic:
positivity
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
⊢ (↑n : ℕ∞) < ENat.card α

Tactic:
simpa using hn
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
⊢ Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)

Tactic:
have : Nontrivial (powersetCard α n) := nontrivial (by positivity) (by simpa using hn)
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
obtain :
  ∀ (s : (↑(powersetCard α n) : Type u_2)),
    IsPreprimitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
⊢ IsPreprimitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)

Tactic:
obtain ⟨s⟩ := this.to_nonempty

Premises used: Nontrivial.to_nonempty
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
rw : IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer ↥(alternatingGroup α) (↑s : Set α))
⊢ IsPreprimitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)

Tactic:
rw [← isCoatom_stabilizer_iff_preprimitive _ s, stabilizer_coe]

Premises used: Set.powersetCard.stabilizer_coe, MulAction.isCoatom_stabilizer_iff_preprimitive
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
h0 : (↑s : Set α).Nonempty
h1 : (↑s : Set α)ᶜ.Nonempty
hs : Nat.card α ≠ 2 * (↑s : Set α).ncard
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer ↥(alternatingGroup α) (↑s : Set α))

Tactic:
apply alternatingGroup.isCoatom_stabilizer

Premises used: alternatingGroup.isCoatom_stabilizer
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
h0 : 1 ≤ n
⊢ (↑s : Set α).Nonempty

Tactic:
rw [powersetCard.coe_nonempty_iff]

Premises used: Set.powersetCard.coe_nonempty_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
⊢ LE.le (α := ℕ) 1 3

Tactic:
norm_num
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
⊢ 1 ≤ n

Tactic:
exact le_trans (by norm_num) h_three_le

Premises used: le_trans
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
⊢ (↑s : Set α)ᶜ.Nonempty

Tactic:
simpa [nonempty_compl, ne_eq, eq_univ_iff_ncard, ncard_eq] using ne_of_lt hn

Premises used: ne_eq, Set.eq_univ_iff_ncard, ne_of_lt, Set.powersetCard.ncard_eq, Set.nonempty_compl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
⊢ Nat.card α ≠ 2 * (↑s : Set α).ncard

Tactic:
simpa only [ncard_eq]

Premises used: Set.powersetCard.ncard_eq
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
x_1 : ↥(fixingSubgroup M s)
x : α
c : M
hc : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c⁻¹

Tactic:
rw [← Subgroup.inv_mem_iff] at hc

Premises used: Subgroup.inv_mem_iff