awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
x : α
hx : (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x
⊢ x ≠ a

Tactic:
have hxa : x ≠ a := by
      rintro rfl
      apply hx
      simp only [mul_apply, swap_apply_right]
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
x : α
hx : (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x
hxa : x ≠ a
⊢ x ∈ l

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

Premises used: List.mem_of_ne_of_mem
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
x : α
hx : (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x
hxa : x ≠ a
refine : ∀ (h : (f : (a : α) → α) x = x), False
⊢ x ∈ l

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

Premises used: List.mem_of_ne_of_mem
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h_1 : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
x : α
hx : (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x
hxa : x ≠ a
h : (f : (a : α) → α) x = x
⊢ ¬(if (f : (a : α) → α) x = a then (f : (a : α) → α) a else if x = a then a else (f : (a : α) → α) x) = x

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

Premises used: Equiv.swap_apply_def, Ne, Equiv.Perm.mul_apply, Equiv.apply_eq_iff_eq
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h_1 : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
x : α
hxa : x ≠ a
h : (f : (a : α) → α) x = x
hx : ¬(if (f : (a : α) → α) x = a then (f : (a : α) → α) a else if x = a then a else (f : (a : α) → α) x) = x
pos : ∀ (h_1 : (f : (a : α) → α) x = a) (hx : ¬(f : (a : α) → α) a = x), False
neg : ∀ (h_1 : ¬(f : (a : α) → α) x = a) (hx : ¬(f : (a : α) → α) x = x), False
⊢ False

Tactic:
split_ifs at hx with h_1
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h_2 : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
x : α
hxa : x ≠ a
h : (f : (a : α) → α) x = x
h_1 : (f : (a : α) → α) x = a
hx : ¬(f : (a : α) → α) a = x
⊢ False

Tactic:
hxa (h.symm.trans h_1)

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h_2 : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
x : α
hxa : x ≠ a
h : (f : (a : α) → α) x = x
h_1 : ¬(f : (a : α) → α) x = a
hx : ¬(f : (a : α) → α) x = x
⊢ False

Tactic:
hx h
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h_2 : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
x : α
hxa : x ≠ a
h : (f : (a : α) → α) x = x
h_1 : (f : (a : α) → α) x = a
hx : ¬(f : (a : α) → α) a = x
⊢ False

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

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
⊢ ∀ (x : α), (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x → x ∈ 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]
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
this_1 : ∀ (x : α), (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) 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]

Premises used: exists_prop, List.mem_append, List.mem_flatMap, permsOfList, List.mem_map
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
this : ∀ (x : α), (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x → x ∈ l
neg : f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f
⊢ 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]
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
this : ∀ (x : α), (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x → x ∈ l
⊢ f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f

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

Premises used: Iff.mpr, HMul.hMul, Equiv.swap, Classical.or_iff_not_imp_left, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
this : ∀ (x : α), (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x → x ∈ l
neg : ∀ (_hfl : f ∉ permsOfList l), Membership.mem (α := α) l ((f : (a : α) → α) a : α)
neg₁ : ∀ (_hfl : f ∉ permsOfList l), Equiv.swap a ((f : (a : α) → α) a) * (Equiv.swap a ((f : (a : α) → α) a) * f) = f
⊢ 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, ?_⟩

Premises used: Iff.mpr, Classical.or_iff_not_imp_left
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
this : ∀ (x : α), (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
⊢ Membership.mem (α := α) l ((f : (a : α) → α) a : α)

Tactic:
mem_of_ne_of_mem hfa (h _ hfa')

Premises used: List.mem_of_ne_of_mem
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
this : ∀ (x : α), (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
⊢ Membership.mem (α := α) l ((f : (a : α) → α) a : α)

Tactic:
exact mem_of_ne_of_mem hfa (h _ hfa')

Premises used: List.mem_of_ne_of_mem
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
this : ∀ (x : α), (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
neg : Equiv.swap a ((f : (a : α) → α) a) * Equiv.swap a ((f : (a : α) → α) a) * f = f
neg₁ : Equiv.trans (Equiv.swap a ((f : (a : α) → α) a)) (Equiv.swap a ((f : (a : α) → α) a)) * f = f
neg₂ : Equiv.refl α * f = f
neg₃ : 1 * f = f
neg₄ neg₅ : f = f
⊢ Equiv.swap a ((f : (a : α) → α) a) * (Equiv.swap a ((f : (a : α) → α) a) * f) = f

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

Premises used: Equiv.Perm.one_def, mul_assoc, Equiv.swap, Equiv.Perm.mul_def, DFunLike.coe, Equiv.swap_swap, one_mul
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l
nil :
  ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x),
    Membership.mem (γ := List (Equiv.Perm α)) (permsOfList []) f
cons :
  ∀ (a : α) (l : List α) (IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l)
    {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l), f ∈ permsOfList (a :: l)
⊢ f ∈ permsOfList l

Tactic:
induction l generalizing f with
  | nil =>
    simp only [not_mem_nil] at h
    exact List.mem_singleton.2 (Equiv.ext fun x => Decidable.byContradiction <| h x)
  | cons a l IH =>
  by_cases hfa : f a = a
  · refine mem_append_left _ (IH fun x hx => mem_of_ne_of_mem ?_ (h x hx))
    rintro rfl
    exact hx hfa
  have hfa' : f (f a) ≠ f a := mt (fun h => f.injective h) hfa
  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]
  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]
  refine or_iff_not_imp_left.2 fun _hfl => ⟨f a, ?_, Equiv.swap a (f a) * f, IH this, ?_⟩
  · exact mem_of_ne_of_mem hfa (h _ hfa')
  · rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul]

Premises used: Iff.mpr, Equiv.Perm.one_def, mul_assoc, Equiv.ext, List.mem_singleton, Classical.or_iff_not_imp_left, Decidable.byContradiction, List.not_mem_nil, Equiv.swap_swap, one_mul, rfl, List.nil
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
f : Equiv.Perm α
h : Membership.mem (γ := List (Equiv.Perm α)) (permsOfList []) f
heq_iff_eq : α
⊢ f = 1

Tactic:
simpa [permsOfList] using h

Premises used: permsOfList
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
f : Equiv.Perm α
h : Membership.mem (γ := List (Equiv.Perm α)) (permsOfList []) f
heq_iff_eq : α
⊢ f = 1

Tactic:
have : f = 1 := by simpa [permsOfList] using h
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
f : Equiv.Perm α
h : Membership.mem (γ := List (Equiv.Perm α)) (permsOfList []) f
heq_iff_eq : α
this : f = 1
rw : (1 : (a : α) → α) heq_iff_eq ≠ heq_iff_eq → Membership.mem (γ := List α) [] heq_iff_eq
⊢ (f : (a : α) → α) heq_iff_eq ≠ heq_iff_eq → Membership.mem (γ := List α) [] heq_iff_eq

Tactic:
rw [this]
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
f : Equiv.Perm α
h : Membership.mem (γ := List (Equiv.Perm α)) (permsOfList []) f
heq_iff_eq : α
this : f = 1
⊢ (1 : (a : α) → α) heq_iff_eq ≠ heq_iff_eq → Membership.mem (γ := List α) [] heq_iff_eq

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : x = a
⊢ x ∈ a :: l

Tactic:
simp [hxa]
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : x = y
rwa rwa₁ rwa₂ rwa₃ : y ∈ l
⊢ x ∈ l

Tactic:
rwa [hxy]
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
rw : (if (f : (a : α) → α) x = a then y else if (f : (a : α) → α) x = y then a else (f : (a : α) → α) x) ≠ x
⊢ (g : (a : α) → α) x ≠ x

Tactic:
rw [eq_inv_mul_iff_mul_eq.2 hg₂, mul_apply, swap_inv, swap_apply_def]

Premises used: Iff.mpr, Equiv.swap_apply_def, eq_inv_mul_iff_mul_eq, Equiv.swap_inv, Equiv.Perm.mul_apply
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
pos : (f : (a : α) → α) x = a → y ≠ x
pos₁ : ¬(f : (a : α) → α) x = a → (f : (a : α) → α) x = y → a ≠ x
neg : ¬(f : (a : α) → α) x = a → ¬(f : (a : α) → α) x = y → (f : (a : α) → α) x ≠ x
⊢ (if (f : (a : α) → α) x = a then y else if (f : (a : α) → α) x = y then a else (f : (a : α) → α) x) ≠ x

Tactic:
split_ifs
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
h_2 : (f : (a : α) → α) x = a
⊢ y ≠ x

Tactic:
Ne.symm hxy

Premises used: Ne.symm
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
h_2 : (f : (a : α) → α) x = a
⊢ y ≠ x

Tactic:
exact Ne.symm hxy

Premises used: Ne.symm
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
h_2 : ¬(f : (a : α) → α) x = a
h_3 : (f : (a : α) → α) x = y
⊢ a ≠ x

Tactic:
Ne.symm hxa

Premises used: Ne.symm
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
h_2 : ¬(f : (a : α) → α) x = a
h_3 : (f : (a : α) → α) x = y
⊢ a ≠ x

Tactic:
exact Ne.symm hxa

Premises used: Ne.symm
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
h_2 : ¬(f : (a : α) → α) x = a
h_3 : ¬(f : (a : α) → α) x = y
⊢ (f : (a : α) → α) x ≠ x

Tactic:
hx
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
h_2 : ¬(f : (a : α) → α) x = a
h_3 : ¬(f : (a : α) → α) x = y
⊢ (f : (a : α) → α) x ≠ x

Tactic:
exact hx
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
neg : ¬(f : (a : α) → α) x = a → (if (f : (a : α) → α) x = y then a else (f : (a : α) → α) x) ≠ x
pos : (f : (a : α) → α) x = a → y ≠ x
pos₁ : ¬(f : (a : α) → α) x = a → (f : (a : α) → α) x = y → a ≠ x
neg₁ : ¬(f : (a : α) → α) x = a → ¬(f : (a : α) → α) x = y → (f : (a : α) → α) x ≠ x
pos₂ : (f : (a : α) → α) x = a → y ≠ x
pos₃ : ¬(f : (a : α) → α) x = a → (f : (a : α) → α) x = y → a ≠ x
neg₂ : ¬(f : (a : α) → α) x = a → ¬(f : (a : α) → α) x = y → (f : (a : α) → α) x ≠ x
⊢ (if (f : (a : α) → α) x = a then y else if (f : (a : α) → α) x = y then a else (f : (a : α) → α) x) ≠ x

Tactic:
split_ifs <;> [exact Ne.symm hxy; exact Ne.symm hxa; exact hx]

Premises used: Ne.symm
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
f : Equiv.Perm α
⊢ f ∈ permsOfList l ↔ ∀ {x : α}, (f : (a : α) → α) x ≠ x → x ∈ l

Tactic:
⟨mem_of_mem_permsOfList, mem_permsOfList_of_mem⟩

Premises used: Iff.intro, mem_permsOfList_of_mem, mem_of_mem_permsOfList
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
h : Nodup.{u_1} (α := α) []
⊢ Nodup.{u_1} (α := Equiv.Perm α) (permsOfList [])

Tactic:
simp [permsOfList]

Premises used: permsOfList
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
⊢ l.Nodup

Tactic:
have hl' : l.Nodup := hl.of_cons
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
⊢ (permsOfList l).Nodup

Tactic:
have hln' : (permsOfList l).Nodup := nodup_permsOfList hl'
-- Module: Mathlib.Data.Fintype.Perm
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
⊢ ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → (f : (a : α) → α) a = a

Tactic:
have hmeml : ∀ {f : Perm α}, f ∈ permsOfList l → f a = a := fun {f} hf =>
      not_not.1 (mt (mem_of_mem_permsOfList hf) (nodup_cons.1 hl).1)