awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
n : ℕ
s t : (↑(powersetCard α n) : Type u_2)
inst_2 : DecidableEq α
g : G
f : Fin n ↪ α
⊢ Eq (α := Finset α) (Finset.image (⇑(Equiv.toEmbedding (toPerm g)) : (a : α) → α) (Finset.map f Finset.univ))
    (Finset.image (fun (x : α) ↦ id g • x) (Finset.map f Finset.univ))

Tactic:
simp [toPerm]

Premises used: MulAction.toPerm
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
n : ℕ
inst_2 : DecidableEq α
f : Fin n ↪ α
⊢ (↑(MulActionHom.toFun (mulActionHom_of_embedding G α n) f) : Finset α) = Finset.map f Finset.univ

Tactic:
rfl

Premises used: Finset.map, rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
n : ℕ
inst_2 : DecidableEq α
s : Finset α
hs : s ∈ powersetCard α n
rw : Fintype.card (Fin n) = n
rw₁ : n = n
rw₂ : ℕ
rw₃ : n = n
rw₄ : ℕ
⊢ Fintype.card (Fin n) = #s

Tactic:
rw [hs, Fintype.card_fin]

Premises used: Fintype.card_fin
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
n : ℕ
inst_2 : DecidableEq α
s : Finset α
hs : s ∈ powersetCard α n
obtain :
  ∀ (f : Fin n ↪ α) (hf : Finset.map f Finset.univ = s),
    ∃ (a : Fin n ↪ α),
      (mulActionHom_of_embedding G α n : (a : Fin n ↪ α) → (↑(powersetCard α n) : Type u_2)) a =
        Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α n) s hs
⊢ ∃ (a : Fin n ↪ α),
    (mulActionHom_of_embedding G α n : (a : Fin n ↪ α) → (↑(powersetCard α n) : Type u_2)) a =
      Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α n) s hs

Tactic:
obtain ⟨f : Fin n ↪ α, hf⟩ :=
    Function.Embedding.exists_of_card_eq_finset (by rw [hs, Fintype.card_fin])

Premises used: Function.Embedding.exists_of_card_eq_finset, Fin
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
n : ℕ
inst_2 : DecidableEq α
s : Finset α
hs : s ∈ powersetCard α n
f : Fin n ↪ α
hf : Finset.map f Finset.univ = s
⊢ ∃ (a : Fin n ↪ α),
    (mulActionHom_of_embedding G α n : (a : Fin n ↪ α) → (↑(powersetCard α n) : Type u_2)) a =
      Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α n) s hs

Tactic:
⟨f, Subtype.ext hf⟩

Premises used: Exists.intro, Subtype.ext
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
n : ℕ
inst_2 : DecidableEq α
s : Finset α
hs : s ∈ powersetCard α n
f : Fin n ↪ α
hf : Finset.map f Finset.univ = s
⊢ ∃ (a : Fin n ↪ α),
    (mulActionHom_of_embedding G α n : (a : Fin n ↪ α) → (↑(powersetCard α n) : Type u_2)) a =
      Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α n) s hs

Tactic:
exact ⟨f, Subtype.ext hf⟩
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
n : ℕ
inst_2 : DecidableEq α
h : IsMultiplyPretransitive G α n
⊢ IsPretransitive.{u_1, u_2} G (↑(powersetCard α n) : Type u_2)

Tactic:
IsPretransitive.of_surjective_map (mulActionHom_of_embedding_surjective G α) h

Premises used: MulAction.IsPretransitive.of_surjective_map, Set.powersetCard.mulActionHom_of_embedding_surjective
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
⊢ IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)

Tactic:
isPretransitive_of_isMultiplyPretransitive _ (isMultiplyPretransitive α n)

Premises used: Set.powersetCard.isPretransitive_of_isMultiplyPretransitive, Equiv.Perm.isMultiplyPretransitive
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
n : ℕ
s_1 t : (↑(powersetCard α n) : Type u_2)
inst_2 : DecidableEq α
inst_3 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
g : G
s : (↑(powersetCard α n) : Type u_2)
a :
  ∀ (a : α),
    Membership.mem (γ := Finset α)
        (↑((compl hm : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α m) : Type u_2)) (g • s)) : Finset α)
        a ↔
      a ∈
        (↑(HSMul.hSMul (β := (↑(powersetCard α m) : Type u_2)) (id g)
              ((compl hm : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α m) : Type u_2)) s :
                (↑(powersetCard α m) : Type u_2))) :
          Finset α)
