case nil
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
hx✝ : ¬x ∈ s
hx : ¬x ∈ []
⊢ Nodup (permutations'Aux x [])

case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
hx✝ : ¬x ∈ s✝
y : α
s : List α
IH : ¬x ∈ s → Nodup (permutations'Aux x s)
hx : ¬x ∈ y :: s
⊢ Nodup (permutations'Aux x (y :: s))
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
hx : ¬x ∈ s
⊢ Nodup (permutations'Aux x s)
induction' s with y s IH
no goals
case nil
α : Type uu
β : Type vv
l₁ l₂ s : List α
x : α
hx✝ : ¬x ∈ s
hx : ¬x ∈ []
⊢ Nodup (permutations'Aux x [])
simp
case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
hx✝ : ¬x ∈ s✝
y : α
s : List α
IH : ¬x ∈ s → Nodup (permutations'Aux x s)
hx : ¬x = y ∧ ¬x ∈ s
⊢ Nodup (permutations'Aux x (y :: s))
case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
hx✝ : ¬x ∈ s✝
y : α
s : List α
IH : ¬x ∈ s → Nodup (permutations'Aux x s)
hx : ¬x ∈ y :: s
⊢ Nodup (permutations'Aux x (y :: s))
simp only [not_or, mem_cons] at hx
case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
hx✝ : ¬x ∈ s✝
y : α
s : List α
IH : ¬x ∈ s → Nodup (permutations'Aux x s)
hx : ¬x = y ∧ ¬x ∈ s
⊢ (y :: s ∈ permutations'Aux x s → ¬y = x) ∧ Nodup (map (cons y) (permutations'Aux x s))
case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
hx✝ : ¬x ∈ s✝
y : α
s : List α
IH : ¬x ∈ s → Nodup (permutations'Aux x s)
hx : ¬x = y ∧ ¬x ∈ s
⊢ Nodup (permutations'Aux x (y :: s))
simp only [permutations'Aux, nodup_cons, mem_map, cons.injEq, exists_eq_right_right, not_and]
case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
hx✝ : ¬x ∈ s✝
y : α
s : List α
IH : ¬x ∈ s → Nodup (permutations'Aux x s)
hx : ¬x = y ∧ ¬x ∈ s
⊢ Nodup (map (cons y) (permutations'Aux x s))
case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
hx✝ : ¬x ∈ s✝
y : α
s : List α
IH : ¬x ∈ s → Nodup (permutations'Aux x s)
hx : ¬x = y ∧ ¬x ∈ s
⊢ (y :: s ∈ permutations'Aux x s → ¬y = x) ∧ Nodup (map (cons y) (permutations'Aux x s))
refine' ⟨fun _ => Ne.symm hx.left, _⟩
case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
hx✝ : ¬x ∈ s✝
y : α
s : List α
IH : ¬x ∈ s → Nodup (permutations'Aux x s)
hx : ¬x = y ∧ ¬x ∈ s
⊢ Nodup (permutations'Aux x s)

case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
hx✝ : ¬x ∈ s✝
y : α
s : List α
IH : ¬x ∈ s → Nodup (permutations'Aux x s)
hx : ¬x = y ∧ ¬x ∈ s
⊢ Function.Injective (cons y)
case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
hx✝ : ¬x ∈ s✝
y : α
s : List α
IH : ¬x ∈ s → Nodup (permutations'Aux x s)
hx : ¬x = y ∧ ¬x ∈ s
⊢ Nodup (map (cons y) (permutations'Aux x s))
rw [nodup_map_iff]
no goals
case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
hx✝ : ¬x ∈ s✝
y : α
s : List α
IH : ¬x ∈ s → Nodup (permutations'Aux x s)
hx : ¬x = y ∧ ¬x ∈ s
⊢ Nodup (permutations'Aux x s)
exact IH hx.right
no goals
case cons
α : Type uu
β : Type vv
l₁ l₂ s✝ : List α
x : α
hx✝ : ¬x ∈ s✝
y : α
s : List α
IH : ¬x ∈ s → Nodup (permutations'Aux x s)
hx : ¬x = y ∧ ¬x ∈ s
⊢ Function.Injective (cons y)
simp