-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
theorem CNF.unsat_of_convertLRAT_unsat (cnf : CNF Nat) :
    Unsatisfiable (PosFin (cnf.numLiterals + 1)) (CNF.convertLRAT cnf)
      →
    cnf.Unsat

Proof state:
case a
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
⊢ CNF.eval assignment (lift cnf) = false

Tactic:
apply eq_false_of_ne_true

Result:
case a.a
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
⊢ ¬CNF.eval assignment (lift cnf) = true

Proof state:
cnf : CNF Nat
⊢ Unsatisfiable (PosFin (cnf.numLiterals + 1)) (convertLRAT cnf) → cnf.Unsat

Tactic:
intro h1

Result:
cnf : CNF Nat
h1 : Unsatisfiable (PosFin (cnf.numLiterals + 1)) (convertLRAT cnf)
⊢ cnf.Unsat

Proof state:
case a.a.intro.intro
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
h2 : CNF.eval assignment (lift cnf) = true
lratClause : DefaultClause (cnf.numLiterals + 1)
reflectClause : CNF.Clause (PosFin (cnf.numLiterals + 1))
hrclause1 : reflectClause ∈ lift cnf
hrclause2 :
  (match Clause.convertLRAT' reflectClause with
    | some clause => some (some clause)
    | none => none) =
    some (some lratClause)
⊢ assignment ⊨ lratClause

Tactic:
simp only [CNF.eval, List.all_eq_true] at h2

Result:
case a.a.intro.intro
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
lratClause : DefaultClause (cnf.numLiterals + 1)
reflectClause : CNF.Clause (PosFin (cnf.numLiterals + 1))
hrclause1 : reflectClause ∈ lift cnf
hrclause2 :
  (match Clause.convertLRAT' reflectClause with
    | some clause => some (some clause)
    | none => none) =
    some (some lratClause)
h2 : ∀ (x : CNF.Clause (PosFin (cnf.numLiterals + 1))), x ∈ lift cnf → CNF.Clause.eval assignment x = true
⊢ assignment ⊨ lratClause

Proof state:
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
lratClause : DefaultClause (cnf.numLiterals + 1)
reflectClause : CNF.Clause (PosFin (cnf.numLiterals + 1))
hrclause1 : reflectClause ∈ lift cnf
h2 : ∀ (x : CNF.Clause (PosFin (cnf.numLiterals + 1))), x ∈ lift cnf → CNF.Clause.eval assignment x = true
x✝ : Option (DefaultClause (cnf.numLiterals + 1))
clause✝ : DefaultClause (cnf.numLiterals + 1)
heq : Clause.convertLRAT' reflectClause = some clause✝
hrclause2 : some (Clause.convertLRAT' reflectClause) = some (some lratClause)
⊢ assignment ⊨ lratClause

Tactic:
simp only [Option.some.injEq] at hrclause2

Result:
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
lratClause : DefaultClause (cnf.numLiterals + 1)
reflectClause : CNF.Clause (PosFin (cnf.numLiterals + 1))
hrclause1 : reflectClause ∈ lift cnf
h2 : ∀ (x : CNF.Clause (PosFin (cnf.numLiterals + 1))), x ∈ lift cnf → CNF.Clause.eval assignment x = true
x✝ : Option (DefaultClause (cnf.numLiterals + 1))
clause✝ : DefaultClause (cnf.numLiterals + 1)
heq : Clause.convertLRAT' reflectClause = some clause✝
hrclause2 : Clause.convertLRAT' reflectClause = some lratClause
⊢ assignment ⊨ lratClause

Proof state:
case a.a.intro.intro
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
lratClause : DefaultClause (cnf.numLiterals + 1)
reflectClause : CNF.Clause (PosFin (cnf.numLiterals + 1))
hrclause1 : reflectClause ∈ lift cnf
hrclause2 :
  (match Clause.convertLRAT' reflectClause with
    | some clause => some (some clause)
    | none => none) =
    some (some lratClause)
h2 : ∀ (x : CNF.Clause (PosFin (cnf.numLiterals + 1))), x ∈ lift cnf → CNF.Clause.eval assignment x = true
⊢ assignment ⊨ lratClause

Tactic:
split at hrclause2

Result:
case a.a.intro.intro.h_1
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
lratClause : DefaultClause (cnf.numLiterals + 1)
reflectClause : CNF.Clause (PosFin (cnf.numLiterals + 1))
hrclause1 : reflectClause ∈ lift cnf
h2 : ∀ (x : CNF.Clause (PosFin (cnf.numLiterals + 1))), x ∈ lift cnf → CNF.Clause.eval assignment x = true
x✝ : Option (DefaultClause (cnf.numLiterals + 1))
clause✝ : DefaultClause (cnf.numLiterals + 1)
heq✝ : Clause.convertLRAT' reflectClause = some clause✝
hrclause2 : some (some clause✝) = some (some lratClause)
⊢ assignment ⊨ lratClause

case a.a.intro.intro.h_2
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
lratClause : DefaultClause (cnf.numLiterals + 1)
reflectClause : CNF.Clause (PosFin (cnf.numLiterals + 1))
hrclause1 : reflectClause ∈ lift cnf
h2 : ∀ (x : CNF.Clause (PosFin (cnf.numLiterals + 1))), x ∈ lift cnf → CNF.Clause.eval assignment x = true
x✝ : Option (DefaultClause (cnf.numLiterals + 1))
heq✝ : Clause.convertLRAT' reflectClause = none
hrclause2 : none = some (some lratClause)
⊢ assignment ⊨ lratClause

Proof state:
case a.a
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
h2 : CNF.eval assignment (lift cnf) = true
⊢ ∀ (x : DefaultClause (cnf.numLiterals + 1)),
    x ∈ Formula.toList (DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray) → assignment ⊨ x

Tactic:
intro lratClause hlclause

Result:
case a.a
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
h2 : CNF.eval assignment (lift cnf) = true
lratClause : DefaultClause (cnf.numLiterals + 1)
hlclause : lratClause ∈ Formula.toList (DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
⊢ assignment ⊨ lratClause

Proof state:
case a.a.intro.intro.h_1
cnf : CNF Nat
assignment : PosFin (cnf.numLiterals + 1) → Bool
h1 : ¬(assignment ⊨ DefaultFormula.ofArray (convertLRAT' (lift cnf)).toArray)
lratClause : DefaultClause (cnf.numLiterals + 1)
reflectClause : CNF.Clause (PosFin (cnf.numLiterals + 1))
hrclause1 : reflectClause ∈ lift cnf
h2 : ∀ (x : CNF.Clause (PosFin (cnf.numLiterals + 1))), x ∈ lift cnf → CNF.Clause.eval assignment x = true
x✝ : Option (DefaultClause (cnf.numLiterals + 1))
clause✝ : DefaultClause (cnf.numLiterals + 1)
heq✝ : Clause.convertLRAT' reflectClause = some clause✝
hrclause2 : some (some clause✝) = some (some lratClause)
⊢ assignment ⊨ lratClause

Tactic:
next heq =>
rw [← heq] at hrclause2
simp only [Option.some.injEq] at hrclause2
simp [CNF.Clause.convertLRAT_sat_of_sat reflectClause hrclause2, h2 reflectClause hrclause1]

Result:
no goals