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

State before:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
⊢ ↑i ≠ j → (as.set i x)[j] = as[j]
Tactic:
intro h
State after:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i ≠ j
⊢ (as.set i x)[j] = as[j]

State before:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i ≠ j
⊢ (as.set i x)[j] = as[j]
Tactic:
have hj' : j < as.size := as.size_set i x ▸ hj
State after:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i ≠ j
hj' : j < as.size
⊢ (as.set i x)[j] = as[j]

State before:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i ≠ j
hj' : j < as.size
⊢ (as.set i x)[j] = as[j]
Tactic:
rw [as.get_set i j hj']
State after:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i ≠ j
hj' : j < as.size
⊢ (if ↑i = j then x else as[j]) = as[j]

State before:
α : Type u_1
as : Array α
i : Fin as.size
j : Nat
x : α
hj : j < (as.set i x).size
h : ↑i ≠ j
hj' : j < as.size
⊢ (if ↑i = j then x else as[j]) = as[j]
Tactic:
rw [if_neg h]
State after:
no goals