Theorem: concat_aux_eqs
Proof state before:
α : Type
n m l p : ℕ
s : p + 1 + m = l
seq1 : FinSeq (p + 1) α
seq2 : FinSeq m α
k : ℕ
ss : p + (m + 1) = l :=
  Eq.mpr (id (congrArg (fun _a => p + (m + 1) = _a) s.symm))
    (Eq.mpr (id (congrArg (fun _a => p + _a = p + 1 + m) (Nat.add_comm m 1)))
      (Eq.mpr (id (congrArg (fun _a => p + (1 + m) = _a) (Nat.add_assoc p 1 m))) (Eq.refl (p + (1 + m)))))
resolve : concatSeqAux s seq1 seq2 = concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) := rfl
hyp : ∀ (k : ℕ),
  (∀ (kw : k < p) (w : k < l),
      concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) k w = FinSeq.init seq1 k kw) ∧
    ∀ (kw : k < m + 1) (w : p + k < l),
      concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + k) w = (FinSeq.last seq1+|seq2) k kw :=
  concat_aux_eqs ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2)
hyp1 : ∀ (kw : k < p) (w : k < l),
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) k w = FinSeq.init seq1 k kw :=
  (hyp k).left
⊢ (∀ (kw : k < p + 1) (w : k < l), concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) k w = seq1 k kw) ∧
    ∀ (kw : k < m) (w : p + 1 + k < l),
      concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + 1 + k) w = seq2 k kw
Tactic:
apply And.intro
Proof state after:
case left
α : Type
n m l p : ℕ
s : p + 1 + m = l
seq1 : FinSeq (p + 1) α
seq2 : FinSeq m α
k : ℕ
ss : p + (m + 1) = l :=
  Eq.mpr (id (congrArg (fun _a => p + (m + 1) = _a) s.symm))
    (Eq.mpr (id (congrArg (fun _a => p + _a = p + 1 + m) (Nat.add_comm m 1)))
      (Eq.mpr (id (congrArg (fun _a => p + (1 + m) = _a) (Nat.add_assoc p 1 m))) (Eq.refl (p + (1 + m)))))
resolve : concatSeqAux s seq1 seq2 = concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) := rfl
hyp : ∀ (k : ℕ),
  (∀ (kw : k < p) (w : k < l),
      concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) k w = FinSeq.init seq1 k kw) ∧
    ∀ (kw : k < m + 1) (w : p + k < l),
      concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + k) w = (FinSeq.last seq1+|seq2) k kw :=
  concat_aux_eqs ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2)
hyp1 : ∀ (kw : k < p) (w : k < l),
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) k w = FinSeq.init seq1 k kw :=
  (hyp k).left
⊢ ∀ (kw : k < p + 1) (w : k < l), concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) k w = seq1 k kw

case right
α : Type
n m l p : ℕ
s : p + 1 + m = l
seq1 : FinSeq (p + 1) α
seq2 : FinSeq m α
k : ℕ
ss : p + (m + 1) = l :=
  Eq.mpr (id (congrArg (fun _a => p + (m + 1) = _a) s.symm))
    (Eq.mpr (id (congrArg (fun _a => p + _a = p + 1 + m) (Nat.add_comm m 1)))
      (Eq.mpr (id (congrArg (fun _a => p + (1 + m) = _a) (Nat.add_assoc p 1 m))) (Eq.refl (p + (1 + m)))))
resolve : concatSeqAux s seq1 seq2 = concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) := rfl
hyp : ∀ (k : ℕ),
  (∀ (kw : k < p) (w : k < l),
      concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) k w = FinSeq.init seq1 k kw) ∧
    ∀ (kw : k < m + 1) (w : p + k < l),
      concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + k) w = (FinSeq.last seq1+|seq2) k kw :=
  concat_aux_eqs ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2)
hyp1 : ∀ (kw : k < p) (w : k < l),
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) k w = FinSeq.init seq1 k kw :=
  (hyp k).left
⊢ ∀ (kw : k < m) (w : p + 1 + k < l),
    concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + 1 + k) w = seq2 k kw