no goals
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x✝ : Nodup []
⊢ Nodup (permsOfList [])
simp [permsOfList]
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
⊢ Nodup (permsOfList (a :: l))
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
⊢ Nodup (permsOfList (a :: l))
have hl' : l.Nodup := hl.of_cons
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
⊢ Nodup (permsOfList (a :: l))
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
⊢ Nodup (permsOfList (a :: l))
have hln' : (permsOfList l).Nodup := nodup_permsOfList hl'
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ Nodup (permsOfList (a :: l))
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
⊢ Nodup (permsOfList (a :: l))
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)
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ Nodup (permsOfList l) ∧
    ((∀ (x : α), x ∈ l → Nodup (List.map (fun f => Equiv.swap a x * f) (permsOfList l))) ∧
        ∀ (i j : Fin (length l)),
          i < j →
            List.Disjoint (List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l))
              (List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l))) ∧
      List.Disjoint (permsOfList l) (List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l))
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ Nodup (permsOfList (a :: l))
rw [permsOfList, List.nodup_append, List.nodup_bind, pairwise_iff_get]
case refine_1
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ Nodup (permsOfList l)

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

case refine_3
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ ∀ (i j : Fin (length l)),
    i < j →
      List.Disjoint (List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l))
        (List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l))

case refine_4
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ List.Disjoint (permsOfList l) (List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l))
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ Nodup (permsOfList l) ∧
    ((∀ (x : α), x ∈ l → Nodup (List.map (fun f => Equiv.swap a x * f) (permsOfList l))) ∧
        ∀ (i j : Fin (length l)),
          i < j →
            List.Disjoint (List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l))
              (List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l))) ∧
      List.Disjoint (permsOfList l) (List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l))
refine ⟨?_, ⟨⟨?_,?_ ⟩, ?_⟩⟩
no goals
case refine_1
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ Nodup (permsOfList l)
exact hln'
no goals
case refine_2
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ ∀ (x : α), x ∈ l → Nodup (List.map (fun f => Equiv.swap a x * f) (permsOfList l))
exact fun _ _ => hln'.map fun _ _ => mul_left_cancel
case refine_3
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
⊢ False
case refine_3
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ ∀ (i j : Fin (length l)),
    i < j →
      List.Disjoint (List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l))
        (List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l))
intros i j hij x hx₁ hx₂
case refine_3
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
⊢ False
case refine_3
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
⊢ False
let ⟨f, hf⟩ := List.mem_map.1 hx₁
case refine_3
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
⊢ False
case refine_3
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
⊢ False
let ⟨g, hg⟩ := List.mem_map.1 hx₂
case refine_3
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
hix : ↑x a = List.get l i
⊢ False
case refine_3
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
⊢ False
have hix : x a = List.get l i := by
  rw [← hf.2, mul_apply, hmeml hf.1, swap_apply_left]
case refine_3
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
hix : ↑x a = List.get l i
hiy : ↑x a = List.get l j
⊢ False
case refine_3
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
hix : ↑x a = List.get l i
⊢ False
have hiy : x a = List.get l j := by
  rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left]
case refine_3
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
hix : ↑x a = List.get l i
hiy : ↑x a = List.get l j
hieqj : i = j
⊢ False
case refine_3
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
hix : ↑x a = List.get l i
hiy : ↑x a = List.get l j
⊢ False
have hieqj : i = j := nodup_iff_injective_get.1 hl' (hix.symm.trans hiy)
no goals
case refine_3
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
hix : ↑x a = List.get l i
hiy : ↑x a = List.get l j
hieqj : i = j
⊢ False
exact absurd hieqj (_root_.ne_of_lt hij)
no goals
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
⊢ ↑x a = List.get l i
rw [← hf.2, mul_apply, hmeml hf.1, swap_apply_left]
no goals
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
i j : Fin (length l)
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ List.map (fun f => Equiv.swap a (List.get l i) * f) (permsOfList l)
hx₂ : x ∈ List.map (fun f => Equiv.swap a (List.get l j) * f) (permsOfList l)
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (List.get l i) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (List.get l j) * g = x
hix : ↑x a = List.get l i
⊢ ↑x a = List.get l j
rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left]
case refine_4
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
⊢ False
case refine_4
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
⊢ List.Disjoint (permsOfList l) (List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l))
intros f hf₁ hf₂
case refine_4
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
⊢ False
case refine_4
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
⊢ False
let ⟨x, hx, hx'⟩ := List.mem_bind.1 hf₂
case refine_4
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList 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
⊢ False
case refine_4
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList l)
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f => Equiv.swap a x * f) (permsOfList l)
⊢ False
let ⟨g, hg⟩ := List.mem_map.1 hx'
case refine_4
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList 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
⊢ False
case refine_4
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList 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
⊢ False
have hgxa : g⁻¹ x = a := f.injective <| by rw [hmeml hf₁, ← hg.2]; simp
case refine_4
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList 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
case refine_4
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList 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
⊢ False
have hxa : x ≠ a := fun h => (List.nodup_cons.1 hl).1 (h ▸ hx)
no goals
case refine_4
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList 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
exact  (List.nodup_cons.1 hl).1 <|
    hgxa ▸ mem_of_mem_permsOfList hg.1 _ (by rwa [apply_inv_self, hgxa])
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList 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
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList 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
rw [hmeml hf₁, ← hg.2]
no goals
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList 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
simp
no goals
α : Type u_1
β : Type ?u.36858
γ : Type ?u.36861
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
a : α
l : List α
hl : Nodup (a :: l)
hl' : Nodup l
hln' : Nodup (permsOfList l)
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → ↑f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ List.bind l fun b => List.map (fun f => Equiv.swap a b * f) (permsOfList 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
⊢ ↑g (↑g⁻¹ x) ≠ ↑g⁻¹ x
rwa [apply_inv_self, hgxa]