-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
theorem safe_insert_of_performRupCheck_insertRat {n : Nat} (f : DefaultFormula n)
    (hf : f.ratUnits = #[] ∧ AssignmentsInvariant f) (c : DefaultClause n) (rupHints : Array Nat) :
    (performRupCheck (insertRatUnits f (negate c)).1 rupHints).2.2.1 = true
      →
    Limplies (PosFin n) f (f.insert c)

Proof state:
case inl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c

Tactic:
exact sat_of_confirmRupHint_of_insertRat_fold f hf c rupHints p pf performRupCheck_success

Result:
no goals

Proof state:
case inl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c'

Tactic:
rw [c'_eq_c]

Result:
case inl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
⊢ ((f.insertRatUnits c.negate).fst.performRupCheck rupHints).snd.snd.fst = true → Limplies (PosFin n) f (f.insert c)

Tactic:
intro performRupCheck_success p pf

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success : ((f.insertRatUnits c.negate).fst.performRupCheck rupHints).snd.snd.fst = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.insert c

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_fc : c' ∈ (f.insert c).toList
⊢ p ⊨ c'

Tactic:
rw [insert_iff] at c'_in_fc

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_fc : c' = c ∨ c' ∈ f.toList
⊢ p ⊨ c'

Proof state:
case inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'

Tactic:
simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq] at pf

Result:
case inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pf : ∀ (x : DefaultClause n), x ∈ f.toList → p ⊨ x
⊢ p ⊨ c'

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.insert c

Tactic:
simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq]

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
pf : p ⊨ f
⊢ ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success : ((f.insertRatUnits c.negate).fst.performRupCheck rupHints).snd.snd.fst = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.insert c

Tactic:
simp only [performRupCheck] at performRupCheck_success

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.insert c

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_fc : c' = c ∨ c' ∈ f.toList
⊢ p ⊨ c'

Tactic:
rcases c'_in_fc with c'_eq_c | c'_in_f

Result:
case inl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c'

case inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'

Proof state:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
pf : p ⊨ f
⊢ ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x

Tactic:
intro c' c'_in_fc

Result:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant
c : DefaultClause n
rupHints : Array Nat
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints).2.2.fst =
    true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_fc : c' ∈ (f.insert c).toList
⊢ p ⊨ c'