internlm/Lean-Github huggingface dataset:
Theorem: List.map_modifyLast
Proof state before:
α✝ : Type u_1
β✝ : Type u_2
f : α✝ → β✝
h : α✝ → α✝
g : β✝ → β✝
l : List α✝
P : Function.Semiconj f h g
heq : ¬l = []
⊢ map f (modifyLast h l) = modifyLast g (map f l)
Tactic:
rw [← List.dropLast_append_getLast heq, List.modifyLast_append_one, map_append, map_append,
  map_singleton, map_singleton,List.modifyLast_append_one, P.eq]
Proof state after:
no goals
Theorem: List.map_dropLast
Proof state before:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
l : List α✝¹
⊢ map f (dropLast l) = dropLast (map f l)
Tactic:
simp only [dropLast_eq_take, map_take, length_map]
Proof state after:
no goals
Theorem: Int.not_newline_mem_reprΔ
Proof state before:
n : ℤ
⊢ ¬Char.ofNat 10 ∈ reprΔ n
Tactic:
unfold reprΔ
Proof state after:
n : ℤ
⊢ ¬Char.ofNat 10 ∈
      match n with
      | ofNat m => Nat.toDigits 10 m
      | -[m+1] => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m)
Theorem: Int.not_newline_mem_reprΔ
Proof state before:
n : ℤ
⊢ ¬Char.ofNat 10 ∈
      match n with
      | ofNat m => Nat.toDigits 10 m
      | -[m+1] => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m)
Tactic:
intro contr
Proof state after:
n : ℤ
contr :
  Char.ofNat 10 ∈
    match n with
    | ofNat m => Nat.toDigits 10 m
    | -[m+1] => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m)
⊢ False
Theorem: Int.not_newline_mem_reprΔ
Proof state before:
n : ℤ
contr :
  Char.ofNat 10 ∈
    match n with
    | ofNat m => Nat.toDigits 10 m
    | -[m+1] => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m)
⊢ False
Tactic:
split at contr
Proof state after:
case h_1
i✝ : ℤ
m✝ : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 m✝
⊢ False

case h_2
i✝ : ℤ
m✝ : ℕ
contr : Char.ofNat 10 ∈ [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m✝)
⊢ False
Theorem: Int.not_newline_mem_reprΔ
Proof state before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 n
⊢ False
Tactic:
case h_1 n =>
    have isdig := Nat.toDigits_digits 10 n
    simp only [beq_iff_eq, List.all_eq_true, forall_true_left] at isdig
    have h := isdig '\n' contr
    simp only at h
Proof state after:
no goals
Theorem: Int.not_newline_mem_reprΔ
Proof state before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ n)
⊢ False
Tactic:
case h_2 n =>
  simp only [List.singleton_append, List.find?, List.mem_cons, false_or] at contr
  have isdig := Nat.toDigits_digits 10 (Nat.succ n)
  simp only [beq_iff_eq, List.all_eq_true, forall_true_left] at isdig
  have h := isdig '\n' contr
  simp only at h
