Theorem: Finperm.swapsOf_support_subset (Bruhat/Finperm.lean)

State before:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
t : Set α
hf : f ∈ swapsOf t
⊢ ↑f.support ⊆ t
Tactic:
obtain ⟨i,j, hi, hj, hne, rfl⟩ := hf
State after:
case intro.intro.intro.intro.intro
α : Type u_1
x y : α
g : Finperm α
inst✝ : DecidableEq α
t : Set α
i j : α
hi : i ∈ t
hj : j ∈ t
hne : i ≠ j
⊢ ↑(swap i j).support ⊆ t

State before:
case intro.intro.intro.intro.intro
α : Type u_1
x y : α
g : Finperm α
inst✝ : DecidableEq α
t : Set α
i j : α
hi : i ∈ t
hj : j ∈ t
hne : i ≠ j
⊢ ↑(swap i j).support ⊆ t
Tactic:
rwa [swap_support_of_ne hne, coe_insert, Set.insert_subset_iff, coe_singleton,
  Set.singleton_subset_iff, and_iff_right hi]
State after:
no goals