awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
n : ℕ
h : n < l.tails.length
nil :
  ∀ (n : ℕ) (h : n < length.{u_1} (α := List α) (tails [])),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (tails []) n h = drop n []
cons :
  ∀ (a : α) (l : List α)
    (ihl :
      ∀ (n : ℕ) (h : n < l.tails.length),
        getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.tails n h = drop n l)
    (n : ℕ) (h : n < (a :: l).tails.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).tails n h = drop n (a :: l)
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.tails n h = drop n l

Tactic:
induction l generalizing n with
  | nil => simp
  | cons a l ihl =>
    cases n with
    | zero => simp
    | succ n => simp [ihl]

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
n : Fin l.tails.length
⊢ l.tails.get n = drop (↑n : ℕ) l

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
n : ℕ
h : n < length.{u_1} (α := List α) (inits [])
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (inits []) n h = take n []

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
a : α
l : List α
ihl :
  ∀ (n : ℕ) (h : n < l.inits.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.inits n h = take n l
h : 0 < (a :: l).inits.length
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).inits 0 h = take 0 (a :: l)

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
a : α
l : List α
ihl :
  ∀ (n : ℕ) (h : n < l.inits.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.inits n h = take n l
n : ℕ
h : n + 1 < (a :: l).inits.length
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).inits (n + 1) h = take (n + 1) (a :: l)

Tactic:
simp [ihl]
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
a : α
l : List α
ihl :
  ∀ (n : ℕ) (h : n < l.inits.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.inits n h = take n l
n : ℕ
h : n < (a :: l).inits.length
cons :
  ∀ (h : 0 < (a :: l).inits.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).inits 0 h = take 0 (a :: l)
cons₁ :
  ∀ (n : ℕ) (h : n + 1 < (a :: l).inits.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).inits (n + 1) h = take (n + 1) (a :: l)
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).inits n h = take n (a :: l)

Tactic:
cases n with
    | zero => simp
    | succ n => simp [ihl]
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
n : ℕ
h : n < l.inits.length
nil :
  ∀ (n : ℕ) (h : n < length.{u_1} (α := List α) (inits [])),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (inits []) n h = take n []
cons :
  ∀ (a : α) (l : List α)
    (ihl :
      ∀ (n : ℕ) (h : n < l.inits.length),
        getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.inits n h = take n l)
    (n : ℕ) (h : n < (a :: l).inits.length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (a :: l).inits n h = take n (a :: l)
⊢ getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) l.inits n h = take n l

Tactic:
induction l generalizing n with
  | nil => simp
  | cons a l ihl =>
    cases n with
    | zero => simp
    | succ n => simp [ihl]

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
n : Fin l.inits.length
⊢ l.inits.get n = take (↑n : ℕ) l

Tactic:
simp
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
β : Type u_3
g : α → β
nil : (map g []).inits = map (map g) (inits [])
append_singleton :
  ∀ (l : List α) (a : α),
    (map g l).inits = map (map g) l.inits → (map g (l ++ [a])).inits = map (map g) (l ++ [a]).inits
⊢ (map g l).inits = map (map g) l.inits

Tactic:
induction l using reverseRecOn
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g []).inits = map (map g) (inits [])

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
β : Type u_3
g : α → β
l_1 : List α
a : α
h : (map g l_1).inits = map (map g) l_1.inits
⊢ (map g (l_1 ++ [a])).inits = map (map g) (l_1 ++ [a]).inits

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
β : Type u_3
g : α → β
nil : (map g []).tails = map (map g) (tails [])
append_singleton :
  ∀ (l : List α) (a : α),
    (map g l).tails = map (map g) l.tails → (map g (l ++ [a])).tails = map (map g) (l ++ [a]).tails
⊢ (map g l).tails = map (map g) l.tails

Tactic:
induction l using reverseRecOn
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
β : Type u_3
g : α → β
⊢ (map g []).tails = map (map g) (tails [])

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
β : Type u_3
g : α → β
l_1 : List α
a : α
h : (map g l_1).tails = map (map g) l_1.tails
⊢ (map g (l_1 ++ [a])).tails = map (map g) (l_1 ++ [a]).tails

Tactic:
simp [*]
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
n : ℕ
hl : (take n l).inits.length = (take (n + 1) l.inits).length
h :
  ∀ (i : ℕ) (h₁ : i < (take n l).inits.length) (h₂ : i < (take (n + 1) l.inits).length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take n l).inits i h₁ =
      getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take (n + 1) l.inits) i h₂