Proof state after:
no goals
Theorem: Int.not_newline_mem_reprΔ
Proof state before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 n
⊢ False
Tactic:
have isdig := Nat.toDigits_digits 10 n
Proof state after:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 n
isdig : 10 ≤ 10 → 10 > 1 → (List.all (Nat.toDigits 10 n) Char.isDigit == true) = true
⊢ False
Theorem: Int.not_newline_mem_reprΔ
Proof state before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 n
isdig : 10 ≤ 10 → 10 > 1 → (List.all (Nat.toDigits 10 n) Char.isDigit == true) = true
⊢ False
Tactic:
simp only [beq_iff_eq, List.all_eq_true, forall_true_left] at isdig
Proof state after:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 n
isdig : ∀ (x : Char), x ∈ Nat.toDigits 10 n → Char.isDigit x = true
⊢ False
Theorem: Int.not_newline_mem_reprΔ
Proof state before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 n
isdig : ∀ (x : Char), x ∈ Nat.toDigits 10 n → Char.isDigit x = true
⊢ False
Tactic:
have h := isdig '\n' contr
Proof state after:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 n
isdig : ∀ (x : Char), x ∈ Nat.toDigits 10 n → Char.isDigit x = true
h : Char.isDigit (Char.ofNat 10) = true
⊢ False
Theorem: Int.not_newline_mem_reprΔ
Proof state before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 n
isdig : ∀ (x : Char), x ∈ Nat.toDigits 10 n → Char.isDigit x = true
h : Char.isDigit (Char.ofNat 10) = true
⊢ False
Tactic:
simp only at h
Proof state after:
no goals
Theorem: Int.not_newline_mem_reprΔ
Proof state before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ n)
⊢ False
Tactic:
simp only [List.singleton_append, List.find?, List.mem_cons, false_or] at contr
Proof state after:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 (Nat.succ n)
⊢ False
Theorem: Int.not_newline_mem_reprΔ
Proof state before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 (Nat.succ n)
⊢ False
Tactic:
have isdig := Nat.toDigits_digits 10 (Nat.succ n)
Proof state after:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 (Nat.succ n)
isdig : 10 ≤ 10 → 10 > 1 → (List.all (Nat.toDigits 10 (Nat.succ n)) Char.isDigit == true) = true
⊢ False
Theorem: Int.not_newline_mem_reprΔ
Proof state before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 (Nat.succ n)
isdig : 10 ≤ 10 → 10 > 1 → (List.all (Nat.toDigits 10 (Nat.succ n)) Char.isDigit == true) = true
⊢ False
Tactic:
simp only [beq_iff_eq, List.all_eq_true, forall_true_left] at isdig
Proof state after:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 (Nat.succ n)
isdig : ∀ (x : Char), x ∈ Nat.toDigits 10 (Nat.succ n) → Char.isDigit x = true
⊢ False
Theorem: Int.not_newline_mem_reprΔ
Proof state before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 (Nat.succ n)
isdig : ∀ (x : Char), x ∈ Nat.toDigits 10 (Nat.succ n) → Char.isDigit x = true
⊢ False
Tactic:
have h := isdig '\n' contr
Proof state after:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 (Nat.succ n)
isdig : ∀ (x : Char), x ∈ Nat.toDigits 10 (Nat.succ n) → Char.isDigit x = true
h : Char.isDigit (Char.ofNat 10) = true
⊢ False
Theorem: Int.not_newline_mem_reprΔ
Proof state before:
i✝ : ℤ
n : ℕ
contr : Char.ofNat 10 ∈ Nat.toDigits 10 (Nat.succ n)
isdig : ∀ (x : Char), x ∈ Nat.toDigits 10 (Nat.succ n) → Char.isDigit x = true
h : Char.isDigit (Char.ofNat 10) = true
⊢ False
Tactic:
simp only at h
Proof state after:
no goals
Theorem: List.splitOnList_append
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
⊢ splitOnList delim (l₁ ++ l₂) = modifyLast (fun x => x ++ l₂) (splitOnList delim l₁)
Tactic:
unfold splitOnList
Proof state after:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
⊢ (match delim with
    | [] => [l₁ ++ l₂]
    | head :: tail =>
      Array.toList
        (Array.map Array.toList (splitOnListAux (head :: tail) (l₁ ++ l₂) #[] #[] (_ : ¬head :: tail = [])))) =
    modifyLast (fun x => x ++ l₂)
      (match delim with
      | [] => [l₁]
      | head :: tail =>
        Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) l₁ #[] #[] (_ : ¬head :: tail = []))))
Theorem: List.splitOnList_append
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬delim <:+: lastN (length delim - 1) l₁ ++ l₂
⊢ (match delim with
    | [] => [l₁ ++ l₂]
    | head :: tail =>
      Array.toList
        (Array.map Array.toList (splitOnListAux (head :: tail) (l₁ ++ l₂) #[] #[] (_ : ¬head :: tail = [])))) =
    modifyLast (fun x => x ++ l₂)
      (match delim with
      | [] => [l₁]
      | head :: tail =>
        Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) l₁ #[] #[] (_ : ¬head :: tail = []))))
Tactic:
match delim with
| [] => simp only [modifyLast_singleton]
| hd::tl => 
  simp only [Array.toList_eq, Array.map_data]
  rw [List.splitOnListAux_append _ _ h]
  rw [← map_modifyLast]
  . rw [Array.modifyLast_data]
  . unfold Function.Semiconj
    simp only [Array.toList_eq, Array.append_data, Array.data_toArray, forall_const]
Proof state after:
no goals
Theorem: List.splitOnList_append
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
h : ¬[] <:+: lastN (length [] - 1) l₁ ++ l₂
⊢ (match [] with
    | [] => [l₁ ++ l₂]
    | head :: tail =>
      Array.toList
        (Array.map Array.toList (splitOnListAux (head :: tail) (l₁ ++ l₂) #[] #[] (_ : ¬head :: tail = [])))) =
    modifyLast (fun x => x ++ l₂)
      (match [] with
      | [] => [l₁]
      | head :: tail =>
        Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) l₁ #[] #[] (_ : ¬head :: tail = []))))
Tactic:
simp only [modifyLast_singleton]
Proof state after:
no goals
Theorem: List.splitOnList_append
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ (match hd :: tl with
    | [] => [l₁ ++ l₂]
    | head :: tail =>
      Array.toList
        (Array.map Array.toList (splitOnListAux (head :: tail) (l₁ ++ l₂) #[] #[] (_ : ¬head :: tail = [])))) =
    modifyLast (fun x => x ++ l₂)
      (match hd :: tl with
      | [] => [l₁]
      | head :: tail =>
        Array.toList (Array.map Array.toList (splitOnListAux (head :: tail) l₁ #[] #[] (_ : ¬head :: tail = []))))
Tactic:
simp only [Array.toList_eq, Array.map_data]
Proof state after:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ map Array.toList (splitOnListAux (hd :: tl) (l₁ ++ l₂) #[] #[] (_ : ¬hd :: tl = [])).data =
    modifyLast (fun x => x ++ l₂) (map Array.toList (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = [])).data)
Theorem: List.splitOnList_append
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ map Array.toList (splitOnListAux (hd :: tl) (l₁ ++ l₂) #[] #[] (_ : ¬hd :: tl = [])).data =
    modifyLast (fun x => x ++ l₂) (map Array.toList (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = [])).data)
Tactic:
rw [List.splitOnListAux_append _ _ h]
Proof state after:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ map Array.toList
      (Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = []))).data =
    modifyLast (fun x => x ++ l₂) (map Array.toList (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = [])).data)
Theorem: List.splitOnList_append
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ map Array.toList
      (Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = []))).data =
    modifyLast (fun x => x ++ l₂) (map Array.toList (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = [])).data)
Tactic:
rw [← map_modifyLast]
Proof state after:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ map Array.toList
      (Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = []))).data =
    map Array.toList (modifyLast ?m.340731 (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = [])).data)

α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ Function.Semiconj Array.toList ?m.340731 fun x => x ++ l₂

α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ Array α → Array α
Theorem: List.splitOnList_append
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ map Array.toList
      (Array.modifyLast (fun x => x ++ toArray l₂) (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = []))).data =
    map Array.toList (modifyLast ?m.340731 (splitOnListAux (hd :: tl) l₁ #[] #[] (_ : ¬hd :: tl = [])).data)

α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ Function.Semiconj Array.toList ?m.340731 fun x => x ++ l₂

α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ Array α → Array α
Tactic:
. rw [Array.modifyLast_data]
Proof state after:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ Function.Semiconj Array.toList (fun x => x ++ toArray l₂) fun x => x ++ l₂
Theorem: List.splitOnList_append
Proof state before:
α : Type u_1
delim : List α
inst✝ : DecidableEq α
l₁ l₂ : List α
hd : α
tl : List α
h : ¬hd :: tl <:+: lastN (length (hd :: tl) - 1) l₁ ++ l₂
⊢ Function.Semiconj Array.toList (fun x => x ++ toArray l₂) fun x => x ++ l₂
Tactic:
. unfold Function.Semiconj
  simp only [Array.toList_eq, Array.append_data, Array.data_toArray, forall_const]
Proof state after:
no goals
Theorem: List.modifyHead_eq_modifyNth
Proof state before:
α : Type u_1
f : α → α
l : List α
⊢ modifyHead f l = modifyNth f 0 l
Tactic:
simp only [modifyNth, modifyHead, modifyNthTail]
Proof state after:
no goals
Theorem: List.modifyNth_ge_length
Proof state before:
α✝ : Type u_1
l : List α✝
i : ℕ
f : α✝ → α✝
h : length l ≤ i
⊢ modifyNth f i l = l
Tactic:
simp only [modifyNth_eq_set_get?, zero_le, ge_iff_le, nonpos_iff_eq_zero, List.get?_eq_none.2 h,
  Option.map_eq_map, Option.map_none', Option.getD_none]
Proof state after:
no goals
Theorem: List.modifyNth_modifyNth_ne
Proof state before:
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
if h₁: i < length l then
  if h₂: j < length l then
    rw [List.modifyNth_eq_set_get _ h₁, List.modifyNth_eq_set_get _ h₂, List.modifyNth_eq_set_get, List.modifyNth_eq_set_get, 
      set_comm, get_set_ne, get_set_ne] <;>
      simp only [h, h₁, h₂, ne_eq, not_false_iff,length_set]
    . apply Ne.symm h
    . apply Ne.symm h
  else
    simp only [not_lt] at h₂
    have h₃: length (modifyNth f i l) ≤ j := by simp only [modify_get?_length, h₂]
    rw [modifyNth_ge_length h₂, modifyNth_ge_length h₃]
else
  simp only [not_lt] at h₁
  have h₃: length (modifyNth g j l) ≤ i := by simp only [modify_get?_length, h₁]
  rw [modifyNth_ge_length h₁, modifyNth_ge_length h₃]
Proof state after:
no goals
Theorem: List.modifyNth_modifyNth_ne
Proof state before:
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : i < length l
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
if h₂: j < length l then
  rw [List.modifyNth_eq_set_get _ h₁, List.modifyNth_eq_set_get _ h₂, List.modifyNth_eq_set_get, List.modifyNth_eq_set_get, 
    set_comm, get_set_ne, get_set_ne] <;>
    simp only [h, h₁, h₂, ne_eq, not_false_iff,length_set]
  . apply Ne.symm h
  . apply Ne.symm h
else
  simp only [not_lt] at h₂
  have h₃: length (modifyNth f i l) ≤ j := by simp only [modify_get?_length, h₂]
  rw [modifyNth_ge_length h₂, modifyNth_ge_length h₃]
Proof state after:
no goals
Theorem: List.modifyNth_modifyNth_ne
Proof state before:
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : i < length l
h₂ : j < length l
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
rw [List.modifyNth_eq_set_get _ h₁, List.modifyNth_eq_set_get _ h₂, List.modifyNth_eq_set_get, List.modifyNth_eq_set_get, 
  set_comm, get_set_ne, get_set_ne] <;>
  simp only [h, h₁, h₂, ne_eq, not_false_iff,length_set]
Proof state after:
case h
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : i < length l
h₂ : j < length l
⊢ ¬j = i

case a
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : i < length l
h₂ : j < length l
⊢ ¬j = i
Theorem: List.modifyNth_modifyNth_ne
Proof state before:
case h
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : i < length l
h₂ : j < length l
⊢ ¬j = i

case a
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : i < length l
h₂ : j < length l
⊢ ¬j = i
Tactic:
. apply Ne.symm h
Proof state after:
case a
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : i < length l
h₂ : j < length l
⊢ ¬j = i
Theorem: List.modifyNth_modifyNth_ne
Proof state before:
case a
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : i < length l
h₂ : j < length l
⊢ ¬j = i
Tactic:
. apply Ne.symm h
Proof state after:
no goals
Theorem: List.modifyNth_modifyNth_ne
Proof state before:
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : i < length l
h₂ : ¬j < length l
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
simp only [not_lt] at h₂
Proof state after:
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : i < length l
h₂ : length l ≤ j
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Theorem: List.modifyNth_modifyNth_ne
Proof state before:
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : i < length l
h₂ : length l ≤ j
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
have h₃: length (modifyNth f i l) ≤ j := by simp only [modify_get?_length, h₂]
Proof state after:
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : i < length l
h₂ : length l ≤ j
h₃ : length (modifyNth f i l) ≤ j
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Theorem: List.modifyNth_modifyNth_ne
Proof state before:
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : i < length l
h₂ : length l ≤ j
h₃ : length (modifyNth f i l) ≤ j
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
rw [modifyNth_ge_length h₂, modifyNth_ge_length h₃]
Proof state after:
no goals
Theorem: List.modifyNth_modifyNth_ne
Proof state before:
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : i < length l
h₂ : length l ≤ j
⊢ length (modifyNth f i l) ≤ j
Tactic:
simp only [modify_get?_length, h₂]
Proof state after:
no goals
Theorem: List.modifyNth_modifyNth_ne
Proof state before:
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : ¬i < length l
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
simp only [not_lt] at h₁
Proof state after:
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : length l ≤ i
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Theorem: List.modifyNth_modifyNth_ne
Proof state before:
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : length l ≤ i
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
have h₃: length (modifyNth g j l) ≤ i := by simp only [modify_get?_length, h₁]
Proof state after:
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : length l ≤ i
h₃ : length (modifyNth g j l) ≤ i
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Theorem: List.modifyNth_modifyNth_ne
Proof state before:
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : length l ≤ i
h₃ : length (modifyNth g j l) ≤ i
⊢ modifyNth f i (modifyNth g j l) = modifyNth g j (modifyNth f i l)
Tactic:
rw [modifyNth_ge_length h₁, modifyNth_ge_length h₃]
Proof state after:
no goals
Theorem: List.modifyNth_modifyNth_ne
Proof state before:
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i ≠ j
h₁ : length l ≤ i
⊢ length (modifyNth g j l) ≤ i
Tactic:
simp only [modify_get?_length, h₁]
Proof state after:
no goals
Theorem: List.set_set
Proof state before:
i j : ℕ
α✝ : Type u_1
l : List α✝
b a : α✝
h : i = j
⊢ set (set l j b) i a = set l i a
Tactic:
subst j
Proof state after:
i : ℕ
α✝ : Type u_1
l : List α✝
b a : α✝
⊢ set (set l i b) i a = set l i a
Theorem: List.set_set
Proof state before:
i : ℕ
α✝ : Type u_1
l : List α✝
b a : α✝
⊢ set (set l i b) i a = set l i a
Tactic:
apply List.ext_get
Proof state after:
case hl
i : ℕ
α✝ : Type u_1
l : List α✝
b a : α✝
⊢ length (set (set l i b) i a) = length (set l i a)

case h
i : ℕ
α✝ : Type u_1
l : List α✝
b a : α✝
⊢ ∀ (n : ℕ) (h₁ : n < length (set (set l i b) i a)) (h₂ : n < length (set l i a)),
    get (set (set l i b) i a) { val := n, isLt := h₁ } = get (set l i a) { val := n, isLt := h₂ }
Theorem: List.set_set
Proof state before:
case hl
i : ℕ
α✝ : Type u_1
l : List α✝
b a : α✝
⊢ length (set (set l i b) i a) = length (set l i a)

case h
i : ℕ
α✝ : Type u_1
l : List α✝
b a : α✝
⊢ ∀ (n : ℕ) (h₁ : n < length (set (set l i b) i a)) (h₂ : n < length (set l i a)),
    get (set (set l i b) i a) { val := n, isLt := h₁ } = get (set l i a) { val := n, isLt := h₂ }
Tactic:
. simp only [length_set]
Proof state after:
case h
i : ℕ
α✝ : Type u_1
l : List α✝
b a : α✝
⊢ ∀ (n : ℕ) (h₁ : n < length (set (set l i b) i a)) (h₂ : n < length (set l i a)),
    get (set (set l i b) i a) { val := n, isLt := h₁ } = get (set l i a) { val := n, isLt := h₂ }
Theorem: List.set_set
Proof state before:
case h
i : ℕ
α✝ : Type u_1
l : List α✝
b a : α✝
⊢ ∀ (n : ℕ) (h₁ : n < length (set (set l i b) i a)) (h₂ : n < length (set l i a)),
    get (set (set l i b) i a) { val := n, isLt := h₁ } = get (set l i a) { val := n, isLt := h₂ }
Tactic:
. intro n _ _
  repeat rw [List.get_set]
  split <;> simp only
Proof state after:
no goals
Theorem: List.set_set
Proof state before:
case h
i : ℕ
α✝ : Type u_1
l : List α✝
b a : α✝
n : ℕ
h₁✝ : n < length (set (set l i b) i a)
h₂✝ : n < length (set l i a)
⊢ (if i = n then a else if i = n then b else get l { val := n, isLt := (_ : n < length l) }) =
    get (set l i a) { val := n, isLt := h₂✝ }
Tactic:
rw [List.get_set]
Proof state after:
case h
i : ℕ
α✝ : Type u_1
l : List α✝
b a : α✝
n : ℕ
h₁✝ : n < length (set (set l i b) i a)
h₂✝ : n < length (set l i a)
⊢ (if i = n then a else if i = n then b else get l { val := n, isLt := (_ : n < length l) }) =
    if i = n then a else get l { val := n, isLt := (_ : n < length l) }
Theorem: List.modifyNth_modifyNth_eq
Proof state before:
i j : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h : i = j
⊢ modifyNth f i (modifyNth g j l) = modifyNth (f ∘ g) i l
Tactic:
subst h
Proof state after:
i : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
⊢ modifyNth f i (modifyNth g i l) = modifyNth (f ∘ g) i l
Theorem: List.modifyNth_modifyNth_eq
Proof state before:
i : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
⊢ modifyNth f i (modifyNth g i l) = modifyNth (f ∘ g) i l
Tactic:
if h₁: i < length l then
  rw [List.modifyNth_eq_set_get _ h₁, List.modifyNth_eq_set_get _ h₁, List.modifyNth_eq_set_get,
    List.get_set_eq, set_set, Function.comp_apply] <;>
    simp only [h₁, length_set]
else
  simp only [not_lt] at h₁
  have h₃: length l ≤ i := by simp only [modify_get?_length, h₁]
  rw [modifyNth_ge_length h₁, modifyNth_ge_length h₃, modifyNth_ge_length h₁]
Proof state after:
no goals
Theorem: List.modifyNth_modifyNth_eq
Proof state before:
i : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h₁ : i < length l
⊢ modifyNth f i (modifyNth g i l) = modifyNth (f ∘ g) i l
Tactic:
rw [List.modifyNth_eq_set_get _ h₁, List.modifyNth_eq_set_get _ h₁, List.modifyNth_eq_set_get,
  List.get_set_eq, set_set, Function.comp_apply] <;>
  simp only [h₁, length_set]
Proof state after:
no goals
Theorem: List.modifyNth_modifyNth_eq
Proof state before:
i : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h₁ : ¬i < length l
⊢ modifyNth f i (modifyNth g i l) = modifyNth (f ∘ g) i l
Tactic:
simp only [not_lt] at h₁
Proof state after:
i : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h₁ : length l ≤ i
⊢ modifyNth f i (modifyNth g i l) = modifyNth (f ∘ g) i l
Theorem: List.modifyNth_modifyNth_eq
Proof state before:
i : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h₁ : length l ≤ i
⊢ modifyNth f i (modifyNth g i l) = modifyNth (f ∘ g) i l
Tactic:
have h₃: length l ≤ i := by simp only [modify_get?_length, h₁]
Proof state after:
i : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h₁ : length l ≤ i
h₃ : length l ≤ i
⊢ modifyNth f i (modifyNth g i l) = modifyNth (f ∘ g) i l
Theorem: List.modifyNth_modifyNth_eq
Proof state before:
i : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h₁ : length l ≤ i
h₃ : length l ≤ i
⊢ modifyNth f i (modifyNth g i l) = modifyNth (f ∘ g) i l
Tactic:
rw [modifyNth_ge_length h₁, modifyNth_ge_length h₃, modifyNth_ge_length h₁]
Proof state after:
no goals
Theorem: List.modifyNth_modifyNth_eq
Proof state before:
i : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h₁ : length l ≤ i
⊢ length l ≤ i
Tactic:
simp only [modify_get?_length, h₁]
Proof state after:
no goals