Theorem: Nat.Combination.eq_iff_finset_subset (Jordan/MulActionCombination.lean)

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
⊢ s = t ↔ ↑s ⊆ ↑t
Tactic:
constructor
State after:
case mp
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
⊢ s = t → ↑s ⊆ ↑t

case mpr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
⊢ ↑s ⊆ ↑t → s = t

State before:
case mp
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
⊢ s = t → ↑s ⊆ ↑t
Tactic:
intro h
State after:
case mp
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
h : s = t
⊢ ↑s ⊆ ↑t

State before:
case mp
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
h : s = t
⊢ ↑s ⊆ ↑t
Tactic:
rw [h]
State after:
no goals

State before:
case mpr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
⊢ ↑s ⊆ ↑t → s = t
Tactic:
intro h
State after:
case mpr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
h : ↑s ⊆ ↑t
⊢ s = t

State before:
case mpr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
h : ↑s ⊆ ↑t
⊢ s = t
Tactic:
rw [← Subtype.coe_inj]
State after:
case mpr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
h : ↑s ⊆ ↑t
⊢ ↑s = ↑t

State before:
case mpr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
h : ↑s ⊆ ↑t
⊢ ↑s = ↑t
Tactic:
apply Finset.eq_of_subset_of_card_le h
State after:
case mpr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
h : ↑s ⊆ ↑t
⊢ (↑t).card ≤ (↑s).card

State before:
case mpr
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
h : ↑s ⊆ ↑t
⊢ (↑t).card ≤ (↑s).card
Tactic:
rw [s.prop, t.prop]
State after:
no goals