⊢ (take n l).inits = take (n + 1) l.inits

Tactic:
apply ext_getElem

Premises used: List.ext_getElem
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
n : ℕ
⊢ (take n l).inits.length = (take (n + 1) l.inits).length

Tactic:
simp [take_take]

Premises used: List.take_take
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
n : ℕ
h : ∀ (i : ℕ) (h₂ : i < min n l.length + 1), min i (min n l.length) = min i l.length
⊢ ∀ (i : ℕ) (h₁ : i < (take n l).inits.length) (h₂ : i < (take (n + 1) l.inits).length),
    getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take n l).inits i h₁ =
      getElem (valid := fun (as : List (List α)) (i : ℕ) ↦ i < as.length) (take (n + 1) l.inits) i h₂

Tactic:
simp [take_take]

Premises used: List.take_take
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
l : List α
n : ℕ
⊢ ∀ (i : ℕ) (h₂ : i < min n l.length + 1), min i (min n l.length) = min i l.length

Tactic:
omega
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
simp : insert a l = if elem a l = true then l else a :: l
⊢ insert a l = if a ∈ l then l else a :: l

Tactic:
simp only [← elem_iff]

Premises used: List.elem_iff
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
⊢ insert a l = if elem a l = true then l else a :: l

Tactic:
rfl
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
pos : ∀ (h : a ∈ l), l <:+ List.insert a l
neg : ∀ (h : ¬a ∈ l), l <:+ List.insert a l
⊢ l <:+ List.insert a l

Tactic:
by_cases h : a ∈ l
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ l <:+ List.insert a l

Tactic:
simp only [insert_of_mem h, suffix_refl]

Premises used: List.suffix_refl, List.insert_of_mem
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
h : ¬a ∈ l
⊢ l <:+ List.insert a l

Tactic:
simp only [insert_of_not_mem h, suffix_cons]

Premises used: List.suffix_cons, List.insert_of_not_mem
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
⊢ l <:+: List.insert a l

Tactic:
(suffix_insert a l).isInfix

Premises used: List.suffix_insert, List.IsSuffix.isInfix
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
⊢ l <+ List.insert a l

Tactic:
(suffix_insert a l).sublist

Premises used: List.suffix_insert, List.IsSuffix.sublist
-- Module: Mathlib.Data.List.Infix
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
⊢ l ⊆ List.insert a l

Tactic:
(sublist_insert a l).subset

Premises used: List.Sublist.subset, List.sublist_insert
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
n : ℕ
a : α
⊢ l <+ l.insertIdx n a

Tactic:
simpa only [eraseIdx_insertIdx_self] using eraseIdx_sublist (l.insertIdx n a) n

Premises used: List.insertIdx, List.eraseIdx_insertIdx_self, List.eraseIdx_sublist
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
n : ℕ
a : α
⊢ l ⊆ l.insertIdx n a

Tactic:
(sublist_insertIdx ..).subset

Premises used: List.Sublist.subset, List.sublist_insertIdx
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
n : ℕ
hn : n ≠ l.length
a : α
zero : ∀ {l : List α} (hn : 0 ≠ l.length), (l.eraseIdx 0).insertIdx 0 a = l.set 0 a
succ :
  ∀ (n : ℕ),
    (∀ {l : List α} (hn : n ≠ l.length), (l.eraseIdx n).insertIdx n a = l.set n a) →
      ∀ {l : List α} (hn : n + 1 ≠ l.length), (l.eraseIdx (n + 1)).insertIdx (n + 1) a = l.set (n + 1) a
⊢ (l.eraseIdx n).insertIdx n a = l.set n a

Tactic:
induction n generalizing l
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
a : α
l : List α
hn : 0 ≠ l.length
zero : ∀ (hn : 0 ≠ length.{u} (α := α) []), insertIdx (eraseIdx [] 0) 0 a = set [] 0 a
zero₁ :
  ∀ (head : α) (tail : List α) (hn : 0 ≠ (head :: tail).length),
    ((head :: tail).eraseIdx 0).insertIdx 0 a = (head :: tail).set 0 a
⊢ (l.eraseIdx 0).insertIdx 0 a = l.set 0 a

