-- Mathlib/Data/Fintype/Perm.lean
theorem mem_permsOfList_of_mem {l : List α} {f : Perm α} (h : ∀ x, f x ≠ x → x ∈ l) :
    f ∈ permsOfList l

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h✝ : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
x : α
hx : (Equiv.swap a (f a) * f) x ≠ x
hxa : x ≠ a
h : f x = x
⊢ False

Tactic:
simp only [mul_apply, swap_apply_def, mul_apply, Ne, apply_eq_iff_eq] at hx

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h✝ : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
x : α
hxa : x ≠ a
h : f x = x
hx : ¬(if f x = a then f a else if x = a then a else f x) = x
⊢ False

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
x : α
hx : (Equiv.swap a (f a) * f) x ≠ x
⊢ x ≠ a

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝ : DecidableEq α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
x : α
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfa : ¬f x = x
hfa' : f (f x) ≠ f x
hx : (Equiv.swap x (f x) * f) x ≠ x
⊢ False

Proof state:
case neg.refine_1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
this : ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
⊢ f a ∈ l

Tactic:
exact mem_of_ne_of_mem hfa (h _ hfa')

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
x : α
hx : (Equiv.swap a (f a) * f) x ≠ x
⊢ x ∈ l

Tactic:
have hxa : x ≠ a := by
  rintro rfl
  apply hx
  simp only [mul_apply, swap_apply_right]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
x : α
hx : (Equiv.swap a (f a) * f) x ≠ x
hxa : x ≠ a
⊢ x ∈ l

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : f a = a
⊢ f ∈ permsOfList (a :: l)

Tactic:
refine mem_append_left _ (IH fun x hx => mem_of_ne_of_mem ?_ (h x hx))

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : f a = a
x : α
hx : f x ≠ x
⊢ x ≠ a

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
⊢ ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l

Tactic:
intro x hx

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
x : α
hx : (Equiv.swap a (f a) * f) x ≠ x
⊢ x ∈ l

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
⊢ f ∈ permsOfList (a :: l)

Tactic:
by_cases hfa : f a = a

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : f a = a
⊢ f ∈ permsOfList (a :: l)

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
⊢ f ∈ permsOfList (a :: l)

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : f a = a
x : α
hx : f x ≠ x
⊢ x ≠ a

Tactic:
rintro rfl

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
x : α
hx : f x ≠ x
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfa : f x = x
⊢ False

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
this : ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l
⊢ f ∈ permsOfList (a :: l)

Tactic:
suffices f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f by
  simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_flatMap]

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
this : ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l
⊢ f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f