Theorem: triple_step
Proof state before:
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : ¬Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : ¬kr = triple.pivot
i : ℕ := skipInverse triple.pivot kr ccc
eql : skip triple.pivot (skipInverse triple.pivot kr ccc) = kr := skipInverse_eq triple.pivot kr ccc
iw : i < n := skip_preimage_lt triple.pivotLt rlt eql
leftLem : Vector.get' left kr rlt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kr => Vector.get' left kr) kr (skip triple.pivot i) rlt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kr ccc))))
rightLem : Vector.get' right kr rlt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kr => Vector.get' right kr) kr (skip triple.pivot i) rlt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kr ccc))))
⊢ Vector.get' top kr rlt = Vector.get' top (skip triple.pivot i) (_ : skip triple.pivot i < n + 1)
Tactic:
apply witness_independent
Proof state after:
case a
n : ℕ
left right top : Clause (n + 1)
triple : ResolutionTriple left right top
valuation : Valuation (n + 1)
x✝¹ : ClauseSat left valuation
kl : ℕ
llt : kl < n + 1
wl : VarSat (Vector.get left { val := kl, isLt := llt }) (Vector.get valuation { val := kl, isLt := llt })
x✝ : ClauseSat right valuation
kr : ℕ
rlt : kr < n + 1
wr : VarSat (Vector.get right { val := kr, isLt := rlt }) (Vector.get valuation { val := kr, isLt := rlt })
c : ¬Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = true
cc : Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1) = false := eq_false_of_ne_true c
ccc : ¬kr = triple.pivot
i : ℕ := skipInverse triple.pivot kr ccc
eql : skip triple.pivot (skipInverse triple.pivot kr ccc) = kr := skipInverse_eq triple.pivot kr ccc
iw : i < n := skip_preimage_lt triple.pivotLt rlt eql
leftLem : Vector.get' left kr rlt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kr => Vector.get' left kr) kr (skip triple.pivot i) rlt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kr ccc))))
rightLem : Vector.get' right kr rlt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kr => Vector.get' right kr) kr (skip triple.pivot i) rlt (skip_le_succ iw)
    (Eq.mpr (id (congrArg (fun _a => _a = skip triple.pivot i) eql.symm))
      (Eq.refl (skip triple.pivot (skipInverse triple.pivot kr ccc))))
⊢ kr = skip triple.pivot i