Theorem: Array.get_del (GMLInit/Data/Array/Basic.lean)

State before:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
⊢ (as.del k)[i] = if i = ↑k then as[as.size - 1] else as[i]
Tactic:
have hi' : i ≠ as.size - 1 := Nat.ne_of_lt <| size_del as k ▸ hi
State after:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (as.del k)[i] = if i = ↑k then as[as.size - 1] else as[i]

State before:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (as.del k)[i] = if i = ↑k then as[as.size - 1] else as[i]
Tactic:
simp only [del]
State after:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (as.swap k ⟨as.size - 1, ⋯⟩).pop[i] = if i = ↑k then as[as.size - 1] else as[i]

State before:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (as.swap k ⟨as.size - 1, ⋯⟩).pop[i] = if i = ↑k then as[as.size - 1] else as[i]
Tactic:
rw [get_pop]
State after:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (as.swap k ⟨as.size - 1, ⋯⟩)[i] = if i = ↑k then as[as.size - 1] else as[i]

State before:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (as.swap k ⟨as.size - 1, ⋯⟩)[i] = if i = ↑k then as[as.size - 1] else as[i]
Tactic:
rw [get_swap]
State after:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (if i = ↑k then as[⟨as.size - 1, ⋯⟩] else if i = ↑⟨as.size - 1, ⋯⟩ then as[k] else as[i]) =
    if i = ↑k then as[as.size - 1] else as[i]

case hk
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ i < as.size

State before:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (if i = ↑k then as[⟨as.size - 1, ⋯⟩] else if i = ↑⟨as.size - 1, ⋯⟩ then as[k] else as[i]) =
    if i = ↑k then as[as.size - 1] else as[i]

case hk
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ i < as.size
Tactic:
rw [if_neg hi']
State after:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (if i = ↑k then as[⟨as.size - 1, ⋯⟩] else as[i]) = if i = ↑k then as[as.size - 1] else as[i]

case hk
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ i < as.size

case hk
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ i < as.size

State before:
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ (if i = ↑k then as[⟨as.size - 1, ⋯⟩] else as[i]) = if i = ↑k then as[as.size - 1] else as[i]

case hk
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ i < as.size

case hk
α : Type u_1
as : Array α
k : Fin as.size
i : Nat
hi : i < (as.del k).size
hi' : i ≠ as.size - 1
⊢ i < as.size
Tactic:
rfl
State after:
no goals