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

State before:
α : Type ?u.4204
as : Array α
i j : Fin as.size
⊢ ↑j < (as.swap i j).size
Tactic:
simp [j.isLt]
State after:
no goals

State before:
α : Type u_1
as : Array α
i j : Fin as.size
⊢ (as.swap i j)[↑j] = as[↑i]
Tactic:
simp only [swap]
State after:
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ((as.set i (as.get j)).set (⋯ ▸ j) (as.get i))[↑j] = as[↑i]

State before:
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ((as.set i (as.get j)).set (⋯ ▸ j) (as.get i))[↑j] = as[↑i]
Tactic:
rw [get_set_of_eq]
State after:
α : Type u_1
as : Array α
i j : Fin as.size
⊢ as.get i = as[↑i]

case a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑(⋯ ▸ j) = ↑j

State before:
α : Type u_1
as : Array α
i j : Fin as.size
⊢ as.get i = as[↑i]

case a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑(⋯ ▸ j) = ↑j
Tactic:
rw [get_eq_getElem]
State after:
case a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑(⋯ ▸ j) = ↑j

State before:
case a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑(⋯ ▸ j) = ↑j
Tactic:
apply Fin.val_eq_val_of_heq
State after:
case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ (as.set i (as.get j)).size = as.size

case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ⋯ ▸ j ≅ j

State before:
case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ (as.set i (as.get j)).size = as.size

case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ⋯ ▸ j ≅ j
Tactic:
rw [size_set]
State after:
case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ⋯ ▸ j ≅ j

State before:
case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ⋯ ▸ j ≅ j
Tactic:
elim_casts
State after:
case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ j ≅ j

State before:
case a.a
α : Type u_1
as : Array α
i j : Fin as.size
⊢ j ≅ j
Tactic:
reflexivity
State after:
no goals