-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
theorem CNF.Clause.convertLRAT_sat_of_sat (clause : CNF.Clause (PosFin n))
    (h : Clause.convertLRAT' clause = some lratClause) :
    clause.eval assign → assign ⊨ lratClause

Proof state:
n : Nat
lratClause : DefaultClause n
assign : PosFin n → Bool
clause : CNF.Clause (PosFin n)
h : convertLRAT' clause = some lratClause
h2 : CNF.Clause.eval assign clause = true
⊢ assign ⊨ lratClause

Tactic:
simp only [CNF.Clause.eval, List.any_eq_true, bne_iff_ne, ne_eq] at h2

Result:
n : Nat
lratClause : DefaultClause n
assign : PosFin n → Bool
clause : CNF.Clause (PosFin n)
h : convertLRAT' clause = some lratClause
h2 : ∃ x, x ∈ clause ∧ (assign x.fst == x.snd) = true
⊢ assign ⊨ lratClause

Proof state:
case intro.intro
n : Nat
lratClause : DefaultClause n
assign : PosFin n → Bool
clause : CNF.Clause (PosFin n)
h : convertLRAT' clause = some lratClause
lit : Literal (PosFin n)
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ lit ∈ Clause.toList lratClause ∧ assign lit.fst = lit.snd

Tactic:
constructor

Result:
case intro.intro.left
n : Nat
lratClause : DefaultClause n
assign : PosFin n → Bool
clause : CNF.Clause (PosFin n)
h : convertLRAT' clause = some lratClause
lit : Literal (PosFin n)
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ lit ∈ Clause.toList lratClause

case intro.intro.right
n : Nat
lratClause : DefaultClause n
assign : PosFin n → Bool
clause : CNF.Clause (PosFin n)
h : convertLRAT' clause = some lratClause
lit : Literal (PosFin n)
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ assign lit.fst = lit.snd

Proof state:
case intro.intro.left
n : Nat
lratClause : DefaultClause n
assign : PosFin n → Bool
clause : CNF.Clause (PosFin n)
h : convertLRAT' clause = some lratClause
lit : Literal (PosFin n)
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ lit ∈ Clause.toList lratClause

Tactic:
simp only [Clause.toList, DefaultClause.toList]

Result:
case intro.intro.left
n : Nat
lratClause : DefaultClause n
assign : PosFin n → Bool
clause : CNF.Clause (PosFin n)
h : convertLRAT' clause = some lratClause
lit : Literal (PosFin n)
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ lit ∈ lratClause.clause

Proof state:
case intro.intro.right
n : Nat
lratClause : DefaultClause n
assign : PosFin n → Bool
clause : CNF.Clause (PosFin n)
h : convertLRAT' clause = some lratClause
lit : Literal (PosFin n)
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ assign lit.fst = lit.snd

Tactic:
simp_all

Result:
no goals

Proof state:
case intro.intro.left
n : Nat
lratClause : DefaultClause n
assign : PosFin n → Bool
clause : CNF.Clause (PosFin n)
h : convertLRAT' clause = some lratClause
lit : Literal (PosFin n)
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ lit ∈ lratClause.clause

Tactic:
simp only [convertLRAT'] at h

Result:
case intro.intro.left
n : Nat
lratClause : DefaultClause n
assign : PosFin n → Bool
clause : CNF.Clause (PosFin n)
h : DefaultClause.ofArray (List.toArray clause) = some lratClause
lit : Literal (PosFin n)
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ lit ∈ lratClause.clause

Proof state:
case intro.intro
n : Nat
lratClause : DefaultClause n
assign : PosFin n → Bool
clause : CNF.Clause (PosFin n)
h : convertLRAT' clause = some lratClause
lit : Literal (PosFin n)
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ ∃ x, x ∈ Clause.toList lratClause ∧ assign x.fst = x.snd

Tactic:
apply Exists.intro lit

Result:
case intro.intro
n : Nat
lratClause : DefaultClause n
assign : PosFin n → Bool
clause : CNF.Clause (PosFin n)
h : convertLRAT' clause = some lratClause
lit : Literal (PosFin n)
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ lit ∈ Clause.toList lratClause ∧ assign lit.fst = lit.snd

Proof state:
case intro.intro.left
n : Nat
lratClause : DefaultClause n
assign : PosFin n → Bool
clause : CNF.Clause (PosFin n)
h : DefaultClause.ofArray (List.toArray clause) = some lratClause
lit : Literal (PosFin n)
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ lit ∈ lratClause.clause

Tactic:
exact CNF.Clause.mem_lrat_of_mem clause hlit1 h

Result:
no goals

Proof state:
n : Nat
lratClause : DefaultClause n
assign : PosFin n → Bool
clause : CNF.Clause (PosFin n)
h : convertLRAT' clause = some lratClause
h2 : ∃ x, x ∈ clause ∧ (assign x.fst == x.snd) = true
⊢ ∃ x, x ∈ Clause.toList lratClause ∧ assign x.fst = x.snd

Tactic:
rcases h2 with ⟨lit, ⟨hlit1, hlit2⟩⟩

Result:
case intro.intro
n : Nat
lratClause : DefaultClause n
assign : PosFin n → Bool
clause : CNF.Clause (PosFin n)
h : convertLRAT' clause = some lratClause
lit : Literal (PosFin n)
hlit1 : lit ∈ clause
hlit2 : (assign lit.fst == lit.snd) = true
⊢ ∃ x, x ∈ Clause.toList lratClause ∧ assign x.fst = x.snd

Proof state:
n : Nat
lratClause : DefaultClause n
assign : PosFin n → Bool
clause : CNF.Clause (PosFin n)
h : convertLRAT' clause = some lratClause
⊢ CNF.Clause.eval assign clause = true → assign ⊨ lratClause

Tactic:
intro h2

Result:
n : Nat
lratClause : DefaultClause n
assign : PosFin n → Bool
clause : CNF.Clause (PosFin n)
h : convertLRAT' clause = some lratClause
h2 : CNF.Clause.eval assign clause = true
⊢ assign ⊨ lratClause