Theorem: LRAT.DefaultFormula.performRatCheck_success_entails_c_without_negPivot
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
negPivot : Literal (PosFin n)
ratHint : Nat × Array Nat
c : DefaultClause n
hc : f.clauses[ratHint.fst]! = some c
p : PosFin n → Bool
pf : p ⊨ f
h✝ :
  ¬({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments }.insertRatUnits
          (c.delete negPivot).negate).snd =
      true
performRatCheck_success :
  ({
            clauses :=
              (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                              assignments := f.assignments }.insertRatUnits
                          (c.delete negPivot).negate).fst.performRupCheck
                    ratHint.snd).1.clauses,
            rupUnits :=
              (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                              assignments := f.assignments }.insertRatUnits
                          (c.delete negPivot).negate).fst.performRupCheck
                    ratHint.snd).1.rupUnits,
            ratUnits :=
              (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                              assignments := f.assignments }.insertRatUnits
                          (c.delete negPivot).negate).fst.performRupCheck
                    ratHint.snd).1.ratUnits,
            assignments :=
              restoreAssignments
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete negPivot).negate).fst.performRupCheck
                      ratHint.snd).1.assignments
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete negPivot).negate).fst.performRupCheck
                      ratHint.snd).2.fst }.clearRatUnits,
        true).snd =
    true
h :
  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                        assignments := f.assignments }.insertRatUnits
                    (c.delete negPivot).negate).fst.performRupCheck
              ratHint.snd).2.2.snd =
      false ∧
    (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                        assignments := f.assignments }.insertRatUnits
                    (c.delete negPivot).negate).fst.performRupCheck
              ratHint.snd).2.2.fst =
      true
pfc : ∀ (x : DefaultClause n), x ∈ (f.insert (c.delete negPivot)).toList → decide (Clause.instHSat.1 p x) = true
⊢ c.delete negPivot ∈ (f.insert (c.delete negPivot)).toList
Tactic:
rw [insert_iff]
Proof state after:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
negPivot : Literal (PosFin n)
ratHint : Nat × Array Nat
c : DefaultClause n
hc : f.clauses[ratHint.fst]! = some c
p : PosFin n → Bool
pf : p ⊨ f
h✝ :
  ¬({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments }.insertRatUnits
          (c.delete negPivot).negate).snd =
      true
performRatCheck_success :
  ({
            clauses :=
              (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                              assignments := f.assignments }.insertRatUnits
                          (c.delete negPivot).negate).fst.performRupCheck
                    ratHint.snd).1.clauses,
            rupUnits :=
              (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                              assignments := f.assignments }.insertRatUnits
                          (c.delete negPivot).negate).fst.performRupCheck
                    ratHint.snd).1.rupUnits,
            ratUnits :=
              (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                              assignments := f.assignments }.insertRatUnits
                          (c.delete negPivot).negate).fst.performRupCheck
                    ratHint.snd).1.ratUnits,
            assignments :=
              restoreAssignments
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete negPivot).negate).fst.performRupCheck
                      ratHint.snd).1.assignments
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete negPivot).negate).fst.performRupCheck
                      ratHint.snd).2.fst }.clearRatUnits,
        true).snd =
    true
h :
  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                        assignments := f.assignments }.insertRatUnits
                    (c.delete negPivot).negate).fst.performRupCheck
              ratHint.snd).2.2.snd =
      false ∧
    (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                        assignments := f.assignments }.insertRatUnits
                    (c.delete negPivot).negate).fst.performRupCheck
              ratHint.snd).2.2.fst =
      true
pfc : ∀ (x : DefaultClause n), x ∈ (f.insert (c.delete negPivot)).toList → decide (Clause.instHSat.1 p x) = true
⊢ c.delete negPivot = c.delete negPivot ∨ c.delete negPivot ∈ f.toList