Tactic:
cases l
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {l : List α} (hn : n ≠ l.length), (l.eraseIdx n).insertIdx n a = l.set n a
l : List α
hn : n + 1 ≠ l.length
succ : ∀ (hn : n + 1 ≠ length.{u} (α := α) []), insertIdx (eraseIdx [] (n + 1)) (n + 1) a = set [] (n + 1) a
succ₁ :
  ∀ (head : α) (tail : List α) (hn : n + 1 ≠ (head :: tail).length),
    ((head :: tail).eraseIdx (n + 1)).insertIdx (n + 1) a = (head :: tail).set (n + 1) a
⊢ (l.eraseIdx (n + 1)).insertIdx (n + 1) a = l.set (n + 1) a

Tactic:
cases l
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
a : α
hn : 0 ≠ length.{u} (α := α) []
⊢ insertIdx (eraseIdx [] 0) 0 a = set [] 0 a

Tactic:
simp_all
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
a head : α
tail : List α
hn : 0 ≠ (head :: tail).length
⊢ ((head :: tail).eraseIdx 0).insertIdx 0 a = (head :: tail).set 0 a

Tactic:
simp_all
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {l : List α} (hn : n ≠ l.length), (l.eraseIdx n).insertIdx n a = l.set n a
hn : n + 1 ≠ length.{u} (α := α) []
⊢ insertIdx (eraseIdx [] (n + 1)) (n + 1) a = set [] (n + 1) a

Tactic:
simp_all
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
a : α
n : ℕ
h : ∀ {l : List α} (hn : n ≠ l.length), (l.eraseIdx n).insertIdx n a = l.set n a
head : α
tail : List α
hn : n + 1 ≠ (head :: tail).length
⊢ ((head :: tail).eraseIdx (n + 1)).insertIdx (n + 1) a = (head :: tail).set (n + 1) a

Tactic:
simp_all
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
n : ℕ
hn : n < l.length
⊢ (l.eraseIdx n).insertIdx n (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n hn) = l

Tactic:
simp [Nat.ne_of_lt hn]

Premises used: Nat.ne_of_lt
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l.insertIdx n b
hn : l.length < n
⊢ a ∈ l

Tactic:
rw [insertIdx_of_length_lt hn] at h

Premises used: List.insertIdx_of_length_lt
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l.insertIdx n b
hn : l.length < n
h₁ : a ∈ l
⊢ l.length < n

Tactic:
rw [insertIdx_of_length_lt hn] at h

Premises used: List.insertIdx_of_length_lt
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l
hn : l.length < n
⊢ a = b ∨ a ∈ l

Tactic:
.inr h

Premises used: Or.inr
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l
hn : l.length < n
⊢ a = b ∨ a ∈ l

Tactic:
exact .inr h
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l.insertIdx n b
hn : l.length ≥ n
inr inr₁ inr₂ inr₃ : ∀ (h : a = b ∨ a ∈ l) (hn : l.length ≥ n), a = b ∨ a ∈ l
⊢ a = b ∨ a ∈ l

Tactic:
rwa [mem_insertIdx hn] at h

Premises used: List.mem_insertIdx
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
n : ℕ
a b : α
h : a ∈ l.insertIdx n b
⊢ l.length < n ∨ l.length ≥ n

Tactic:
cases Nat.lt_or_ge (length l) n with
  | inl hn =>
    rw [insertIdx_of_length_lt hn] at h
    exact .inr h
  | inr hn =>
    rwa [mem_insertIdx hn] at h

Premises used: Nat.lt_or_ge, List.length
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
n : ℕ
a : α
l : List α
b : α
hb : b ∈ l.insertIdx n a
⊢ b ∈ a :: l

Tactic:
simpa using eq_or_mem_of_mem_insertIdx hb

Premises used: List.eq_or_mem_of_mem_insertIdx
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
l : List α
hl : ∀ (x : α), x ∈ l → p x
zero :
  ∀ (hl : ∀ (x : α), Membership.mem (γ := List α) [] x → p x),
    (pmap (P := p) f [] hl).insertIdx 0 (f a ha) = pmap (P := p) f (insertIdx [] 0 a) ⋯
zero₁ :
  ∀ (head : α) (tail : List α) (hl : ∀ (x : α), x ∈ head :: tail → p x),
    (pmap (P := p) f (head :: tail) hl).insertIdx 0 (f a ha) = pmap (P := p) f ((head :: tail).insertIdx 0 a) ⋯
⊢ (pmap (P := p) f l hl).insertIdx 0 (f a ha) = pmap (P := p) f (l.insertIdx 0 a) ⋯

