-- Mathlib/Data/List/Lemmas.lean
theorem injOn_insertIdx_index_of_not_mem (l : List α) (x : α) (hx : x ∉ l) :
    Set.InjOn (fun k => insertIdx k x l) { n | n ≤ l.length }

Proof state:
case cons
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
n : ℕ
hn : n ≤ tl.length + 1
m : ℕ
hm : m ≤ tl.length + 1
h : (fun k => insertIdx k x (hd :: tl)) n = (fun k => insertIdx k x (hd :: tl)) m
hx : ¬x = hd ∧ x ∉ tl
⊢ n = m

Tactic:
cases n <;> cases m

Result:
case cons.zero.zero
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : ¬x = hd ∧ x ∉ tl
hn hm : 0 ≤ tl.length + 1
h : (fun k => insertIdx k x (hd :: tl)) 0 = (fun k => insertIdx k x (hd :: tl)) 0
⊢ 0 = 0

case cons.zero.succ
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : ¬x = hd ∧ x ∉ tl
hn : 0 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k => insertIdx k x (hd :: tl)) 0 = (fun k => insertIdx k x (hd :: tl)) (n✝ + 1)
⊢ 0 = n✝ + 1

case cons.succ.zero
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : ¬x = hd ∧ x ∉ tl
n✝ : ℕ
hn : n✝ + 1 ≤ tl.length + 1
hm : 0 ≤ tl.length + 1
h : (fun k => insertIdx k x (hd :: tl)) (n✝ + 1) = (fun k => insertIdx k x (hd :: tl)) 0
⊢ n✝ + 1 = 0

case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : ¬x = hd ∧ x ∉ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k => insertIdx k x (hd :: tl)) (n✝¹ + 1) = (fun k => insertIdx k x (hd :: tl)) (n✝ + 1)
⊢ n✝¹ + 1 = n✝ + 1

Proof state:
case cons.zero.succ
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : ¬x = hd ∧ x ∉ tl
hn : 0 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k => insertIdx k x (hd :: tl)) 0 = (fun k => insertIdx k x (hd :: tl)) (n✝ + 1)
⊢ 0 = n✝ + 1

Tactic:
simp [hx.left] at h

Result:
no goals

Proof state:
case nil
α : Type u_1
x : α
hx : x ∉ []
⊢ Set.InjOn (fun k => insertIdx k x []) {n | n ≤ [].length}

Tactic:
intro n hn m hm _

Result:
case nil
α : Type u_1
x : α
hx : x ∉ []
n : ℕ
hn : n ∈ {n | n ≤ [].length}
m : ℕ
hm : m ∈ {n | n ≤ [].length}
a✝ : (fun k => insertIdx k x []) n = (fun k => insertIdx k x []) m
⊢ n = m

Proof state:
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : ¬x = hd ∧ x ∉ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : hd :: insertIdx n✝¹ x tl = hd :: insertIdx n✝ x tl
⊢ (fun k => insertIdx k x tl) n✝¹ = (fun k => insertIdx k x tl) n✝

Tactic:
injection h

Result:
no goals

Proof state:
case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : ¬x = hd ∧ x ∉ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : hd :: insertIdx n✝¹ x tl = hd :: insertIdx n✝ x tl
⊢ n✝¹ + 1 = n✝ + 1

