Theorem: Nat.combination.smul_ne_iff_hasMem_not_mem (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)
g : G
⊢ g • s ≠ t ↔ ∃ a ∈ ↑s, a ∉ g⁻¹ • ↑t
Tactic:
simp only [ne_eq, exists_prop]
State after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ ¬g • s = t ↔ ∃ a ∈ ↑s, a ∉ g⁻¹ • ↑t

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ ¬g • s = t ↔ ∃ a ∈ ↑s, a ∉ g⁻¹ • ↑t
Tactic:
rw [← Finset.not_subset]
State after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ ¬g • s = t ↔ ¬↑s ⊆ g⁻¹ • ↑t

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ ¬g • s = t ↔ ¬↑s ⊆ g⁻¹ • ↑t
Tactic:
rw [not_iff_not]
State after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ g • s = t ↔ ↑s ⊆ g⁻¹ • ↑t

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ g • s = t ↔ ↑s ⊆ g⁻¹ • ↑t
Tactic:
rw [← Nat.combination_mulAction.coe_apply']
State after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ g • s = t ↔ ↑s ⊆ ↑(g⁻¹ • t)

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ g • s = t ↔ ↑s ⊆ ↑(g⁻¹ • t)
Tactic:
rw [Nat.Combination.eq_iff_finset_subset]
State after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ ↑(g • s) ⊆ ↑t ↔ ↑s ⊆ ↑(g⁻¹ • t)

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ ↑(g • s) ⊆ ↑t ↔ ↑s ⊆ ↑(g⁻¹ • t)
Tactic:
simp only [Nat.combination_mulAction.coe_apply', Finset.le_eq_subset]
State after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ g • ↑s ⊆ ↑t ↔ ↑s ⊆ g⁻¹ • ↑t

State before:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction G α
n : ℕ
s t : ↑(Combination α n)
g : G
⊢ g • ↑s ⊆ ↑t ↔ ↑s ⊆ g⁻¹ • ↑t
Tactic:
exact Finset.smul_finset_subset_iff
State after:
no goals