internlm/Lean-Github huggingface dataset:
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
⊢ g • { val := Set.Finite.toFinset this, property := hs } ≠ { val := Set.Finite.toFinset this, property := hs }
Tactic:
simp only [ne_eq]
Proof state after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
⊢ ¬g • { val := Set.Finite.toFinset this, property := hs } = { val := Set.Finite.toFinset this, property := hs }
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
⊢ ¬g • { val := Set.Finite.toFinset this, property := hs } = { val := Set.Finite.toFinset this, property := hs }
Tactic:
rw [Nat.Combination.eq_iff, ← Finset.coe_inj, combination_mulAction.coe_apply', Finset.coe_smul_finset, Set.Finite.coe_toFinset]
Proof state after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
⊢ ¬g • s = s
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
⊢ ¬g • s = s
Tactic:
intro h
Proof state after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
h : g • s = s
⊢ False
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
h : g • s = s
⊢ False
Tactic:
apply has'
Proof state after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
h : g • s = s
⊢ g • a ∈ s
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
h : g • s = s
⊢ g • a ∈ s
Tactic:
rw [← h]
Proof state after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
h : g • s = s
⊢ g • a ∈ g • s
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
s : Set α
has : a ∈ s
has' : g • a ∉ s
this : Set.Finite s
hs : (Set.Finite.toFinset this).card = n
h : g • s = s
⊢ g • a ∈ g • s
Tactic:
exact Set.smul_mem_smul_set has
Proof state after:
no goals
Theorem: Nat.combination.mulAction_faithful
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
⊢ {a} ⊆ {g • a}ᶜ
Tactic:
simp only [Set.subset_compl_singleton_iff, Set.mem_singleton_iff]
Proof state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
⊢ ¬g • a = a
Theorem: Nat.combination.mulAction_faithful
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
⊢ ¬g • a = a
Tactic:
exact ha
Proof state after:
no goals
Theorem: Nat.combination.mulAction_faithful
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
⊢ ↑n ≤ Set.encard {g • a}ᶜ
Tactic:
rw [← not_lt, ← WithTop.add_one_lt_coe_succ_iff, not_lt, add_comm,
  ← Set.encard_singleton (g • a), Set.encard_add_encard_compl, Set.encard_univ]
Proof state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
⊢ ↑(succ n) ≤ PartENat.withTopEquiv (PartENat.card α)
Theorem: Nat.combination.mulAction_faithful
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
⊢ ↑(succ n) ≤ PartENat.withTopEquiv (PartENat.card α)
Tactic:
rw [← PartENat.withTopEquiv_natCast, PartENat.withTopEquiv_le]
Proof state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
⊢ ↑(succ n) ≤ PartENat.card α
Theorem: Nat.combination.mulAction_faithful
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
⊢ ↑(succ n) ≤ PartENat.card α
Tactic:
exact hα
Proof state after:
no goals
Theorem: Nat.combination.mulAction_faithful
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
⊢ Set.encard {a} ≤ ↑n
Tactic:
rw [Set.encard_singleton, ← Nat.cast_one, Nat.cast_le]
Proof state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
⊢ 1 ≤ n
Theorem: Nat.combination.mulAction_faithful
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
⊢ 1 ≤ n
Tactic:
exact hn
Proof state after:
no goals
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case h.left
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {g • a}ᶜ
hs : Set.encard s = ↑n
⊢ Set.encard s = ↑n
Tactic:
exact hs
Proof state after:
no goals
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case h.right
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
has : {a} ⊆ s
has' : s ⊆ {g • a}ᶜ
hs : Set.encard s = ↑n
⊢ a ∈ s ∧ g • a ∉ s
Tactic:
simp only [Set.singleton_subset_iff, Set.subset_compl_singleton_iff] at has has'
Proof state after:
case h.right
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
has' : g • a ∉ s
⊢ a ∈ s ∧ g • a ∉ s
Theorem: Nat.combination.mulAction_faithful
Proof state before:
case h.right
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑(succ n) ≤ PartENat.card α
g : G
hg : toPerm g ≠ 1
a : α
ha : g • a ≠ a
this : {a} ⊆ {g • a}ᶜ
hα' : ↑n ≤ Set.encard {g • a}ᶜ
s : Set α
hs : Set.encard s = ↑n
has : a ∈ s
has' : g • a ∉ s
⊢ a ∈ s ∧ g • a ∉ s
Tactic:
exact ⟨has, has'⟩
Proof state after:
no goals
Theorem: Finset.exists_fin_enum
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hsn : s.card = n
⊢ ∃ f, map f univ = s
Tactic:
have slc : s.toList.length = n := by rw [← hsn, Finset.length_toList]
Proof state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hsn : s.card = n
slc : List.length (toList s) = n
⊢ ∃ f, map f univ = s
Theorem: Finset.exists_fin_enum
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hsn : s.card = n
slc : List.length (toList s) = n
⊢ ∃ f, map f univ = s
Tactic:
use ⟨s.toList.get, by rw [← List.nodup_iff_injective_get]; exact Finset.nodup_toList s⟩
Proof state after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hsn : s.card = n
slc : List.length (toList s) = n
⊢ map { toFun := List.get (toList s), inj' := ⋯ } univ = s
Theorem: Finset.exists_fin_enum
Proof state before:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hsn : s.card = n
slc : List.length (toList s) = n
⊢ map { toFun := List.get (toList s), inj' := ⋯ } univ = s
Tactic:
ext  a
Proof state after:
case h.a
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hsn : s.card = n
slc : List.length (toList s) = n
a : α
⊢ a ∈ map { toFun := List.get (toList s), inj' := ⋯ } univ ↔ a ∈ s
Theorem: Finset.exists_fin_enum
Proof state before:
case h.a
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hsn : s.card = n
slc : List.length (toList s) = n
a : α
⊢ a ∈ map { toFun := List.get (toList s), inj' := ⋯ } univ ↔ a ∈ s
Tactic:
simp only [Finset.mem_map, Finset.mem_univ, true_and]
Proof state after:
case h.a
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hsn : s.card = n
slc : List.length (toList s) = n
a : α
⊢ (∃ a_1, { toFun := List.get (toList s), inj' := ⋯ } a_1 = a) ↔ a ∈ s
Theorem: Finset.exists_fin_enum
Proof state before:
case h.a
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hsn : s.card = n
slc : List.length (toList s) = n
a : α
⊢ (∃ a_1, { toFun := List.get (toList s), inj' := ⋯ } a_1 = a) ↔ a ∈ s
Tactic:
rw [← Finset.mem_toList, List.mem_iff_get]
Proof state after:
case h.a
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hsn : s.card = n
slc : List.length (toList s) = n
a : α
⊢ (∃ a_1, { toFun := List.get (toList s), inj' := ⋯ } a_1 = a) ↔ ∃ n, List.get (toList s) n = a
Theorem: Finset.exists_fin_enum
Proof state before:
case h.a
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hsn : s.card = n
slc : List.length (toList s) = n
a : α
⊢ (∃ a_1, { toFun := List.get (toList s), inj' := ⋯ } a_1 = a) ↔ ∃ n, List.get (toList s) n = a
Tactic:
rfl
Proof state after:
no goals
Theorem: Finset.exists_fin_enum
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hsn : s.card = n
⊢ List.length (toList s) = n
Tactic:
rw [← hsn, Finset.length_toList]
Proof state after:
no goals
Theorem: Finset.exists_fin_enum
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hsn : s.card = n
slc : List.length (toList s) = n
⊢ Function.Injective (List.get (toList s))
Tactic:
rw [← List.nodup_iff_injective_get]
Proof state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hsn : s.card = n
slc : List.length (toList s) = n
⊢ List.Nodup (toList s)
Theorem: Finset.exists_fin_enum
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hsn : s.card = n
slc : List.length (toList s) = n
⊢ List.Nodup (toList s)
Tactic:
exact Finset.nodup_toList s
Proof state after:
no goals
Theorem: EmbeddingToFinset.map_surjective
Proof state before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
⊢ Function.Surjective ⇑(map G α n)
Tactic:
rintro ⟨s, hs⟩
Proof state after:
case mk
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hs : s ∈ Nat.Combination α n
⊢ ∃ a, (map G α n) a = { val := s, property := hs }
Theorem: EmbeddingToFinset.map_surjective
Proof state before:
case mk
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hs : s ∈ Nat.Combination α n
⊢ ∃ a, (map G α n) a = { val := s, property := hs }
Tactic:
rw [Nat.Combination.mem_iff] at hs
Proof state after:
case mk
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hs✝ : s ∈ Nat.Combination α n
hs : s.card = n
⊢ ∃ a, (map G α n) a = { val := s, property := hs✝ }
Theorem: EmbeddingToFinset.map_surjective
Proof state before:
case mk
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hs✝ : s ∈ Nat.Combination α n
hs : s.card = n
⊢ ∃ a, (map G α n) a = { val := s, property := hs✝ }
Tactic:
obtain ⟨f, hf⟩ := s.exists_fin_enum α hs
Proof state after:
case mk.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hs✝ : s ∈ Nat.Combination α n
hs : s.card = n
f : Fin n ↪ α
hf : Finset.map f Finset.univ = s
⊢ ∃ a, (map G α n) a = { val := s, property := hs✝ }
Theorem: EmbeddingToFinset.map_surjective
Proof state before:
case mk.intro
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hs✝ : s ∈ Nat.Combination α n
hs : s.card = n
f : Fin n ↪ α
hf : Finset.map f Finset.univ = s
⊢ ∃ a, (map G α n) a = { val := s, property := hs✝ }
Tactic:
use { toFun := f, inj' := f.injective }
Proof state after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hs✝ : s ∈ Nat.Combination α n
hs : s.card = n
f : Fin n ↪ α
hf : Finset.map f Finset.univ = s
⊢ (map G α n) { toFun := ⇑f, inj' := ⋯ } = { val := s, property := hs✝ }
Theorem: EmbeddingToFinset.map_surjective
Proof state before:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hs✝ : s ∈ Nat.Combination α n
hs : s.card = n
f : Fin n ↪ α
hf : Finset.map f Finset.univ = s
⊢ (map G α n) { toFun := ⇑f, inj' := ⋯ } = { val := s, property := hs✝ }
Tactic:
simp only [Function.Embedding.mk_coe, Nat.Combination.eq_iff]
Proof state after:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hs✝ : s ∈ Nat.Combination α n
hs : s.card = n
f : Fin n ↪ α
hf : Finset.map f Finset.univ = s
⊢ ↑((map G α n) f) = s
Theorem: EmbeddingToFinset.map_surjective
Proof state before:
case h
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s : Finset α
hs✝ : s ∈ Nat.Combination α n
hs : s.card = n
f : Fin n ↪ α
hf : Finset.map f Finset.univ = s
⊢ ↑((map G α n) f) = s
Tactic:
exact hf
Proof state after:
no goals
Theorem: Nat.Combination_nontrivial
Proof state before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
⊢ Nontrivial ↑(Combination α n)
Tactic:
suffices Nonempty (n.Combination α) by
  obtain ⟨s, hs⟩ := this
  change s.card = n at hs
  let h'1 := id h1
  rw [← hs, Finset.card_pos] at h'1 ; obtain ⟨a, ha⟩ := h'1
  let h'2 := id h2
  rw [← hs, Finset.card_lt_iff_ne_univ, Ne.def, ← Finset.coe_eq_univ, ← Ne.def,
  Set.ne_univ_iff_exists_not_mem] at h'2
  obtain ⟨b, hb⟩ := h'2
  let t : Finset α := insert b (Finset.erase s a)
  rw [nontrivial_iff]
  use ⟨s, hs⟩
  use ⟨t, by
    rw [Nat.Combination.mem_iff]
    rw [Finset.card_insert_of_not_mem]
    rw [Finset.card_erase_of_mem ha]
    rw [hs]; rw [Nat.sub_add_cancel]; exact h1
    intro h; apply hb; apply Finset.erase_subset; exact h⟩
  intro h
  rw [Subtype.mk_eq_mk] at h
  apply hb
  rw [h]
  exact Finset.mem_insert_self b _
Proof state after:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
⊢ Nonempty ↑(Combination α n)
Theorem: Nat.Combination_nontrivial
Proof state before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
⊢ Nonempty ↑(Combination α n)
Tactic:
obtain ⟨s, _, hs'⟩ := Finset.exists_smaller_set (Finset.univ : Finset α) n
  (le_of_lt h2)
Proof state after:
case intro.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
left✝ : s ⊆ Finset.univ
hs' : s.card = n
⊢ Nonempty ↑(Combination α n)
Theorem: Nat.Combination_nontrivial
Proof state before:
case intro.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
left✝ : s ⊆ Finset.univ
hs' : s.card = n
⊢ Nonempty ↑(Combination α n)
Tactic:
use s
Proof state after:
case property
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
left✝ : s ⊆ Finset.univ
hs' : s.card = n
⊢ s ∈ Combination α n
Theorem: Nat.Combination_nontrivial
Proof state before:
case property
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
left✝ : s ⊆ Finset.univ
hs' : s.card = n
⊢ s ∈ Combination α n
Tactic:
exact hs'
Proof state after:
no goals
Theorem: Nat.Combination_nontrivial
Proof state before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
this : Nonempty ↑(Combination α n)
⊢ Nontrivial ↑(Combination α n)
Tactic:
obtain ⟨s, hs⟩ := this
Proof state after:
case intro.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s ∈ Combination α n
⊢ Nontrivial ↑(Combination α n)
Theorem: Nat.Combination_nontrivial
Proof state before:
case intro.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s ∈ Combination α n
⊢ Nontrivial ↑(Combination α n)
Tactic:
change s.card = n at hs
Proof state after:
case intro.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
⊢ Nontrivial ↑(Combination α n)
Theorem: Nat.Combination_nontrivial
Proof state before:
case intro.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
⊢ Nontrivial ↑(Combination α n)
Tactic:
let h'1 := id h1
Proof state after:
case intro.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
h'1 : 0 < n := id h1
⊢ Nontrivial ↑(Combination α n)
Theorem: Nat.Combination_nontrivial
Proof state before:
case intro.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
h'1 : 0 < n := id h1
⊢ Nontrivial ↑(Combination α n)
Tactic:
rw [← hs, Finset.card_pos] at h'1
Proof state after:
case intro.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
h'1 : s.Nonempty
⊢ Nontrivial ↑(Combination α n)
Theorem: Nat.Combination_nontrivial
Proof state before:
case intro.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
h'1 : s.Nonempty
⊢ Nontrivial ↑(Combination α n)
Tactic:
obtain ⟨a, ha⟩ := h'1
Proof state after:
case intro.mk.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
⊢ Nontrivial ↑(Combination α n)
Theorem: Nat.Combination_nontrivial
Proof state before:
case intro.mk.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
⊢ Nontrivial ↑(Combination α n)
Tactic:
let h'2 := id h2
Proof state after:
case intro.mk.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
h'2 : n < Fintype.card α := id h2
⊢ Nontrivial ↑(Combination α n)
Theorem: Nat.Combination_nontrivial
Proof state before:
case intro.mk.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
h'2 : n < Fintype.card α := id h2
⊢ Nontrivial ↑(Combination α n)
Tactic:
rw [← hs, Finset.card_lt_iff_ne_univ, Ne.def, ← Finset.coe_eq_univ, ← Ne.def,
Set.ne_univ_iff_exists_not_mem] at h'2
Proof state after:
case intro.mk.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
h1 : 0 < n
h2 : n < Fintype.card α
s : Finset α
hs : s.card = n
a : α
ha : a ∈ s
h'2 : ∃ a, a ∉ ↑s
⊢ Nontrivial ↑(Combination α n)