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

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:
unfold castAdd GetElem.getElem
State after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
⊢ instGetElemPermutationNatFinLtInstLTNat.1
      { val := Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n),
        size_eq :=
          (_ :
            Array.size
                (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n)) =
              n + m),
        nodup :=
          (_ :
            Array.Nodup
              (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))) }
      i hi =
    Fin.castAdd m (instGetElemPermutationNatFinLtInstLTNat.1 x i h)

State before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
⊢ instGetElemPermutationNatFinLtInstLTNat.1
      { val := Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n),
        size_eq :=
          (_ :
            Array.size
                (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n)) =
              n + m),
        nodup :=
          (_ :
            Array.Nodup
              (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))) }
      i hi =
    Fin.castAdd m (instGetElemPermutationNatFinLtInstLTNat.1 x i h)
Tactic:
simp only [instGetElemPermutationNatFinLtInstLTNat]
State after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
⊢ (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i] =
    Fin.castAdd m x.val[i]

State before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
⊢ (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i] =
    Fin.castAdd m x.val[i]
Tactic:
have : i < x.val.size := x.size_eq.symm ▸ h
State after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
this : i < Array.size x.val
⊢ (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i] =
    Fin.castAdd m x.val[i]

State before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
this : i < Array.size x.val
⊢ (Array.map (Fin.castAdd m) x.val ++ Array.ofFn fun i => Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i] =
    Fin.castAdd m x.val[i]
Tactic:
rewrite [Array.getElem_append_left _ _ ((Array.size_map _ _).symm ▸ this)]
State after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
this : i < Array.size x.val
⊢ (Array.map (Fin.castAdd m) x.val)[i] = Fin.castAdd m x.val[i]

State before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i < n
this : i < Array.size x.val
⊢ (Array.map (Fin.castAdd m) x.val)[i] = Fin.castAdd m x.val[i]
Tactic:
rw [Array.getElem_map]
State after:
no goals