-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
theorem rupAdd_sound {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rupHints : Array Nat)
    (f' : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f)
    (rupAddSuccess : performRupAdd f c rupHints = (f', true)) :
    Liff (PosFin n) f f'

Proof state:
case left
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
f'_def : f' = f.insert c
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
performRupCheck_success : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
rupAddSuccess :
  ({ clauses := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.clauses,
              rupUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.rupUnits,
              ratUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.ratUnits,
              assignments :=
                restoreAssignments ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
f_limplies_fc : Limplies (PosFin n) f (f.insert c)
⊢ Limplies (PosFin n) f (f.insert c)

Tactic:
exact f_limplies_fc

Result:
no goals

Proof state:
case right
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
f'_def : f' = f.insert c
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
performRupCheck_success : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
rupAddSuccess :
  ({ clauses := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.clauses,
              rupUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.rupUnits,
              ratUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.ratUnits,
              assignments :=
                restoreAssignments ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
f_limplies_fc : Limplies (PosFin n) f (f.insert c)
⊢ Limplies (PosFin n) (f.insert c) f

Tactic:
exact limplies_insert f c

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
⊢ p ⊨ f ↔ p ⊨ f'

Tactic:
have f_limplies_fc := safe_insert_of_insertRup f f_readyForRupAdd c insertRupContradiction p

Result:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
f_limplies_fc : p ⊨ f → p ⊨ f.insert c
⊢ p ⊨ f ↔ p ⊨ f'

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
f'_def : f' = f.insert c
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
performRupCheck_success : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false
rupAddSuccess :
  ({ clauses := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.clauses,
              rupUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.rupUnits,
              ratUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.ratUnits,
              assignments :=
                restoreAssignments ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
⊢ Liff (PosFin n) f f'

Tactic:
rw [Bool.not_eq_false] at performRupCheck_success

Result:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
f'_def : f' = f.insert c
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
performRupCheck_success : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
rupAddSuccess :
  ({ clauses := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.clauses,
              rupUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.rupUnits,
              ratUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.ratUnits,
              assignments :=
                restoreAssignments ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
⊢ Liff (PosFin n) f f'

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
f_limplies_fc : p ⊨ f → p ⊨ f.insert c
⊢ p ⊨ f ↔ p ⊨ f'

Tactic:
rw [f'_def]

Result:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
f'_def : f' = f.insert c
insertRupContradiction : (f.insertRupUnits c.negate).snd = true
rupAddSuccess : ((f.insertRupUnits c.negate).fst.clearRupUnits.insert c, true) = (f', true)
p : PosFin n → Bool
f_limplies_fc : p ⊨ f → p ⊨ f.insert c
⊢ p ⊨ f ↔ p ⊨ f.insert c

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
rupAddSuccess : f.performRupAdd c rupHints = (f', true)
⊢ Liff (PosFin n) f f'

Tactic:
have f'_def := rupAdd_result f c rupHints f' f_readyForRupAdd rupAddSuccess

Result:
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
rupAddSuccess : f.performRupAdd c rupHints = (f', true)
f'_def : f' = f.insert c
⊢ Liff (PosFin n) f f'