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

State before:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
⊢ ↑i ≠ k → ↑j ≠ k → (as.swap i j)[k] = as[k]
Tactic:
intro hik hjk
State after:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk : ↑j ≠ k
⊢ (as.swap i j)[k] = as[k]

State before:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk : ↑j ≠ k
⊢ (as.swap i j)[k] = as[k]
Tactic:
have hjk : ((size_set as i (get as j)).symm ▸ j).val ≠ k := by
  intro h
  cases h
  apply hjk
  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
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ (as.swap i j)[k] = as[k]

State before:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ (as.swap i j)[k] = as[k]
Tactic:
simp only [swap]
State after:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ ((as.set i (as.get j)).set (⋯ ▸ j) (as.get i))[k] = as[k]

State before:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ ((as.set i (as.get j)).set (⋯ ▸ j) (as.get i))[k] = as[k]
Tactic:
rw [get_set_of_ne]
State after:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ (as.set i (as.get j))[k] = as[k]

case a
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ ↑(⋯ ▸ j) ≠ k

State before:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ (as.set i (as.get j))[k] = as[k]

case a
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ ↑(⋯ ▸ j) ≠ k
Tactic:
rw [get_set_of_ne as hik]
State after:
case a
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ ↑(⋯ ▸ j) ≠ k

State before:
case a
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk✝ : ↑j ≠ k
hjk : ↑(⋯ ▸ j) ≠ k
⊢ ↑(⋯ ▸ j) ≠ k
Tactic:
exact hjk
State after:
no goals

State before:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk : ↑j ≠ k
⊢ ↑(⋯ ▸ j) ≠ k
Tactic:
intro h
State after:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk : ↑j ≠ k
h : ↑(⋯ ▸ j) = k
⊢ False

State before:
α : Type u_1
as : Array α
i j : Fin as.size
k : Nat
hk : k < (as.swap i j).size
hik : ↑i ≠ k
hjk : ↑j ≠ k
h : ↑(⋯ ▸ j) = k
⊢ False
Tactic:
cases h
State after:
case refl
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ False

State before:
case refl
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ False
Tactic:
apply hjk
State after:
case refl
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ ↑j = ↑(⋯ ▸ j)

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

case refl.a
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ j ≅ ⋯ ▸ j

State before:
case refl.a
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ as.size = (as.set i (as.get j)).size

case refl.a
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ j ≅ ⋯ ▸ j
Tactic:
rw [size_set]
State after:
case refl.a
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ j ≅ ⋯ ▸ j

State before:
case refl.a
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ j ≅ ⋯ ▸ j
Tactic:
elim_casts
State after:
case refl.a
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ j ≅ j

State before:
case refl.a
α : Type u_1
as : Array α
i j : Fin as.size
hk : ↑(⋯ ▸ j) < (as.swap i j).size
hik : ↑i ≠ ↑(⋯ ▸ j)
hjk : ↑j ≠ ↑(⋯ ▸ j)
⊢ j ≅ j
Tactic:
reflexivity
State after:
no goals