Theorem: concat_aux_eqs (Saturn/FinSeq.lean)

State before:
α : Type
n m l : ℕ
⊢ ∀ (s : n + m = l) (seq1 : FinSeq n α) (seq2 : FinSeq m α) (k : ℕ),
    (∀ (kw : k < n) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw) ∧
      ∀ (kw : k < m) (w : n + k < l), concatSeqAux s seq1 seq2 (n + k) w = seq2 k kw
Tactic:
match n with
| zero =>
    intro s seq1 seq2 k
    have ss : l = m := by
      rw [← s]
      apply Nat.zero_add
    have sf : FinSeq l α = FinSeq m α := by
      rw [ss]
    apply And.intro
    focus
      intro kw
      exact nomatch kw
    match l, m, ss, sf, seq2 with
        | d, .(d), rfl, rfl, seq =>
            intro kw w
            apply witness_independent
            apply Nat.zero_add
| p + 1 =>
  intro s seq1 seq2 k
  let ss : p + (m + 1)  = l :=
    by
      rw [← s]
      rw [(Nat.add_comm m 1)]
      rw [(Nat.add_assoc p 1 m)]
      done
  let resolve : concatSeqAux s seq1 seq2=
      concatSeqAux ss (seq1.init) ((seq1.last) +| seq2) := rfl
  rw [resolve]
  let hyp := concat_aux_eqs ss (seq1.init) ((seq1.last) +| seq2)
  let hyp1 := (hyp k).left
  apply And.intro
  focus
      intro kw w
      match Nat.eq_or_lt_of_le kw with
      | Or.inr kww => exact hyp1 (le_of_succ_le_succ kww) w
      | Or.inl eql =>
          match k, eql, kw, w with
          | .(p), rfl, pw, w =>
            let ww : p + zero < l := by
              rw [(Nat.add_zero p)]
              assumption
            let hyp2 := (hyp zero).right (Nat.zero_lt_succ _) ww
            let lem2 : concatSeqAux ss (seq1.init) (seq1.last+|seq2) (p + zero) ww =
                  concatSeqAux ss (seq1.init) (seq1.last+|seq2) p w :=
                  match (p + zero), Nat.add_zero p, ww with
                  | .(p), rfl, ww => rfl
            rw [← lem2]
            rw [hyp2]
            rfl
  let ass := Nat.add_assoc p 1 k
  let comm := Nat.add_comm 1 k
  intro kw w
  match p + 1 + k, ass, w with
  | .(p + (1 + k)), rfl, ww =>
    let hypw := (hyp (1 + k)).right
    let kww : 1 + k < m + 1 := by
      rw [comm]
      apply Nat.succ_lt_succ
      assumption
    let resol := hypw kww ww
    rw [resol]
    match 1 + k, comm, kww with
    | .(k + 1), rfl, kwww => rfl
State after:
no goals

State before:
α : Type
n m l : ℕ
⊢ ∀ (s : zero + m = l) (seq1 : FinSeq zero α) (seq2 : FinSeq m α) (k : ℕ),
    (∀ (kw : k < zero) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw) ∧
      ∀ (kw : k < m) (w : zero + k < l), concatSeqAux s seq1 seq2 (zero + k) w = seq2 k kw
Tactic:
intro s seq1 seq2 k
State after:
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
⊢ (∀ (kw : k < zero) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw) ∧
    ∀ (kw : k < m) (w : zero + k < l), concatSeqAux s seq1 seq2 (zero + k) w = seq2 k kw

State before:
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
⊢ (∀ (kw : k < zero) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw) ∧
    ∀ (kw : k < m) (w : zero + k < l), concatSeqAux s seq1 seq2 (zero + k) w = seq2 k kw
Tactic:
have ss : l = m := by
  rw [← s]
  apply Nat.zero_add
State after:
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
⊢ (∀ (kw : k < zero) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw) ∧
    ∀ (kw : k < m) (w : zero + k < l), concatSeqAux s seq1 seq2 (zero + k) w = seq2 k kw

State before:
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
⊢ (∀ (kw : k < zero) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw) ∧
    ∀ (kw : k < m) (w : zero + k < l), concatSeqAux s seq1 seq2 (zero + k) w = seq2 k kw
Tactic:
have sf : FinSeq l α = FinSeq m α := by
  rw [ss]