⊢ (compl hm : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α m) : Type u_2)) (g • s) =
    HSMul.hSMul (β := (↑(powersetCard α m) : Type u_2)) (id g)
      ((compl hm : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α m) : Type u_2)) s :
        (↑(powersetCard α m) : Type u_2))

Tactic:
ext
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
n : ℕ
s_1 t : (↑(powersetCard α n) : Type u_2)
inst_2 : DecidableEq α
inst_3 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
g : G
s : (↑(powersetCard α n) : Type u_2)
a : α
⊢ Membership.mem (γ := Finset α)
      (↑((compl hm : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α m) : Type u_2)) (g • s)) : Finset α) a ↔
    a ∈
      (↑(HSMul.hSMul (β := (↑(powersetCard α m) : Type u_2)) (id g)
            ((compl hm : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α m) : Type u_2)) s :
              (↑(powersetCard α m) : Type u_2))) :
        Finset α)

Tactic:
simp [← inv_smul_mem_iff]

Premises used: Finset.inv_smul_mem_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
n : ℕ
inst_2 : DecidableEq α
inst_3 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : (↑(powersetCard α n) : Type u_2)
⊢ (↑((mulActionHom_compl G α hm : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α m) : Type u_2)) s) :
      Finset α) =
    (↑s : Finset α)ᶜ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
n : ℕ
inst_2 : DecidableEq α
inst_3 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : (↑(powersetCard α n) : Type u_2)
a : α
⊢ Membership.mem (γ := (↑(powersetCard α m) : Type u_2))
      ((mulActionHom_compl G α hm : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α m) : Type u_2)) s :
        (↑(powersetCard α m) : Type u_2))
      a ↔
    a ∉ s

Tactic:
mem_compl

Premises used: Set.Mem, setOf, Set.powersetCard.mem_compl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
n : ℕ
inst_2 : DecidableEq α
inst_3 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
a :
  ∀ (s : (↑(powersetCard α n) : Type u_2)) (a : α),
    Membership.mem (γ := Finset α)
        (↑((MulActionHom.comp (mulActionHom_compl G α ⋯) (mulActionHom_compl G α hm) :
                (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2))
              s) :
          Finset α)
        a ↔
      Membership.mem (γ := Finset α)
        (↑((MulActionHom.id G : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) s) :
          Finset α)
        a
⊢ Eq (α :=
    MulActionHom.{u_1, u_1, u_2, u_2} (M := G) id (↑(powersetCard α n) : Type u_2) (↑(powersetCard α n) : Type u_2))
    (MulActionHom.comp (mulActionHom_compl G α ⋯) (mulActionHom_compl G α hm)) (MulActionHom.id G)

Tactic:
ext s a
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
n : ℕ
inst_2 : DecidableEq α
inst_3 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : (↑(powersetCard α n) : Type u_2)
a : α
a₁ :
  Membership.mem (γ := (↑(powersetCard α n) : Type u_2))
      ((MulActionHom.comp (mulActionHom_compl G α ⋯) (mulActionHom_compl G α hm) :
            (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2))
          s :
        (↑(powersetCard α n) : Type u_2))
      a ↔
    a ∈ s
⊢ Membership.mem (γ := Finset α)
      (↑((MulActionHom.comp (mulActionHom_compl G α ⋯) (mulActionHom_compl G α hm) :
              (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2))
            s) :
        Finset α)
      a ↔
    Membership.mem (γ := Finset α)
      (↑((MulActionHom.id G : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) s) : Finset α)
      a

Tactic:
change a ∈ (mulActionHom_compl G α _).comp (mulActionHom_compl G α hm) s ↔ a ∈ s

Premises used: MulActionHom.comp, Set.powersetCard.mulActionHom_compl, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
n : ℕ
inst_2 : DecidableEq α
inst_3 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
s : (↑(powersetCard α n) : Type u_2)
a : α
⊢ Membership.mem (γ := (↑(powersetCard α n) : Type u_2))
      ((MulActionHom.comp (mulActionHom_compl G α ⋯) (mulActionHom_compl G α hm) :
            (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2))
          s :
        (↑(powersetCard α n) : Type u_2))
      a ↔
    a ∈ s

