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

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

State before:
α : Type u_1
as : Array α
i j : Fin as.size
⊢ (as.swap i j)[↑i] = as[↑j]
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))[↑i] = as[↑j]

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

case hj
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑i < (as.set i (as.get j)).size

State before:
α : Type u_1
as : Array α
i j : Fin as.size
⊢ (if ↑(⋯ ▸ j) = ↑i then as.get i else (as.set i (as.get j))[↑i]) = as[↑j]

case hj
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑i < (as.set i (as.get j)).size
Tactic:
split
State after:
case isTrue
α : Type u_1
as : Array α
i j : Fin as.size
h✝ : ↑(⋯ ▸ j) = ↑i
⊢ as.get i = as[↑j]

case isFalse
α : Type u_1
as : Array α
i j : Fin as.size
h✝ : ¬↑(⋯ ▸ j) = ↑i
⊢ (as.set i (as.get j))[↑i] = as[↑j]

case hj
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑i < (as.set i (as.get j)).size

State before:
case isTrue
α : Type u_1
as : Array α
i j : Fin as.size
h✝ : ↑(⋯ ▸ j) = ↑i
⊢ as.get i = as[↑j]

case isFalse
α : Type u_1
as : Array α
i j : Fin as.size
h✝ : ¬↑(⋯ ▸ j) = ↑i
⊢ (as.set i (as.get j))[↑i] = as[↑j]

case hj
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑i < (as.set i (as.get j)).size
Tactic:
next heq =>
  have : j.val = i.val := by
    rw [←heq]
    apply Fin.val_eq_val_of_heq
    rw [size_set]
    elim_casts
    reflexivity
  simp [get_eq_getElem, this]
State after:
case isFalse
α : Type u_1
as : Array α
i j : Fin as.size
h✝ : ¬↑(⋯ ▸ j) = ↑i
⊢ (as.set i (as.get j))[↑i] = as[↑j]

case hj
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑i < (as.set i (as.get j)).size

State before:
case isFalse
α : Type u_1
as : Array α
i j : Fin as.size
h✝ : ¬↑(⋯ ▸ j) = ↑i
⊢ (as.set i (as.get j))[↑i] = as[↑j]

case hj
α : Type u_1
as : Array α
i j : Fin as.size
⊢ ↑i < (as.set i (as.get j)).size
Tactic:
next =>
  rw [get_set_eq, get_eq_getElem]
State after:
no goals

State before:
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
⊢ as.get i = as[↑j]
Tactic:
have : j.val = i.val := by
  rw [←heq]
  apply Fin.val_eq_val_of_heq
  rw [size_set]
  elim_casts
  reflexivity
State after:
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
this : ↑j = ↑i
⊢ as.get i = as[↑j]

State before:
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
this : ↑j = ↑i
⊢ as.get i = as[↑j]
Tactic:
simp [get_eq_getElem, this]
State after:
no goals

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

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

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

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

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

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

State before:
case a
α : Type u_1
as : Array α
i j : Fin as.size
heq : ↑(⋯ ▸ j) = ↑i
⊢ j ≅ j
Tactic:
reflexivity
State after:
no goals

State before:
α : Type u_1
as : Array α
i j : Fin as.size
h✝ : ¬↑(⋯ ▸ j) = ↑i
⊢ (as.set i (as.get j))[↑i] = as[↑j]
Tactic:
rw [get_set_eq, get_eq_getElem]
State after:
no goals