Theorem: Equiv.Perm.support'_eq_empty (Bruhat/Perm.lean)

State before:
α : Type u_1
x y : α
f✝ f : Perm α
⊢ support' f = ∅ ↔ f = 1
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.symm ▸ support'_one α⟩
State after:
α : Type u_1
x y : α
f✝ f : Perm α
h : support' f = ∅
⊢ f = 1

State before:
α : Type u_1
x y : α
f✝ f : Perm α
h : support' f = ∅
⊢ f = 1
Tactic:
ext x
State after:
case H
α : Type u_1
x✝ y : α
f✝ f : Perm α
h : support' f = ∅
x : α
⊢ f x = 1 x

State before:
case H
α : Type u_1
x✝ y : α
f✝ f : Perm α
h : support' f = ∅
x : α
⊢ f x = 1 x
Tactic:
simp only [support', ne_eq, eq_empty_iff_forall_not_mem, mem_setOf_eq, not_not] at h
State after:
case H
α : Type u_1
x✝ y : α
f✝ f : Perm α
x : α
h : ∀ (x : α), f x = x
⊢ f x = 1 x

State before:
case H
α : Type u_1
x✝ y : α
f✝ f : Perm α
x : α
h : ∀ (x : α), f x = x
⊢ f x = 1 x
Tactic:
exact h x
State after:
no goals