internlm/Lean-Github huggingface dataset:
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
⊢ (∀ (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)
Proof 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
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)
⊢ (∀ (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
Proof 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
Theorem: concat_aux_eqs
Proof 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
Proof 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
Theorem: concat_aux_eqs
Proof 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
Proof 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
Theorem: concat_aux_eqs
Proof 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
Proof 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
Theorem: concat_aux_eqs
Proof 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
Proof state after:
no goals
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 : ℕ
⊢ p + (m + 1) = l
Tactic:
rw [← s]
Proof 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
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 : ℕ
⊢ p + (m + 1) = p + 1 + m
Tactic:
rw [(Nat.add_comm m 1)]
Proof 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
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 : ℕ
⊢ p + (1 + m) = p + 1 + m
Tactic:
rw [(Nat.add_assoc p 1 m)]
Proof state after:
no goals
Theorem: concat_aux_eqs
Proof 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
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
Theorem: concat_aux_eqs
Proof 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
Proof state after:
no goals
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
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
Proof state after:
no goals
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
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
Proof state after:
no goals
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
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
Proof 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