Theorem: List.modifyNth_modifyNth_eq (One.lean)

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
State after:
i : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
⊢ modifyNth f i (modifyNth g i l) = modifyNth (f ∘ g) i l

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

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

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

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

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

State before:
i : ℕ
α✝ : Type u_1
f g : α✝ → α✝
l : List α✝
h₁ : length l ≤ i
⊢ length l ≤ i
Tactic:
simp only [modify_get?_length, h₁]
State after:
no goals