State after:
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
sf : FinSeq l α = FinSeq m α
⊢ (∀ (kw : k < zero) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw) ∧
    ∀ (kw : k < m) (w : zero + k < l), concatSeqAux s seq1 seq2 (zero + k) w = seq2 k kw

State before:
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
sf : FinSeq l α = FinSeq m α
⊢ (∀ (kw : k < zero) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw) ∧
    ∀ (kw : k < m) (w : zero + k < l), concatSeqAux s seq1 seq2 (zero + k) w = seq2 k kw
Tactic:
apply And.intro
State after:
case left
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
sf : FinSeq l α = FinSeq m α
⊢ ∀ (kw : k < zero) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw

case right
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
sf : FinSeq l α = FinSeq m α
⊢ ∀ (kw : k < m) (w : zero + k < l), concatSeqAux s seq1 seq2 (zero + k) w = seq2 k kw

State before:
case left
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
sf : FinSeq l α = FinSeq m α
⊢ ∀ (kw : k < zero) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw

case right
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
sf : FinSeq l α = FinSeq m α
⊢ ∀ (kw : k < m) (w : zero + k < l), concatSeqAux s seq1 seq2 (zero + k) w = seq2 k kw
Tactic:
focus
  intro kw
  exact nomatch kw
State after:
case right
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
sf : FinSeq l α = FinSeq m α
⊢ ∀ (kw : k < m) (w : zero + k < l), concatSeqAux s seq1 seq2 (zero + k) w = seq2 k kw

State before:
case right
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
sf : FinSeq l α = FinSeq m α
⊢ ∀ (kw : k < m) (w : zero + k < l), concatSeqAux s seq1 seq2 (zero + k) w = seq2 k kw
Tactic:
match l, m, ss, sf, seq2 with
    | d, .(d), rfl, rfl, seq =>
        intro kw w
        apply witness_independent
        apply Nat.zero_add
State after:
no goals

State before:
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
⊢ l = m
Tactic:
rw [← s]
State after:
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
⊢ zero + m = m

State before:
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
⊢ zero + m = m
Tactic:
apply Nat.zero_add
State after:
no goals

State before:
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
⊢ FinSeq l α = FinSeq m α
Tactic:
rw [ss]
State after:
no goals

State before:
case left
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
sf : FinSeq l α = FinSeq m α
⊢ ∀ (kw : k < zero) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw
Tactic:
intro kw
State after:
case left
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
sf : FinSeq l α = FinSeq m α
kw : k < zero
⊢ ∀ (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw

State before:
case left
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
sf : FinSeq l α = FinSeq m α
kw : k < zero
⊢ ∀ (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw
Tactic:
exact nomatch kw
State after:
no goals

State before:
α : Type
n m l : ℕ
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
sf : FinSeq l α = FinSeq m α
d : ℕ
seq : FinSeq d α
s : zero + d = d
⊢ ∀ (kw : k < d) (w : zero + k < d), concatSeqAux s seq1 seq (zero + k) w = seq k kw
Tactic:
intro kw w
State after:
α : Type
n m l : ℕ
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
sf : FinSeq l α = FinSeq m α
d : ℕ
seq : FinSeq d α
s : zero + d = d
kw : k < d
w : zero + k < d
⊢ concatSeqAux s seq1 seq (zero + k) w = seq k kw

State before:
α : Type
n m l : ℕ
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
sf : FinSeq l α = FinSeq m α
d : ℕ
seq : FinSeq d α
s : zero + d = d
kw : k < d
w : zero + k < d
⊢ concatSeqAux s seq1 seq (zero + k) w = seq k kw
Tactic:
apply witness_independent
State after:
case a
α : Type
n m l : ℕ
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
sf : FinSeq l α = FinSeq m α
d : ℕ
seq : FinSeq d α
s : zero + d = d
kw : k < d
w : zero + k < d
⊢ zero + k = k

State before:
case a
α : Type
n m l : ℕ
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
ss : l = m
sf : FinSeq l α = FinSeq m α
d : ℕ
seq : FinSeq d α
s : zero + d = d
kw : k < d
w : zero + k < d
⊢ zero + k = k
Tactic:
apply Nat.zero_add
State after:
no goals

State before:
α : Type
n m l p : ℕ
⊢ ∀ (s : p + 1 + m = l) (seq1 : FinSeq (p + 1) α) (seq2 : FinSeq m α) (k : ℕ),
    (∀ (kw : k < p + 1) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw) ∧
      ∀ (kw : k < m) (w : p + 1 + k < l), concatSeqAux s seq1 seq2 (p + 1 + k) w = seq2 k kw
Tactic:
intro s seq1 seq2 k
State after:
α : Type
n m l p : ℕ
s : p + 1 + m = l
seq1 : FinSeq (p + 1) α
seq2 : FinSeq m α
k : ℕ
⊢ (∀ (kw : k < p + 1) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw) ∧
    ∀ (kw : k < m) (w : p + 1 + k < l), concatSeqAux s seq1 seq2 (p + 1 + k) w = seq2 k kw

State before:
α : Type
n m l p : ℕ
s : p + 1 + m = l
seq1 : FinSeq (p + 1) α
seq2 : FinSeq m α
k : ℕ
⊢ (∀ (kw : k < p + 1) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw) ∧
    ∀ (kw : k < m) (w : p + 1 + k < l), concatSeqAux s seq1 seq2 (p + 1 + k) w = seq2 k kw
Tactic:
let ss : p + (m + 1)  = l :=
  by
    rw [← s]
    rw [(Nat.add_comm m 1)]
    rw [(Nat.add_assoc p 1 m)]
    done
State after:
α : 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)))))
⊢ (∀ (kw : k < p + 1) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw) ∧
    ∀ (kw : k < m) (w : p + 1 + k < l), concatSeqAux s seq1 seq2 (p + 1 + k) w = seq2 k kw

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)))))
⊢ (∀ (kw : k < p + 1) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw) ∧
    ∀ (kw : k < m) (w : p + 1 + k < l), concatSeqAux s seq1 seq2 (p + 1 + k) w = seq2 k kw
