Theorem: Equiv.Perm.isInvariant_of_support_le (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : support c ≤ s
x : α
⊢ x ∈ s ↔ c x ∈ s
Tactic:
by_cases hx' : x ∈ c.support
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : support c ≤ s
x : α
hx' : x ∈ support c
⊢ x ∈ s ↔ c x ∈ s

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : support c ≤ s
x : α
hx' : x ∉ support c
⊢ x ∈ s ↔ c x ∈ s

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : support c ≤ s
x : α
hx' : x ∉ support c
⊢ x ∈ s ↔ c x ∈ s
Tactic:
rw [Equiv.Perm.not_mem_support.mp hx']
State after:
no goals

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : support c ≤ s
x : α
hx' : x ∈ support c
⊢ x ∈ s ↔ c x ∈ s
Tactic:
simp only [hcs hx', true_iff_iff]
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : support c ≤ s
x : α
hx' : x ∈ support c
⊢ c x ∈ s

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : support c ≤ s
x : α
hx' : x ∈ support c
⊢ c x ∈ s
Tactic:
exact hcs (Equiv.Perm.apply_mem_support.mpr hx')
State after:
no goals