Theorem: ArraySet.not_eq_getElem_of_not_mem (Aoc2023/Utils.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ¬x ∈ as
⊢ ∀ (i : Nat) (h : i < Array.size as.content), as.content[i] ≠ x
Tactic:
intro i hi
State after:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ¬x ∈ as
i : Nat
hi : i < Array.size as.content
⊢ as.content[i] ≠ x

State before:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ¬x ∈ as
i : Nat
hi : i < Array.size as.content
⊢ as.content[i] ≠ x
Tactic:
rw [mem_def, Array.mem_def, List.mem_iff_get, not_exists] at hx
State after:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ∀ (x_1 : Fin (List.length as.content.data)), ¬List.get as.content.data x_1 = x
i : Nat
hi : i < Array.size as.content
⊢ as.content[i] ≠ x

State before:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ∀ (x_1 : Fin (List.length as.content.data)), ¬List.get as.content.data x_1 = x
i : Nat
hi : i < Array.size as.content
⊢ as.content[i] ≠ x
Tactic:
specialize hx ⟨i, hi⟩
State after:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
i : Nat
hi : i < Array.size as.content
hx : ¬List.get as.content.data { val := i, isLt := hi } = x
⊢ as.content[i] ≠ x

State before:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
i : Nat
hi : i < Array.size as.content
hx : ¬List.get as.content.data { val := i, isLt := hi } = x
⊢ as.content[i] ≠ x
Tactic:
rwa [Array.getElem_eq_data_get]
State after:
no goals