Theorem: clauseContains_beyond_vacuously (Saturn/Containment.lean)

State before:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
⊢ n ≤ m → clauseContainsTail cl1 cl2 m
Tactic:
intro h k kw ineq
State after:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
h : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
⊢ ∀ (b : Bool), get' cl2 k kw = some b → get' cl1 k kw = some b

State before:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
h : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
⊢ ∀ (b : Bool), get' cl2 k kw = some b → get' cl1 k kw = some b
Tactic:
let inq := Nat.le_trans h ineq
State after:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
h : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
inq : n ≤ k := Nat.le_trans h ineq
⊢ ∀ (b : Bool), get' cl2 k kw = some b → get' cl1 k kw = some b

State before:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
h : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
inq : n ≤ k := Nat.le_trans h ineq
⊢ ∀ (b : Bool), get' cl2 k kw = some b → get' cl1 k kw = some b
Tactic:
let inq2 := Nat.lt_of_lt_of_le kw inq
State after:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
h : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
inq : n ≤ k := Nat.le_trans h ineq
inq2 : k < k := Nat.lt_of_lt_of_le kw inq
⊢ ∀ (b : Bool), get' cl2 k kw = some b → get' cl1 k kw = some b

State before:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
h : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
inq : n ≤ k := Nat.le_trans h ineq
inq2 : k < k := Nat.lt_of_lt_of_le kw inq
⊢ ∀ (b : Bool), get' cl2 k kw = some b → get' cl1 k kw = some b
Tactic:
exact (False.elim (Nat.lt_irrefl k inq2))
State after:
no goals