Theorem: LRAT.DefaultFormula.limplies_of_insert (LeanSAT/LRAT/Formula/Basic.lean)

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ limplies (PosFin n) (f.insert c) f
Tactic:
intro p
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
⊢ p ⊨ f.insert c → p ⊨ f

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
⊢ p ⊨ f.insert c → p ⊨ f
Tactic:
simp only [formulaHSat_def, List.all_eq_true, decide_eq_true_eq]
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
⊢ (∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x) → ∀ (x : DefaultClause n), x ∈ f.toList → p ⊨ x

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
⊢ (∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x) → ∀ (x : DefaultClause n), x ∈ f.toList → p ⊨ x
Tactic:
intro h c' c'_in_f
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'
Tactic:
have c'_in_fc : c' ∈ toList (insert f c) := by
  simp only [insert_iff, Array.toList_eq, Array.data_toArray, List.mem_singleton]
  exact Or.inr c'_in_f
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
c'_in_fc : c' ∈ (f.insert c).toList
⊢ p ⊨ c'

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
c'_in_fc : c' ∈ (f.insert c).toList
⊢ p ⊨ c'
Tactic:
exact h c' c'_in_fc
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ c' ∈ (f.insert c).toList
Tactic:
simp only [insert_iff, Array.toList_eq, Array.data_toArray, List.mem_singleton]
State after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ c' = c ∨ c' ∈ f.toList

State before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ c' = c ∨ c' ∈ f.toList
Tactic:
exact Or.inr c'_in_f
State after:
no goals