awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
refine_1 :
  ∀ (h : Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1),
    Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
refine_2 :
  ∀ (h : Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1),
    Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1
⊢ Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1 ↔
    Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1
refine_1 :
  ∀ (h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1),
    ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1
⊢ Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1

Tactic:
contrapose h with h
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
⊢ ∃ (a : α), g +ᵥ a ≠ a

Tactic:
simpa [Equiv.ext_iff] using h

Premises used: Equiv.ext_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
⊢ ∃ (a : α), g +ᵥ a ≠ a

Tactic:
have : ∃ a, (g +ᵥ a : α) ≠ a := by simpa [Equiv.ext_iff] using h
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
this : ∃ (a : α), g +ᵥ a ≠ a
refine_1 :
  ∀ (a : α) (ha : g +ᵥ a ≠ a), ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1
⊢ ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1

Tactic:
obtain ⟨a, ha⟩ := this
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
a : α
ha : g +ᵥ a ≠ a
refine_1 :
  ∀ (s : (↑(powersetCard α n) : Type u_2)) (has : a ∈ s) (has' : g +ᵥ a ∉ s),
    ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1
⊢ ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1

Tactic:
obtain ⟨s, has, has'⟩ := exists_mem_notMem hn hα (Ne.symm ha)

Premises used: Set.powersetCard.exists_mem_notMem, Ne.symm
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
a : α
ha : g +ᵥ a ≠ a
s : (↑(powersetCard α n) : Type u_2)
has : a ∈ s
has' : g +ᵥ a ∉ s
refine_1 :
  ∃ (x : (↑(powersetCard α n) : Type u_2)),
    ¬Eq (α := (↑(powersetCard α n) : Type u_2))
        ((AddAction.toPerm g : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) x :
          (↑(powersetCard α n) : Type u_2))
        ((1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) x :
          (↑(powersetCard α n) : Type u_2))
⊢ ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1

Tactic:
rw [Equiv.ext_iff, not_forall]

Premises used: Equiv.ext_iff, Classical.not_forall
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
a : α
ha : g +ᵥ a ≠ a
s : (↑(powersetCard α n) : Type u_2)
has : a ∈ s
has' : g +ᵥ a ∉ s
h₁ :
  ¬Eq (α := (↑(powersetCard α n) : Type u_2))
      ((AddAction.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))
⊢ ∃ (x : (↑(powersetCard α n) : Type u_2)),
    ¬Eq (α := (↑(powersetCard α n) : Type u_2))
        ((AddAction.toPerm g : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) x :
          (↑(powersetCard α n) : Type u_2))
        ((1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) x :
          (↑(powersetCard α n) : Type u_2))

Tactic:
use s
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
a : α
ha : g +ᵥ a ≠ a
s : (↑(powersetCard α n) : Type u_2)
has : a ∈ s
has' : g +ᵥ a ∉ s
h₁ :
  ∀
    (has' :
      Eq (α := (↑(powersetCard α n) : Type u_2))
        ((AddAction.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))),
    g +ᵥ a ∈ s
⊢ ¬Eq (α := (↑(powersetCard α n) : Type u_2))
      ((AddAction.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:
contrapose has'
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
a : α
ha : g +ᵥ a ≠ a
s : (↑(powersetCard α n) : Type u_2)
has : a ∈ s
has' :
  Eq (α := (↑(powersetCard α n) : Type u_2))
    ((AddAction.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))
⊢ g +ᵥ s = s

Tactic:
simp only [AddAction.toPerm_apply, coe_one, id_eq] at has'

Premises used: Equiv.Perm.coe_one, AddAction.toPerm_apply, id_eq
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
a : α
ha : g +ᵥ a ≠ a
s : (↑(powersetCard α n) : Type u_2)
has : a ∈ s
has' : g +ᵥ s = s
h₁ : g +ᵥ a ∈ g +ᵥ s
⊢ g +ᵥ a ∈ s

Tactic:
rw [← has']
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
a : α
ha : g +ᵥ a ≠ a
s : (↑(powersetCard α n) : Type u_2)
has : a ∈ s
has' : g +ᵥ s = s
⊢ g +ᵥ a ∈ g +ᵥ s

Tactic:
simpa [← mem_coe_iff]

Premises used: Set.powersetCard.mem_coe_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) 1
refine_2 :
  ∀ (h : ∀ (x : α), g +ᵥ x = (1 : (a : α) → α) x) (x : (↑(powersetCard α n) : Type u_2)),
    g +ᵥ x = (1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) x
⊢ Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1

Tactic:
simp only [Equiv.ext_iff, AddAction.toPerm_apply] at h ⊢

Premises used: Equiv.ext_iff, AddAction.toPerm_apply
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ∀ (x : α), g +ᵥ x = (1 : (a : α) → α) x
⊢ ∀ (x : (↑(powersetCard α n) : Type u_2)),
    g +ᵥ x = (1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) x

Tactic:
simp [Subtype.ext_iff, Finset.ext_iff, mem_vadd_finset, h]

Premises used: Finset.ext_iff, Finset.mem_vadd_finset, Subtype.ext_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
inst_3 : FaithfulVAdd G α
rw : ∀ (g : G), (∀ (a : (↑(powersetCard α n) : Type u_2)), g +ᵥ a = a) → g = 0
⊢ FaithfulVAdd.{u_3, u_2} G (↑(powersetCard α n) : Type u_2)

Tactic:
rw [faithfulVAdd_iff]

Premises used: faithfulVAdd_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
inst_3 : FaithfulVAdd G α
g : G
hg : ∀ (a : (↑(powersetCard α n) : Type u_2)), g +ᵥ a = a
a : Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) (AddAction.toPerm.{u_3, u_2} (α := G) 0)
⊢ g = 0

Tactic:
apply AddAction.toPerm_injective (α := G) (β := α)

Premises used: AddAction.toPerm_injective
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
inst_3 : FaithfulVAdd G α
g : G
hg : ∀ (a : (↑(powersetCard α n) : Type u_2)), g +ᵥ a = a
a : Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1
⊢ Eq.{u_2 + 1} (α := Perm α) (AddAction.toPerm g) (AddAction.toPerm.{u_3, u_2} (α := G) 0)

Tactic:
rw [AddAction.toPerm_zero, ← addAction_faithful hn hα]

Premises used: AddAction.toPerm_zero, Set.powersetCard.addAction_faithful
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
inst_3 : FaithfulVAdd G α
g : G
hg : ∀ (a : (↑(powersetCard α n) : Type u_2)), g +ᵥ a = a
⊢ Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1

Tactic:
Perm.ext_iff.mpr hg

Premises used: Iff.mpr, Equiv.Perm.ext_iff
-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Goal:
α : Type u_2
inst : DecidableEq α
G : Type u_3
inst_1 : AddGroup G
inst_2 : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
inst_3 : FaithfulVAdd G α
g : G
hg : ∀ (a : (↑(powersetCard α n) : Type u_2)), g +ᵥ a = a
⊢ Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1

Tactic:
exact Perm.ext_iff.mpr hg

Premises used: Iff.mpr, Equiv.Perm.ext_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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
⊢ Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1 ↔ Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
refine_1 :
  ∀ (h : Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1),
    Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1
refine_2 :
  ∀ (h : Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1),
    Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1
⊢ Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1 ↔ Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1
refine_1 :
  ∀ (h : ¬Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1),
    ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1
⊢ Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1

Tactic:
contrapose h with h
-- 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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1
⊢ ∃ (a : α), g • a ≠ a

Tactic:
simpa [Equiv.ext_iff] using h

Premises used: Equiv.ext_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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1
⊢ ∃ (a : α), g • a ≠ a

Tactic:
have : ∃ a, (g • a : α) ≠ a := by simpa [Equiv.ext_iff] using h
-- 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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1
this : ∃ (a : α), g • a ≠ a
refine_1 : ∀ (a : α) (ha : g • a ≠ a), ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1
⊢ ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1

Tactic:
obtain ⟨a, ha⟩ := this
-- 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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1
a : α
ha : g • a ≠ a
refine_1 :
  ∀ (s : (↑(powersetCard α n) : Type u_2)) (has : a ∈ s) (has' : g • a ∉ s),
    ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1
⊢ ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1

Tactic:
obtain ⟨s, has, has'⟩ := exists_mem_notMem hn hα (Ne.symm ha)

Premises used: Set.powersetCard.exists_mem_notMem, Ne.symm
-- 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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1
a : α
ha : g • a ≠ a
s : (↑(powersetCard α n) : Type u_2)
has : a ∈ s
has' : g • a ∉ s
refine_1 :
  ∃ (x : (↑(powersetCard α n) : Type u_2)),
    ¬Eq (α := (↑(powersetCard α n) : Type u_2))
        ((toPerm g : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) x :
          (↑(powersetCard α n) : Type u_2))
        ((1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) x :
          (↑(powersetCard α n) : Type u_2))
⊢ ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1

Tactic:
rw [Equiv.ext_iff, not_forall]

Premises used: Equiv.ext_iff, Classical.not_forall
-- 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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1
a : α
ha : g • a ≠ a
s : (↑(powersetCard α n) : Type u_2)
has : a ∈ s
has' : g • a ∉ s
h₁ :
  ¬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))
⊢ ∃ (x : (↑(powersetCard α n) : Type u_2)),
    ¬Eq (α := (↑(powersetCard α n) : Type u_2))
        ((toPerm g : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) x :
          (↑(powersetCard α n) : Type u_2))
        ((1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) x :
          (↑(powersetCard α n) : Type u_2))

Tactic:
use s
-- 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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1
a : α
ha : g • a ≠ a
s : (↑(powersetCard α n) : Type u_2)
has : a ∈ s
has' : g • a ∉ s
h₁ :
  ∀
    (has' :
      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))),
    g • a ∈ s
