Theorem: Permutation.get_castAdd_ge (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] = { val := i, isLt := hi }
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 =
    { val := i, isLt := hi }

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 =
    { val := i, isLt := hi }
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] =
    { val := i, isLt := hi }

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] =
    { val := i, isLt := hi }
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] =
    { val := i, isLt := hi }

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] =
    { val := i, isLt := hi }
Tactic:
rewrite [Array.getElem_append_right _ _ ((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.ofFn fun i =>
        Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i - Array.size (Array.map (Fin.castAdd m) x.val)] =
    { val := i, isLt := hi }

State before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ (Array.ofFn fun i =>
        Fin.cast (_ : m + n = n + m) (Fin.addNat i n))[i - Array.size (Array.map (Fin.castAdd m) x.val)] =
    { val := i, isLt := hi }
Tactic:
rewrite [Array.getElem_ofFn]
State after:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ Fin.cast (_ : m + n = n + m)
      (Fin.addNat
        { val := i - Array.size (Array.map (Fin.castAdd m) x.val),
          isLt := (_ : i - Array.size (Array.map (Fin.castAdd m) x.val) < m) }
        n) =
    { val := i, isLt := hi }

State before:
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ Fin.cast (_ : m + n = n + m)
      (Fin.addNat
        { val := i - Array.size (Array.map (Fin.castAdd m) x.val),
          isLt := (_ : i - Array.size (Array.map (Fin.castAdd m) x.val) < m) }
        n) =
    { val := i, isLt := hi }
Tactic:
apply Fin.eq_of_val_eq
State after:
case a
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ ↑(Fin.cast (_ : m + n = n + m)
        (Fin.addNat
          { val := i - Array.size (Array.map (Fin.castAdd m) x.val),
            isLt := (_ : i - Array.size (Array.map (Fin.castAdd m) x.val) < m) }
          n)) =
    ↑{ val := i, isLt := hi }

State before:
case a
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ ↑(Fin.cast (_ : m + n = n + m)
        (Fin.addNat
          { val := i - Array.size (Array.map (Fin.castAdd m) x.val),
            isLt := (_ : i - Array.size (Array.map (Fin.castAdd m) x.val) < m) }
          n)) =
    ↑{ val := i, isLt := hi }
Tactic:
simp only [Array.size_map, Fin.addNat_mk, Fin.cast_mk, x.size_eq]
State after:
case a
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ i - n + n = i

State before:
case a
n m : Nat
x : Permutation n
i : Nat
hi : i < n + m
h : i ≥ n
this : i ≥ Array.size x.val
⊢ i - n + n = i
Tactic:
exact Nat.sub_add_cancel h
State after:
no goals