Theorem: Array.get_push' (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
a : α
as : Array α
i : Nat
h : i < size (push as a)
⊢ (push as a)[i] = if h : i < size as then as[i] else a
Tactic:
cases as with | mk l =>
simp only [getElem_eq_data_get]
dsimp [push, size] at h ⊢
rw [List.get_of_eq (l.concat_eq_append a)]
if hil : i < l.length
then rw [dif_pos hil]; apply List.get_append_left
else
  rw [dif_neg hil]
  have : i = l.length := by
    refine Nat.le_antisymm ?_ (Nat.ge_of_not_lt hil)
    rw [l.length_concat a] at h
    exact Nat.le_of_succ_le_succ h
  simp only [this]
  exact l.get_concat_length a _
State after:
no goals

State before:
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < size (push { data := l } a)
⊢ (push { data := l } a)[i] = if h : i < size { data := l } then { data := l }[i] else a
Tactic:
simp only [getElem_eq_data_get]
State after:
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < size (push { data := l } a)
⊢ List.get (push { data := l } a).data { val := i, isLt := h } =
    if h : i < size { data := l } then List.get l { val := i, isLt := (_ : i < size { data := l }) } else a

State before:
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < size (push { data := l } a)
⊢ List.get (push { data := l } a).data { val := i, isLt := h } =
    if h : i < size { data := l } then List.get l { val := i, isLt := (_ : i < size { data := l }) } else a
Tactic:
dsimp [push, size] at h ⊢
State after:
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
⊢ List.get (List.concat l a) { val := i, isLt := h } =
    if h : i < List.length l then List.get l { val := i, isLt := (_ : i < List.length l) } else a

State before:
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
⊢ List.get (List.concat l a) { val := i, isLt := h } =
    if h : i < List.length l then List.get l { val := i, isLt := (_ : i < List.length l) } else a
Tactic:
rw [List.get_of_eq (l.concat_eq_append a)]
State after:
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    if h : i < List.length l then List.get l { val := i, isLt := (_ : i < List.length l) } else a

State before:
case mk
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    if h : i < List.length l then List.get l { val := i, isLt := (_ : i < List.length l) } else a
Tactic:
if hil : i < l.length
then rw [dif_pos hil]; apply List.get_append_left
else
  rw [dif_neg hil]
  have : i = l.length := by
    refine Nat.le_antisymm ?_ (Nat.ge_of_not_lt hil)
    rw [l.length_concat a] at h
    exact Nat.le_of_succ_le_succ h
  simp only [this]
  exact l.get_concat_length a _
State after:
no goals

State before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : i < List.length l
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    if h : i < List.length l then List.get l { val := i, isLt := (_ : i < List.length l) } else a
Tactic:
rw [dif_pos hil]
State after:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : i < List.length l
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    List.get l { val := i, isLt := (_ : i < List.length l) }

State before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : i < List.length l
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    List.get l { val := i, isLt := (_ : i < List.length l) }
Tactic:
apply List.get_append_left
State after:
no goals

State before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    if h : i < List.length l then List.get l { val := i, isLt := (_ : i < List.length l) } else a
Tactic:
rw [dif_neg hil]
State after:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    a

State before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    a
Tactic:
have : i = l.length := by
  refine Nat.le_antisymm ?_ (Nat.ge_of_not_lt hil)
  rw [l.length_concat a] at h
  exact Nat.le_of_succ_le_succ h
State after:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
this : i = List.length l
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    a

State before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
this : i = List.length l
⊢ List.get (l ++ [a])
      { val := ↑{ val := i, isLt := h }, isLt := (_ : ↑{ val := i, isLt := h } < List.length (l ++ [a])) } =
    a
Tactic:
simp only [this]
State after:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
this : i = List.length l
⊢ List.get (l ++ [a]) { val := List.length l, isLt := (_ : List.length l < List.length (l ++ [a])) } = a

State before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
this : i = List.length l
⊢ List.get (l ++ [a]) { val := List.length l, isLt := (_ : List.length l < List.length (l ++ [a])) } = a
Tactic:
exact l.get_concat_length a _
State after:
no goals

State before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
⊢ i = List.length l
Tactic:
refine Nat.le_antisymm ?_ (Nat.ge_of_not_lt hil)
State after:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
⊢ i ≤ List.length l

State before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length (List.concat l a)
hil : ¬i < List.length l
⊢ i ≤ List.length l
Tactic:
rw [l.length_concat a] at h
State after:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length l + 1
hil : ¬i < List.length l
⊢ i ≤ List.length l

State before:
α : Type u
a : α
i : Nat
l : List α
h : i < List.length l + 1
hil : ¬i < List.length l
⊢ i ≤ List.length l
Tactic:
exact Nat.le_of_succ_le_succ h
State after:
no goals