awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
⊢ s.length = t.length

Tactic:
have hl : s.length = t.length := by simpa using congr_arg length h
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ s.length < (permutations'Aux x s).length

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ s.length < (permutations'Aux x t).length

Tactic:
simp [hl]
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
a :
  (permutations'Aux x s).get (⟨s.length, ⋯⟩ : Fin (permutations'Aux x s).length) =
    (permutations'Aux x t).get (⟨s.length, ⋯⟩ : Fin (permutations'Aux x t).length)
⊢ s.insertIdx s.length x = t.insertIdx s.length x

Tactic:
rw [← get_permutations'Aux s x s.length (by simp),
    ← get_permutations'Aux t x s.length (by simp [hl])]

Premises used: List.get_permutations'Aux, List.length
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ (permutations'Aux x s).get (⟨s.length, ⋯⟩ : Fin (permutations'Aux x s).length) =
    (permutations'Aux x t).get (⟨s.length, ⋯⟩ : Fin (permutations'Aux x t).length)

Tactic:
simp only [get_eq_getElem, h, hl]

Premises used: List.get_eq_getElem
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x : α
hx : ¬Membership.mem (γ := List α) [] x
⊢ (permutations'Aux x []).Nodup

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x y : α
s : List α
IH : ∀ (hx : ¬x ∈ s), (permutations'Aux x s).Nodup
hx : ¬x ∈ y :: s
⊢ ¬x = y ∧ ¬x ∈ s

Tactic:
simp only [not_or, mem_cons] at hx

Premises used: not_or, List.mem_cons
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x y : α
s : List α
IH : ∀ (hx : ¬x ∈ s), (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
cons : (y :: s ∈ permutations'Aux x s → ¬y = x) ∧ (map (List.cons y) (permutations'Aux x s)).Nodup
⊢ (permutations'Aux x (y :: s)).Nodup

Tactic:
simp only [permutations'Aux, nodup_cons, mem_map, cons.injEq, exists_eq_right_right, not_and]

Premises used: exists_eq_right_right, List.cons.injEq, List.nodup_cons, List.permutations'Aux, List.mem_map, not_and
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x y : α
s : List α
IH : ∀ (hx : ¬x ∈ s), (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ (y :: s ∈ permutations'Aux x s → ¬y = x) ∧ (map (cons y) (permutations'Aux x s)).Nodup

Tactic:
⟨fun _ => Ne.symm hx.left, ?_⟩

Premises used: Ne.symm, And.left, And.intro
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x y : α
s : List α
IH : ∀ (hx : ¬x ∈ s), (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
cons : (map (List.cons y) (permutations'Aux x s)).Nodup
⊢ (y :: s ∈ permutations'Aux x s → ¬y = x) ∧ (map (List.cons y) (permutations'Aux x s)).Nodup

Tactic:
refine ⟨fun _ => Ne.symm hx.left, ?_⟩
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x y : α
s : List α
IH : ∀ (hx : ¬x ∈ s), (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
cons : (permutations'Aux x s).Nodup
cons₁ : Injective (List.cons y)
⊢ (map (List.cons y) (permutations'Aux x s)).Nodup

Tactic:
rw [nodup_map_iff]

Premises used: List.nodup_map_iff
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x y : α
s : List α
IH : ∀ (hx : ¬x ∈ s), (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ (permutations'Aux x s).Nodup

Tactic:
IH hx.right

Premises used: And.right
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x y : α
s : List α
IH : ∀ (hx : ¬x ∈ s), (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ (permutations'Aux x s).Nodup

Tactic:
exact IH hx.right

Premises used: And.right
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
x y : α
s : List α
IH : ∀ (hx : ¬x ∈ s), (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ Injective (cons y)

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
hx : ¬x ∈ s
nil : ∀ (hx : ¬Membership.mem (γ := List α) [] x), (permutations'Aux x []).Nodup
cons :
  ∀ (y : α) (s : List α) (IH : ∀ (hx : ¬x ∈ s), (permutations'Aux x s).Nodup) (hx : ¬x ∈ y :: s),
    (permutations'Aux x (y :: s)).Nodup
⊢ (permutations'Aux x s).Nodup

Tactic:
induction s with
  | nil => simp
  | cons y s IH =>
    simp only [not_or, mem_cons] at hx
    simp only [permutations'Aux, nodup_cons, mem_map, cons.injEq, exists_eq_right_right, not_and]
    refine ⟨fun _ => Ne.symm hx.left, ?_⟩
    rw [nodup_map_iff]
    · exact IH hx.right
    · simp

Premises used: exists_eq_right_right, not_or, List.cons, List.cons.injEq, List.nodup_cons, List.permutations'Aux, List.mem_cons, List.nodup_map_iff, List.mem_map, not_and, List.nil
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
⊢ (permutations'Aux x s).Nodup ↔ ¬x ∈ s

Tactic:
⟨fun h H ↦ ?_, nodup_permutations'Aux_of_notMem _ _⟩

Premises used: List.nodup_permutations'Aux_of_notMem, Iff.intro
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
refine : ∀ (h : (permutations'Aux x s).Nodup) (H : x ∈ s), False
⊢ (permutations'Aux x s).Nodup ↔ ¬x ∈ s

Tactic:
refine ⟨fun h H ↦ ?_, nodup_permutations'Aux_of_notMem _ _⟩
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
h : (permutations'Aux x s).Nodup
H : x ∈ s
obtain : ∀ (k : ℕ) (hk : k < s.length) (hk' : s.get (⟨k, hk⟩ : Fin s.length) = x), False
⊢ False

Tactic:
obtain ⟨⟨k, hk⟩, hk'⟩ := get_of_mem H

Premises used: List.get_of_mem
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
h : (permutations'Aux x s).Nodup
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get (⟨k, hk⟩ : Fin s.length) = x
rw :
  ∀ (h : Injective (permutations'Aux x s).get) (H : x ∈ s) (k : ℕ) (hk : k < s.length)
    (hk' : s.get (⟨k, hk⟩ : Fin s.length) = x), False
⊢ False

Tactic:
rw [nodup_iff_injective_get] at h

Premises used: List.nodup_iff_injective_get
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get (⟨k, hk⟩ : Fin s.length) = x
apply : k = k.succ
⊢ False

Tactic:
apply k.succ_ne_self.symm

Premises used: Nat.succ_ne_self, Ne.symm
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get (⟨k, hk⟩ : Fin s.length) = x
⊢ k < (permutations'Aux x s).length

Tactic:
simpa [Nat.lt_succ_iff] using hk.le

Premises used: LT.lt.le, Nat.lt_succ_iff
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get (⟨k, hk⟩ : Fin s.length) = x
⊢ k < (permutations'Aux x s).length

Tactic:
have kl : k < (permutations'Aux x s).length := by simpa [Nat.lt_succ_iff] using hk.le
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get (⟨k, hk⟩ : Fin s.length) = x
kl : k < (permutations'Aux x s).length
⊢ k + 1 < (permutations'Aux x s).length

Tactic:
simpa using hk
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get (⟨k, hk⟩ : Fin s.length) = x
kl : k < (permutations'Aux x s).length
⊢ k + 1 < (permutations'Aux x s).length

Tactic:
have k1l : k + 1 < (permutations'Aux x s).length := by simpa using hk
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get (⟨k, hk⟩ : Fin s.length) = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
rw : (⟨k, kl⟩ : Fin (permutations'Aux x s).length) = ⟨k + 1, k1l⟩
⊢ k = k.succ

Tactic:
rw [← @Fin.mk.inj_iff _ _ _ kl k1l]

Premises used: Fin.mk.inj_iff
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get (⟨k, hk⟩ : Fin s.length) = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
a :
  (permutations'Aux x s).get (⟨k, kl⟩ : Fin (permutations'Aux x s).length) =
    (permutations'Aux x s).get (⟨k + 1, k1l⟩ : Fin (permutations'Aux x s).length)
⊢ (⟨k, kl⟩ : Fin (permutations'Aux x s).length) = ⟨k + 1, k1l⟩

Tactic:
apply h
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get (⟨k, hk⟩ : Fin s.length) = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
a : s.insertIdx k x = s.insertIdx (k + 1) x
⊢ (permutations'Aux x s).get (⟨k, kl⟩ : Fin (permutations'Aux x s).length) =
    (permutations'Aux x s).get (⟨k + 1, k1l⟩ : Fin (permutations'Aux x s).length)

Tactic:
rw [get_permutations'Aux, get_permutations'Aux]

Premises used: List.get_permutations'Aux
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get (⟨k, hk⟩ : Fin s.length) = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
rw : s.length + 1 = (s.insertIdx (k + 1) x).length
rw₁ rw₂ : s.length + 1 = s.length + 1
⊢ (s.insertIdx k x).length = (s.insertIdx (k + 1) x).length

Tactic:
rw [length_insertIdx_of_le_length hk.le, length_insertIdx_of_le_length (Nat.succ_le_of_lt hk)]

Premises used: Nat.succ_le_of_lt, List.length_insertIdx_of_le_length, LT.lt.le
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get (⟨k, hk⟩ : Fin s.length) = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
⊢ (s.insertIdx k x).length = (s.insertIdx (k + 1) x).length

Tactic:
have hl : length (s.insertIdx k x) = length (s.insertIdx (k + 1) x) := by
    rw [length_insertIdx_of_le_length hk.le, length_insertIdx_of_le_length (Nat.succ_le_of_lt hk)]
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get (⟨k, hk⟩ : Fin s.length) = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
hl : (s.insertIdx k x).length = (s.insertIdx (k + 1) x).length
n : ℕ
hn : n < (s.insertIdx k x).length
hn' : n < (s.insertIdx (k + 1) x).length
⊢ (s.insertIdx k x).get (⟨n, hn⟩ : Fin (s.insertIdx k x).length) =
    (s.insertIdx (k + 1) x).get (⟨n, hn'⟩ : Fin (s.insertIdx (k + 1) x).length)

Tactic:
grind
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
h : Injective (permutations'Aux x s).get
H : x ∈ s
k : ℕ
hk : k < s.length
hk' : s.get (⟨k, hk⟩ : Fin s.length) = x
kl : k < (permutations'Aux x s).length
k1l : k + 1 < (permutations'Aux x s).length
hl : (s.insertIdx k x).length = (s.insertIdx (k + 1) x).length
⊢ s.insertIdx k x = s.insertIdx (k + 1) x

Tactic:
exact ext_get hl fun n hn hn' => by grind

Premises used: List.ext_get
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
hs : s.Nodup
rw : s.permutations'.Nodup
⊢ s.permutations.Nodup

Tactic:
rw [(permutations_perm_permutations' s).nodup_iff]

Premises used: List.Perm.nodup_iff, List.permutations_perm_permutations'
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
⊢ Nodup.{u_1} (α := List α) (permutations' [])

Tactic:
simp
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
cons :
  (∀ (x_1 : List α), x_1 ∈ l.permutations' → (permutations'Aux x x_1).Nodup) ∧
    Pairwise (Disjoint on permutations'Aux x) l.permutations'
⊢ (flatMap (permutations'Aux x) l.permutations').Nodup

Tactic:
rw [nodup_flatMap]

Premises used: List.nodup_flatMap
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
cons : ∀ (x_1 : List α), x_1 ∈ l.permutations' → (permutations'Aux x x_1).Nodup
cons₁ : Pairwise (Disjoint on permutations'Aux x) l.permutations'
⊢ (∀ (x_1 : List α), x_1 ∈ l.permutations' → (permutations'Aux x x_1).Nodup) ∧
    Pairwise (Disjoint on permutations'Aux x) l.permutations'

Tactic:
constructor
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
ys : List α
hy : ys ∈ l.permutations'
⊢ ys ~ l

Tactic:
rw [mem_permutations'] at hy

Premises used: List.mem_permutations'
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
ys : List α
hy : ys ~ l
cons : ¬x ∈ l
⊢ (permutations'Aux x ys).Nodup

Tactic:
rw [nodup_permutations'Aux_iff, hy.mem_iff]

Premises used: List.nodup_permutations'Aux_iff, List.Perm.mem_iff
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
ys : List α
hy : ys ~ l
⊢ ¬x ∈ l

Tactic:
fun H => h x H rfl

Premises used: Not, rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
ys : List α
hy : ys ~ l
⊢ ¬x ∈ l

Tactic:
exact fun H => h x H rfl

Premises used: rfl
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
⊢ Pairwise (Disjoint on permutations'Aux x) l.permutations'

Tactic:
IH.pairwise_of_forall_ne fun as ha bs hb H => ?_

Premises used: List.Nodup.pairwise_of_forall_ne
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
cons :
  ∀ (as : List α) (ha : as ∈ l.permutations') (bs : List α) (hb : bs ∈ l.permutations') (H : as ≠ bs),
    (Disjoint on permutations'Aux x) as bs
⊢ Pairwise (Disjoint on permutations'Aux x) l.permutations'

Tactic:
refine IH.pairwise_of_forall_ne fun as ha bs hb H => ?_

Premises used: List.Nodup.pairwise_of_forall_ne
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ∈ l.permutations'
bs : List α
hb : bs ∈ l.permutations'
H : as ≠ bs
cons : ∀ (a : List α), a ∈ permutations'Aux x as → ∀ (b : List α), b ∈ permutations'Aux x bs → a ≠ b
⊢ (Disjoint on permutations'Aux x) as bs

Tactic:
rw [Function.onFun, disjoint_iff_ne]

Premises used: List.disjoint_iff_ne, Function.onFun
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ∈ l.permutations'
bs : List α
hb : bs ∈ l.permutations'
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
cons :
  ∀ (n : ℕ) (hn : n < (permutations'Aux x as).length)
    (hn' : (permutations'Aux x as).get (⟨n, hn⟩ : Fin (permutations'Aux x as).length) = a), False
⊢ False

Tactic:
obtain ⟨⟨n, hn⟩, hn'⟩ := get_of_mem ha'

Premises used: List.get_of_mem
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ∈ l.permutations'
bs : List α
hb : bs ∈ l.permutations'
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn : n < (permutations'Aux x as).length
hn' : (permutations'Aux x as).get (⟨n, hn⟩ : Fin (permutations'Aux x as).length) = a
cons :
  ∀ (m : ℕ) (hm : m < (permutations'Aux x bs).length)
    (hm' : (permutations'Aux x bs).get (⟨m, hm⟩ : Fin (permutations'Aux x bs).length) = a), False
⊢ False

Tactic:
obtain ⟨⟨m, hm⟩, hm'⟩ := get_of_mem hb'

Premises used: List.get_of_mem
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ∈ l.permutations'
bs : List α
hb : bs ∈ l.permutations'
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn : n < (permutations'Aux x as).length
hn' : (permutations'Aux x as).get (⟨n, hn⟩ : Fin (permutations'Aux x as).length) = a
m : ℕ
hm : m < (permutations'Aux x bs).length
hm' : (permutations'Aux x bs).get (⟨m, hm⟩ : Fin (permutations'Aux x bs).length) = a
cons :
  ∀ (ha : as ~ l) (bs : List α) (hb : bs ~ l) (H : as ≠ bs) (a : List α) (ha' : a ∈ permutations'Aux x as)
    (hb' : a ∈ permutations'Aux x bs) (n : ℕ) (hn : n < (permutations'Aux x as).length)
    (hn' : (permutations'Aux x as).get (⟨n, hn⟩ : Fin (permutations'Aux x as).length) = a) (m : ℕ)
    (hm : m < (permutations'Aux x bs).length)
    (hm' : (permutations'Aux x bs).get (⟨m, hm⟩ : Fin (permutations'Aux x bs).length) = a), False
⊢ False

Tactic:
rw [mem_permutations'] at ha hb

Premises used: List.mem_permutations'
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn : n < (permutations'Aux x as).length
hn' : (permutations'Aux x as).get (⟨n, hn⟩ : Fin (permutations'Aux x as).length) = a
m : ℕ
hm : m < (permutations'Aux x bs).length
hm' : (permutations'Aux x bs).get (⟨m, hm⟩ : Fin (permutations'Aux x bs).length) = a
⊢ as.length = bs.length

Tactic:
have hl : as.length = bs.length := (ha.trans hb.symm).length_eq
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn : n < (permutations'Aux x as).length
hn' : (permutations'Aux x as).get (⟨n, hn⟩ : Fin (permutations'Aux x as).length) = a
m : ℕ
hm : m < (permutations'Aux x bs).length
hm' : (permutations'Aux x bs).get (⟨m, hm⟩ : Fin (permutations'Aux x bs).length) = a
hl : as.length = bs.length
⊢ n ≤ as.length

Tactic:
simp only [Nat.lt_succ_iff, length_permutations'Aux] at hn hm

Premises used: List.length_permutations'Aux, Nat.lt_succ_iff
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn : n < (permutations'Aux x as).length
hn' : (permutations'Aux x as).get (⟨n, hn⟩ : Fin (permutations'Aux x as).length) = a
m : ℕ
hm : m < (permutations'Aux x bs).length
hm' : (permutations'Aux x bs).get (⟨m, hm⟩ : Fin (permutations'Aux x bs).length) = a
hl : as.length = bs.length
hn₁ : n ≤ as.length
⊢ m ≤ bs.length

Tactic:
simp only [Nat.lt_succ_iff, length_permutations'Aux] at hn hm

Premises used: List.length_permutations'Aux, Nat.lt_succ_iff
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : (permutations'Aux x as).get (⟨n, hn_1⟩ : Fin (permutations'Aux x as).length) = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : (permutations'Aux x bs).get (⟨m, hm_1⟩ : Fin (permutations'Aux x bs).length) = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
cons :
  ∀ (hn' : as.insertIdx n x = a) (m : ℕ) (hm : m < (permutations'Aux x bs).length) (hm' : bs.insertIdx m x = a)
    (hl : as.length = bs.length) (hn : n ≤ as.length) (hm : m ≤ bs.length), False
⊢ False

Tactic:
rw [get_permutations'Aux] at hn' hm'

Premises used: List.get_permutations'Aux
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
rwa : m < as.length + 1
rwa₁ : m ≤ as.length
rwa₂ rwa₃ rwa₄ rwa₅ : m ≤ bs.length
⊢ m < (as.insertIdx n x).length

Tactic:
rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff, hl]

Premises used: List.length_insertIdx_of_le_length, Nat.lt_succ_iff
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x

Tactic:
simp [hn', ← hm']
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x

Tactic:
have hx : (as.insertIdx n x)[m]'(by
          rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff, hl]) = x := by
        simp [hn', ← hm']
-- Module: Mathlib.Data.List.Permutation
Goal:
α : Type u_1
s : List α
x : α
l : List α
h : ∀ (a' : α), a' ∈ l → x ≠ a'
h' : Pairwise (fun (x1 x2 : α) ↦ x1 ≠ x2) l
IH : l.permutations'.Nodup
as : List α
ha : as ~ l
bs : List α
hb : bs ~ l
H : as ≠ bs
a : List α
ha' : a ∈ permutations'Aux x as
hb' : a ∈ permutations'Aux x bs
n : ℕ
hn_1 : n < (permutations'Aux x as).length
hn' : as.insertIdx n x = a
m : ℕ
hm_1 : m < (permutations'Aux x bs).length
hm' : bs.insertIdx m x = a
hl : as.length = bs.length
hn : n ≤ as.length
hm : m ≤ bs.length
hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m ⋯ = x
rwa : n < bs.length + 1
rwa₁ : n ≤ bs.length
rwa₂ rwa₃ rwa₄ rwa₅ : n ≤ as.length
⊢ n < (bs.insertIdx m x).length

Tactic:
rwa [length_insertIdx_of_le_length hm, Nat.lt_succ_iff, ← hl]

Premises used: List.length_insertIdx_of_le_length, Nat.lt_succ_iff