Theorem: Array.swap_comm (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
x : Array α
i j : Fin (size x)
⊢ swap x i j = swap x j i
Tactic:
refine Array.ext _ _ (by simp only [size_swap]) ?_
State after:
α : Type u
x : Array α
i j : Fin (size x)
⊢ ∀ (i_1 : Nat) (hi₁ : i_1 < size (swap x i j)) (hi₂ : i_1 < size (swap x j i)), (swap x i j)[i_1] = (swap x j i)[i_1]

State before:
α : Type u
x : Array α
i j : Fin (size x)
⊢ ∀ (i_1 : Nat) (hi₁ : i_1 < size (swap x i j)) (hi₂ : i_1 < size (swap x j i)), (swap x i j)[i_1] = (swap x j i)[i_1]
Tactic:
intro k hk hk'
State after:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
⊢ (swap x i j)[k] = (swap x j i)[k]

State before:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
⊢ (swap x i j)[k] = (swap x j i)[k]
Tactic:
simp only [getElem_swap]
State after:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]

State before:
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]
Tactic:
apply dite (i.1 = k) <;> apply dite (j.1 = k) <;> intros hjk hik
State after:
case t.t
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ↑j = k
hik : ↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]

case t.e
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ¬↑j = k
hik : ↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]

case e.t
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ↑j = k
hik : ¬↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]

case e.e
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ¬↑j = k
hik : ¬↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]

State before:
case t.t
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ↑j = k
hik : ↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]

case t.e
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ¬↑j = k
hik : ↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]

case e.t
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ↑j = k
hik : ¬↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]

case e.e
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ¬↑j = k
hik : ¬↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]
Tactic:
all_goals simp only [hik, hjk, if_true, if_false]
State after:
no goals

State before:
α : Type u
x : Array α
i j : Fin (size x)
⊢ size (swap x i j) = size (swap x j i)
Tactic:
simp only [size_swap]
State after:
no goals

State before:
case e.e
α : Type u
x : Array α
i j : Fin (size x)
k : Nat
hk : k < size (swap x i j)
hk' : k < size (swap x j i)
hjk : ¬↑j = k
hik : ¬↑i = k
⊢ (if ↑j = k then x[↑i] else if ↑i = k then x[↑j] else x[k]) = if ↑i = k then x[↑j] else if ↑j = k then x[↑i] else x[k]
Tactic:
simp only [hik, hjk, if_true, if_false]
State after:
no goals