Theorem: LRAT.DefaultFormula.deleteOne_subset
Proof state before:
case h_3
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : f.clauses[id]! = some val✝
h1 :
  c ∈
      List.filterMap _root_.id
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments }.clauses.toList ∨
    c ∈
        List.map unit
          { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                assignments := f.assignments }.rupUnits.toList ∨
      c ∈
        List.map unit
          { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                assignments := f.assignments }.ratUnits.toList
⊢ c ∈ List.filterMap _root_.id f.clauses.toList ∨
    c ∈ List.map unit f.rupUnits.toList ∨ c ∈ List.map unit f.ratUnits.toList
Tactic:
rcases h1 with h1 | h1 | h1
Proof state after:
case h_3.inl
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : f.clauses[id]! = some val✝
h1 :
  c ∈
    List.filterMap _root_.id
      { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }.clauses.toList
⊢ c ∈ List.filterMap _root_.id f.clauses.toList ∨
    c ∈ List.map unit f.rupUnits.toList ∨ c ∈ List.map unit f.ratUnits.toList

case h_3.inr.inl
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : f.clauses[id]! = some val✝
h1 :
  c ∈
    List.map unit
      { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }.rupUnits.toList
⊢ c ∈ List.filterMap _root_.id f.clauses.toList ∨
    c ∈ List.map unit f.rupUnits.toList ∨ c ∈ List.map unit f.ratUnits.toList

case h_3.inr.inr
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : f.clauses[id]! = some val✝
h1 :
  c ∈
    List.map unit
      { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }.ratUnits.toList
⊢ c ∈ List.filterMap _root_.id f.clauses.toList ∨
    c ∈ List.map unit f.rupUnits.toList ∨ c ∈ List.map unit f.ratUnits.toList