Theorem: EmbeddingToFinset.map_surjective (Jordan/MulActionCombination.lean)

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

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

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

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

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

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