Theorem: support_empty_iff_id (Bruhat/Word.lean)

State before:
α : Type u_1
f : Equiv.Perm α
⊢ support f = ∅ ↔ f = 1
Tactic:
simp only [Set.eq_empty_iff_forall_not_mem, support,
            ne_eq, Set.mem_setOf_eq, not_not]
State after:
α : Type u_1
f : Equiv.Perm α
⊢ (∀ (x : α), f x = x) ↔ f = 1

State before:
α : Type u_1
f : Equiv.Perm α
⊢ (∀ (x : α), f x = x) ↔ f = 1
Tactic:
exact Iff.symm Equiv.ext_iff
State after:
no goals