internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq✝ : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝ : Option (DefaultClause n)
l : Literal (PosFin n)
nodupkey✝ : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l]
nodup✝ : [l].Nodup
heq : c = { clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ }
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
rw [heq] at hl
Proof state after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq✝ : f.clauses[id]! = some c
x✝ : Option (DefaultClause n)
l : Literal (PosFin n)
nodupkey✝ : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l]
nodup✝ : [l].Nodup
hl :
  ∀ (x : PosFin n),
    ¬{ clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ } = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬{ clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ } = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
heq : c = { clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ }
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq✝ : f.clauses[id]! = some c
x✝ : Option (DefaultClause n)
l : Literal (PosFin n)
nodupkey✝ : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l]
nodup✝ : [l].Nodup
hl :
  ∀ (x : PosFin n),
    ¬{ clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ } = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬{ clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ } = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
heq : c = { clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ }
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
specialize hl l.1
Proof state after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq✝ : f.clauses[id]! = some c
x✝ : Option (DefaultClause n)
l : Literal (PosFin n)
nodupkey✝ : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l]
nodup✝ : [l].Nodup
heq : c = { clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ }
hl :
  ¬{ clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ } =
        { clause := [(l.fst, false)], nodupkey := ⋯, nodup := ⋯ } ∧
    ¬{ clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ } =
        { clause := [(l.fst, true)], nodupkey := ⋯, nodup := ⋯ }
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq✝ : f.clauses[id]! = some c
x✝ : Option (DefaultClause n)
l : Literal (PosFin n)
nodupkey✝ : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l]
nodup✝ : [l].Nodup
heq : c = { clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ }
hl :
  ¬{ clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ } =
        { clause := [(l.fst, false)], nodupkey := ⋯, nodup := ⋯ } ∧
    ¬{ clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ } =
        { clause := [(l.fst, true)], nodupkey := ⋯, nodup := ⋯ }
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
simp only [DefaultClause.mk.injEq, List.cons.injEq, and_true] at hl
Proof state after:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq✝ : f.clauses[id]! = some c
x✝ : Option (DefaultClause n)
l : Literal (PosFin n)
nodupkey✝ : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l]
nodup✝ : [l].Nodup
heq : c = { clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ }
hl : ¬l = (l.fst, false) ∧ ¬l = (l.fst, true)
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq✝ : f.clauses[id]! = some c
x✝ : Option (DefaultClause n)
l : Literal (PosFin n)
nodupkey✝ : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l]
nodup✝ : [l].Nodup
heq : c = { clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ }
hl : ¬l = (l.fst, false) ∧ ¬l = (l.fst, true)
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
by_cases hl2 : l.2
Proof state after:
case pos
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq✝ : f.clauses[id]! = some c
x✝ : Option (DefaultClause n)
l : Literal (PosFin n)
nodupkey✝ : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l]
nodup✝ : [l].Nodup
heq : c = { clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ }
hl : ¬l = (l.fst, false) ∧ ¬l = (l.fst, true)
hl2 : l.snd = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq✝ : f.clauses[id]! = some c
x✝ : Option (DefaultClause n)
l : Literal (PosFin n)
nodupkey✝ : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l]
nodup✝ : [l].Nodup
heq : c = { clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ }
hl : ¬l = (l.fst, false) ∧ ¬l = (l.fst, true)
hl2 : ¬l.snd = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case pos
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq✝ : f.clauses[id]! = some c
x✝ : Option (DefaultClause n)
l : Literal (PosFin n)
nodupkey✝ : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l]
nodup✝ : [l].Nodup
heq : c = { clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ }
hl : ¬l = (l.fst, false) ∧ ¬l = (l.fst, true)
hl2 : l.snd = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList

