-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddSound.lean
theorem unsat_of_encounteredBoth {n : Nat} (c : DefaultClause n)
    (assignment : Array Assignment) :
    reduce c assignment = encounteredBoth → Unsatisfiable (PosFin n) assignment

Proof state:
case h_2
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
ih : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
h :
  (match assignment[l.fst.val]! with
    | pos => if l.snd = true then reducedToUnit l else reducedToEmpty
    | neg => if (!l.snd) = true then reducedToUnit l else reducedToEmpty
    | both => encounteredBoth
    | unassigned => reducedToUnit l) =
    encounteredBoth
⊢ Unsatisfiable (PosFin n) assignment

Tactic:
split at h

Result:
case h_2.h_1
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
ih : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = pos
h : (if l.snd = true then reducedToUnit l else reducedToEmpty) = encounteredBoth
⊢ Unsatisfiable (PosFin n) assignment

case h_2.h_2
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
ih : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = neg
h : (if (!l.snd) = true then reducedToUnit l else reducedToEmpty) = encounteredBoth
⊢ Unsatisfiable (PosFin n) assignment

case h_2.h_3
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
ih : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = both
h : encounteredBoth = encounteredBoth
⊢ Unsatisfiable (PosFin n) assignment

case h_2.h_4
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
ih : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = unassigned
h : reducedToUnit l = encounteredBoth
⊢ Unsatisfiable (PosFin n) assignment

Proof state:
case h_2.h_1
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
ih : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = pos
h : (if l.snd = true then reducedToUnit l else reducedToEmpty) = encounteredBoth
⊢ Unsatisfiable (PosFin n) assignment

Tactic:
split at h <;> simp at h

Result:
no goals

Proof state:
case h_3.h_2
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → Unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = neg
h : (if (!l.snd) = true then reducedToNonunit else reducedToUnit l'✝) = encounteredBoth
⊢ Unsatisfiable (PosFin n) assignment

Tactic:
split at h <;> simp at h

Result:
no goals

Proof state:
n : Nat
c : DefaultClause n
assignment : Array Assignment
⊢ c.reduce assignment = encounteredBoth → Unsatisfiable (PosFin n) assignment

Tactic:
have hb : (reducedToEmpty : ReduceResult (PosFin n)) = encounteredBoth → Unsatisfiable (PosFin n) assignment := by
  simp

Result:
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
⊢ c.reduce assignment = encounteredBoth → Unsatisfiable (PosFin n) assignment

Proof state:
case h_2.h_2
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
ih : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = neg
h : (if (!l.snd) = true then reducedToUnit l else reducedToEmpty) = encounteredBoth
⊢ Unsatisfiable (PosFin n) assignment

Tactic:
split at h <;> simp at h

Result:
no goals

Proof state:
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
res : ReduceResult (PosFin n)
ih : res = encounteredBoth → Unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝ : l ∈ c.clause
h : reduce_fold_fn assignment res l = encounteredBoth
⊢ Unsatisfiable (PosFin n) assignment

Tactic:
rw [reduce_fold_fn.eq_def] at h

Result:
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → Unsatisfiable (PosFin n) assignment
res : ReduceResult (PosFin n)
ih : res = encounteredBoth → Unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝ : l ∈ c.clause
h :
  (match res with
    | encounteredBoth => encounteredBoth
    | reducedToEmpty =>
      match assignment[l.fst.val]! with
      | pos => if l.snd = true then reducedToUnit l else reducedToEmpty
      | neg => if (!l.snd) = true then reducedToUnit l else reducedToEmpty
      | both => encounteredBoth
      | unassigned => reducedToUnit l
    | reducedToUnit l' =>
      match assignment[l.fst.val]! with
      | pos => if l.snd = true then reducedToNonunit else reducedToUnit l'
      | neg => if (!l.snd) = true then reducedToNonunit else reducedToUnit l'
      | both => encounteredBoth
      | unassigned => reducedToNonunit
    | reducedToNonunit => reducedToNonunit) =
    encounteredBoth
⊢ Unsatisfiable (PosFin n) assignment