-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
theorem safe_insert_of_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : ReadyForRupAdd f)
    (c : DefaultClause n) :
    (insertRupUnits f (negate c)).2 = true → Limplies (PosFin n) f (f.insert c)

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = 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
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = 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
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = 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
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = 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
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'

Proof state:
case inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c

Tactic:
exact sat_of_insertRup f f_readyForRupAdd c p pf h

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
⊢ (f.insertRupUnits c.negate).snd = true → Limplies (PosFin n) f (f.insert c)

Tactic:
intro h p pf

Result:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.insert c

Proof state:
case inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = 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
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = 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
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = 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
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_fc : c' ∈ (f.insert c).toList
⊢ p ⊨ c'

Proof state:
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = 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
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_in_fc : c' = c ∨ c' ∈ f.toList
⊢ p ⊨ c'

Proof state:
case inl
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = 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
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = true
p : PosFin n → Bool
pf : p ⊨ f
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c

Proof state:
case inr
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
c : DefaultClause n
h : (f.insertRupUnits c.negate).snd = 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'

Tactic:
exact pf c' c'_in_f

Result:
no goals