Theorem: clauseContains_prepend (Saturn/Containment.lean)

State before:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
⊢ v1 ≥ v2 → cl1⊇cl2 → v1 ::ᵥ cl1⊇v2 ::ᵥ cl2
Tactic:
intro hyp1 hyp2 k
State after:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k : ℕ
⊢ ∀ (kw : k < succ n) (b : Bool), get' (v2 ::ᵥ cl2) k kw = some b → get' (v1 ::ᵥ cl1) k kw = some b

State before:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k : ℕ
⊢ ∀ (kw : k < succ n) (b : Bool), get' (v2 ::ᵥ cl2) k kw = some b → get' (v1 ::ᵥ cl1) k kw = some b
Tactic:
match k with
| zero =>
  intro w b hb
  exact hyp1 b hb
| j + 1  =>
  intro kw b hb
  have w : j < n := by
      apply le_of_succ_le_succ
      exact kw
  exact hyp2 j w b hb
State after:
no goals

State before:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k : ℕ
⊢ ∀ (kw : zero < succ n) (b : Bool), get' (v2 ::ᵥ cl2) zero kw = some b → get' (v1 ::ᵥ cl1) zero kw = some b
Tactic:
intro w b hb
State after:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k : ℕ
w : zero < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) zero w = some b
⊢ get' (v1 ::ᵥ cl1) zero w = some b

State before:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k : ℕ
w : zero < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) zero w = some b
⊢ get' (v1 ::ᵥ cl1) zero w = some b
Tactic:
exact hyp1 b hb
State after:
no goals

State before:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k j : ℕ
⊢ ∀ (kw : j + 1 < succ n) (b : Bool), get' (v2 ::ᵥ cl2) (j + 1) kw = some b → get' (v1 ::ᵥ cl1) (j + 1) kw = some b
Tactic:
intro kw b hb
State after:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k j : ℕ
kw : j + 1 < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) (j + 1) kw = some b
⊢ get' (v1 ::ᵥ cl1) (j + 1) kw = some b

State before:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k j : ℕ
kw : j + 1 < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) (j + 1) kw = some b
⊢ get' (v1 ::ᵥ cl1) (j + 1) kw = some b
Tactic:
have w : j < n := by
    apply le_of_succ_le_succ
    exact kw
State after:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k j : ℕ
kw : j + 1 < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) (j + 1) kw = some b
w : j < n
⊢ get' (v1 ::ᵥ cl1) (j + 1) kw = some b

State before:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k j : ℕ
kw : j + 1 < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) (j + 1) kw = some b
w : j < n
⊢ get' (v1 ::ᵥ cl1) (j + 1) kw = some b
Tactic:
exact hyp2 j w b hb
State after:
no goals

State before:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k j : ℕ
kw : j + 1 < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) (j + 1) kw = some b
⊢ j < n
Tactic:
apply le_of_succ_le_succ
State after:
case a
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k j : ℕ
kw : j + 1 < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) (j + 1) kw = some b
⊢ succ (succ j) ≤ succ n

State before:
case a
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k j : ℕ
kw : j + 1 < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) (j + 1) kw = some b
⊢ succ (succ j) ≤ succ n
Tactic:
exact kw
State after:
no goals