⊢ ¬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:
contrapose! has'
-- 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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1
a : α
ha : g • a ≠ a
s : (↑(powersetCard α n) : Type u_2)
has : a ∈ s
has' :
  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))
⊢ g • s = s

Tactic:
simp only [toPerm_apply, coe_one, id_eq] at has'

Premises used: MulAction.toPerm_apply, Equiv.Perm.coe_one, id_eq
-- 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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1
a : α
ha : g • a ≠ a
s : (↑(powersetCard α n) : Type u_2)
has : a ∈ s
has' : g • s = s
h₁ : g • a ∈ g • s
⊢ g • a ∈ s

Tactic:
rw [← has']
-- 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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ¬Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1
a : α
ha : g • a ≠ a
s : (↑(powersetCard α n) : Type u_2)
has : a ∈ s
has' : g • s = s
⊢ g • a ∈ g • s

Tactic:
simpa only [coe_smul, smul_mem_smul_finset_iff, ← mem_coe_iff]

Premises used: Finset.smul_mem_smul_finset_iff, Set.powersetCard.mem_coe_iff, Set.powersetCard.coe_smul
-- 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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1
refine_2 :
  ∀ (h : ∀ (x : α), g • x = (1 : (a : α) → α) x) (x : (↑(powersetCard α n) : Type u_2)),
    g • x = (1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) x
⊢ Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1

Tactic:
simp only [Equiv.ext_iff, toPerm_apply] at h ⊢

Premises used: MulAction.toPerm_apply, Equiv.ext_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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
g : G
h : ∀ (x : α), g • x = (1 : (a : α) → α) x
⊢ ∀ (x : (↑(powersetCard α n) : Type u_2)),
    g • x = (1 : (a : (↑(powersetCard α n) : Type u_2)) → (↑(powersetCard α n) : Type u_2)) x

Tactic:
simp [Subtype.ext_iff, Finset.ext_iff, mem_smul_finset, h]

Premises used: Finset.ext_iff, Subtype.ext_iff, Finset.mem_smul_finset
-- 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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
inst_3 : FaithfulSMul G α
rw : ∀ (g : G), (∀ (a : (↑(powersetCard α n) : Type u_2)), g • a = a) → g = 1
⊢ FaithfulSMul.{u_1, u_2} G (↑(powersetCard α n) : Type u_2)

Tactic:
rw [faithfulSMul_iff]

Premises used: faithfulSMul_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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
inst_3 : FaithfulSMul G α
g : G
hg : ∀ (a : (↑(powersetCard α n) : Type u_2)), g • a = a
a : Eq.{u_2 + 1} (α := Perm α) (toPerm g) (toPerm.{u_1, u_2} (α := G) 1)
⊢ g = 1

Tactic:
apply toPerm_injective (α := G) (β := α)

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 α
n : ℕ
inst_2 : DecidableEq α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
inst_3 : FaithfulSMul G α
g : G
hg : ∀ (a : (↑(powersetCard α n) : Type u_2)), g • a = a
a : Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1
⊢ Eq.{u_2 + 1} (α := Perm α) (toPerm g) (toPerm.{u_1, u_2} (α := G) 1)

Tactic:
rw [toPerm_one, ← mulAction_faithful hn hα]

Premises used: Set.powersetCard.mulAction_faithful, MulAction.toPerm_one
-- 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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
inst_3 : FaithfulSMul G α
g : G
hg : ∀ (a : (↑(powersetCard α n) : Type u_2)), g • a = a
⊢ Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1

Tactic:
Perm.ext_iff.mpr hg

Premises used: Iff.mpr, Equiv.Perm.ext_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 α
hn : 1 ≤ n
hα : (↑n : ℕ∞) < ENat.card α
inst_3 : FaithfulSMul G α
g : G
hg : ∀ (a : (↑(powersetCard α n) : Type u_2)), g • a = a
⊢ Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1

Tactic:
exact Perm.ext_iff.mpr hg

Premises used: Iff.mpr, Equiv.Perm.ext_iff
-- 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 ↪ α
rw :
  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))
⊢ ofFinEmb n α (g • f) = id g • ofFinEmb n α f

Tactic:
rw [← Subtype.coe_inj, coe_smul, f.smul_def, val_ofFinEmb, val_ofFinEmb,
      smul_finset_def, ← map_map, map_eq_image]

Premises used: Set.powersetCard.val_ofFinEmb, Subtype.coe_inj, Function.Embedding.smul_def, Finset.map_eq_image, Finset.smul_finset_def, Finset.map_map, Set.powersetCard.coe_smul