Theorem: Array.get_set_of_eq (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] = x
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] = x

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] = x
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] = x

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] = x
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]) = x

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]) = x
Tactic:
rw [if_pos h]
State after:
no goals