Tactic:
rw [Nat.succ_inj']

Result:
case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : ¬x = hd ∧ x ∉ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : hd :: insertIdx n✝¹ x tl = hd :: insertIdx n✝ x tl
⊢ n✝¹ = n✝

Proof state:
case cons
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : x ∉ hd :: tl
⊢ Set.InjOn (fun k => insertIdx k x (hd :: tl)) {n | n ≤ (hd :: tl).length}

Tactic:
intro n hn m hm h

Result:
case cons
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : x ∉ hd :: tl
n : ℕ
hn : n ∈ {n | n ≤ (hd :: tl).length}
m : ℕ
hm : m ∈ {n | n ≤ (hd :: tl).length}
h : (fun k => insertIdx k x (hd :: tl)) n = (fun k => insertIdx k x (hd :: tl)) m
⊢ n = m

Proof state:
α : Type u_1
l : List α
x : α
hx : x ∉ l
⊢ Set.InjOn (fun k => insertIdx k x l) {n | n ≤ l.length}

Tactic:
induction' l with hd tl IH

Result:
case nil
α : Type u_1
x : α
hx : x ∉ []
⊢ Set.InjOn (fun k => insertIdx k x []) {n | n ≤ [].length}

case cons
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : x ∉ hd :: tl
⊢ Set.InjOn (fun k => insertIdx k x (hd :: tl)) {n | n ≤ (hd :: tl).length}

Proof state:
case nil
α : Type u_1
x : α
hx : x ∉ []
n : ℕ
hn : n ∈ {n | n ≤ [].length}
m : ℕ
hm : m ∈ {n | n ≤ [].length}
a✝ : (fun k => insertIdx k x []) n = (fun k => insertIdx k x []) m
⊢ n = m

Tactic:
simp_all [Set.mem_singleton_iff, Set.setOf_eq_eq_singleton, length]

Result:
no goals

Proof state:
case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : ¬x = hd ∧ x ∉ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : (fun k => insertIdx k x (hd :: tl)) (n✝¹ + 1) = (fun k => insertIdx k x (hd :: tl)) (n✝ + 1)
⊢ n✝¹ + 1 = n✝ + 1

Tactic:
simp only [true_and, eq_self_iff_true, insertIdx_succ_cons] at h

Result:
case cons.succ.succ
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : ¬x = hd ∧ x ∉ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : hd :: insertIdx n✝¹ x tl = hd :: insertIdx n✝ x tl
⊢ n✝¹ + 1 = n✝ + 1

Proof state:
case cons.succ.zero
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : ¬x = hd ∧ x ∉ tl
n✝ : ℕ
hn : n✝ + 1 ≤ tl.length + 1
hm : 0 ≤ tl.length + 1
h : (fun k => insertIdx k x (hd :: tl)) (n✝ + 1) = (fun k => insertIdx k x (hd :: tl)) 0
⊢ n✝ + 1 = 0

Tactic:
simp [Ne.symm hx.left] at h

Result:
no goals

Proof state:
case cons
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : x ∉ hd :: tl
n : ℕ
hn : n ∈ {n | n ≤ (hd :: tl).length}
m : ℕ
hm : m ∈ {n | n ≤ (hd :: tl).length}
h : (fun k => insertIdx k x (hd :: tl)) n = (fun k => insertIdx k x (hd :: tl)) m
⊢ n = m

Tactic:
simp only [length, Set.mem_setOf_eq] at hn hm

Result:
case cons
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : x ∉ hd :: tl
n : ℕ
hn : n ≤ tl.length + 1
m : ℕ
hm : m ≤ tl.length + 1
h : (fun k => insertIdx k x (hd :: tl)) n = (fun k => insertIdx k x (hd :: tl)) m
⊢ n = m

Proof state:
case cons.succ.succ.refine_2
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : ¬x = hd ∧ x ∉ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : hd :: insertIdx n✝¹ x tl = hd :: insertIdx n✝ x tl
⊢ n✝ ∈ {n | n ≤ tl.length}

Tactic:
simpa [Nat.succ_le_succ_iff] using hm

Result:
no goals

Proof state:
case cons.succ.succ.refine_1
α : Type u_1
x hd : α
tl : List α
IH : x ∉ tl → Set.InjOn (fun k => insertIdx k x tl) {n | n ≤ tl.length}
hx : ¬x = hd ∧ x ∉ tl
n✝¹ : ℕ
hn : n✝¹ + 1 ≤ tl.length + 1
n✝ : ℕ
hm : n✝ + 1 ≤ tl.length + 1
h : hd :: insertIdx n✝¹ x tl = hd :: insertIdx n✝ x tl
⊢ n✝¹ ∈ {n | n ≤ tl.length}

Tactic:
simpa [Nat.succ_le_succ_iff] using hn

Result:
no goals