Tactic:
let resolve : concatSeqAux s seq1 seq2=
    concatSeqAux ss (seq1.init) ((seq1.last) +| seq2) := rfl
State after:
α : 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
⊢ (∀ (kw : k < p + 1) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw) ∧
    ∀ (kw : k < m) (w : p + 1 + k < l), concatSeqAux s seq1 seq2 (p + 1 + k) w = seq2 k kw

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
⊢ (∀ (kw : k < p + 1) (w : k < l), concatSeqAux s seq1 seq2 k w = seq1 k kw) ∧
    ∀ (kw : k < m) (w : p + 1 + k < l), concatSeqAux s seq1 seq2 (p + 1 + k) w = seq2 k kw
Tactic:
rw [resolve]
State after:
α : 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
⊢ (∀ (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

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
⊢ (∀ (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:
let hyp := concat_aux_eqs ss (seq1.init) ((seq1.last) +| seq2)
State after:
α : 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)
⊢ (∀ (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

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)
⊢ (∀ (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:
let hyp1 := (hyp k).left
State after:
α : 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

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
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

State before:
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
Tactic:
focus
    intro kw w
    match Nat.eq_or_lt_of_le kw with
    | Or.inr kww => exact hyp1 (le_of_succ_le_succ kww) w
    | Or.inl eql =>
        match k, eql, kw, w with
        | .(p), rfl, pw, w =>
          let ww : p + zero < l := by
            rw [(Nat.add_zero p)]
            assumption
          let hyp2 := (hyp zero).right (Nat.zero_lt_succ _) ww
          let lem2 : concatSeqAux ss (seq1.init) (seq1.last+|seq2) (p + zero) ww =
                concatSeqAux ss (seq1.init) (seq1.last+|seq2) p w :=
                match (p + zero), Nat.add_zero p, ww with
                | .(p), rfl, ww => rfl
          rw [← lem2]
          rw [hyp2]
          rfl
State after:
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

State before:
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
Tactic:
let ass := Nat.add_assoc p 1 k
State after:
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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
⊢ ∀ (kw : k < m) (w : p + 1 + k < l),
    concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + 1 + k) w = seq2 k kw

State before:
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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
⊢ ∀ (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:
let comm := Nat.add_comm 1 k
State after:
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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
⊢ ∀ (kw : k < m) (w : p + 1 + k < l),
    concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + 1 + k) w = seq2 k kw

State before:
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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
⊢ ∀ (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:
intro kw w
State after:
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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
kw : k < m
w : p + 1 + k < l
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + 1 + k) w = seq2 k kw

State before:
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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
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:
match p + 1 + k, ass, w with
| .(p + (1 + k)), rfl, ww =>
  let hypw := (hyp (1 + k)).right
  let kww : 1 + k < m + 1 := by
    rw [comm]
    apply Nat.succ_lt_succ
    assumption
  let resol := hypw kww ww
  rw [resol]
  match 1 + k, comm, kww with
  | .(k + 1), rfl, kwww => rfl
State after:
no goals

State before:
α : Type
n m l p : ℕ
s : p + 1 + m = l
seq1 : FinSeq (p + 1) α
seq2 : FinSeq m α
k : ℕ
⊢ p + (m + 1) = l
Tactic:
rw [← s]
State after:
α : Type
n m l p : ℕ
s : p + 1 + m = l
seq1 : FinSeq (p + 1) α
seq2 : FinSeq m α
k : ℕ
⊢ p + (m + 1) = p + 1 + m

State before:
α : Type
n m l p : ℕ
s : p + 1 + m = l
seq1 : FinSeq (p + 1) α
seq2 : FinSeq m α
k : ℕ
⊢ p + (m + 1) = p + 1 + m
Tactic:
rw [(Nat.add_comm m 1)]
State after:
α : Type
n m l p : ℕ
s : p + 1 + m = l
seq1 : FinSeq (p + 1) α
seq2 : FinSeq m α
k : ℕ
⊢ p + (1 + m) = p + 1 + m

State before:
α : Type
n m l p : ℕ
s : p + 1 + m = l
seq1 : FinSeq (p + 1) α
seq2 : FinSeq m α
k : ℕ
⊢ p + (1 + m) = p + 1 + m
Tactic:
rw [(Nat.add_assoc p 1 m)]
State after:
no goals

State before:
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
Tactic:
intro kw w
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

State before:
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
Tactic:
match Nat.eq_or_lt_of_le kw with
| Or.inr kww => exact hyp1 (le_of_succ_le_succ kww) w
| Or.inl eql =>
    match k, eql, kw, w with
    | .(p), rfl, pw, w =>
      let ww : p + zero < l := by
        rw [(Nat.add_zero p)]
        assumption
      let hyp2 := (hyp zero).right (Nat.zero_lt_succ _) ww
      let lem2 : concatSeqAux ss (seq1.init) (seq1.last+|seq2) (p + zero) ww =
            concatSeqAux ss (seq1.init) (seq1.last+|seq2) p w :=
            match (p + zero), Nat.add_zero p, ww with
            | .(p), rfl, ww => rfl
      rw [← lem2]
      rw [hyp2]
      rfl
State after:
no goals

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
kww : succ k < p + 1
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) k w = seq1 k kw
Tactic:
exact hyp1 (le_of_succ_le_succ kww) w
State after:
no goals

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
eql : succ k = p + 1
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) k w = seq1 k kw
Tactic:
match k, eql, kw, w with
| .(p), rfl, pw, w =>
  let ww : p + zero < l := by
    rw [(Nat.add_zero p)]
    assumption
  let hyp2 := (hyp zero).right (Nat.zero_lt_succ _) ww
  let lem2 : concatSeqAux ss (seq1.init) (seq1.last+|seq2) (p + zero) ww =
        concatSeqAux ss (seq1.init) (seq1.last+|seq2) p w :=
        match (p + zero), Nat.add_zero p, ww with
        | .(p), rfl, ww => rfl
  rw [← lem2]
  rw [hyp2]
  rfl
State after:
no goals

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
eql : succ k = p + 1
pw : p < p + 1
w : p < l
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) p w = seq1 p pw
Tactic:
let ww : p + zero < l := by
  rw [(Nat.add_zero p)]
  assumption
State after:
α : 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
eql : succ k = p + 1
pw : p < p + 1
w : p < l
ww : p + zero < l := Eq.mpr (id (congrArg (fun _a => _a < l) (Nat.add_zero p))) w
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) p w = seq1 p pw

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
eql : succ k = p + 1
pw : p < p + 1
w : p < l
ww : p + zero < l := Eq.mpr (id (congrArg (fun _a => _a < l) (Nat.add_zero p))) w
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) p w = seq1 p pw
Tactic:
let hyp2 := (hyp zero).right (Nat.zero_lt_succ _) ww
State after:
α : 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
eql : succ k = p + 1
pw : p < p + 1
w : p < l
ww : p + zero < l := Eq.mpr (id (congrArg (fun _a => _a < l) (Nat.add_zero p))) w
hyp2 : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + zero) ww =
  (FinSeq.last seq1+|seq2) zero (_ : 0 < succ m) :=
  (hyp zero).right (zero_lt_succ m) ww
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) p w = seq1 p pw

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
eql : succ k = p + 1
pw : p < p + 1
w : p < l
ww : p + zero < l := Eq.mpr (id (congrArg (fun _a => _a < l) (Nat.add_zero p))) w
hyp2 : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + zero) ww =
  (FinSeq.last seq1+|seq2) zero (_ : 0 < succ m) :=
  (hyp zero).right (zero_lt_succ m) ww
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) p w = seq1 p pw
Tactic:
let lem2 : concatSeqAux ss (seq1.init) (seq1.last+|seq2) (p + zero) ww =
      concatSeqAux ss (seq1.init) (seq1.last+|seq2) p w :=
      match (p + zero), Nat.add_zero p, ww with
      | .(p), rfl, ww => rfl
