α : Type uu
β : Type vv
l₁ l₂ : List α
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
⊢ s = t
α : Type uu
β : Type vv
l₁ l₂ : List α
x : α
⊢ Function.Injective (permutations'Aux x)
intro s t h
case a
α : Type uu
β : Type vv
l₁ l₂ : List α
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
⊢ insertNth (length s) x s = insertNth (length s) x t
α : Type uu
β : Type vv
l₁ l₂ : List α
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
⊢ s = t
apply insertNth_injective s.length x
case a
α : Type uu
β : Type vv
l₁ l₂ : List α
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : length s = length t
⊢ insertNth (length s) x s = insertNth (length s) x t
case a
α : Type uu
β : Type vv
l₁ l₂ : List α
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
⊢ insertNth (length s) x s = insertNth (length s) x t
have hl : s.length = t.length := by simpa using congr_arg length h
case a
α : Type uu
β : Type vv
l₁ l₂ : List α
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : length s = length t
⊢ nthLe (permutations'Aux x s) (length s) (_ : length s < length (permutations'Aux x s)) =
    nthLe (permutations'Aux x t) (length s) (_ : length s < length (permutations'Aux x t))
case a
α : Type uu
β : Type vv
l₁ l₂ : List α
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : length s = length t
⊢ insertNth (length s) x s = insertNth (length s) x t
rw [← nthLe_permutations'Aux s x s.length (by simp), ←
  nthLe_permutations'Aux t x s.length (by simp [hl])]
no goals
case a
α : Type uu
β : Type vv
l₁ l₂ : List α
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : length s = length t
⊢ nthLe (permutations'Aux x s) (length s) (_ : length s < length (permutations'Aux x s)) =
    nthLe (permutations'Aux x t) (length s) (_ : length s < length (permutations'Aux x t))
simp [h, hl]
no goals
α : Type uu
β : Type vv
l₁ l₂ : List α
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
⊢ length s = length t
simpa using congr_arg length h
no goals
α : Type uu
β : Type vv
l₁ l₂ : List α
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : length s = length t
⊢ length s < length (permutations'Aux x s)
simp
no goals
α : Type uu
β : Type vv
l₁ l₂ : List α
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : length s = length t
⊢ length s < length (permutations'Aux x t)
simp [hl]