Theorem: SizedArray.set_set_comm (Algdata/Data/Array/Sized.lean)

State before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
⊢ (set (set x i a) j b)[k] = (set (set x j b) i a)[k]
Tactic:
simp only [get_set_ite]
State after:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]

State before:
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]
Tactic:
apply dite (j.1 = k) <;> apply dite (i.1 = k) <;> intro hik hjk
State after:
case t.t
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]

case t.e
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]

case e.t
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]

case e.e
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]

State before:
case t.t
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]

case t.e
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]

case e.t
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]

case e.e
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]
Tactic:
all_goals simp only [hik, hjk, if_pos, if_neg]
State after:
case t.t
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ↑i = k
hjk : ↑j = k
⊢ b = a

State before:
case t.t
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ↑i = k
hjk : ↑j = k
⊢ b = a
Tactic:
cases hjk
State after:
case t.t.refl
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
hk : ↑j < n
hik : ↑i = ↑j
⊢ b = a

State before:
case t.t.refl
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
hk : ↑j < n
hik : ↑i = ↑j
⊢ b = a
Tactic:
exact absurd (Fin.eq_of_val_eq hik) h
State after:
no goals

State before:
case e.e
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
h : i ≠ j
a b : α
k : Nat
hk : k < n
hik : ¬↑i = k
hjk : ¬↑j = k
⊢ (if ↑j = k then b else if ↑i = k then a else x[k]) = if ↑i = k then a else if ↑j = k then b else x[k]
Tactic:
simp only [hik, hjk, if_pos, if_neg]
State after:
no goals