Theorem: triple_step (Saturn/Resolution.lean)

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 : kl = triple.pivot
⊢ ClauseSat top valuation
Tactic:
have lem1 : left.get' kl llt  =
  left.get' triple.pivot triple.pivotLt := by
  apply witness_independent
  apply cc
State after:
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 : kl = triple.pivot
lem1 : Vector.get' left kl llt = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation

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 : kl = triple.pivot
lem1 : Vector.get' left kl llt = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation
Tactic:
have lem2 : valuation.get' kl llt =
  valuation.get' triple.pivot triple.pivotLt := by
  apply witness_independent
  apply cc
State after:
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 : kl = triple.pivot
lem1 : Vector.get' left kl llt = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kl llt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation

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 : kl = triple.pivot
lem1 : Vector.get' left kl llt = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kl llt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation
Tactic:
rw [Vector.get'] at lem1
State after:
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 : kl = triple.pivot
lem1 : Vector.get left { val := kl, isLt := llt } = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kl llt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation

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 : kl = triple.pivot
lem1 : Vector.get left { val := kl, isLt := llt } = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kl llt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation
Tactic:
have lem3 : some true = some false := by
  rw [← c, ← lem2, Vector.get', ← wl, lem1, triple.leftPivot]
State after:
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 : kl = triple.pivot
lem1 : Vector.get left { val := kl, isLt := llt } = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kl llt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
lem3 : some true = some false
⊢ ClauseSat top valuation

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 : kl = triple.pivot
lem1 : Vector.get left { val := kl, isLt := llt } = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kl llt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
lem3 : some true = some false
⊢ ClauseSat top valuation
Tactic:
simp at lem3
State after:
no goals

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 : kl = triple.pivot
⊢ Vector.get' left kl llt = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
Tactic:
apply witness_independent
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 : kl = triple.pivot
⊢ kl = triple.pivot

State before:
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 : kl = triple.pivot
⊢ kl = triple.pivot
Tactic:
apply cc
State after:
no goals

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 : kl = triple.pivot
lem1 : Vector.get' left kl llt = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
⊢ Vector.get' valuation kl llt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
Tactic:
apply witness_independent
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 : kl = triple.pivot
lem1 : Vector.get' left kl llt = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
⊢ kl = triple.pivot

State before:
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 : kl = triple.pivot
lem1 : Vector.get' left kl llt = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
⊢ kl = triple.pivot
Tactic:
apply cc
State after:
no goals

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 : kl = triple.pivot
lem1 : Vector.get left { val := kl, isLt := llt } = Vector.get' left triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kl llt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ some true = some false
Tactic:
rw [← c, ← lem2, Vector.get', ← wl, lem1, triple.leftPivot]
State after:
no goals

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 : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
⊢ Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1)
Tactic:
apply witness_independent
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 : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
⊢ kl = skip triple.pivot i

State before:
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 : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
⊢ kl = skip triple.pivot i
Tactic:
rw [← eql]
State after:
no goals

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 : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
leftLem : Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' left kl) kl (skip triple.pivot i) llt (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 kl cc))))
⊢ Vector.get' right kl llt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1)
Tactic:
apply witness_independent
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 : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
leftLem : Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' left kl) kl (skip triple.pivot i) llt (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 kl cc))))
⊢ kl = skip triple.pivot i

State before:
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 : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
leftLem : Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' left kl) kl (skip triple.pivot i) llt (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 kl cc))))
⊢ kl = skip triple.pivot i
Tactic:
rw [← eql]
State after:
no goals

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 : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
leftLem : Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' left kl) kl (skip triple.pivot i) llt (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 kl cc))))
rightLem : Vector.get' right kl llt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' right kl) kl (skip triple.pivot i) llt (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 kl cc))))
⊢ Vector.get' top kl llt = Vector.get' top (skip triple.pivot i) (_ : skip triple.pivot i < n + 1)
Tactic:
apply witness_independent
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 : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
leftLem : Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' left kl) kl (skip triple.pivot i) llt (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 kl cc))))
rightLem : Vector.get' right kl llt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' right kl) kl (skip triple.pivot i) llt (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 kl cc))))
⊢ kl = skip triple.pivot i