Tactic:
cases l
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
hl : ∀ (x : α), Membership.mem (γ := List α) [] x → p x
⊢ (pmap (P := p) f [] hl).insertIdx 0 (f a ha) = pmap (P := p) f (insertIdx [] 0 a) ⋯

Tactic:
simp
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
head : α
tail : List α
hl : ∀ (x : α), x ∈ head :: tail → p x
⊢ (pmap (P := p) f (head :: tail) hl).insertIdx 0 (f a ha) = pmap (P := p) f ((head :: tail).insertIdx 0 a) ⋯

Tactic:
simp
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
n : ℕ
ihn :
  ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x),
    (pmap (P := p) f l hl).insertIdx n (f a ha) = pmap (P := p) f (l.insertIdx n a) ⋯
l : List α
hl : ∀ (x : α), x ∈ l → p x
succ :
  ∀ (hl : ∀ (x : α), Membership.mem (γ := List α) [] x → p x),
    (pmap (P := p) f [] hl).insertIdx (n + 1) (f a ha) = pmap (P := p) f (insertIdx [] (n + 1) a) ⋯
succ₁ :
  ∀ (head : α) (tail : List α) (hl : ∀ (x : α), x ∈ head :: tail → p x),
    (pmap (P := p) f (head :: tail) hl).insertIdx (n + 1) (f a ha) =
      pmap (P := p) f ((head :: tail).insertIdx (n + 1) a) ⋯
⊢ (pmap (P := p) f l hl).insertIdx (n + 1) (f a ha) = pmap (P := p) f (l.insertIdx (n + 1) a) ⋯

Tactic:
cases l
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
n : ℕ
ihn :
  ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x),
    (pmap (P := p) f l hl).insertIdx n (f a ha) = pmap (P := p) f (l.insertIdx n a) ⋯
hl : ∀ (x : α), Membership.mem (γ := List α) [] x → p x
⊢ (pmap (P := p) f [] hl).insertIdx (n + 1) (f a ha) = pmap (P := p) f (insertIdx [] (n + 1) a) ⋯

Tactic:
simp_all
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
n : ℕ
ihn :
  ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x),
    (pmap (P := p) f l hl).insertIdx n (f a ha) = pmap (P := p) f (l.insertIdx n a) ⋯
head : α
tail : List α
hl : ∀ (x : α), x ∈ head :: tail → p x
⊢ (pmap (P := p) f (head :: tail) hl).insertIdx (n + 1) (f a ha) =
    pmap (P := p) f ((head :: tail).insertIdx (n + 1) a) ⋯

Tactic:
simp_all
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
a : α
n : ℕ
hl : ∀ (x : α), x ∈ l → p x
ha : p a
zero :
  ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x),
    (pmap (P := p) f l hl).insertIdx 0 (f a ha) = pmap (P := p) f (l.insertIdx 0 a) ⋯
succ :
  ∀ (n : ℕ)
    (ihn :
      ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x),
        (pmap (P := p) f l hl).insertIdx n (f a ha) = pmap (P := p) f (l.insertIdx n a) ⋯)
    {l : List α} (hl : ∀ (x : α), x ∈ l → p x),
    (pmap (P := p) f l hl).insertIdx (n + 1) (f a ha) = pmap (P := p) f (l.insertIdx (n + 1) a) ⋯
⊢ (pmap (P := p) f l hl).insertIdx n (f a ha) = pmap (P := p) f (l.insertIdx n a) ⋯

Tactic:
induction n generalizing l with
  | zero => cases l <;> simp
  | succ n ihn => cases l <;> simp_all

Premises used: Nat.zero, Nat.succ
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
β : Type v
f : α → β
l : List α
n : ℕ
a : α
⊢ map f (l.insertIdx n a) = (map f l).insertIdx n (f a)

Tactic:
simpa only [pmap_eq_map] using (insertIdx_pmap (fun a _ ↦ f a) (fun _ _ ↦ trivial) trivial).symm

Premises used: trivial, List.insertIdx_pmap, Eq.symm, List.pmap_eq_map
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
hl : ∀ (a : α), a ∈ l → p a
n_1 : ℕ
a : α
as : List α
h : ∀ (a_1 : α), a_1 ∈ a :: as → p a_1
n : ℕ
rw :
  ∀ (h_1 : p a ∧ ∀ (x : α), x ∈ as → p x) (n : ℕ),
    (pmap (P := p) f (a :: as) h).eraseIdx (n + 1) = pmap (P := p) f ((a :: as).eraseIdx (n + 1)) ⋯