Tactic:
simp [MulActionHom.comp_apply, mem_mulActionHom_compl]

Premises used: Set.powersetCard.mem_mulActionHom_compl, MulActionHom.comp_apply
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
n : ℕ
inst_2 : DecidableEq α
inst_3 : Fintype α
m : ℕ
hm : m + n = Fintype.card α
⊢ Function.Bijective (α := (↑(powersetCard α n) : Type u_2)) (β := (↑(powersetCard α m) : Type u_2))
    (⇑(mulActionHom_compl G α hm) : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α m) : Type u_2))

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨mulActionHom_compl G α ((n.add_comm m).trans hm),
    DFunLike.ext_iff.mp (mulActionHom_compl_mulActionHom_compl G α hm),
    DFunLike.ext_iff.mp (mulActionHom_compl_mulActionHom_compl G α _)⟩

Premises used: Iff.mpr, DFunLike.ext_iff, Set.powersetCard.mulActionHom_compl_mulActionHom_compl, Function.bijective_iff_has_inverse, And.intro, Exists.intro, Iff.mp, Set.powersetCard.mulActionHom_compl, DFunLike.coe, Eq.trans, Nat.add_comm
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Nontrivial G
inst_4 : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
obtain :
  ∀ (g : G) (h : g ≠ 1),
    Ne.{u_2 + 1} (α := Set (↑(powersetCard α n) : Type u_2)) (fixedPoints G (↑(powersetCard α n) : Type u_2)) univ
⊢ Ne.{u_2 + 1} (α := Set (↑(powersetCard α n) : Type u_2)) (fixedPoints G (↑(powersetCard α n) : Type u_2)) univ

Tactic:
obtain ⟨g, h⟩ := exists_ne (1 : G)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Nontrivial G
inst_4 : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h : g ≠ 1
contrapose! :
  ∀
    (h :
      Eq.{u_2 + 1} (α := Set (↑(powersetCard α n) : Type u_2)) (fixedPoints G (↑(powersetCard α n) : Type u_2)) univ),
    g = 1
⊢ Ne.{u_2 + 1} (α := Set (↑(powersetCard α n) : Type u_2)) (fixedPoints G (↑(powersetCard α n) : Type u_2)) univ

Tactic:
contrapose! h
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Nontrivial G
inst_4 : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h : Eq.{u_2 + 1} (α := Set (↑(powersetCard α n) : Type u_2)) (fixedPoints G (↑(powersetCard α n) : Type u_2)) univ
H :
  ∀ (s : (↑(powersetCard α n) : Type u_2)),
    Eq (α := (↑(powersetCard α n) : Type u_2))
      ((toPerm g : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) s :
        (↑(powersetCard α n) : Type u_2))
      ((1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) s :
        (↑(powersetCard α n) : Type u_2))
⊢ Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1

Tactic:
ext1 s
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Nontrivial G
inst_4 : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h : Eq.{u_2 + 1} (α := Set (↑(powersetCard α n) : Type u_2)) (fixedPoints G (↑(powersetCard α n) : Type u_2)) univ
s : (↑(powersetCard α n) : Type u_2)
⊢ Eq (α := (↑(powersetCard α n) : Type u_2))
    ((toPerm g : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) s :
      (↑(powersetCard α n) : Type u_2))
    ((1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) s :
      (↑(powersetCard α n) : Type u_2))

Tactic:
eq_univ_iff_forall.mp h s g

Premises used: Set.eq_univ_iff_forall, Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Nontrivial G
inst_4 : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h : Eq.{u_2 + 1} (α := Set (↑(powersetCard α n) : Type u_2)) (fixedPoints G (↑(powersetCard α n) : Type u_2)) univ
s : (↑(powersetCard α n) : Type u_2)
⊢ Eq (α := (↑(powersetCard α n) : Type u_2))
    ((toPerm g : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) s :
      (↑(powersetCard α n) : Type u_2))
    ((1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) s :
      (↑(powersetCard α n) : Type u_2))

Tactic:
exact eq_univ_iff_forall.mp h s g

