Theorem: List.modifyNth_modifyNth_ne (One.lean)

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₃]
State after:
no goals

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₃]
State after:
no goals

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]
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

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
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

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
State after:
no goals

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₂
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)

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₂]
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)

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₃]
State after:
no goals

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₂]
State after:
no goals

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₁
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)

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₁]
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)

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₃]
State after:
no goals

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₁]
State after:
no goals