State after:
α : 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
eql : succ k = p + 1
pw : p < p + 1
w : p < l
ww : p + zero < l := Eq.mpr (id (congrArg (fun _a => _a < l) (Nat.add_zero p))) w
hyp2 : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + zero) ww =
  (FinSeq.last seq1+|seq2) zero (_ : 0 < succ m) :=
  (hyp zero).right (zero_lt_succ m) ww
lem2 : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + zero) ww =
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) p w :=
  match p + zero, Nat.add_zero p, ww with
  | .(p), Eq.refl p, ww => rfl
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) p w = seq1 p pw

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
eql : succ k = p + 1
pw : p < p + 1
w : p < l
ww : p + zero < l := Eq.mpr (id (congrArg (fun _a => _a < l) (Nat.add_zero p))) w
hyp2 : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + zero) ww =
  (FinSeq.last seq1+|seq2) zero (_ : 0 < succ m) :=
  (hyp zero).right (zero_lt_succ m) ww
lem2 : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + zero) ww =
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) p w :=
  match p + zero, Nat.add_zero p, ww with
  | .(p), Eq.refl p, ww => rfl
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) p w = seq1 p pw
Tactic:
rw [← lem2]
State after:
α : 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
eql : succ k = p + 1
pw : p < p + 1
w : p < l
ww : p + zero < l := Eq.mpr (id (congrArg (fun _a => _a < l) (Nat.add_zero p))) w
hyp2 : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + zero) ww =
  (FinSeq.last seq1+|seq2) zero (_ : 0 < succ m) :=
  (hyp zero).right (zero_lt_succ m) ww
