Theorem: LRAT.DefaultFormula.mem_of_insertRatUnits (LeanSAT/LRAT/Formula/Basic.lean)

State before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
⊢ c ∈ (f.insertRatUnits units).fst.toList → c ∈ List.map Clause.unit units ∨ c ∈ f.toList
Tactic:
simp only [toList, insertRatUnits, Prod.mk.eta, Array.toList_eq, List.append_assoc, List.mem_append,
  List.mem_filterMap, id_eq, exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool]
State after:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
⊢ (some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a,
          (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, false) = c ∨
            (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
              unit (a, true) = c) →
    (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
      some c ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

State before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
⊢ (some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a,
          (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, false) = c ∨
            (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
              unit (a, true) = c) →
    (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
      some c ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
intro h
State after:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, true) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

State before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, true) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
have hb : ∀ l : Literal (PosFin n), l ∈ (f.ratUnits, f.assignments, false).1.data → (l ∈ f.ratUnits.data ∨ l ∈ units) :=
  fun _ => Or.inl
State after:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

State before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
have hl (acc : Array (Literal (PosFin n)) × Array Assignment × Bool)
  (ih : ∀ l : Literal (PosFin n), l ∈ acc.1.data → l ∈ f.ratUnits.data ∨ l ∈ units)
  (unit : Literal (PosFin n)) (unit_in_units : unit ∈ units) :
  ∀ l : Literal (PosFin n), l ∈ (insertUnit acc unit).1.data → (l ∈ f.ratUnits.data ∨ l ∈ units) := by
  intro l hl
  rw [insertUnit] at hl
  simp only [Prod.mk.eta] at hl
  split at hl
  . exact ih l hl
  . simp only [Array.push_data, List.mem_append, List.mem_singleton] at hl
    rcases hl with l_in_acc | l_eq_unit
    . exact ih l l_in_acc
    . rw [l_eq_unit]
      exact Or.inr unit_in_units
State after:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

State before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
have h_insertUnit_fold := List.foldlRecOn units insertUnit (f.ratUnits, f.assignments, false) hb hl
State after:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

State before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
rcases h with h | h | ⟨i, ⟨h1, h2⟩ | ⟨h1, h2⟩⟩
State after:
case inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h : some c ∈ f.clauses.data
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

case inr.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

case inr.inr.intro.inl.intro
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

case inr.inr.intro.inr.intro
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

State before:
case inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h : some c ∈ f.clauses.data
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

case inr.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

case inr.inr.intro.inl.intro
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

case inr.inr.intro.inr.intro
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
. exact Or.inr $ Or.inl h
State after:
case inr.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

case inr.inr.intro.inl.intro
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

case inr.inr.intro.inr.intro
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

State before:
case inr.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

case inr.inr.intro.inl.intro
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

case inr.inr.intro.inr.intro
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
. exact (Or.inr ∘ Or.inr ∘ Or.inl) h
State after:
case inr.inr.intro.inl.intro
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

case inr.inr.intro.inr.intro
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

State before:
case inr.inr.intro.inl.intro
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

case inr.inr.intro.inr.intro
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
. rcases h_insertUnit_fold (i, false) h1 with h_insertUnit_fold | h_insertUnit_fold
  . apply Or.inr ∘ Or.inr ∘ Or.inr ∘ Exists.intro i ∘ Or.inl
    exact ⟨h_insertUnit_fold, h2⟩
  . apply Or.inl ∘ Exists.intro i ∘ Or.inl
    exact ⟨h_insertUnit_fold, h2⟩
State after:
case inr.inr.intro.inr.intro
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

State before:
case inr.inr.intro.inr.intro
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
. rcases h_insertUnit_fold (i, true) h1 with h_insertUnit_fold | h_insertUnit_fold
  . apply Or.inr ∘ Or.inr ∘ Or.inr ∘ Exists.intro i ∘ Or.inr
    exact ⟨h_insertUnit_fold, h2⟩
  . apply Or.inl ∘ Exists.intro i ∘ Or.inr
    exact ⟨h_insertUnit_fold, h2⟩
State after:
no goals

State before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
⊢ ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
Tactic:
intro l hl
State after:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
hl : l ∈ (insertUnit acc unit).fst.data
⊢ l ∈ f.ratUnits.data ∨ l ∈ units

State before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
hl : l ∈ (insertUnit acc unit).fst.data
⊢ l ∈ f.ratUnits.data ∨ l ∈ units
Tactic:
rw [insertUnit] at hl
State after:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
hl :
  l ∈
    (match acc with
        | (units, assignments, foundContradiction) =>
          match unit with
          | (l, b) =>
            let curAssignment := assignments[l.val]!;
            if hasAssignment b curAssignment = true then (units, assignments, foundContradiction)
            else
              (units.push (l, b), assignments.modify l.val (addAssignment b),
                foundContradiction || curAssignment != unassigned)).fst.data
⊢ l ∈ f.ratUnits.data ∨ l ∈ units

State before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
hl :
  l ∈
    (match acc with
        | (units, assignments, foundContradiction) =>
          match unit with
          | (l, b) =>
            let curAssignment := assignments[l.val]!;
            if hasAssignment b curAssignment = true then (units, assignments, foundContradiction)
            else
              (units.push (l, b), assignments.modify l.val (addAssignment b),
                foundContradiction || curAssignment != unassigned)).fst.data
⊢ l ∈ f.ratUnits.data ∨ l ∈ units
Tactic:
simp only [Prod.mk.eta] at hl
State after:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
hl :
  l ∈
    (if hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true then acc
        else
          (acc.fst.push unit, acc.2.fst.modify unit.fst.val (addAssignment unit.snd),
            acc.2.snd || acc.2.fst[unit.fst.val]! != unassigned)).fst.data
⊢ l ∈ f.ratUnits.data ∨ l ∈ units

State before:
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
hl :
  l ∈
    (if hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true then acc
        else
          (acc.fst.push unit, acc.2.fst.modify unit.fst.val (addAssignment unit.snd),
            acc.2.snd || acc.2.fst[unit.fst.val]! != unassigned)).fst.data
⊢ l ∈ f.ratUnits.data ∨ l ∈ units
Tactic:
split at hl
State after:
case isTrue
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
hl : l ∈ acc.fst.data
⊢ l ∈ f.ratUnits.data ∨ l ∈ units

case isFalse
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
hl :
  l ∈
    (acc.fst.push unit, acc.2.fst.modify unit.fst.val (addAssignment unit.snd),
          acc.2.snd || acc.2.fst[unit.fst.val]! != unassigned).fst.data
⊢ l ∈ f.ratUnits.data ∨ l ∈ units

State before:
case isTrue
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
hl : l ∈ acc.fst.data
⊢ l ∈ f.ratUnits.data ∨ l ∈ units

case isFalse
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
hl :
  l ∈
    (acc.fst.push unit, acc.2.fst.modify unit.fst.val (addAssignment unit.snd),
          acc.2.snd || acc.2.fst[unit.fst.val]! != unassigned).fst.data
⊢ l ∈ f.ratUnits.data ∨ l ∈ units
Tactic:
. exact ih l hl
State after:
case isFalse
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
hl :
  l ∈
    (acc.fst.push unit, acc.2.fst.modify unit.fst.val (addAssignment unit.snd),
          acc.2.snd || acc.2.fst[unit.fst.val]! != unassigned).fst.data
⊢ l ∈ f.ratUnits.data ∨ l ∈ units

State before:
case isFalse
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
hl :
  l ∈
    (acc.fst.push unit, acc.2.fst.modify unit.fst.val (addAssignment unit.snd),
          acc.2.snd || acc.2.fst[unit.fst.val]! != unassigned).fst.data
⊢ l ∈ f.ratUnits.data ∨ l ∈ units
Tactic:
. simp only [Array.push_data, List.mem_append, List.mem_singleton] at hl
  rcases hl with l_in_acc | l_eq_unit
  . exact ih l l_in_acc
  . rw [l_eq_unit]
    exact Or.inr unit_in_units
State after:
no goals

State before:
case isTrue
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
hl : l ∈ acc.fst.data
⊢ l ∈ f.ratUnits.data ∨ l ∈ units
Tactic:
exact ih l hl
State after:
no goals

State before:
case isFalse
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
hl :
  l ∈
    (acc.fst.push unit, acc.2.fst.modify unit.fst.val (addAssignment unit.snd),
          acc.2.snd || acc.2.fst[unit.fst.val]! != unassigned).fst.data
⊢ l ∈ f.ratUnits.data ∨ l ∈ units
Tactic:
simp only [Array.push_data, List.mem_append, List.mem_singleton] at hl
State after:
case isFalse
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
hl : l ∈ acc.fst.data ∨ l = unit
⊢ l ∈ f.ratUnits.data ∨ l ∈ units

State before:
case isFalse
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
hl : l ∈ acc.fst.data ∨ l = unit
⊢ l ∈ f.ratUnits.data ∨ l ∈ units
Tactic:
rcases hl with l_in_acc | l_eq_unit
State after:
case isFalse.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
l_in_acc : l ∈ acc.fst.data
⊢ l ∈ f.ratUnits.data ∨ l ∈ units

case isFalse.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
l_eq_unit : l = unit
⊢ l ∈ f.ratUnits.data ∨ l ∈ units

State before:
case isFalse.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
l_in_acc : l ∈ acc.fst.data
⊢ l ∈ f.ratUnits.data ∨ l ∈ units

case isFalse.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
l_eq_unit : l = unit
⊢ l ∈ f.ratUnits.data ∨ l ∈ units
Tactic:
. exact ih l l_in_acc
State after:
case isFalse.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
l_eq_unit : l = unit
⊢ l ∈ f.ratUnits.data ∨ l ∈ units

State before:
case isFalse.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
l_eq_unit : l = unit
⊢ l ∈ f.ratUnits.data ∨ l ∈ units
Tactic:
. rw [l_eq_unit]
  exact Or.inr unit_in_units
State after:
no goals

State before:
case isFalse.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
l_in_acc : l ∈ acc.fst.data
⊢ l ∈ f.ratUnits.data ∨ l ∈ units
Tactic:
exact ih l l_in_acc
State after:
no goals

State before:
case isFalse.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
l_eq_unit : l = unit
⊢ l ∈ f.ratUnits.data ∨ l ∈ units
Tactic:
rw [l_eq_unit]
State after:
case isFalse.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
l_eq_unit : l = unit
⊢ unit ∈ f.ratUnits.data ∨ unit ∈ units

State before:
case isFalse.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.rupUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
l_eq_unit : l = unit
⊢ unit ∈ f.ratUnits.data ∨ unit ∈ units
Tactic:
exact Or.inr unit_in_units
State after:
no goals

State before:
case inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h : some c ∈ f.clauses.data
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
exact Or.inr $ Or.inl h
State after:
no goals

State before:
case inr.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
exact (Or.inr ∘ Or.inr ∘ Or.inl) h
State after:
no goals

State before:
case inr.inr.intro.inl.intro
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
rcases h_insertUnit_fold (i, false) h1 with h_insertUnit_fold | h_insertUnit_fold
State after:
case inr.inr.intro.inl.intro.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
h_insertUnit_fold : (i, false) ∈ f.ratUnits.data
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

case inr.inr.intro.inl.intro.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
h_insertUnit_fold : (i, false) ∈ units
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

State before:
case inr.inr.intro.inl.intro.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
h_insertUnit_fold : (i, false) ∈ f.ratUnits.data
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

case inr.inr.intro.inl.intro.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
h_insertUnit_fold : (i, false) ∈ units
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
. apply Or.inr ∘ Or.inr ∘ Or.inr ∘ Exists.intro i ∘ Or.inl
  exact ⟨h_insertUnit_fold, h2⟩
State after:
case inr.inr.intro.inl.intro.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
h_insertUnit_fold : (i, false) ∈ units
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

State before:
case inr.inr.intro.inl.intro.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
h_insertUnit_fold : (i, false) ∈ units
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
. apply Or.inl ∘ Exists.intro i ∘ Or.inl
  exact ⟨h_insertUnit_fold, h2⟩
State after:
no goals

State before:
case inr.inr.intro.inl.intro.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
h_insertUnit_fold : (i, false) ∈ f.ratUnits.data
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
apply Or.inr ∘ Or.inr ∘ Or.inr ∘ Exists.intro i ∘ Or.inl
State after:
case inr.inr.intro.inl.intro.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
h_insertUnit_fold : (i, false) ∈ f.ratUnits.data
⊢ (i, false) ∈ f.ratUnits.data ∧ unit (i, false) = c

State before:
case inr.inr.intro.inl.intro.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
h_insertUnit_fold : (i, false) ∈ f.ratUnits.data
⊢ (i, false) ∈ f.ratUnits.data ∧ unit (i, false) = c
Tactic:
exact ⟨h_insertUnit_fold, h2⟩
State after:
no goals

State before:
case inr.inr.intro.inl.intro.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
h_insertUnit_fold : (i, false) ∈ units
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
apply Or.inl ∘ Exists.intro i ∘ Or.inl
State after:
case inr.inr.intro.inl.intro.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
h_insertUnit_fold : (i, false) ∈ units
⊢ (i, false) ∈ units ∧ Clause.unit (i, false) = c

State before:
case inr.inr.intro.inl.intro.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, false) = c
h_insertUnit_fold : (i, false) ∈ units
⊢ (i, false) ∈ units ∧ Clause.unit (i, false) = c
Tactic:
exact ⟨h_insertUnit_fold, h2⟩
State after:
no goals

State before:
case inr.inr.intro.inr.intro
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
rcases h_insertUnit_fold (i, true) h1 with h_insertUnit_fold | h_insertUnit_fold
State after:
case inr.inr.intro.inr.intro.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
h_insertUnit_fold : (i, true) ∈ f.ratUnits.data
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

case inr.inr.intro.inr.intro.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
h_insertUnit_fold : (i, true) ∈ units
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

State before:
case inr.inr.intro.inr.intro.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
h_insertUnit_fold : (i, true) ∈ f.ratUnits.data
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

case inr.inr.intro.inr.intro.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
h_insertUnit_fold : (i, true) ∈ units
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
. apply Or.inr ∘ Or.inr ∘ Or.inr ∘ Exists.intro i ∘ Or.inr
  exact ⟨h_insertUnit_fold, h2⟩
State after:
case inr.inr.intro.inr.intro.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
h_insertUnit_fold : (i, true) ∈ units
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c

State before:
case inr.inr.intro.inr.intro.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
h_insertUnit_fold : (i, true) ∈ units
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
. apply Or.inl ∘ Exists.intro i ∘ Or.inr
  exact ⟨h_insertUnit_fold, h2⟩
State after:
no goals

State before:
case inr.inr.intro.inr.intro.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
h_insertUnit_fold : (i, true) ∈ f.ratUnits.data
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
apply Or.inr ∘ Or.inr ∘ Or.inr ∘ Exists.intro i ∘ Or.inr
State after:
case inr.inr.intro.inr.intro.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
h_insertUnit_fold : (i, true) ∈ f.ratUnits.data
⊢ (i, true) ∈ f.ratUnits.data ∧ unit (i, true) = c

State before:
case inr.inr.intro.inr.intro.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
h_insertUnit_fold : (i, true) ∈ f.ratUnits.data
⊢ (i, true) ∈ f.ratUnits.data ∧ unit (i, true) = c
Tactic:
exact ⟨h_insertUnit_fold, h2⟩
State after:
no goals

State before:
case inr.inr.intro.inr.intro.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
h_insertUnit_fold : (i, true) ∈ units
⊢ (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
    some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c
Tactic:
apply Or.inl ∘ Exists.intro i ∘ Or.inr
State after:
case inr.inr.intro.inr.intro.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
h_insertUnit_fold : (i, true) ∈ units
⊢ (i, true) ∈ units ∧ Clause.unit (i, true) = c

State before:
case inr.inr.intro.inr.intro.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.ratUnits, f.assignments, false).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
hl :
  ∀ (acc : Array (Literal (PosFin n)) × Array Assignment × Bool),
    (∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.ratUnits.data ∨ l ∈ units) →
      ∀ (unit : Literal (PosFin n)),
        unit ∈ units → ∀ (l : Literal (PosFin n)), l ∈ (insertUnit acc unit).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
h_insertUnit_fold✝ :
  ∀ (l : Literal (PosFin n)),
    l ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data → l ∈ f.ratUnits.data ∨ l ∈ units
i : PosFin n
h1 : (i, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data
h2 : unit (i, true) = c
h_insertUnit_fold : (i, true) ∈ units
⊢ (i, true) ∈ units ∧ Clause.unit (i, true) = c
Tactic:
exact ⟨h_insertUnit_fold, h2⟩
State after:
no goals