Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant (LeanSAT/LRAT/Formula/RupAddResult.lean)

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
ih : ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
  ∃ hsize, f.derivedLits_invariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst
Tactic:
rcases ih with ⟨hsize, ih⟩
State after:
case intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
  ∃ hsize, f.derivedLits_invariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst

State before:
case intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
  ∃ hsize, f.derivedLits_invariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst
Tactic:
have hsize' : Array.size ((confirmRupHint f.clauses) acc rupHints[i]).1 = n := by
  rw [confirmRupHint_preserves_assignments_size]
  exact hsize
State after:
case intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
⊢ let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
  ∃ hsize, f.derivedLits_invariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst

State before:
case intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
⊢ let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
  ∃ hsize, f.derivedLits_invariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst
Tactic:
apply Exists.intro hsize'
State after:
case intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
⊢ f.derivedLits_invariant f_assignments_size (confirmRupHint f.clauses acc rupHints[i]).fst hsize'
    (confirmRupHint f.clauses acc rupHints[i]).snd.fst

State before:
case intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
⊢ f.derivedLits_invariant f_assignments_size (confirmRupHint f.clauses acc rupHints[i]).fst hsize'
    (confirmRupHint f.clauses acc rupHints[i]).snd.fst
Tactic:
simp only [confirmRupHint, Fin.getElem_fin]
State after:
case intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
⊢ f.derivedLits_invariant f_assignments_size
    (if (acc.2.2.snd || acc.2.2.fst) = true then (acc.fst, acc.2.fst, acc.2.2.fst, acc.2.2.snd)
      else
        match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (if (acc.2.2.snd || acc.2.2.fst) = true then (acc.fst, acc.2.fst, acc.2.2.fst, acc.2.2.snd)
        else
          match f.clauses[rupHints[↑i]]? with
          | some (some c) =>
            match c.reduce acc.fst with
            | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
            | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
            | ReduceResult.reducedToUnit (l, b) =>
              if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
              else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
            | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
          | some none => (acc.fst, acc.2.fst, false, true)
          | none => (acc.fst, acc.2.fst, false, true)).snd.fst

State before:
case intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
⊢ f.derivedLits_invariant f_assignments_size
    (if (acc.2.2.snd || acc.2.2.fst) = true then (acc.fst, acc.2.fst, acc.2.2.fst, acc.2.2.snd)
      else
        match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (if (acc.2.2.snd || acc.2.2.fst) = true then (acc.fst, acc.2.fst, acc.2.2.fst, acc.2.2.snd)
        else
          match f.clauses[rupHints[↑i]]? with
          | some (some c) =>
            match c.reduce acc.fst with
            | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
            | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
            | ReduceResult.reducedToUnit (l, b) =>
              if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
              else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
            | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
          | some none => (acc.fst, acc.2.fst, false, true)
          | none => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
split
State after:
case intro.isTrue
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : (acc.2.2.snd || acc.2.2.fst) = true
⊢ f.derivedLits_invariant f_assignments_size (acc.fst, acc.2.fst, acc.2.2.fst, acc.2.2.snd).fst ⋯
    (acc.fst, acc.2.fst, acc.2.2.fst, acc.2.2.snd).snd.fst

case intro.isFalse
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst

State before:
case intro.isTrue
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : (acc.2.2.snd || acc.2.2.fst) = true
⊢ f.derivedLits_invariant f_assignments_size (acc.fst, acc.2.fst, acc.2.2.fst, acc.2.2.snd).fst ⋯
    (acc.fst, acc.2.fst, acc.2.2.fst, acc.2.2.snd).snd.fst

case intro.isFalse
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
. exact ih
State after:
case intro.isFalse
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst

State before:
case intro.isFalse
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
. have rupHint_clause_options :
    f.clauses[rupHints[i.1]]? = none ∨ f.clauses[rupHints[i.1]]? = some none ∨ ∃ c, f.clauses[rupHints[i.val]]? = some (some c) := by
    match f.clauses[rupHints[i.val]]? with
    | none => exact Or.inl rfl
    | some none => exact Or.inr $ Or.inl rfl
    | some (some c) => exact (Or.inr ∘ Or.inr ∘ Exists.intro c) rfl
  rcases rupHint_clause_options with rupHint_clause_eq_none | rupHint_clause_eq_some_none | ⟨c, rupHint_clause_eq_c⟩
  . simp only [rupHint_clause_eq_none]
    exact ih
  . simp only [rupHint_clause_eq_some_none]
    exact ih
  . simp only [rupHint_clause_eq_c]
    have reduce_c_options : reduce c acc.1 = ReduceResult.encounteredBoth ∨ reduce c acc.1 = ReduceResult.reducedToEmpty ∨
      (∃ l : Literal (PosFin n), reduce c acc.1 = ReduceResult.reducedToUnit l) ∨ reduce c acc.1 = ReduceResult.reducedToNonunit := by
      match reduce c acc.fst with
      | ReduceResult.encounteredBoth => exact Or.inl rfl
      | ReduceResult.reducedToEmpty => exact (Or.inr ∘ Or.inl) rfl
      | ReduceResult.reducedToUnit l => exact (Or.inr ∘ Or.inr ∘ Or.inl ∘ Exists.intro l) rfl
      | ReduceResult.reducedToNonunit => exact (Or.inr ∘ Or.inr ∘ Or.inr) rfl
    rcases reduce_c_options with hencounteredBoth | hreducedToEmpty | ⟨l, hreducedToUnit⟩ | hreducedToNonunit
    . simp only [hencounteredBoth]
      exact ih
    . simp only [hreducedToEmpty]
      exact ih
    . simp only [hreducedToUnit, Prod.mk.eta]
      by_cases h : hasAssignment l.snd acc.fst[l.fst.val]!
      . simp only [h, ite_true]
        exact ih
      . simp only [h, ite_false]
        exact confirmRupHint_preserves_invariant_helper f f_assignments_size acc hsize l ih h
    . simp only [hreducedToNonunit]
      exact ih
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
Tactic:
rw [confirmRupHint_preserves_assignments_size]
State after:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ acc.fst.size = n

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ acc.fst.size = n
Tactic:
exact hsize
State after:
no goals

State before:
case intro.isTrue
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : (acc.2.2.snd || acc.2.2.fst) = true
⊢ f.derivedLits_invariant f_assignments_size (acc.fst, acc.2.fst, acc.2.2.fst, acc.2.2.snd).fst ⋯
    (acc.fst, acc.2.fst, acc.2.2.fst, acc.2.2.snd).snd.fst
Tactic:
exact ih
State after:
no goals

State before:
case intro.isFalse
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
have rupHint_clause_options :
  f.clauses[rupHints[i.1]]? = none ∨ f.clauses[rupHints[i.1]]? = some none ∨ ∃ c, f.clauses[rupHints[i.val]]? = some (some c) := by
  match f.clauses[rupHints[i.val]]? with
  | none => exact Or.inl rfl
  | some none => exact Or.inr $ Or.inl rfl
  | some (some c) => exact (Or.inr ∘ Or.inr ∘ Exists.intro c) rfl
State after:
case intro.isFalse
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
rupHint_clause_options :
  f.clauses[rupHints[↑i]]? = none ∨ f.clauses[rupHints[↑i]]? = some none ∨ ∃ c, f.clauses[rupHints[↑i]]? = some (some c)
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst

State before:
case intro.isFalse
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
rupHint_clause_options :
  f.clauses[rupHints[↑i]]? = none ∨ f.clauses[rupHints[↑i]]? = some none ∨ ∃ c, f.clauses[rupHints[↑i]]? = some (some c)
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
rcases rupHint_clause_options with rupHint_clause_eq_none | rupHint_clause_eq_some_none | ⟨c, rupHint_clause_eq_c⟩
State after:
case intro.isFalse.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
rupHint_clause_eq_none : f.clauses[rupHints[↑i]]? = none
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
rupHint_clause_eq_some_none : f.clauses[rupHints[↑i]]? = some none
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inr.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst

State before:
case intro.isFalse.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
rupHint_clause_eq_none : f.clauses[rupHints[↑i]]? = none
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
rupHint_clause_eq_some_none : f.clauses[rupHints[↑i]]? = some none
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inr.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
. simp only [rupHint_clause_eq_none]
  exact ih
State after:
case intro.isFalse.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
rupHint_clause_eq_some_none : f.clauses[rupHints[↑i]]? = some none
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inr.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst

State before:
case intro.isFalse.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
rupHint_clause_eq_some_none : f.clauses[rupHints[↑i]]? = some none
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inr.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
. simp only [rupHint_clause_eq_some_none]
  exact ih
State after:
case intro.isFalse.inr.inr.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst

State before:
case intro.isFalse.inr.inr.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
. simp only [rupHint_clause_eq_c]
  have reduce_c_options : reduce c acc.1 = ReduceResult.encounteredBoth ∨ reduce c acc.1 = ReduceResult.reducedToEmpty ∨
    (∃ l : Literal (PosFin n), reduce c acc.1 = ReduceResult.reducedToUnit l) ∨ reduce c acc.1 = ReduceResult.reducedToNonunit := by
    match reduce c acc.fst with
    | ReduceResult.encounteredBoth => exact Or.inl rfl
    | ReduceResult.reducedToEmpty => exact (Or.inr ∘ Or.inl) rfl
    | ReduceResult.reducedToUnit l => exact (Or.inr ∘ Or.inr ∘ Or.inl ∘ Exists.intro l) rfl
    | ReduceResult.reducedToNonunit => exact (Or.inr ∘ Or.inr ∘ Or.inr) rfl
  rcases reduce_c_options with hencounteredBoth | hreducedToEmpty | ⟨l, hreducedToUnit⟩ | hreducedToNonunit
  . simp only [hencounteredBoth]
    exact ih
  . simp only [hreducedToEmpty]
    exact ih
  . simp only [hreducedToUnit, Prod.mk.eta]
    by_cases h : hasAssignment l.snd acc.fst[l.fst.val]!
    . simp only [h, ite_true]
      exact ih
    . simp only [h, ite_false]
      exact confirmRupHint_preserves_invariant_helper f f_assignments_size acc hsize l ih h
  . simp only [hreducedToNonunit]
    exact ih
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
⊢ f.clauses[rupHints[↑i]]? = none ∨ f.clauses[rupHints[↑i]]? = some none ∨ ∃ c, f.clauses[rupHints[↑i]]? = some (some c)
Tactic:
match f.clauses[rupHints[i.val]]? with
| none => exact Or.inl rfl
| some none => exact Or.inr $ Or.inl rfl
| some (some c) => exact (Or.inr ∘ Or.inr ∘ Exists.intro c) rfl
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
⊢ none = none ∨ none = some none ∨ ∃ c, none = some (some c)
Tactic:
exact Or.inl rfl
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
⊢ some none = none ∨ some none = some none ∨ ∃ c, some none = some (some c)
Tactic:
exact Or.inr $ Or.inl rfl
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
⊢ some (some c) = none ∨ some (some c) = some none ∨ ∃ c_1, some (some c) = some (some c_1)
Tactic:
exact (Or.inr ∘ Or.inr ∘ Exists.intro c) rfl
State after:
no goals

State before:
case intro.isFalse.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
rupHint_clause_eq_none : f.clauses[rupHints[↑i]]? = none
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
simp only [rupHint_clause_eq_none]
State after:
case intro.isFalse.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
rupHint_clause_eq_none : f.clauses[rupHints[↑i]]? = none
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst

State before:
case intro.isFalse.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
rupHint_clause_eq_none : f.clauses[rupHints[↑i]]? = none
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst
Tactic:
exact ih
State after:
no goals

State before:
case intro.isFalse.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
rupHint_clause_eq_some_none : f.clauses[rupHints[↑i]]? = some none
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
simp only [rupHint_clause_eq_some_none]
State after:
case intro.isFalse.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
rupHint_clause_eq_some_none : f.clauses[rupHints[↑i]]? = some none
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst

State before:
case intro.isFalse.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
rupHint_clause_eq_some_none : f.clauses[rupHints[↑i]]? = some none
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst
Tactic:
exact ih
State after:
no goals

State before:
case intro.isFalse.inr.inr.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
⊢ f.derivedLits_invariant f_assignments_size
    (match f.clauses[rupHints[↑i]]? with
      | some (some c) =>
        match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
      | some none => (acc.fst, acc.2.fst, false, true)
      | none => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match f.clauses[rupHints[↑i]]? with
        | some (some c) =>
          match c.reduce acc.fst with
          | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
          | ReduceResult.reducedToUnit (l, b) =>
            if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
            else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
          | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)
        | some none => (acc.fst, acc.2.fst, false, true)
        | none => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
simp only [rupHint_clause_eq_c]
State after:
case intro.isFalse.inr.inr.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

State before:
case intro.isFalse.inr.inr.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
have reduce_c_options : reduce c acc.1 = ReduceResult.encounteredBoth ∨ reduce c acc.1 = ReduceResult.reducedToEmpty ∨
  (∃ l : Literal (PosFin n), reduce c acc.1 = ReduceResult.reducedToUnit l) ∨ reduce c acc.1 = ReduceResult.reducedToNonunit := by
  match reduce c acc.fst with
  | ReduceResult.encounteredBoth => exact Or.inl rfl
  | ReduceResult.reducedToEmpty => exact (Or.inr ∘ Or.inl) rfl
  | ReduceResult.reducedToUnit l => exact (Or.inr ∘ Or.inr ∘ Or.inl ∘ Exists.intro l) rfl
  | ReduceResult.reducedToNonunit => exact (Or.inr ∘ Or.inr ∘ Or.inr) rfl
State after:
case intro.isFalse.inr.inr.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
reduce_c_options :
  c.reduce acc.fst = ReduceResult.encounteredBoth ∨
    c.reduce acc.fst = ReduceResult.reducedToEmpty ∨
      (∃ l, c.reduce acc.fst = ReduceResult.reducedToUnit l) ∨ c.reduce acc.fst = ReduceResult.reducedToNonunit
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

State before:
case intro.isFalse.inr.inr.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
reduce_c_options :
  c.reduce acc.fst = ReduceResult.encounteredBoth ∨
    c.reduce acc.fst = ReduceResult.reducedToEmpty ∨
      (∃ l, c.reduce acc.fst = ReduceResult.reducedToUnit l) ∨ c.reduce acc.fst = ReduceResult.reducedToNonunit
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
rcases reduce_c_options with hencounteredBoth | hreducedToEmpty | ⟨l, hreducedToUnit⟩ | hreducedToNonunit
State after:
case intro.isFalse.inr.inr.intro.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hencounteredBoth : c.reduce acc.fst = ReduceResult.encounteredBoth
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inr.intro.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToEmpty : c.reduce acc.fst = ReduceResult.reducedToEmpty
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inr.intro.inr.inr.inl.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inr.intro.inr.inr.inr
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToNonunit : c.reduce acc.fst = ReduceResult.reducedToNonunit
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

State before:
case intro.isFalse.inr.inr.intro.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hencounteredBoth : c.reduce acc.fst = ReduceResult.encounteredBoth
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inr.intro.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToEmpty : c.reduce acc.fst = ReduceResult.reducedToEmpty
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inr.intro.inr.inr.inl.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inr.intro.inr.inr.inr
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToNonunit : c.reduce acc.fst = ReduceResult.reducedToNonunit
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
. simp only [hencounteredBoth]
  exact ih
State after:
case intro.isFalse.inr.inr.intro.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToEmpty : c.reduce acc.fst = ReduceResult.reducedToEmpty
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inr.intro.inr.inr.inl.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inr.intro.inr.inr.inr
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToNonunit : c.reduce acc.fst = ReduceResult.reducedToNonunit
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

State before:
case intro.isFalse.inr.inr.intro.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToEmpty : c.reduce acc.fst = ReduceResult.reducedToEmpty
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inr.intro.inr.inr.inl.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inr.intro.inr.inr.inr
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToNonunit : c.reduce acc.fst = ReduceResult.reducedToNonunit
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
. simp only [hreducedToEmpty]
  exact ih
State after:
case intro.isFalse.inr.inr.intro.inr.inr.inl.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inr.intro.inr.inr.inr
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToNonunit : c.reduce acc.fst = ReduceResult.reducedToNonunit
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

State before:
case intro.isFalse.inr.inr.intro.inr.inr.inl.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

case intro.isFalse.inr.inr.intro.inr.inr.inr
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToNonunit : c.reduce acc.fst = ReduceResult.reducedToNonunit
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
. simp only [hreducedToUnit, Prod.mk.eta]
  by_cases h : hasAssignment l.snd acc.fst[l.fst.val]!
  . simp only [h, ite_true]
    exact ih
  . simp only [h, ite_false]
    exact confirmRupHint_preserves_invariant_helper f f_assignments_size acc hsize l ih h
State after:
case intro.isFalse.inr.inr.intro.inr.inr.inr
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToNonunit : c.reduce acc.fst = ReduceResult.reducedToNonunit
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst

State before:
case intro.isFalse.inr.inr.intro.inr.inr.inr
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToNonunit : c.reduce acc.fst = ReduceResult.reducedToNonunit
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
. simp only [hreducedToNonunit]
  exact ih
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
⊢ c.reduce acc.fst = ReduceResult.encounteredBoth ∨
    c.reduce acc.fst = ReduceResult.reducedToEmpty ∨
      (∃ l, c.reduce acc.fst = ReduceResult.reducedToUnit l) ∨ c.reduce acc.fst = ReduceResult.reducedToNonunit
Tactic:
match reduce c acc.fst with
| ReduceResult.encounteredBoth => exact Or.inl rfl
| ReduceResult.reducedToEmpty => exact (Or.inr ∘ Or.inl) rfl
| ReduceResult.reducedToUnit l => exact (Or.inr ∘ Or.inr ∘ Or.inl ∘ Exists.intro l) rfl
| ReduceResult.reducedToNonunit => exact (Or.inr ∘ Or.inr ∘ Or.inr) rfl
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
⊢ ReduceResult.encounteredBoth = ReduceResult.encounteredBoth ∨
    ReduceResult.encounteredBoth = ReduceResult.reducedToEmpty ∨
      (∃ l, ReduceResult.encounteredBoth = ReduceResult.reducedToUnit l) ∨
        ReduceResult.encounteredBoth = ReduceResult.reducedToNonunit
Tactic:
exact Or.inl rfl
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
⊢ ReduceResult.reducedToEmpty = ReduceResult.encounteredBoth ∨
    ReduceResult.reducedToEmpty = ReduceResult.reducedToEmpty ∨
      (∃ l, ReduceResult.reducedToEmpty = ReduceResult.reducedToUnit l) ∨
        ReduceResult.reducedToEmpty = ReduceResult.reducedToNonunit
Tactic:
exact (Or.inr ∘ Or.inl) rfl
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
⊢ ReduceResult.reducedToUnit l = ReduceResult.encounteredBoth ∨
    ReduceResult.reducedToUnit l = ReduceResult.reducedToEmpty ∨
      (∃ l_1, ReduceResult.reducedToUnit l = ReduceResult.reducedToUnit l_1) ∨
        ReduceResult.reducedToUnit l = ReduceResult.reducedToNonunit
Tactic:
exact (Or.inr ∘ Or.inr ∘ Or.inl ∘ Exists.intro l) rfl
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
⊢ ReduceResult.reducedToNonunit = ReduceResult.encounteredBoth ∨
    ReduceResult.reducedToNonunit = ReduceResult.reducedToEmpty ∨
      (∃ l, ReduceResult.reducedToNonunit = ReduceResult.reducedToUnit l) ∨
        ReduceResult.reducedToNonunit = ReduceResult.reducedToNonunit
Tactic:
exact (Or.inr ∘ Or.inr ∘ Or.inr) rfl
State after:
no goals

State before:
case intro.isFalse.inr.inr.intro.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hencounteredBoth : c.reduce acc.fst = ReduceResult.encounteredBoth
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
simp only [hencounteredBoth]
State after:
case intro.isFalse.inr.inr.intro.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hencounteredBoth : c.reduce acc.fst = ReduceResult.encounteredBoth
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst

State before:
case intro.isFalse.inr.inr.intro.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hencounteredBoth : c.reduce acc.fst = ReduceResult.encounteredBoth
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst
Tactic:
exact ih
State after:
no goals

State before:
case intro.isFalse.inr.inr.intro.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToEmpty : c.reduce acc.fst = ReduceResult.reducedToEmpty
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
simp only [hreducedToEmpty]
State after:
case intro.isFalse.inr.inr.intro.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToEmpty : c.reduce acc.fst = ReduceResult.reducedToEmpty
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst

State before:
case intro.isFalse.inr.inr.intro.inr.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToEmpty : c.reduce acc.fst = ReduceResult.reducedToEmpty
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst
Tactic:
exact ih
State after:
no goals

State before:
case intro.isFalse.inr.inr.intro.inr.inr.inl.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
simp only [hreducedToUnit, Prod.mk.eta]
State after:
case intro.isFalse.inr.inr.intro.inr.inr.inl.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
⊢ f.derivedLits_invariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).snd.fst

State before:
case intro.isFalse.inr.inr.intro.inr.inr.inl.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
⊢ f.derivedLits_invariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).snd.fst
Tactic:
by_cases h : hasAssignment l.snd acc.fst[l.fst.val]!
State after:
case pos
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).snd.fst

