Theorem: Nat.bijective_toCombination_one_equivariant (Jordan/MulActionCombination.lean)

State before:
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
⊢ Function.Bijective ⇑(toCombination_one_equivariant G α)
Tactic:
constructor
State after:
case left
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
⊢ Function.Injective ⇑(toCombination_one_equivariant G α)

case right
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
⊢ Function.Surjective ⇑(toCombination_one_equivariant G α)

State before:
case left
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
⊢ Function.Injective ⇑(toCombination_one_equivariant G α)
Tactic:
intro a b h
State after:
case left
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
a b : α
h : (toCombination_one_equivariant G α) a = (toCombination_one_equivariant G α) b
⊢ a = b

State before:
case left
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
a b : α
h : (toCombination_one_equivariant G α) a = (toCombination_one_equivariant G α) b
⊢ a = b
Tactic:
simp only [toCombination_one_equivariant, Combination.eq_iff] at h
State after:
case left
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
a b : α
h :
  ↑({ toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } a) =
    ↑({ toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } b)
⊢ a = b

State before:
case left
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
a b : α
h :
  ↑({ toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } a) =
    ↑({ toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } b)
⊢ a = b
Tactic:
apply Finset.singleton_injective
State after:
case left.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
a b : α
h :
  ↑({ toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } a) =
    ↑({ toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } b)
⊢ {a} = {b}

State before:
case left.a
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
a b : α
h :
  ↑({ toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } a) =
    ↑({ toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } b)
⊢ {a} = {b}
Tactic:
exact h
State after:
no goals

State before:
case right
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
⊢ Function.Surjective ⇑(toCombination_one_equivariant G α)
Tactic:
rintro ⟨s, hs⟩
State after:
case right.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs : s ∈ Combination α 1
⊢ ∃ a, (toCombination_one_equivariant G α) a = { val := s, property := hs }

State before:
case right.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs : s ∈ Combination α 1
⊢ ∃ a, (toCombination_one_equivariant G α) a = { val := s, property := hs }
Tactic:
simp [Nat.Combination.mem_iff, Finset.card_eq_one] at hs
State after:
case right.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs✝ : s ∈ Combination α 1
hs : ∃ a, s = {a}
⊢ ∃ a, (toCombination_one_equivariant G α) a = { val := s, property := hs✝ }

State before:
case right.mk
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs✝ : s ∈ Combination α 1
hs : ∃ a, s = {a}
⊢ ∃ a, (toCombination_one_equivariant G α) a = { val := s, property := hs✝ }
Tactic:
obtain ⟨a, ha⟩ := hs
State after:
case right.mk.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs : s ∈ Combination α 1
a : α
ha : s = {a}
⊢ ∃ a, (toCombination_one_equivariant G α) a = { val := s, property := hs }

State before:
case right.mk.intro
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs : s ∈ Combination α 1
a : α
ha : s = {a}
⊢ ∃ a, (toCombination_one_equivariant G α) a = { val := s, property := hs }
Tactic:
use a
State after:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs : s ∈ Combination α 1
a : α
ha : s = {a}
⊢ (toCombination_one_equivariant G α) a = { val := s, property := hs }

State before:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs : s ∈ Combination α 1
a : α
ha : s = {a}
⊢ (toCombination_one_equivariant G α) a = { val := s, property := hs }
Tactic:
simp only [toCombination_one_equivariant, ha]
State after:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs : s ∈ Combination α 1
a : α
ha : s = {a}
⊢ { toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } a = { val := {a}, property := ⋯ }

State before:
case h
G : Type u_1
inst✝³ : Group G
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : MulAction G α
n : ℕ
inst✝ : Fintype α
s : Finset α
hs : s ∈ Combination α 1
a : α
ha : s = {a}
⊢ { toFun := fun x => { val := {x}, property := ⋯ }, map_smul' := ⋯ } a = { val := {a}, property := ⋯ }
Tactic:
rfl
State after:
no goals