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

State before:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
⊢ support' f ≠ {a}
Tactic:
intro h
State after:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
h : support' f = {a}
⊢ False

State before:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
h : support' f = {a}
⊢ False
Tactic:
simp only [Set.ext_iff, mem_support', ne_eq, mem_singleton_iff] at h
State after:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
h : ∀ (x : α), ¬f x = x ↔ x = a
⊢ False

State before:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
h : ∀ (x : α), ¬f x = x ↔ x = a
⊢ False
Tactic:
specialize h (f.symm a)
State after:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
h : ¬f (f.symm a) = f.symm a ↔ f.symm a = a
⊢ False

State before:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
h : ¬f (f.symm a) = f.symm a ↔ f.symm a = a
⊢ False
Tactic:
rw [eq_comm] at h
State after:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
h : ¬f.symm a = f (f.symm a) ↔ f.symm a = a
⊢ False

State before:
α : Type u_1
x y : α
f✝ f : Perm α
a : α
h : ¬f.symm a = f (f.symm a) ↔ f.symm a = a
⊢ False
Tactic:
simp only [apply_symm_apply, not_iff_self] at h
State after:
no goals