lem2 : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + zero) ww =
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) p w :=
  match p + zero, Nat.add_zero p, ww with
  | .(p), Eq.refl p, ww => rfl
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + zero) ww = seq1 p pw

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
eql : succ k = p + 1
pw : p < p + 1
w : p < l
ww : p + zero < l := Eq.mpr (id (congrArg (fun _a => _a < l) (Nat.add_zero p))) w
hyp2 : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + zero) ww =
  (FinSeq.last seq1+|seq2) zero (_ : 0 < succ m) :=
  (hyp zero).right (zero_lt_succ m) ww
lem2 : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + zero) ww =
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) p w :=
  match p + zero, Nat.add_zero p, ww with
  | .(p), Eq.refl p, ww => rfl
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + zero) ww = seq1 p pw
Tactic:
rw [hyp2]
State after:
α : 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
eql : succ k = p + 1
pw : p < p + 1
w : p < l
ww : p + zero < l := Eq.mpr (id (congrArg (fun _a => _a < l) (Nat.add_zero p))) w
hyp2 : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + zero) ww =
  (FinSeq.last seq1+|seq2) zero (_ : 0 < succ m) :=
  (hyp zero).right (zero_lt_succ m) ww
lem2 : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + zero) ww =
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) p w :=
  match p + zero, Nat.add_zero p, ww with
  | .(p), Eq.refl p, ww => rfl
