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

State before:
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
⊢ swapsAt x t ⊆ swapsOf (insert x t)
Tactic:
rintro s ⟨i, hi, rfl⟩
State after:
case intro.intro
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
i : α
hi : i ∈ t \ {x}
⊢ (fun x_1 => swap x x_1) i ∈ swapsOf (insert x t)

State before:
case intro.intro
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
i : α
hi : i ∈ t \ {x}
⊢ (fun x_1 => swap x x_1) i ∈ swapsOf (insert x t)
Tactic:
exact ⟨x, _, Or.inl rfl, Or.inr hi.1, Ne.symm hi.2, rfl⟩
State after:
no goals