-- Mathlib/Data/Fintype/Perm.lean
theorem nodup_permsOfList : ∀ {l : List α}, l.Nodup → (permsOfList l).Nodup
  | [], _ => by simp [permsOfList]
  | a :: l, hl => by
    have hl' : l.Nodup := hl.of_cons
    have hln' : (permsOfList l).Nodup := nodup_permsOfList hl'
    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)
    rw [permsOfList, List.nodup_append, List.nodup_flatMap, pairwise_iff_getElem]
    refine ⟨?_, ⟨⟨?_,?_ ⟩, ?_⟩⟩
    · exact hln'
    · exact fun _ _ => hln'.map fun _ _ => mul_left_cancel
    · intros i j hi hj hij x hx₁ hx₂
      let ⟨f, hf⟩ := List.mem_map.1 hx₁
      let ⟨g, hg⟩ := List.mem_map.1 hx₂
      have hix : x a = l[i]

Proof state:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ (fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)) l[i]
hx₂ : x ∈ (fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)) l[j]
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a l[i] * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a l[j] * g = x
hix : x a = l[i]
hiy : x a = l[j]
⊢ False

Tactic:
have hieqj : i = j := hl'.getElem_inj_iff.1 (hix.symm.trans hiy)

Result:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ (fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)) l[i]
hx₂ : x ∈ (fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)) l[j]
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a l[i] * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a l[j] * g = x
hix : x a = l[i]
hiy : x a = l[j]
hieqj : i = j
⊢ False

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ (fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)) l[i]
hx₂ : x ∈ (fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)) l[j]
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a l[i] * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a l[j] * g = x
hix : x a = l[i]
⊢ x a = l[j]

Tactic:
rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ (permsOfList l).Nodup ∧
    ((∀ x ∈ l, (List.map (fun f => Equiv.swap a x * f) (permsOfList l)).Nodup) ∧
        ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length),
          i < j → (List.Disjoint on fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)) l[i] l[j]) ∧
      (permsOfList l).Disjoint (flatMap (fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)) l)

Tactic:
refine ⟨?_, ⟨⟨?_,?_ ⟩, ?_⟩⟩

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ (permsOfList l).Nodup

case refine_2
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ ∀ x ∈ l, (List.map (fun f => Equiv.swap a x * f) (permsOfList l)).Nodup

case refine_3
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length),
    i < j → (List.Disjoint on fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)) l[i] l[j]

case refine_4
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ (permsOfList l).Disjoint (flatMap (fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)) l)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
⊢ (permsOfList (a :: l)).Nodup

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)

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ (permsOfList (a :: l)).Nodup

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ ∀ x ∈ l, (List.map (fun f => Equiv.swap a x * f) (permsOfList l)).Nodup

Tactic:
exact fun _ _ => hln'.map fun _ _ => mul_left_cancel

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ (permsOfList (a :: l)).Nodup

Tactic:
rw [permsOfList, List.nodup_append, List.nodup_flatMap, pairwise_iff_getElem]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ (permsOfList l).Nodup ∧
    ((∀ x ∈ l, (List.map (fun f => Equiv.swap a x * f) (permsOfList l)).Nodup) ∧
        ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length),
          i < j → (List.Disjoint on fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)) l[i] l[j]) ∧
      (permsOfList l).Disjoint (flatMap (fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)) l)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ flatMap (fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)) l
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
⊢ f (g⁻¹ x) = f a

Tactic:
rw [hmeml hf₁, ← hg.2]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ flatMap (fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)) l
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
⊢ (Equiv.swap a x * g) (g⁻¹ x) = a

Proof state:
case refine_4
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ flatMap (fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)) l
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
hgxa : g⁻¹ x = a
hxa : x ≠ a
⊢ False

Tactic:
exact (List.nodup_cons.1 hl).1 <|
    hgxa ▸ mem_of_mem_permsOfList hg.1 _ (by rwa [apply_inv_self, hgxa])

Result:
no goals