awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
Goal:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
⊢ s.insertIdx s.length x = t.insertIdx s.length x
have hl : s.length = t.length
Tactic: have hl : s.length = t.length := by simpa using congr_arg length h
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ s.insertIdx s.length x = t.insertIdx s.length x
have a : (permutations'Aux x s).get (⟨s.length, sorry⟩ : Fin (permutations'Aux x s).length) =
  (permutations'Aux x t).get (⟨s.length, sorry⟩ : Fin (permutations'Aux x t).length)
Tactic: rw [← get_permutations'Aux s x s.length (by simp),
    ← get_permutations'Aux t x s.length (by simp [hl])]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
Goal:
α : Type u_1
x y : α
s : List α
IH : ∀ (hx : ¬x ∈ s), (permutations'Aux x s).Nodup
hx : ¬x ∈ y :: s
⊢ (permutations'Aux x (y :: s)).Nodup
have hx₁ : ¬x = y ∧ ¬x ∈ s
Tactic: simp only [not_or, mem_cons] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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 (y :: s)).Nodup
have cons : (y :: s ∈ permutations'Aux x s → ¬y = x) ∧ (map (cons y) (permutations'Aux x s)).Nodup
Tactic: simp only [permutations'Aux, nodup_cons, mem_map, cons.injEq, exists_eq_right_right, not_and]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
have cons : (map (cons y) (permutations'Aux x s)).Nodup
Tactic: refine ⟨fun _ => Ne.symm hx.left, ?_⟩
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
x y : α
s : List α
IH : ∀ (hx : ¬x ∈ s), (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ (map (cons y) (permutations'Aux x s)).Nodup
have cons : (permutations'Aux x s).Nodup
Tactic: rw [nodup_map_iff]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ (map (List.cons y) (permutations'Aux x s)).Nodup
have cons₁ : Injective (List.cons y)
Tactic: rw [nodup_map_iff]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
x : α
hx : ¬x ∈ s
⊢ (permutations'Aux x s).Nodup
have nil : ∀ (hx : ¬Membership.mem (γ := List α) [] x), (permutations'Aux x []).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
Cleared hypotheses: s, hx
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
x : α
hx : ¬x ∈ s
nil : ∀ (hx : ¬Membership.mem (γ := List α) [] x), (permutations'Aux x []).Nodup
⊢ (permutations'Aux x s).Nodup
have cons : ∀ (y : α) (s : List α) (IH : ∀ (hx : ¬x ∈ s), (permutations'Aux x s).Nodup) (hx : ¬x ∈ y :: s),
  (permutations'Aux x (y :: 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
Cleared hypotheses: s, hx
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
x : α
⊢ (permutations'Aux x s).Nodup ↔ ¬x ∈ s
have refine : ∀ (h : (permutations'Aux x s).Nodup) (H : x ∈ s), False
Tactic: refine ⟨fun h H ↦ ?_, nodup_permutations'Aux_of_notMem _ _⟩
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
x : α
h : (permutations'Aux x s).Nodup
H : x ∈ s
⊢ False
have obtain : ∀ (k : ℕ) (hk : k < s.length) (hk' : s.get (⟨k, hk⟩ : Fin s.length) = x), False
Tactic: obtain ⟨⟨k, hk⟩, hk'⟩ := get_of_mem H
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ False
have 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
Tactic: rw [nodup_iff_injective_get] at h
Cleared hypotheses: h, H, k, hk, hk'
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ False
have apply : k = k.succ
Tactic: apply k.succ_ne_self.symm
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
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 = k.succ
have kl : k < (permutations'Aux x s).length
Tactic: have kl : k < (permutations'Aux x s).length := by simpa [Nat.lt_succ_iff] using hk.le
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
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 = k.succ
have k1l : k + 1 < (permutations'Aux x s).length
Tactic: have k1l : k + 1 < (permutations'Aux x s).length := by simpa using hk
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ k = k.succ
have rw : (⟨k, kl⟩ : Fin (permutations'Aux x s).length) = ⟨k + 1, k1l⟩
Tactic: rw [← @Fin.mk.inj_iff _ _ _ kl k1l]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ (⟨k, kl⟩ : Fin (permutations'Aux x s).length) = ⟨k + 1, k1l⟩
have 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)
Tactic: apply h
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ (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)
have a : s.insertIdx k x = s.insertIdx (k + 1) x
Tactic: rw [get_permutations'Aux, get_permutations'Aux]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
have rw : s.length + 1 = (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)]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ (s.insertIdx k x).length = (s.insertIdx (k + 1) x).length
have rw₁ : s.length + 1 = s.length + 1
Tactic: rw [length_insertIdx_of_le_length hk.le, length_insertIdx_of_le_length (Nat.succ_le_of_lt hk)]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
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 = s.insertIdx (k + 1) x
have hl : (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)]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
Goal:
α : Type u_1
s : List α
hs : s.Nodup
⊢ s.permutations.Nodup
have rw : s.permutations'.Nodup
Tactic: rw [(permutations_perm_permutations' s).nodup_iff]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ (flatMap (permutations'Aux x) l.permutations').Nodup
have cons : (∀ (x_1 : List α), x_1 ∈ l.permutations' → (permutations'Aux x x_1).Nodup) ∧
  Pairwise (Disjoint on permutations'Aux x) l.permutations'
Tactic: rw [nodup_flatMap]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ (∀ (x_1 : List α), x_1 ∈ l.permutations' → (permutations'Aux x x_1).Nodup) ∧
    Pairwise (Disjoint on permutations'Aux x) l.permutations'
have cons : ∀ (x_1 : List α), x_1 ∈ l.permutations' → (permutations'Aux x x_1).Nodup
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ (∀ (x_1 : List α), x_1 ∈ l.permutations' → (permutations'Aux x x_1).Nodup) ∧
    Pairwise (Disjoint on permutations'Aux x) l.permutations'
have cons₁ : Pairwise (Disjoint on permutations'Aux x) l.permutations'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
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'
⊢ (permutations'Aux x ys).Nodup
have hy₁ : ys ~ l
Tactic: rw [mem_permutations'] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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'Aux x ys).Nodup
have cons : ¬x ∈ l
Tactic: rw [nodup_permutations'Aux_iff, hy.mem_iff]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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'
have cons : ∀ (as : List α) (ha : as ∈ l.permutations') (bs : List α) (hb : bs ∈ l.permutations') (H : as ≠ bs),
  (Disjoint on permutations'Aux x) as bs
Tactic: refine IH.pairwise_of_forall_ne fun as ha bs hb H => ?_
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ (Disjoint on permutations'Aux x) as bs
have cons : ∀ (a : List α), a ∈ permutations'Aux x as → ∀ (b : List α), b ∈ permutations'Aux x bs → a ≠ b
Tactic: rw [Function.onFun, disjoint_iff_ne]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ False
have 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
Tactic: obtain ⟨⟨n, hn⟩, hn'⟩ := get_of_mem ha'
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ False
have 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
Tactic: obtain ⟨⟨m, hm⟩, hm'⟩ := get_of_mem hb'
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ False
have 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
Tactic: rw [mem_permutations'] at ha hb
Cleared hypotheses: ha, bs, hb, H, a, ha', hb', n, hn, hn', m, hm, hm'
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
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
⊢ False
have hl : as.length = bs.length
Tactic: have hl : as.length = bs.length := (ha.trans hb.symm).length_eq
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
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
⊢ False
have hn₁ : n ≤ as.length
Tactic: simp only [Nat.lt_succ_iff, length_permutations'Aux] at hn hm
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
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
⊢ False
have hm₁ : m ≤ bs.length
Tactic: simp only [Nat.lt_succ_iff, length_permutations'Aux] at hn hm
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ False
have 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
Tactic: rw [get_permutations'Aux] at hn' hm'
Cleared hypotheses: hn', m, hm_1, hm', hl, hn, hm
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ m < (as.insertIdx n x).length
have rwa : m < as.length + 1
Tactic: rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff, hl]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ m < (as.insertIdx n x).length
have rwa₁ : m ≤ as.length
Tactic: rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff, hl]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
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
⊢ False
have hx : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (as.insertIdx n x) m sorry = 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']
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ n < (bs.insertIdx m x).length
have rwa : n < bs.length + 1
Tactic: rwa [length_insertIdx_of_le_length hm, Nat.lt_succ_iff, ← hl]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
⊢ n < (bs.insertIdx m x).length
have rwa₁ : n ≤ bs.length
Tactic: rwa [length_insertIdx_of_le_length hm, Nat.lt_succ_iff, ← hl]
-- Lean 4 proof step from Mathlib.Data.List.Permutation (hypothesis)
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
⊢ False
have hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n sorry = x
Tactic: have hx' : (bs.insertIdx m x)[n]'(by
          rwa [length_insertIdx_of_le_length hm, Nat.lt_succ_iff, ← hl]) = x := by
        simp [hm', ← hn']
-- Lean 4 proof step from Mathlib.Data.List.Permutation (goal)
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
hx' : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (bs.insertIdx m x) n ⋯ = x
⊢ False
have cons : ∀ (ht : n < m), False
Tactic: rcases lt_trichotomy n m with (ht | ht | ht)