Theorem: Finset.exists_fin_enum (Jordan/MulActionCombination.lean)

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]
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

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⟩
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

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
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

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]
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

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]
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

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
State after:
no goals

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]
State after:
no goals

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]
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)

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
State after:
no goals