awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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 α) (AddAction.toPerm g) (AddAction.toPerm.{u_3, u_2} (α := G) 0)
have a : Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (AddAction.toPerm g) 1
Tactic: rw [AddAction.toPerm_zero, ← addAction_faithful hn hα]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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
have refine_1 : ∀ (h : 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 ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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
⊢ Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1 ↔ Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1
have refine_2 : ∀ (h : Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1), Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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
⊢ Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1
have refine_1 : ∀ (h : ¬Eq.{u_2 + 1} (α := Perm α) (toPerm g) 1),
  ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1
Tactic: contrapose h with h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (hypothesis)
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
⊢ ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1
have this : ∃ (a : α), g • a ≠ a
Tactic: have : ∃ a, (g • a : α) ≠ a := by simpa [Equiv.ext_iff] using h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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
⊢ ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1
have refine_1 : ∀ (a : α) (ha : g • a ≠ a), ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1
Tactic: obtain ⟨a, ha⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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
⊢ ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1
have 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
Tactic: obtain ⟨s, has, has'⟩ := exists_mem_notMem hn hα (Ne.symm ha)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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
⊢ ¬Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1
have 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))
Tactic: rw [Equiv.ext_iff, not_forall]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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
⊢ ∃ (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))
have 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))
Tactic: use s
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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
⊢ ¬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))
have 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
Tactic: contrapose! has'
Cleared hypotheses: has'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (hypothesis)
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 • a ∈ s
have has'₁ : g • s = s
Tactic: simp only [toPerm_apply, coe_one, id_eq] at has'
Cleared hypotheses: has'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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 ∈ s
have h₁ : g • a ∈ g • s
Tactic: rw [← has']
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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
⊢ Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1
have 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
Tactic: simp only [Equiv.ext_iff, toPerm_apply] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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 α
⊢ FaithfulSMul.{u_1, u_2} G (↑(powersetCard α n) : Type u_2)
have rw : ∀ (g : G), (∀ (a : (↑(powersetCard α n) : Type u_2)), g • a = a) → g = 1
Tactic: rw [faithfulSMul_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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
⊢ g = 1
have a : Eq.{u_2 + 1} (α := Perm α) (toPerm g) (toPerm.{u_1, u_2} (α := G) 1)
Tactic: apply toPerm_injective (α := G) (β := α)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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 α) (toPerm g) (toPerm.{u_1, u_2} (α := G) 1)
have a : Eq.{u_2 + 1} (α := Perm (↑(powersetCard α n) : Type u_2)) (toPerm g) 1
Tactic: rw [toPerm_one, ← mulAction_faithful hn hα]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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 ↪ α
⊢ ofFinEmb n α (g • f) = id g • ofFinEmb n α f
have 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))
Tactic: rw [← Subtype.coe_inj, coe_smul, f.smul_def, val_ofFinEmb, val_ofFinEmb,
      smul_finset_def, ← map_map, map_eq_image]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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
⊢ Fintype.card (Fin n) = #s
have rw : Fintype.card (Fin n) = n
Tactic: rw [hs, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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
⊢ Fintype.card (Fin n) = #s
have rw₁ : n = n
Tactic: rw [hs, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨f : Fin n ↪ α, hf⟩ :=
    Function.Embedding.exists_of_card_eq_finset (by rw [hs, Fintype.card_fin])
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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)
⊢ (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))
have 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 α)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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 α
⊢ 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)
have a : ∀ (s : (↑(powersetCard α n) : Type u_2)) (a : α),
  Membership.mem (γ := Finset α)
      (↑((MulActionHom.comp (mulActionHom_compl G α sorry) (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: ext s a
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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 (γ := 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
have a₁ : Membership.mem (γ := (↑(powersetCard α n) : Type u_2))
    ((MulActionHom.comp (mulActionHom_compl G α sorry) (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: change a ∈ (mulActionHom_compl G α _).comp (mulActionHom_compl G α hm) s ↔ a ∈ s
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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 α
⊢ Ne.{u_2 + 1} (α := Set (↑(powersetCard α n) : Type u_2)) (fixedPoints G (↑(powersetCard α n) : Type u_2)) univ
have obtain : ∀ (g : G) (h : g ≠ 1),
  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)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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
⊢ Ne.{u_2 + 1} (α := Set (↑(powersetCard α n) : Type u_2)) (fixedPoints G (↑(powersetCard α n) : Type u_2)) univ
have contrapose! : ∀ (h : Eq.{u_2 + 1} (α := Set (↑(powersetCard α n) : Type u_2)) (fixedPoints G (↑(powersetCard α n) : Type u_2)) univ),
  g = 1
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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
have 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))
Tactic: ext1 s
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (hypothesis)
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
⊢ g = 1
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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
⊢ g = 1
have 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))
Tactic: rwa [← toPermHom_apply, map_eq_one_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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))
⊢ 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))
have 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))
Tactic: have := powersetCard.faithfulSMul (G := G) (α := α) hn ?_
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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))
⊢ 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))
have hf₁ : (↑n : ℕ∞) < ENat.card α
Tactic: have := powersetCard.faithfulSMul (G := G) (α := α) hn ?_
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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))
have 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
Tactic: refine ⟨fun a b h ↦ Finset.singleton_injective congr($h.1), fun ⟨s, hs⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
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
⊢ ∃ (a : α),
    (mulActionHom_singleton G α : (a : α) → (↑(powersetCard α 1) : Type u_2)) a =
      Subtype.mk (p := fun (x : Finset α) ↦ x ∈ powersetCard α 1) s hs
have 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
Tactic: obtain ⟨a, rfl⟩ := card_eq_one.mp hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
⊢ IsPreprimitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
have this : Finite α
Tactic: have : Finite α := Nat.finite_of_card_ne_zero (Nat.ne_zero_of_lt hn)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this : Finite α
⊢ IsPreprimitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
have have : ∀ (this : Fintype α), IsPreprimitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
Tactic: have : Fintype α := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (hypothesis)
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 α
⊢ IsPreprimitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
have this₁ : IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
Tactic: have : IsPretransitive (Perm α) (powersetCard α n) := powersetCard.isPretransitive
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (hypothesis)
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)
⊢ IsPreprimitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
have this₁ : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
Tactic: have : Nontrivial (powersetCard α n) := powersetCard.nontrivial' h_one_le hn