Theorem: Permutation.get_castAdd_ite (Fifteen/Data/Permutation/Basic.lean)

State before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
⊢ (castAdd m x)[i] = if h : i < n then Fin.castAdd m x[i] else { val := i, isLt := hi }
Tactic:
if h : i < n then
  rewrite [dif_pos h]; exact x.get_castAdd_lt m i h
else
  rewrite [dif_neg h]; exact x.get_castAdd_ge m i (Nat.le_of_not_lt h)
State after:
no goals

State before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
⊢ (castAdd m x)[i] = if h : i < n then Fin.castAdd m x[i] else { val := i, isLt := hi }
Tactic:
rewrite [dif_pos h]
State after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
⊢ (castAdd m x)[i] = Fin.castAdd m x[i]

State before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
⊢ (castAdd m x)[i] = Fin.castAdd m x[i]
Tactic:
exact x.get_castAdd_lt m i h
State after:
no goals

State before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : ¬i < n
⊢ (castAdd m x)[i] = if h : i < n then Fin.castAdd m x[i] else { val := i, isLt := hi }
Tactic:
rewrite [dif_neg h]
State after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : ¬i < n
⊢ (castAdd m x)[i] = { val := i, isLt := hi }

State before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : ¬i < n
⊢ (castAdd m x)[i] = { val := i, isLt := hi }
Tactic:
exact x.get_castAdd_ge m i (Nat.le_of_not_lt h)
State after:
no goals