internlm/Lean-Github huggingface dataset:
Theorem: Vector.ext'
Proof state before:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
i : ℕ
iw : i < n
⊢ get' v1 i iw = get' v2 i iw
Tactic:
let lem := congrFun h i
Proof state after:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
i : ℕ
iw : i < n
lem : get' v1 i = get' v2 i := congrFun h i
⊢ get' v1 i iw = get' v2 i iw
Theorem: Vector.ext'
Proof state before:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
i : ℕ
iw : i < n
lem : get' v1 i = get' v2 i := congrFun h i
⊢ get' v1 i iw = get' v2 i iw
Tactic:
let lem' := (congrFun lem iw)
Proof state after:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
i : ℕ
iw : i < n
lem : get' v1 i = get' v2 i := congrFun h i
lem' : get' v1 i iw = get' v2 i iw := congrFun lem iw
⊢ get' v1 i iw = get' v2 i iw
Theorem: Vector.ext'
Proof state before:
case x
α : Type
n : ℕ
v1 v2 : Vector α n
h : get' v1 = get' v2
i : ℕ
iw : i < n
lem : get' v1 i = get' v2 i := congrFun h i
lem' : get' v1 i iw = get' v2 i iw := congrFun lem iw
⊢ get' v1 i iw = get' v2 i iw
Tactic:
exact lem'
Proof state after:
no goals
Theorem: Vector.of_Fn'_get'
Proof state before:
α : Type
n : ℕ
⊢ ∀ (seq : FinSeq n α), get' (ofFn' seq) = seq
Tactic:
intro seq
Proof state after:
α : Type
n : ℕ
seq : FinSeq n α
⊢ get' (ofFn' seq) = seq
Theorem: Vector.of_Fn'_get'
Proof state before:
α : Type
n : ℕ
seq : FinSeq n α
⊢ get' (ofFn' seq) = seq
Tactic:
apply funext
Proof state after:
case h
α : Type
n : ℕ
seq : FinSeq n α
⊢ ∀ (x : ℕ), get' (ofFn' seq) x = seq x
Theorem: Vector.of_Fn'_get'
Proof state before:
case h
α : Type
n : ℕ
seq : FinSeq n α
⊢ ∀ (x : ℕ), get' (ofFn' seq) x = seq x
Tactic:
intro k
Proof state after:
case h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
⊢ get' (ofFn' seq) k = seq k
Theorem: Vector.of_Fn'_get'
Proof state before:
case h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
⊢ get' (ofFn' seq) k = seq k
Tactic:
apply funext
Proof state after:
case h.h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
⊢ ∀ (x : k < n), get' (ofFn' seq) k x = seq k x
Theorem: Vector.of_Fn'_get'
Proof state before:
case h.h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
⊢ ∀ (x : k < n), get' (ofFn' seq) k x = seq k x
Tactic:
intro kw
Proof state after:
case h.h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n
⊢ get' (ofFn' seq) k kw = seq k kw
Theorem: Vector.of_Fn'_get'
Proof state before:
case h.h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n
⊢ get' (ofFn' seq) k kw = seq k kw
Tactic:
simp [Vector.get', Vector.ofFn']
Proof state after:
no goals
Theorem: Vector.of_Fn'_get
Proof state before:
α : Type
n : ℕ
⊢ ∀ (seq : FinSeq n α) (k : Fin n), get (ofFn' seq) k = seq ↑k (_ : ↑k < n)
Tactic:
intro seq ⟨k, kw⟩
Proof state after:
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n
⊢ get (ofFn' seq) { val := k, isLt := kw } = seq ↑{ val := k, isLt := kw } (_ : ↑{ val := k, isLt := kw } < n)
Theorem: Vector.of_Fn'_get
Proof state before:
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n
⊢ get (ofFn' seq) { val := k, isLt := kw } = seq ↑{ val := k, isLt := kw } (_ : ↑{ val := k, isLt := kw } < n)
Tactic:
let lem := congrFun (Vector.of_Fn'_get' seq) k
Proof state after:
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n
lem : get' (ofFn' seq) k = seq k := congrFun (of_Fn'_get' seq) k
⊢ get (ofFn' seq) { val := k, isLt := kw } = seq ↑{ val := k, isLt := kw } (_ : ↑{ val := k, isLt := kw } < n)
Theorem: Vector.of_Fn'_get
Proof state before:
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n
lem : get' (ofFn' seq) k = seq k := congrFun (of_Fn'_get' seq) k
⊢ get (ofFn' seq) { val := k, isLt := kw } = seq ↑{ val := k, isLt := kw } (_ : ↑{ val := k, isLt := kw } < n)
Tactic:
let lem' := (congrFun lem kw)
Proof state after:
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n
lem : get' (ofFn' seq) k = seq k := congrFun (of_Fn'_get' seq) k
lem' : get' (ofFn' seq) k kw = seq k kw := congrFun lem kw
⊢ get (ofFn' seq) { val := k, isLt := kw } = seq ↑{ val := k, isLt := kw } (_ : ↑{ val := k, isLt := kw } < n)
Theorem: Vector.of_Fn'_get
Proof state before:
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n
lem : get' (ofFn' seq) k = seq k := congrFun (of_Fn'_get' seq) k
lem' : get' (ofFn' seq) k kw = seq k kw := congrFun lem kw
⊢ get (ofFn' seq) { val := k, isLt := kw } = seq ↑{ val := k, isLt := kw } (_ : ↑{ val := k, isLt := kw } < n)
Tactic:
exact lem'
Proof state after:
no goals
Theorem: cons_commutes
Proof state before:
α : Type
n : ℕ
head : α
tail : Vector α n
⊢ get' (head ::ᵥ tail) = head+|get' tail
Tactic:
apply funext
Proof state after:
case h
α : Type
n : ℕ
head : α
tail : Vector α n
⊢ ∀ (x : ℕ), get' (head ::ᵥ tail) x = (head+|get' tail) x
Theorem: cons_commutes
Proof state before:
case h
α : Type
n : ℕ
head : α
tail : Vector α n
⊢ ∀ (x : ℕ), get' (head ::ᵥ tail) x = (head+|get' tail) x
Tactic:
intro k
Proof state after:
case h
α : Type
n : ℕ
head : α
tail : Vector α n
k : ℕ
⊢ get' (head ::ᵥ tail) k = (head+|get' tail) k
Theorem: cons_commutes
Proof state before:
case h
α : Type
n : ℕ
head : α
tail : Vector α n
k : ℕ
⊢ get' (head ::ᵥ tail) k = (head+|get' tail) k
Tactic:
induction k with
| zero =>
  apply funext
  intro kw
  rfl
| succ k' =>
  apply funext
  intro kw
  rfl
Proof state after:
no goals
Theorem: cons_commutes
Proof state before:
case h.zero
α : Type
n : ℕ
head : α
tail : Vector α n
⊢ get' (head ::ᵥ tail) zero = (head+|get' tail) zero
Tactic:
apply funext
Proof state after:
case h.zero.h
α : Type
n : ℕ
head : α
tail : Vector α n
⊢ ∀ (x : zero < succ n), get' (head ::ᵥ tail) zero x = (head+|get' tail) zero x
Theorem: cons_commutes
Proof state before:
case h.zero.h
α : Type
n : ℕ
head : α
tail : Vector α n
⊢ ∀ (x : zero < succ n), get' (head ::ᵥ tail) zero x = (head+|get' tail) zero x
Tactic:
intro kw
Proof state after:
case h.zero.h
α : Type
n : ℕ
head : α
tail : Vector α n
kw : zero < succ n
⊢ get' (head ::ᵥ tail) zero kw = (head+|get' tail) zero kw
Theorem: cons_commutes
Proof state before:
case h.zero.h
α : Type
n : ℕ
head : α
tail : Vector α n
kw : zero < succ n
⊢ get' (head ::ᵥ tail) zero kw = (head+|get' tail) zero kw
Tactic:
rfl
Proof state after:
no goals
Theorem: cons_commutes
Proof state before:
case h.succ
α : Type
n : ℕ
head : α
tail : Vector α n
k' : ℕ
n_ih✝ : get' (head ::ᵥ tail) k' = (head+|get' tail) k'
⊢ get' (head ::ᵥ tail) (succ k') = (head+|get' tail) (succ k')
Tactic:
apply funext
Proof state after:
case h.succ.h
α : Type
n : ℕ
head : α
tail : Vector α n
k' : ℕ
n_ih✝ : get' (head ::ᵥ tail) k' = (head+|get' tail) k'
⊢ ∀ (x : succ k' < succ n), get' (head ::ᵥ tail) (succ k') x = (head+|get' tail) (succ k') x
Theorem: cons_commutes
Proof state before:
case h.succ.h
α : Type
n : ℕ
head : α
tail : Vector α n
k' : ℕ
n_ih✝ : get' (head ::ᵥ tail) k' = (head+|get' tail) k'
⊢ ∀ (x : succ k' < succ n), get' (head ::ᵥ tail) (succ k') x = (head+|get' tail) (succ k') x
Tactic:
intro kw
Proof state after:
case h.succ.h
α : Type
n : ℕ
head : α
tail : Vector α n
k' : ℕ
n_ih✝ : get' (head ::ᵥ tail) k' = (head+|get' tail) k'
kw : succ k' < succ n
⊢ get' (head ::ᵥ tail) (succ k') kw = (head+|get' tail) (succ k') kw
Theorem: cons_commutes
Proof state before:
case h.succ.h
α : Type
n : ℕ
head : α
tail : Vector α n
k' : ℕ
n_ih✝ : get' (head ::ᵥ tail) k' = (head+|get' tail) k'
kw : succ k' < succ n
⊢ get' (head ::ᵥ tail) (succ k') kw = (head+|get' tail) (succ k') kw
Tactic:
rfl
Proof state after:
no goals
Theorem: Vector.get'_of_Fn'
Proof state before:
α : Type
n : ℕ
f : (k : ℕ) → k < n → α
k : ℕ
kw : k < n
⊢ get' (ofFn' f) k kw = f k kw
Tactic:
let lem := Vector.of_Fn'_get' f
Proof state after:
α : Type
n : ℕ
f : (k : ℕ) → k < n → α
k : ℕ
kw : k < n
lem : get' (ofFn' f) = f := of_Fn'_get' f
⊢ get' (ofFn' f) k kw = f k kw
Theorem: Vector.get'_of_Fn'
Proof state before:
α : Type
n : ℕ
f : (k : ℕ) → k < n → α
k : ℕ
kw : k < n
lem : get' (ofFn' f) = f := of_Fn'_get' f
⊢ get' (ofFn' f) k kw = f k kw
Tactic:
let lem' := congrFun lem k
Proof state after:
α : Type
n : ℕ
f : (k : ℕ) → k < n → α
k : ℕ
kw : k < n
lem : get' (ofFn' f) = f := of_Fn'_get' f
lem' : get' (ofFn' f) k = f k := congrFun lem k
⊢ get' (ofFn' f) k kw = f k kw
Theorem: Vector.get'_of_Fn'
Proof state before:
α : Type
n : ℕ
f : (k : ℕ) → k < n → α
k : ℕ
kw : k < n
lem : get' (ofFn' f) = f := of_Fn'_get' f
lem' : get' (ofFn' f) k = f k := congrFun lem k
⊢ get' (ofFn' f) k kw = f k kw
Tactic:
apply congrFun lem'
Proof state after:
no goals
Theorem: get'_cons_succ
Proof state before:
α : Type
n : ℕ
x : α
ys : Vector α n
i : ℕ
iw : i < n
⊢ get' (x ::ᵥ ys) (i + 1) (_ : succ (i + 1) ≤ succ n) = get' ys i iw
Tactic:
rfl
Proof state after:
no goals
Theorem: get'_map
Proof state before:
α β : Type
n : ℕ
vec : Vector α n
f : α → β
j : ℕ
jw : Nat.lt j n
⊢ get' (map f vec) j jw = f (get' vec j jw)
Tactic:
rw [get']
Proof state after:
α β : Type
n : ℕ
vec : Vector α n
f : α → β
j : ℕ
jw : Nat.lt j n
⊢ Vector.get (map f vec) { val := j, isLt := jw } = f (get' vec j jw)
Theorem: get'_map
Proof state before:
α β : Type
n : ℕ
vec : Vector α n
f : α → β
j : ℕ
jw : Nat.lt j n
⊢ Vector.get (map f vec) { val := j, isLt := jw } = f (get' vec j jw)
Tactic:
simp [Vector.get_map]
Proof state after:
α β : Type
n : ℕ
vec : Vector α n
f : α → β
j : ℕ
jw : Nat.lt j n
⊢ f (Vector.get vec { val := j, isLt := jw }) = f (get' vec j jw)
Theorem: get'_map
Proof state before:
α β : Type
n : ℕ
vec : Vector α n
f : α → β
j : ℕ
jw : Nat.lt j n
⊢ f (Vector.get vec { val := j, isLt := jw }) = f (get' vec j jw)
Tactic:
rfl
Proof state after:
no goals
Theorem: not_sat_and_unsat
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
⊢ IsSat clauses → IsUnSat clauses → False
Tactic:
intro ⟨v, p⟩ h2
Proof state after:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
v : Valuation (n + 1)
p :
  ∀ (p : ℕ) (pw : p < num_clauses),
    ∃ k kw,
      Vector.get (Vector.get clauses { val := p, isLt := pw }) { val := k, isLt := kw } =
        some (Vector.get v { val := k, isLt := kw })
h2 : IsUnSat clauses
⊢ False
Theorem: not_sat_and_unsat
Proof state before:
num_clauses n : ℕ
clauses : Vector (Clause (n + 1)) num_clauses
v : Valuation (n + 1)
p :
  ∀ (p : ℕ) (pw : p < num_clauses),
    ∃ k kw,
      Vector.get (Vector.get clauses { val := p, isLt := pw }) { val := k, isLt := kw } =
        some (Vector.get v { val := k, isLt := kw })
h2 : IsUnSat clauses
⊢ False
Tactic:
exact h2 v p
Proof state after:
no goals
Theorem: concat_aux_eqs
Proof 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
Proof state after:
no goals
Theorem: concat_aux_eqs
Proof 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
Proof 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
Theorem: concat_aux_eqs
Proof 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
Proof 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
Theorem: concat_aux_eqs
Proof 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]
Proof 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
Theorem: concat_aux_eqs
Proof 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
Proof 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
Theorem: concat_aux_eqs
Proof 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
Proof 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
Theorem: concat_aux_eqs
Proof 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
Proof state after:
no goals
Theorem: concat_aux_eqs
Proof state before:
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
⊢ l = m
Tactic:
rw [← s]
Proof state after:
α : Type
n m l : ℕ
s : zero + m = l
seq1 : FinSeq zero α
seq2 : FinSeq m α
k : ℕ
⊢ zero + m = m
Theorem: concat_aux_eqs
Proof 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
Proof state after:
no goals
Theorem: concat_aux_eqs
Proof 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]
Proof state after:
no goals
Theorem: concat_aux_eqs
Proof 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
Proof 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
Theorem: concat_aux_eqs
Proof 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
Proof state after:
no goals
Theorem: concat_aux_eqs
Proof 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
Proof 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
Theorem: concat_aux_eqs
Proof 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
Proof 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
Theorem: concat_aux_eqs
Proof 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
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 : ℕ),
    (∀ (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
Proof 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
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 : ℕ
⊢ (∀ (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
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)))))
⊢ (∀ (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
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)))))
⊢ (∀ (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
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
⊢ (∀ (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
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 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]
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
⊢ (∀ (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