⊢ (FinSeq.last seq1+|seq2) zero (_ : 0 < succ m) = seq1 p pw

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
eql : succ k = p + 1
pw : p < p + 1
w : p < l
ww : p + zero < l := Eq.mpr (id (congrArg (fun _a => _a < l) (Nat.add_zero p))) w
hyp2 : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + zero) ww =
  (FinSeq.last seq1+|seq2) zero (_ : 0 < succ m) :=
  (hyp zero).right (zero_lt_succ m) ww
lem2 : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + zero) ww =
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) p w :=
  match p + zero, Nat.add_zero p, ww with
  | .(p), Eq.refl p, ww => rfl
⊢ (FinSeq.last seq1+|seq2) zero (_ : 0 < succ m) = seq1 p pw
Tactic:
rfl
State after:
no goals

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
eql : succ k = p + 1
pw : p < p + 1
w : p < l
⊢ p + zero < l
Tactic:
rw [(Nat.add_zero p)]
State after:
α : 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
eql : succ k = p + 1
pw : p < p + 1
w : p < l
⊢ p < l

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
eql : succ k = p + 1
pw : p < p + 1
w : p < l
⊢ p < l
Tactic:
assumption
State after:
no goals

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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
kw : k < m
w : p + 1 + k < l
ww : p + (1 + k) < l
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) ww = seq2 k kw
Tactic:
let hypw := (hyp (1 + k)).right
State after:
α : 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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
kw : k < m
w : p + 1 + k < l
ww : p + (1 + k) < l
hypw : ∀ (kw : 1 + k < m + 1) (w : p + (1 + k) < l),
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) w = (FinSeq.last seq1+|seq2) (1 + k) kw :=
  (hyp (1 + k)).right
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) ww = seq2 k kw

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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
kw : k < m
w : p + 1 + k < l
ww : p + (1 + k) < l
hypw : ∀ (kw : 1 + k < m + 1) (w : p + (1 + k) < l),
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) w = (FinSeq.last seq1+|seq2) (1 + k) kw :=
  (hyp (1 + k)).right
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) ww = seq2 k kw
Tactic:
let kww : 1 + k < m + 1 := by
  rw [comm]
  apply Nat.succ_lt_succ
  assumption
State after:
α : 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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
kw : k < m
w : p + 1 + k < l
ww : p + (1 + k) < l
hypw : ∀ (kw : 1 + k < m + 1) (w : p + (1 + k) < l),
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) w = (FinSeq.last seq1+|seq2) (1 + k) kw :=
  (hyp (1 + k)).right
kww : 1 + k < m + 1 := Eq.mpr (id (congrArg (fun _a => _a < m + 1) comm)) (succ_lt_succ kw)
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) ww = seq2 k kw

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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
kw : k < m
w : p + 1 + k < l
ww : p + (1 + k) < l
hypw : ∀ (kw : 1 + k < m + 1) (w : p + (1 + k) < l),
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) w = (FinSeq.last seq1+|seq2) (1 + k) kw :=
  (hyp (1 + k)).right
kww : 1 + k < m + 1 := Eq.mpr (id (congrArg (fun _a => _a < m + 1) comm)) (succ_lt_succ kw)
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) ww = seq2 k kw
Tactic:
let resol := hypw kww ww
State after:
α : 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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
kw : k < m
w : p + 1 + k < l
ww : p + (1 + k) < l
hypw : ∀ (kw : 1 + k < m + 1) (w : p + (1 + k) < l),
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) w = (FinSeq.last seq1+|seq2) (1 + k) kw :=
  (hyp (1 + k)).right
kww : 1 + k < m + 1 := Eq.mpr (id (congrArg (fun _a => _a < m + 1) comm)) (succ_lt_succ kw)
resol : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) ww =
  (FinSeq.last seq1+|seq2) (1 + k) kww :=
  hypw kww ww
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) ww = seq2 k kw

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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
kw : k < m
w : p + 1 + k < l
ww : p + (1 + k) < l
hypw : ∀ (kw : 1 + k < m + 1) (w : p + (1 + k) < l),
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) w = (FinSeq.last seq1+|seq2) (1 + k) kw :=
  (hyp (1 + k)).right
kww : 1 + k < m + 1 := Eq.mpr (id (congrArg (fun _a => _a < m + 1) comm)) (succ_lt_succ kw)
resol : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) ww =
  (FinSeq.last seq1+|seq2) (1 + k) kww :=
  hypw kww ww
