Theorem: ArrayLike.get_set_ite (Algdata/Classes/ArrayLike.lean)

State before:
cont : Type u
idx : Type v
elem : Type w
domGet : cont → idx → Prop
domSet : cont → idx → elem → Prop
inst✝¹ : ArrayLike cont idx elem domGet domSet
inst✝ : DecidableEq idx
xs : cont
i j : idx
e : elem
hi : domSet xs i e
hj : domGet (SetElem.setElem xs i e hi) j
⊢ (SetElem.setElem xs i e hi)[j] = if i = j then e else xs[j]
Tactic:
if h : i = j then
  cases h
  exact Eq.trans (get_set_eq xs i e) (if_pos rfl).symm
else
  exact Eq.trans (get_set_ne xs h e hj) (if_neg h).symm
State after:
no goals

State before:
cont : Type u
idx : Type v
elem : Type w
domGet : cont → idx → Prop
domSet : cont → idx → elem → Prop
inst✝¹ : ArrayLike cont idx elem domGet domSet
inst✝ : DecidableEq idx
xs : cont
i j : idx
e : elem
hi : domSet xs i e
hj : domGet (SetElem.setElem xs i e hi) j
h : i = j
⊢ (SetElem.setElem xs i e hi)[j] = if i = j then e else xs[j]
Tactic:
cases h
State after:
case refl
cont : Type u
idx : Type v
elem : Type w
domGet : cont → idx → Prop
domSet : cont → idx → elem → Prop
inst✝¹ : ArrayLike cont idx elem domGet domSet
inst✝ : DecidableEq idx
xs : cont
i : idx
e : elem
hi : domSet xs i e
hj : domGet (SetElem.setElem xs i e hi) i
⊢ (SetElem.setElem xs i e hi)[i] = if i = i then e else xs[i]

State before:
case refl
cont : Type u
idx : Type v
elem : Type w
domGet : cont → idx → Prop
domSet : cont → idx → elem → Prop
inst✝¹ : ArrayLike cont idx elem domGet domSet
inst✝ : DecidableEq idx
xs : cont
i : idx
e : elem
hi : domSet xs i e
hj : domGet (SetElem.setElem xs i e hi) i
⊢ (SetElem.setElem xs i e hi)[i] = if i = i then e else xs[i]
Tactic:
exact Eq.trans (get_set_eq xs i e) (if_pos rfl).symm
State after:
no goals

State before:
cont : Type u
idx : Type v
elem : Type w
domGet : cont → idx → Prop
domSet : cont → idx → elem → Prop
inst✝¹ : ArrayLike cont idx elem domGet domSet
inst✝ : DecidableEq idx
xs : cont
i j : idx
e : elem
hi : domSet xs i e
hj : domGet (SetElem.setElem xs i e hi) j
h : ¬i = j
⊢ (SetElem.setElem xs i e hi)[j] = if i = j then e else xs[j]
Tactic:
exact Eq.trans (get_set_ne xs h e hj) (if_neg h).symm
State after:
no goals