-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
theorem unsat_of_cons_none_unsat (clauses : List (Option (DefaultClause n))) :
    Unsatisfiable (PosFin n) (DefaultFormula.ofArray (none :: clauses).toArray)
      →
    Unsatisfiable (PosFin n) (DefaultFormula.ofArray clauses.toArray)

Proof state:
n : Nat
clauses : List (Option (DefaultClause n))
h : Unsatisfiable (PosFin n) (DefaultFormula.ofArray (none :: clauses).toArray)
assign : PosFin n → Bool
hassign : ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray clauses.toArray) → assign ⊨ x
clause : DefaultClause n
hclause : clause ∈ Formula.toList (DefaultFormula.ofArray (none :: clauses).toArray)
⊢ assign ⊨ clause

Tactic:
simp_all[DefaultFormula.ofArray, Formula.toList, DefaultFormula.toList]

Result:
no goals

Proof state:
n : Nat
clauses : List (Option (DefaultClause n))
⊢ Unsatisfiable (PosFin n) (DefaultFormula.ofArray (none :: clauses).toArray) →
    Unsatisfiable (PosFin n) (DefaultFormula.ofArray clauses.toArray)

Tactic:
intro h assign hassign

Result:
n : Nat
clauses : List (Option (DefaultClause n))
h : Unsatisfiable (PosFin n) (DefaultFormula.ofArray (none :: clauses).toArray)
assign : PosFin n → Bool
hassign : assign ⊨ DefaultFormula.ofArray clauses.toArray
⊢ False

Proof state:
n : Nat
clauses : List (Option (DefaultClause n))
h : Unsatisfiable (PosFin n) (DefaultFormula.ofArray (none :: clauses).toArray)
assign : PosFin n → Bool
hassign : assign ⊨ DefaultFormula.ofArray clauses.toArray
⊢ assign ⊨ DefaultFormula.ofArray (none :: clauses).toArray

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

Result:
n : Nat
clauses : List (Option (DefaultClause n))
h : Unsatisfiable (PosFin n) (DefaultFormula.ofArray (none :: clauses).toArray)
assign : PosFin n → Bool
hassign : ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray clauses.toArray) → assign ⊨ x
⊢ ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray (none :: clauses).toArray) → assign ⊨ x

Proof state:
n : Nat
clauses : List (Option (DefaultClause n))
h : Unsatisfiable (PosFin n) (DefaultFormula.ofArray (none :: clauses).toArray)
assign : PosFin n → Bool
hassign : ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray clauses.toArray) → assign ⊨ x
⊢ ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray (none :: clauses).toArray) → assign ⊨ x

Tactic:
intro clause hclause

Result:
n : Nat
clauses : List (Option (DefaultClause n))
h : Unsatisfiable (PosFin n) (DefaultFormula.ofArray (none :: clauses).toArray)
assign : PosFin n → Bool
hassign : ∀ (x : DefaultClause n), x ∈ Formula.toList (DefaultFormula.ofArray clauses.toArray) → assign ⊨ x
clause : DefaultClause n
hclause : clause ∈ Formula.toList (DefaultFormula.ofArray (none :: clauses).toArray)
⊢ assign ⊨ clause

Proof state:
n : Nat
clauses : List (Option (DefaultClause n))
h : Unsatisfiable (PosFin n) (DefaultFormula.ofArray (none :: clauses).toArray)
assign : PosFin n → Bool
hassign : assign ⊨ DefaultFormula.ofArray clauses.toArray
⊢ False

Tactic:
apply h assign

Result:
n : Nat
clauses : List (Option (DefaultClause n))
h : Unsatisfiable (PosFin n) (DefaultFormula.ofArray (none :: clauses).toArray)
assign : PosFin n → Bool
hassign : assign ⊨ DefaultFormula.ofArray clauses.toArray
⊢ assign ⊨ DefaultFormula.ofArray (none :: clauses).toArray