Theorem: Equiv.Perm.exists_ne_of_mem_support' (Bruhat/Perm.lean)

State before:
α : Type u_1
x y : α
f : Perm α
a : α
ha : a ∈ support' f
⊢ ∃ b ∈ support' f, b ≠ a
Tactic:
refine by_contra <| fun h ↦ support'_ne_singleton f a ?_
State after:
α : Type u_1
x y : α
f : Perm α
a : α
ha : a ∈ support' f
h : ¬∃ b ∈ support' f, b ≠ a
⊢ support' f = {a}

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

State before:
α : Type u_1
x y : α
f : Perm α
a : α
ha : a ∈ support' f
h : ¬∃ b ∈ support' f, b ≠ a
⊢ ∀ (x : α), ¬f x = x ↔ x = a
Tactic:
simp only [mem_support', ne_eq, not_exists, not_and, not_not] at h
State after:
α : Type u_1
x y : α
f : Perm α
a : α
ha : a ∈ support' f
h : ∀ (x : α), ¬f x = x → x = a
⊢ ∀ (x : α), ¬f x = x ↔ x = a

State before:
α : Type u_1
x y : α
f : Perm α
a : α
ha : a ∈ support' f
h : ∀ (x : α), ¬f x = x → x = a
⊢ ∀ (x : α), ¬f x = x ↔ x = a
Tactic:
refine fun x ↦ ⟨fun h' ↦ h _ h', ?_⟩
State after:
α : Type u_1
x✝ y : α
f : Perm α
a : α
ha : a ∈ support' f
h : ∀ (x : α), ¬f x = x → x = a
x : α
⊢ x = a → ¬f x = x

State before:
α : Type u_1
x✝ y : α
f : Perm α
a : α
ha : a ∈ support' f
h : ∀ (x : α), ¬f x = x → x = a
x : α
⊢ x = a → ¬f x = x
Tactic:
rintro rfl
State after:
α : Type u_1
x✝ y : α
f : Perm α
x : α
ha : x ∈ support' f
h : ∀ (x_1 : α), ¬f x_1 = x_1 → x_1 = x
⊢ ¬f x = x

State before:
α : Type u_1
x✝ y : α
f : Perm α
x : α
ha : x ∈ support' f
h : ∀ (x_1 : α), ¬f x_1 = x_1 → x_1 = x
⊢ ¬f x = x
Tactic:
exact ha
State after:
no goals