case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq✝ : f.clauses[id]! = some c
x✝ : Option (DefaultClause n)
l : Literal (PosFin n)
nodupkey✝ : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l]
nodup✝ : [l].Nodup
heq : c = { clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ }
hl : ¬l = (l.fst, false) ∧ ¬l = (l.fst, true)
hl2 : ¬l.snd = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
. simp only [← hl2, Prod.mk.eta, not_true, and_false] at hl
Proof state after:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq✝ : f.clauses[id]! = some c
x✝ : Option (DefaultClause n)
l : Literal (PosFin n)
nodupkey✝ : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l]
nodup✝ : [l].Nodup
heq : c = { clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ }
hl : ¬l = (l.fst, false) ∧ ¬l = (l.fst, true)
hl2 : ¬l.snd = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq✝ : f.clauses[id]! = some c
x✝ : Option (DefaultClause n)
l : Literal (PosFin n)
nodupkey✝ : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l]
nodup✝ : [l].Nodup
heq : c = { clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ }
hl : ¬l = (l.fst, false) ∧ ¬l = (l.fst, true)
hl2 : ¬l.snd = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
. simp only [Bool.not_eq_true] at hl2
  simp only [← hl2, Prod.mk.eta, not_true, false_and] at hl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case pos
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq✝ : f.clauses[id]! = some c
x✝ : Option (DefaultClause n)
l : Literal (PosFin n)
nodupkey✝ : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l]
nodup✝ : [l].Nodup
heq : c = { clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ }
hl : ¬l = (l.fst, false) ∧ ¬l = (l.fst, true)
hl2 : l.snd = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
simp only [← hl2, Prod.mk.eta, not_true, and_false] at hl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq✝ : f.clauses[id]! = some c
x✝ : Option (DefaultClause n)
l : Literal (PosFin n)
nodupkey✝ : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l]
nodup✝ : [l].Nodup
heq : c = { clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ }
hl : ¬l = (l.fst, false) ∧ ¬l = (l.fst, true)
hl2 : ¬l.snd = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
simp only [Bool.not_eq_true] at hl2
Proof state after:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq✝ : f.clauses[id]! = some c
x✝ : Option (DefaultClause n)
l : Literal (PosFin n)
nodupkey✝ : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l]
nodup✝ : [l].Nodup
heq : c = { clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ }
hl : ¬l = (l.fst, false) ∧ ¬l = (l.fst, true)
hl2 : l.snd = false
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case neg
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq✝ : f.clauses[id]! = some c
x✝ : Option (DefaultClause n)
l : Literal (PosFin n)
nodupkey✝ : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l]
nodup✝ : [l].Nodup
heq : c = { clause := [l], nodupkey := nodupkey✝, nodup := nodup✝ }
hl : ¬l = (l.fst, false) ∧ ¬l = (l.fst, true)
hl2 : l.snd = false
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }.toList
Tactic:
simp only [← hl2, Prod.mk.eta, not_true, false_and] at hl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case neg.h_3
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments }.toList
Tactic:
have deleteOne_f_rw : deleteOne f id = ⟨Array.set! f.clauses id none, f.rupUnits, f.ratUnits, f.assignments⟩ := by
  simp only [deleteOne]
  split
  . next heq2 =>
    simp only [heq] at heq2
  . next l _ _ heq2 =>
    simp only [heq, Option.some.injEq] at heq2
    rw [heq2] at hl
    specialize hl l.1
    simp only [DefaultClause.mk.injEq, List.cons.injEq, and_true] at hl
    by_cases hl2 : l.2
    . simp only [← hl2, Prod.mk.eta, not_true, and_false] at hl
    . simp only [Bool.not_eq_true] at hl2
      simp only [← hl2, Prod.mk.eta, not_true, false_and] at hl
  . rfl
Proof state after:
case neg.h_3
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments }.toList
Theorem: LRAT.DefaultFormula.deleteOne_preserves_strong_assignments_invariant
Proof state before:
case neg.h_3
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.deleteOne id).assignments[i.val] = true
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments }.toList
Tactic:
simp only [deleteOne_f_rw] at hb
Proof state after:
case neg.h_3
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
⊢ unit (i, b) ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments }.toList