Theorem: LRAT.DefaultFormula.mem_of_insertRatUnits
Proof 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⟩⟩
Proof 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