Premises used: Set.eq_univ_iff_forall, Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Nontrivial G
inst_4 : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h : Eq.{u_2 + 1} (α := Set (↑(powersetCard α n) : Type u_2)) (fixedPoints G (↑(powersetCard α n) : Type u_2)) univ
⊢ Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1

Tactic:
replace h : (toPerm g : Perm (powersetCard α n)) = 1 := by
    ext1 s
    exact eq_univ_iff_forall.mp h s g
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Nontrivial G
inst_4 : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h : Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1
hf :
  ∀
    (h :
      Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2))
        ((toPermHom G (↑(powersetCard α n) : Type u_2) : (a : G) → Perm (↑(powersetCard α n) : Type u_2)) g :
          Perm (↑(powersetCard α n) : Type u_2))
        (1 : Perm (↑(powersetCard α n) : Type u_2))),
    Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := Perm (↑(powersetCard α n) : Type u_2))
      (⇑(toPermHom G (↑(powersetCard α n) : Type u_2)) : (a : G) → Perm (↑(powersetCard α n) : Type u_2))
⊢ g = 1

Tactic:
rwa [← toPermHom_apply, map_eq_one_iff] at h

Premises used: MulAction.toPermHom_apply, map_eq_one_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Nontrivial G
inst_4 : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h :
  Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2))
    ((toPermHom G (↑(powersetCard α n) : Type u_2) : (a : G) → Perm (↑(powersetCard α n) : Type u_2)) g :
      Perm (↑(powersetCard α n) : Type u_2))
    (1 : Perm (↑(powersetCard α n) : Type u_2))
hf :
  ∀ (this : FaithfulSMul.{u_1, u_2} G (↑(powersetCard α n) : Type u_2)),
    Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := Perm (↑(powersetCard α n) : Type u_2))
      (⇑(toPermHom G (↑(powersetCard α n) : Type u_2)) : (a : G) → Perm (↑(powersetCard α n) : Type u_2))
hf₁ : (↑n : ℕ∞) < ENat.card α
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := Perm (↑(powersetCard α n) : Type u_2))
    (⇑(toPermHom G (↑(powersetCard α n) : Type u_2)) : (a : G) → Perm (↑(powersetCard α n) : Type u_2))

Tactic:
have := powersetCard.faithfulSMul (G := G) (α := α) hn ?_
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Nontrivial G
inst_4 : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h :
  Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2))
    ((toPermHom G (↑(powersetCard α n) : Type u_2) : (a : G) → Perm (↑(powersetCard α n) : Type u_2)) g :
      Perm (↑(powersetCard α n) : Type u_2))
    (1 : Perm (↑(powersetCard α n) : Type u_2))
this : FaithfulSMul.{u_1, u_2} G (↑(powersetCard α n) : Type u_2)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := Perm (↑(powersetCard α n) : Type u_2))
    (⇑(toPermHom G (↑(powersetCard α n) : Type u_2)) : (a : G) → Perm (↑(powersetCard α n) : Type u_2))

Tactic:
MulAction.toPerm_injective

Premises used: MulAction.toPerm, MulAction.toPerm_injective
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Nontrivial G
inst_4 : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h :
  Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2))
    ((toPermHom G (↑(powersetCard α n) : Type u_2) : (a : G) → Perm (↑(powersetCard α n) : Type u_2)) g :
      Perm (↑(powersetCard α n) : Type u_2))
    (1 : Perm (↑(powersetCard α n) : Type u_2))
this : FaithfulSMul.{u_1, u_2} G (↑(powersetCard α n) : Type u_2)
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := G) (β := Perm (↑(powersetCard α n) : Type u_2))
    (⇑(toPermHom G (↑(powersetCard α n) : Type u_2)) : (a : G) → Perm (↑(powersetCard α n) : Type u_2))

Tactic:
exact MulAction.toPerm_injective

Premises used: MulAction.toPerm_injective
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
inst_3 : Nontrivial G
inst_4 : FaithfulSMul G α
n : ℕ
hn : 0 < n
hn' : n < Nat.card α
g : G
h :
  Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2))
    ((toPermHom G (↑(powersetCard α n) : Type u_2) : (a : G) → Perm (↑(powersetCard α n) : Type u_2)) g :
      Perm (↑(powersetCard α n) : Type u_2))
    (1 : Perm (↑(powersetCard α n) : Type u_2))