⊢ (pmap (P := p) f (a :: as) h).eraseIdx (n + 1) = pmap (P := p) f ((a :: as).eraseIdx (n + 1)) ⋯

Tactic:
rw [forall_mem_cons] at h

Premises used: List.forall_mem_cons
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
hl : ∀ (a : α), a ∈ l → p a
n_1 : ℕ
a : α
as : List α
h_1 : ∀ (a_1 : α), a_1 ∈ a :: as → p a_1
h : p a ∧ ∀ (x : α), x ∈ as → p x
n : ℕ
⊢ (pmap (P := p) f (a :: as) h_1).eraseIdx (n + 1) = pmap (P := p) f ((a :: as).eraseIdx (n + 1)) ⋯

Tactic:
simp [eraseIdx_pmap f h.2 n]

Premises used: And.right
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
β : Type v
f : α → β
l : List α
n : ℕ
⊢ (map f l).eraseIdx n = map f (l.eraseIdx n)

Tactic:
simpa only [pmap_eq_map] using eraseIdx_pmap (fun a _ ↦ f a) (fun _ _ ↦ trivial) n

Premises used: trivial, List.eraseIdx_pmap, List.pmap_eq_map
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
x : α
n k : ℕ
hn : k < n
hk : k < l.length
hk' : k < (l.insertIdx n x).length
⊢ (l.insertIdx n x).get (⟨k, hk'⟩ : Fin (l.insertIdx n x).length) = l.get (⟨k, hk⟩ : Fin l.length)

Tactic:
simp_all [getElem_insertIdx_of_lt]

Premises used: List.getElem_insertIdx_of_lt
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
β : Type v
a : α
l : List α
x : α
n : ℕ
hn : n ≤ l.length
rwa : n < l.length + 1
rwa₁ rwa₂ rwa₃ rwa₄ : n ≤ l.length
⊢ n < (l.insertIdx n x).length

Tactic:
rwa [length_insertIdx_of_le_length hn, Nat.lt_succ_iff]

Premises used: List.length_insertIdx_of_le_length, Nat.lt_succ_iff
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
x : α
n : ℕ
hn : n ≤ l.length
hn' : n < (l.insertIdx n x).length
⊢ (l.insertIdx n x).get (⟨n, hn'⟩ : Fin (l.insertIdx n x).length) = x

Tactic:
simp
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
β : Type v
a : α
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
⊢ n ≤ l.length

Tactic:
lia
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
β : Type v
a : α
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
rwa : n + k + 1 < l.length + 1
rwa₁ rwa₂ rwa₃ rwa₄ : n + k < l.length
⊢ n + k + 1 < (l.insertIdx n x).length

Tactic:
rwa [length_insertIdx_of_le_length (by lia), Nat.succ_lt_succ_iff]

Premises used: Nat.succ_lt_succ_iff, List.length_insertIdx_of_le_length
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
hk : n + k + 1 < (l.insertIdx n x).length
⊢ getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (l.insertIdx n x) (n + k + 1) hk =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l (n + k) hk'

Tactic:
grind
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
hk : n + k + 1 < (l.insertIdx n x).length
⊢ (l.insertIdx n x).get (⟨n + k + 1, hk⟩ : Fin (l.insertIdx n x).length) = l.get (⟨n + k, hk'⟩ : Fin l.length)

Tactic:
simp [getElem_insertIdx_add_succ, hk']

Premises used: List.getElem_insertIdx_add_succ, List.getElem_insertIdx_add_succ._proof_2
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
n : ℕ
x : α
l₁ l₂ : List α
hl : Eq.{u + 1} (α := List α) ((fun (l : List α) ↦ l.insertIdx n x) l₁) ((fun (l : List α) ↦ l.insertIdx n x) l₂)
⊢ l₁ = l₂

Tactic:
simpa using congr($hl |>.eraseIdx n)
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
x : α
i j : ℕ
h : i ≤ j
⊢ (take i (l.insertIdx j x)).length = (take i l).length

Tactic:
grind
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
x : α
i j : ℕ
h : i ≤ j
⊢ ∀ (i_1 : ℕ) (h₁ : i_1 < (take i (l.insertIdx j x)).length) (h₂ : i_1 < (take i l).length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take i (l.insertIdx j x)) i_1 h₁ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take i l) i_1 h₂

Tactic:
grind
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
i j : ℕ
h : i ≤ j
⊢ (take i (l.eraseIdx j)).length = (take i l).length

Tactic:
grind
-- Module: Mathlib.Data.List.InsertIdx
Goal:
α : Type u
l : List α
i j : ℕ
h : i ≤ j
⊢ ∀ (i_1 : ℕ) (h₁ : i_1 < (take i (l.eraseIdx j)).length) (h₂ : i_1 < (take i l).length),
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take i (l.eraseIdx j)) i_1 h₁ =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (take i l) i_1 h₂

Tactic:
grind
-- Module: Mathlib.Data.List.Intervals
Goal:
n : ℕ
rw : range' 0 (n - 0) = range n
rw₁ : range' 0 n = range n
rw₂ rw₃ : range' 0 n = range' 0 n
⊢ Ico 0 n = range n

Tactic:
rw [Ico, Nat.sub_zero, range_eq_range']

Premises used: List.range_eq_range', Nat.sub_zero, List.Ico
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
⊢ (range' n (m - n)).length = m - n

Tactic:
simp [length_range']

Premises used: List.length_range'
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
⊢ Pairwise (fun (x1 x2 : ℕ) ↦ x1 < x2) (range' n (m - n))

Tactic:
simp [pairwise_lt_range']

Premises used: List.pairwise_lt_range', OfNat.ofNat
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
⊢ (range' n (m - n)).Nodup

Tactic:
simp [nodup_range']

Premises used: List.nodup_range', OfNat.ofNat
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
this : n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
⊢ l ∈ Ico n m ↔ n ≤ l ∧ l < m

Tactic:
simp [Ico, this]

Premises used: List.Ico
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
suffices : n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m
⊢ l ∈ Ico n m ↔ n ≤ l ∧ l < m

Tactic:
suffices n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m by simp [Ico, this]
-- Module: Mathlib.Data.List.Intervals
Goal:
n m l : ℕ
⊢ n ≤ l ∧ l < n + (m - n) ↔ n ≤ l ∧ l < m

Tactic:
lia
-- Module: Mathlib.Data.List.Intervals
Goal:
n m : ℕ
h : m ≤ n
⊢ Ico n m = []

Tactic:
simp [Ico, Nat.sub_eq_zero_iff_le.mpr h]

Premises used: Iff.mpr, Nat.sub_eq_zero_iff_le, List.Ico
-- Module: Mathlib.Data.List.Intervals
Goal:
n m k : ℕ
rw : map (fun (x : ℕ) ↦ k + x) (range' n (m - n)) = Ico (n + k) (m + k)
rw₁ : map (fun (x : ℕ) ↦ k + x) (range' n (m - n)) = range' (n + k) (m + k - (n + k))
rw₂ : range' (k + n) (m - n) = range' (n + k) (m + k - (n + k))
rw₃ : range' (k + n) (m - n) = range' (n + k) (m - n)
rw₄ rw₅ : range' (k + n) (m - n) = range' (k + n) (m - n)
⊢ map (fun (x : ℕ) ↦ k + x) (Ico n m) = Ico (n + k) (m + k)

Tactic:
rw [Ico, Ico, map_add_range', Nat.add_sub_add_right m k, Nat.add_comm n k]

Premises used: List.map_add_range', Nat.add_sub_add_right, List.Ico, Nat.add_comm
-- Module: Mathlib.Data.List.Intervals
Goal:
n m k : ℕ
h₁ : k ≤ n
rw : map (fun (x : ℕ) ↦ x - k) (range' n (m - n)) = Ico (n - k) (m - k)
rw₁ : map (fun (x : ℕ) ↦ x - k) (range' n (m - n)) = range' (n - k) (m - k - (n - k))
rw₂ : map (fun (x : ℕ) ↦ x - k) (range' n (m - n)) = range' (n - k) (m - n)
rw₃ rw₄ : range' (n - k) (m - n) = range' (n - k) (m - n)
⊢ map (fun (x : ℕ) ↦ x - k) (Ico n m) = Ico (n - k) (m - k)

Tactic:
rw [Ico, Ico, Nat.sub_sub_sub_cancel_right h₁, map_sub_range' h₁]

Premises used: Nat.sub_sub_sub_cancel_right, List.Ico, List.map_sub_range'