-- 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
this✝ : ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l
this : f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f
⊢ f ∈ permsOfList (a :: l)

Tactic:
simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_flatMap]

Result:
no goals

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 l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f

Tactic:
refine or_iff_not_imp_left.2 fun _hfl => ⟨f a, ?_, Equiv.swap a (f a) * f, IH this, ?_⟩

Result:
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

case neg.refine_2
α : 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
⊢ Equiv.swap a (f a) * (Equiv.swap a (f a) * f) = f

Proof state:
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

Tactic:
exact hx hfa

Result:
no goals

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
⊢ f ∈ permsOfList (a :: l)

Tactic:
have hfa' : f (f a) ≠ f a := mt (fun h => f.injective h) hfa

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
⊢ f ∈ permsOfList (a :: l)

Proof state:
case neg.refine_2
α : 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
⊢ Equiv.swap a (f a) * (Equiv.swap a (f a) * f) = f

Tactic:
rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul]

Result:
no goals

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
⊢ f ∈ permsOfList (a :: l)

Tactic:
have : ∀ x : α, (Equiv.swap a (f a) * f) x ≠ x → x ∈ l := by
  intro x hx
  have hxa : x ≠ a := by
    rintro rfl
    apply hx
    simp only [mul_apply, swap_apply_right]
  refine List.mem_of_ne_of_mem hxa (h x fun h => ?_)
  simp only [mul_apply, swap_apply_def, mul_apply, Ne, apply_eq_iff_eq] at hx
  split_ifs at hx with h_1
  exacts [hxa (h.symm.trans h_1), hx h]

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 (a :: l)

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → False
⊢ f ∈ permsOfList []

Tactic:
exact List.mem_singleton.2 (Equiv.ext fun x => Decidable.byContradiction <| h x)

Result:
no goals

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
hfa' : f (f a) ≠ f a
x : α
hxa : x ≠ a
h : f x = x
h_1 : f x = a
hx : ¬f a = x
⊢ False

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
x : α
hxa : x ≠ a
h : f x = x
h_1 : ¬f x = a
hx : ¬f x = x
⊢ False

Tactic:
exacts [hxa (h.symm.trans h_1), hx h]

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 : α
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

Tactic:
split_ifs at hx with h_1

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
hfa' : f (f a) ≠ f a
x : α
hxa : x ≠ a
h : f x = x
h_1 : f x = a
hx : ¬f a = x
⊢ False

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
x : α
hxa : x ≠ a
h : f x = x
h_1 : ¬f x = a
hx : ¬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
hxa : x ≠ a
⊢ x ∈ l

Tactic:
refine List.mem_of_ne_of_mem hxa (h x fun h => ?_)

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
h : f x = x
⊢ False

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ []
⊢ f ∈ permsOfList []

Tactic:
simp only [not_mem_nil] at h

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → False
⊢ f ∈ permsOfList []

Proof state:
α : 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
⊢ (Equiv.swap x (f x) * f) x = x

Tactic:
simp only [mul_apply, swap_apply_right]

Result:
no goals

Proof state:
α : 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

Tactic:
apply hx

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
⊢ (Equiv.swap x (f x) * f) x = x