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

State before:
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
⊢ swap x x = refl
Tactic:
apply coe_inj
State after:
case h
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
⊢ (swap x x).toPerm = refl.toPerm

State before:
case h
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
⊢ (swap x x).toPerm = refl.toPerm
Tactic:
simp only [swap_toPerm, Equiv.swap_self, refl_toPerm]
State after:
case h
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
⊢ Equiv.refl α = 1

State before:
case h
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
⊢ Equiv.refl α = 1
Tactic:
rfl
State after:
no goals