case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).snd.fst

State before:
case pos
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).snd.fst

case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).snd.fst
Tactic:
. simp only [h, ite_true]
  exact ih
State after:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).snd.fst

State before:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).snd.fst
Tactic:
. simp only [h, ite_false]
  exact confirmRupHint_preserves_invariant_helper f f_assignments_size acc hsize l ih h
State after:
no goals

State before:
case pos
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).snd.fst
Tactic:
simp only [h, ite_true]
State after:
case pos
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst

State before:
case pos
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst
Tactic:
exact ih
State after:
no goals

State before:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), l :: acc.2.fst, false, false)).snd.fst
Tactic:
simp only [h, ite_false]
State after:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size (acc.fst.modify l.fst.val (addAssignment l.snd)) ⋯ (l :: acc.2.fst)

State before:
case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.derivedLits_invariant f_assignments_size (acc.fst.modify l.fst.val (addAssignment l.snd)) ⋯ (l :: acc.2.fst)
Tactic:
exact confirmRupHint_preserves_invariant_helper f f_assignments_size acc hsize l ih h
State after:
no goals

State before:
case intro.isFalse.inr.inr.intro.inr.inr.inr
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToNonunit : c.reduce acc.fst = ReduceResult.reducedToNonunit
⊢ f.derivedLits_invariant f_assignments_size
    (match c.reduce acc.fst with
      | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
      | ReduceResult.reducedToUnit (l, b) =>
        if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
      | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).fst
    ⋯
    (match c.reduce acc.fst with
        | ReduceResult.encounteredBoth => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToEmpty => (acc.fst, acc.2.fst, true, false)
        | ReduceResult.reducedToUnit (l, b) =>
          if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
          else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
        | ReduceResult.reducedToNonunit => (acc.fst, acc.2.fst, false, true)).snd.fst
Tactic:
simp only [hreducedToNonunit]
State after:
case intro.isFalse.inr.inr.intro.inr.inr.inr
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToNonunit : c.reduce acc.fst = ReduceResult.reducedToNonunit
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst

State before:
case intro.isFalse.inr.inr.intro.inr.inr.inr
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToNonunit : c.reduce acc.fst = ReduceResult.reducedToNonunit
⊢ f.derivedLits_invariant f_assignments_size acc.fst ⋯ acc.2.fst
Tactic:
exact ih
State after:
no goals