Theorem: support_inv (Bruhat/Word.lean)

State before:
α : Type u_1
f : Equiv.Perm α
⊢ support f = support f⁻¹
Tactic:
ext a
State after:
case h
α : Type u_1
f : Equiv.Perm α
a : α
⊢ a ∈ support f ↔ a ∈ support f⁻¹

State before:
case h
α : Type u_1
f : Equiv.Perm α
a : α
⊢ a ∈ support f ↔ a ∈ support f⁻¹
Tactic:
simp [support, not_iff_not]
State after:
case h
α : Type u_1
f : Equiv.Perm α
a : α
⊢ f a = a ↔ f⁻¹ a = a

State before:
case h
α : Type u_1
f : Equiv.Perm α
a : α
⊢ f a = a ↔ f⁻¹ a = a
Tactic:
rw [← Equiv.Perm.eq_inv_iff_eq, eq_comm]
State after:
no goals