Theorem: List.set_set (One.lean)

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
State after:
i : ℕ
α✝ : Type u_1
l : List α✝
b a : α✝
⊢ set (set l i b) i a = set l i a

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

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

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

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