⊢ (↑n : ℕ∞) < ENat.card α

Tactic:
simpa [ENat.card_eq_coe_natCard, Nat.cast_lt, Nat.finite_of_card_ne_zero (ne_zero_of_lt hn')]

Premises used: ne_zero_of_lt, Nat.finite_of_card_ne_zero, Nat.cast_lt, ENat.card_eq_coe_natCard
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
⊢ Function.Bijective (α := α) (β := (↑(powersetCard α 1) : Type u_2))
    (⇑(mulActionHom_singleton G α) : (a : α) → (↑(powersetCard α 1) : Type u_2))

Tactic:
⟨fun a b h ↦ Finset.singleton_injective congr($h.1), fun ⟨s, hs⟩ ↦ ?_⟩

Premises used: congrArg, Set.powersetCard.mulActionHom_singleton, _private.0.Set.powersetCard.mulActionHom_singleton_bijective.match_1, Exists, id, Finset.singleton_injective, And.intro, Function.Bijective, Subtype.val, Eq, DFunLike.coe
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
refine :
  ∀ (x : (↑(powersetCard α 1) : Type u_2)) (s : Finset α) (hs : s ∈ powersetCard α 1),
    ∃ (a : α),
      (mulActionHom_singleton G α : (a : α) → (↑(powersetCard α 1) : Type u_2)) a =
        Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α 1) s hs
⊢ Function.Bijective (α := α) (β := (↑(powersetCard α 1) : Type u_2))
    (⇑(mulActionHom_singleton G α) : (a : α) → (↑(powersetCard α 1) : Type u_2))

Tactic:
refine ⟨fun a b h ↦ Finset.singleton_injective congr($h.1), fun ⟨s, hs⟩ ↦ ?_⟩
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
x : (↑(powersetCard α 1) : Type u_2)
s : Finset α
hs : s ∈ powersetCard α 1
obtain :
  ∀ (a : α) (hs : {a} ∈ powersetCard α 1),
    ∃ (a_1 : α),
      (mulActionHom_singleton G α : (a : α) → (↑(powersetCard α 1) : Type u_2)) a_1 =
        Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α 1) {a} hs
⊢ ∃ (a : α),
    (mulActionHom_singleton G α : (a : α) → (↑(powersetCard α 1) : Type u_2)) a =
      Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α 1) s hs

Tactic:
obtain ⟨a, rfl⟩ := card_eq_one.mp hs

Premises used: Finset.card_eq_one, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
x : (↑(powersetCard α 1) : Type u_2)
a : α
hs : {a} ∈ powersetCard α 1
⊢ ∃ (a_1 : α),
    (mulActionHom_singleton G α : (a : α) → (↑(powersetCard α 1) : Type u_2)) a_1 =
      Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α 1) {a} hs

Tactic:
⟨a, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
inst_2 : DecidableEq α
x : (↑(powersetCard α 1) : Type u_2)
a : α
hs : {a} ∈ powersetCard α 1
⊢ ∃ (a_1 : α),
    (mulActionHom_singleton G α : (a : α) → (↑(powersetCard α 1) : Type u_2)) a_1 =
      Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α 1) {a} hs

Tactic:
exact ⟨a, rfl⟩
-- 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
⊢ Finite α

Tactic:
have : Finite α := Nat.finite_of_card_ne_zero (Nat.ne_zero_of_lt hn)
-- 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 : Finite α
have : ∀ (this : Fintype α), IsPreprimitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
⊢ IsPreprimitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)

Tactic:
have : Fintype α := Fintype.ofFinite α
-- 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 : Fintype α
⊢ IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)

Tactic:
have : IsPretransitive (Perm α) (powersetCard α n) := powersetCard.isPretransitive
-- 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 : IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
⊢ Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)

Tactic:
have : Nontrivial (powersetCard α n) := powersetCard.nontrivial' h_one_le hn
-- 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)
obtain : ∀ (s : (↑(powersetCard α n) : Type u_2)), IsPreprimitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
⊢ IsPreprimitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)

Tactic:
obtain ⟨s⟩ := this.to_nonempty

Premises used: Nontrivial.to_nonempty