⊢ concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) ww = seq2 k kw
Tactic:
rw [resol]
State after:
α : 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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
kw : k < m
w : p + 1 + k < l
ww : p + (1 + k) < l
hypw : ∀ (kw : 1 + k < m + 1) (w : p + (1 + k) < l),
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) w = (FinSeq.last seq1+|seq2) (1 + k) kw :=
  (hyp (1 + k)).right
kww : 1 + k < m + 1 := Eq.mpr (id (congrArg (fun _a => _a < m + 1) comm)) (succ_lt_succ kw)
resol : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) ww =
  (FinSeq.last seq1+|seq2) (1 + k) kww :=
  hypw kww ww
⊢ (FinSeq.last seq1+|seq2) (1 + k) kww = seq2 k kw

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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
kw : k < m
w : p + 1 + k < l
ww : p + (1 + k) < l
hypw : ∀ (kw : 1 + k < m + 1) (w : p + (1 + k) < l),
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) w = (FinSeq.last seq1+|seq2) (1 + k) kw :=
  (hyp (1 + k)).right
kww : 1 + k < m + 1 := Eq.mpr (id (congrArg (fun _a => _a < m + 1) comm)) (succ_lt_succ kw)
resol : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) ww =
  (FinSeq.last seq1+|seq2) (1 + k) kww :=
  hypw kww ww
⊢ (FinSeq.last seq1+|seq2) (1 + k) kww = seq2 k kw
Tactic:
match 1 + k, comm, kww with
| .(k + 1), rfl, kwww => rfl
State after:
no goals

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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
kw : k < m
w : p + 1 + k < l
ww : p + (1 + k) < l
hypw : ∀ (kw : 1 + k < m + 1) (w : p + (1 + k) < l),
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) w = (FinSeq.last seq1+|seq2) (1 + k) kw :=
  (hyp (1 + k)).right
⊢ 1 + k < m + 1
Tactic:
rw [comm]
State after:
α : 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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
kw : k < m
w : p + 1 + k < l
ww : p + (1 + k) < l
hypw : ∀ (kw : 1 + k < m + 1) (w : p + (1 + k) < l),
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) w = (FinSeq.last seq1+|seq2) (1 + k) kw :=
  (hyp (1 + k)).right
⊢ k + 1 < m + 1

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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
kw : k < m
w : p + 1 + k < l
ww : p + (1 + k) < l
hypw : ∀ (kw : 1 + k < m + 1) (w : p + (1 + k) < l),
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) w = (FinSeq.last seq1+|seq2) (1 + k) kw :=
  (hyp (1 + k)).right
⊢ k + 1 < m + 1
Tactic:
apply Nat.succ_lt_succ
State after:
case a
α : 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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
kw : k < m
w : p + 1 + k < l
ww : p + (1 + k) < l
hypw : ∀ (kw : 1 + k < m + 1) (w : p + (1 + k) < l),
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) w = (FinSeq.last seq1+|seq2) (1 + k) kw :=
  (hyp (1 + k)).right
⊢ k < m

State before:
case a
α : 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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
kw : k < m
w : p + 1 + k < l
ww : p + (1 + k) < l
hypw : ∀ (kw : 1 + k < m + 1) (w : p + (1 + k) < l),
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) w = (FinSeq.last seq1+|seq2) (1 + k) kw :=
  (hyp (1 + k)).right
⊢ k < m
Tactic:
assumption
State after:
no goals

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
ass : p + 1 + k = p + (1 + k) := Nat.add_assoc p 1 k
comm : 1 + k = k + 1 := Nat.add_comm 1 k
kw : k < m
w : p + 1 + k < l
ww : p + (1 + k) < l
hypw : ∀ (kw : 1 + k < m + 1) (w : p + (1 + k) < l),
  concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) w = (FinSeq.last seq1+|seq2) (1 + k) kw :=
  (hyp (1 + k)).right
kww : 1 + k < m + 1 := Eq.mpr (id (congrArg (fun _a => _a < m + 1) comm)) (succ_lt_succ kw)
resol : concatSeqAux ss (FinSeq.init seq1) (FinSeq.last seq1+|seq2) (p + (1 + k)) ww =
  (FinSeq.last seq1+|seq2) (1 + k) kww :=
  hypw kww ww
kwww : k + 1 < m + 1
⊢ (FinSeq.last seq1+|seq2) (k + 1) kwww = seq2 k kw
Tactic:
rfl
State after:
no goals