State before:
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 : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
leftLem : Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' left kl) kl (skip triple.pivot i) llt (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 kl cc))))
rightLem : Vector.get' right kl llt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' right kl) kl (skip triple.pivot i) llt (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 kl cc))))
⊢ kl = skip triple.pivot i
Tactic:
rw [← eql]
State after:
no goals

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 : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
leftLem : Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' left kl) kl (skip triple.pivot i) llt (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 kl cc))))
rightLem : Vector.get' right kl llt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' right kl) kl (skip triple.pivot i) llt (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 kl cc))))
topLem : Vector.get' top kl llt = Vector.get' top (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' top kl) kl (skip triple.pivot i) llt (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 kl cc))))
⊢ IsJoin (Vector.get' left kl llt) (Vector.get' right kl llt) (Vector.get' top kl llt)
Tactic:
rw [leftLem, rightLem, topLem]
State after:
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 : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
leftLem : Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' left kl) kl (skip triple.pivot i) llt (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 kl cc))))
rightLem : Vector.get' right kl llt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' right kl) kl (skip triple.pivot i) llt (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 kl cc))))
topLem : Vector.get' top kl llt = Vector.get' top (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' top kl) kl (skip triple.pivot i) llt (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 kl cc))))
⊢ IsJoin (Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))
    (Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))
    (Vector.get' top (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))

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 : ¬kl = triple.pivot
i : ℕ := skipInverse triple.pivot kl cc
eql : skip triple.pivot (skipInverse triple.pivot kl cc) = kl := skipInverse_eq triple.pivot kl cc
iw : i < n := skip_preimage_lt triple.pivotLt llt eql
leftLem : Vector.get' left kl llt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' left kl) kl (skip triple.pivot i) llt (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 kl cc))))
rightLem : Vector.get' right kl llt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' right kl) kl (skip triple.pivot i) llt (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 kl cc))))
topLem : Vector.get' top kl llt = Vector.get' top (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kl => Vector.get' top kl) kl (skip triple.pivot i) llt (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 kl cc))))
⊢ IsJoin (Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))
    (Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))
    (Vector.get' top (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))
Tactic:
exact triple.joinRest i iw
State after:
no goals

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
⊢ ClauseSat top valuation
Tactic:
have lem1 : right.get' kr rlt =
      right.get' triple.pivot triple.pivotLt := by
      apply witness_independent
      apply ccc
State after:
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
lem1 : Vector.get' right kr rlt = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation

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
lem1 : Vector.get' right kr rlt = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation
Tactic:
have lem2 : valuation.get' kr rlt =
      valuation.get' triple.pivot triple.pivotLt := by
      apply witness_independent
      apply ccc
State after:
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
lem1 : Vector.get' right kr rlt = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kr rlt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation

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
lem1 : Vector.get' right kr rlt = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kr rlt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation
Tactic:
rw [Vector.get'] at lem1
State after:
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
lem1 : Vector.get right { val := kr, isLt := rlt } = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kr rlt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation

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
lem1 : Vector.get right { val := kr, isLt := rlt } = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kr rlt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ ClauseSat top valuation
Tactic:
have lem5 : some false = some true := by
  rw [← cc, ← lem2, Vector.get', ← wr, lem1, triple.rightPivot]
State after:
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
lem1 : Vector.get right { val := kr, isLt := rlt } = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kr rlt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
lem5 : some false = some true
⊢ ClauseSat top valuation

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
lem1 : Vector.get right { val := kr, isLt := rlt } = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kr rlt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
lem5 : some false = some true
⊢ ClauseSat top valuation
Tactic:
simp at lem5
State after:
no goals

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
⊢ Vector.get' right kr rlt = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
Tactic:
apply witness_independent
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
⊢ kr = triple.pivot

State before:
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
⊢ kr = triple.pivot
Tactic:
apply ccc
State after:
no goals

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
lem1 : Vector.get' right kr rlt = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
⊢ Vector.get' valuation kr rlt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
Tactic:
apply witness_independent
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
lem1 : Vector.get' right kr rlt = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
⊢ kr = triple.pivot

State before:
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
lem1 : Vector.get' right kr rlt = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
⊢ kr = triple.pivot
Tactic:
apply ccc
State after:
no goals

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
lem1 : Vector.get right { val := kr, isLt := rlt } = Vector.get' right triple.pivot (_ : triple.pivot < n + 1)
lem2 : Vector.get' valuation kr rlt = Vector.get' valuation triple.pivot (_ : triple.pivot < n + 1)
⊢ some false = some true
Tactic:
rw [← cc, ← lem2, Vector.get', ← wr, lem1, triple.rightPivot]
State after:
no goals

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
⊢ Vector.get' left kr rlt = Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1)
Tactic:
apply witness_independent
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
⊢ kr = skip triple.pivot i

State before:
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
⊢ kr = skip triple.pivot i
Tactic:
rw [← eql]
State after:
no goals

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))))
⊢ Vector.get' right kr rlt = Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1)
Tactic:
apply witness_independent
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))))
⊢ kr = skip triple.pivot i

State before:
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))))
⊢ kr = skip triple.pivot i
Tactic:
rw [← eql]
State after:
no goals

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
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

State before:
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
Tactic:
rw [← eql]
State after:
no goals

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))))
topLem : Vector.get' top kr rlt = Vector.get' top (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kr => Vector.get' top 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))))
⊢ IsJoin (Vector.get' left kr rlt) (Vector.get' right kr rlt) (Vector.get' top kr rlt)
Tactic:
rw [leftLem, rightLem, topLem]
State after:
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))))
topLem : Vector.get' top kr rlt = Vector.get' top (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kr => Vector.get' top 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))))
⊢ IsJoin (Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))
    (Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))
    (Vector.get' top (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))

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))))
topLem : Vector.get' top kr rlt = Vector.get' top (skip triple.pivot i) (_ : skip triple.pivot i < n + 1) :=
  witness_independent (fun kr => Vector.get' top 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))))
⊢ IsJoin (Vector.get' left (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))
    (Vector.get' right (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))
    (Vector.get' top (skip triple.pivot i) (_ : skip triple.pivot i < n + 1))
Tactic:
exact triple.joinRest i iw
State after:
no goals