Theorem: elem_not_beyond_vacuously (Saturn/FinSeq.lean)

State before:
α : Type
n : ℕ
seq : FinSeq n α
elem : α
m : ℕ
⊢ n ≤ m → elemNotBeyond seq elem m
Tactic:
intro hyp k kw ineq
State after:
α : Type
n : ℕ
seq : FinSeq n α
elem : α
m : ℕ
hyp : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
⊢ ¬seq k kw = elem

State before:
α : Type
n : ℕ
seq : FinSeq n α
elem : α
m : ℕ
hyp : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
⊢ ¬seq k kw = elem
Tactic:
let inq := Nat.le_trans hyp ineq
State after:
α : Type
n : ℕ
seq : FinSeq n α
elem : α
m : ℕ
hyp : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
inq : n ≤ k := Nat.le_trans hyp ineq
⊢ ¬seq k kw = elem

State before:
α : Type
n : ℕ
seq : FinSeq n α
elem : α
m : ℕ
hyp : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
inq : n ≤ k := Nat.le_trans hyp ineq
⊢ ¬seq k kw = elem
Tactic:
let inq2 := Nat.lt_of_lt_of_le kw inq
State after:
α : Type
n : ℕ
seq : FinSeq n α
elem : α
m : ℕ
hyp : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
inq : n ≤ k := Nat.le_trans hyp ineq
inq2 : k < k := Nat.lt_of_lt_of_le kw inq
⊢ ¬seq k kw = elem

State before:
α : Type
n : ℕ
seq : FinSeq n α
elem : α
m : ℕ
hyp : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
inq : n ≤ k := Nat.le_trans hyp ineq
inq2 : k < k := Nat.lt_of_lt_of_le kw inq
⊢ ¬seq k kw = elem
Tactic:
exact (False.elim (Nat.lt_irrefl k inq2))
State after:
no goals