-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
theorem ratAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (p : Literal (PosFin n))
  (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat)) (f' : DefaultFormula n)
  (f_readyForRatAdd : ReadyForRatAdd f) (_pc : p ∈ Clause.toList c)
  (ratAddSuccess : performRatAdd f c p rupHints ratHints = (f', true)) : f' = insert f c

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.ReadyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negate ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
performRupCheck_res : DefaultFormula n := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
hsize : performRupCheck_res.assignments.size = n
⊢ performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n

Tactic:
exact And.intro f_readyForRatAdd.1 hsize

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.ReadyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negate ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
performRupCheck_res : DefaultFormula n := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
⊢ performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n

Tactic:
have hsize : performRupCheck_res.assignments.size = n := by
  rw [size_assignments_performRupCheck, size_assignments_insertRupUnits, f_readyForRatAdd.2.2.1]

Result:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.ReadyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negate ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
performRupCheck_res : DefaultFormula n := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
hsize : performRupCheck_res.assignments.size = n
⊢ performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n

Proof state:
case isTrue.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.ReadyForRatAdd
_pc : p ∈ Clause.toList c
h✝² : f.ratHintsExhaustive p ratHints = true
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
ratAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ f' = f.insert c

Tactic:
simp at ratAddSuccess

Result:
no goals

Proof state:
case isTrue.isFalse.isFalse.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.ReadyForRatAdd
_pc : p ∈ Clause.toList c
h✝⁴ : f.ratHintsExhaustive p ratHints = true
h✝³ : ¬(f.insertRupUnits c.negate).snd = true
h✝² : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
h✝ :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negate ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).snd =
    false
ratAddSuccess :
  ((Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negate ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).fst,
      false) =
    (f', true)
⊢ f' = f.insert c

Tactic:
simp at ratAddSuccess

Result:
no goals