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

State before:
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
⊢ c ∈ (f.deleteOne id).toList → c ∈ f.toList
Tactic:
simp only [deleteOne]
State after:
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
⊢ c ∈
      (match f.clauses[id]! with
        | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
        | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
          { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
        | some val =>
          { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }).toList →
    c ∈ f.toList

State before:
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
⊢ c ∈
      (match f.clauses[id]! with
        | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
        | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
          { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
        | some val =>
          { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }).toList →
    c ∈ f.toList
Tactic:
intro h1
State after:
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
h1 :
  c ∈
    (match f.clauses[id]! with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList
⊢ c ∈ f.toList

State before:
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
h1 :
  c ∈
    (match f.clauses[id]! with
      | none => { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
      | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l.fst.val (removeAssignment l.snd) }
      | some val =>
        { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }).toList
⊢ c ∈ f.toList
Tactic:
split at h1 <;> first
| exact h1
| rw [toList, List.mem_append, List.mem_append, or_assoc] at h1
  rw [toList, List.mem_append, List.mem_append, or_assoc]
  rcases h1 with h1 | h1 | h1
  . apply Or.inl
    simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right] at h1
    simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right]
    rw [Array.set!, Array.setD] at h1
    split at h1
    . simp only [Array.data_set] at h1
      rcases List.get_of_mem h1 with ⟨i, h4⟩
      rw [List.get_set] at h4
      split at h4
      . exact False.elim h4
      . rw [← h4]
        apply List.get_mem
    . exact h1
  . exact (Or.inr ∘ Or.inl) h1
  . exact (Or.inr ∘ Or.inr) h1
State after:
no goals

State before:
case h_1
n : Nat
f : DefaultFormula n
id : Nat
c : DefaultClause n
x✝ : Option (DefaultClause n)
heq✝ : f.clauses[id]! = none
h1 : c ∈ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }.toList
⊢ c ∈ f.toList
Tactic:
exact h1
State after:
no goals

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 ∈
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments }.toList
⊢ c ∈ f.toList
Tactic:
rw [toList, List.mem_append, List.mem_append, or_assoc] at h1
State after:
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 ∈ f.toList

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 ∈ f.toList
Tactic:
rw [toList, List.mem_append, List.mem_append, or_assoc]
State after:
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

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
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

State before:
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
Tactic:
. apply Or.inl
  simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right] at h1
  simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right]
  rw [Array.set!, Array.setD] at h1
  split at h1
  . simp only [Array.data_set] at h1
    rcases List.get_of_mem h1 with ⟨i, h4⟩
    rw [List.get_set] at h4
    split at h4
    . exact False.elim h4
    . rw [← h4]
      apply List.get_mem
  . exact h1
State after:
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

State before:
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
Tactic:
. exact (Or.inr ∘ Or.inl) h1
State after:
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

State before:
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
Tactic:
. exact (Or.inr ∘ Or.inr) h1
State after:
no goals

State before:
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
Tactic:
apply Or.inl
State after:
case h_3.inl.h
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

State before:
case h_3.inl.h
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
Tactic:
simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right] at h1
State after:
case h_3.inl.h
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 : some c ∈ (f.clauses.set! id none).data
⊢ c ∈ List.filterMap _root_.id f.clauses.toList

State before:
case h_3.inl.h
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 : some c ∈ (f.clauses.set! id none).data
⊢ c ∈ List.filterMap _root_.id f.clauses.toList
Tactic:
simp only [Array.toList_eq, List.mem_filterMap, id_eq, exists_eq_right]
State after:
case h_3.inl.h
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 : some c ∈ (f.clauses.set! id none).data
⊢ some c ∈ f.clauses.data

State before:
case h_3.inl.h
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 : some c ∈ (f.clauses.set! id none).data
⊢ some c ∈ f.clauses.data
Tactic:
rw [Array.set!, Array.setD] at h1
State after:
case h_3.inl.h
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 : some c ∈ (if h : id < f.clauses.size then f.clauses.set ⟨id, h⟩ none else f.clauses).data
⊢ some c ∈ f.clauses.data

State before:
case h_3.inl.h
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 : some c ∈ (if h : id < f.clauses.size then f.clauses.set ⟨id, h⟩ none else f.clauses).data
⊢ some c ∈ f.clauses.data
Tactic:
split at h1
State after:
case h_3.inl.h.isTrue
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✝
h✝ : id < f.clauses.size
h1 : some c ∈ (f.clauses.set ⟨id, h✝⟩ none).data
⊢ some c ∈ f.clauses.data

case h_3.inl.h.isFalse
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✝
h✝ : ¬id < f.clauses.size
h1 : some c ∈ f.clauses.data
⊢ some c ∈ f.clauses.data

State before:
case h_3.inl.h.isTrue
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✝
h✝ : id < f.clauses.size
h1 : some c ∈ (f.clauses.set ⟨id, h✝⟩ none).data
⊢ some c ∈ f.clauses.data

case h_3.inl.h.isFalse
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✝
h✝ : ¬id < f.clauses.size
h1 : some c ∈ f.clauses.data
⊢ some c ∈ f.clauses.data
Tactic:
. simp only [Array.data_set] at h1
  rcases List.get_of_mem h1 with ⟨i, h4⟩
  rw [List.get_set] at h4
  split at h4
  . exact False.elim h4
  . rw [← h4]
    apply List.get_mem
State after:
case h_3.inl.h.isFalse
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✝
h✝ : ¬id < f.clauses.size
h1 : some c ∈ f.clauses.data
⊢ some c ∈ f.clauses.data

State before:
case h_3.inl.h.isFalse
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✝
h✝ : ¬id < f.clauses.size
h1 : some c ∈ f.clauses.data
⊢ some c ∈ f.clauses.data
Tactic:
. exact h1
State after:
no goals

State before:
case h_3.inl.h.isTrue
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✝
h✝ : id < f.clauses.size
h1 : some c ∈ (f.clauses.set ⟨id, h✝⟩ none).data
⊢ some c ∈ f.clauses.data
Tactic:
simp only [Array.data_set] at h1
State after:
case h_3.inl.h.isTrue
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✝
h✝ : id < f.clauses.size
h1 : some c ∈ f.clauses.data.set id none
⊢ some c ∈ f.clauses.data

State before:
case h_3.inl.h.isTrue
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✝
h✝ : id < f.clauses.size
h1 : some c ∈ f.clauses.data.set id none
⊢ some c ∈ f.clauses.data
Tactic:
rcases List.get_of_mem h1 with ⟨i, h4⟩
State after:
case h_3.inl.h.isTrue.intro
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✝
h✝ : id < f.clauses.size
h1 : some c ∈ f.clauses.data.set id none
i : Fin (f.clauses.data.set id none).length
h4 : (f.clauses.data.set id none).get i = some c
⊢ some c ∈ f.clauses.data

State before:
case h_3.inl.h.isTrue.intro
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✝
h✝ : id < f.clauses.size
h1 : some c ∈ f.clauses.data.set id none
i : Fin (f.clauses.data.set id none).length
h4 : (f.clauses.data.set id none).get i = some c
⊢ some c ∈ f.clauses.data
Tactic:
rw [List.get_set] at h4
State after:
case h_3.inl.h.isTrue.intro
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✝
h✝ : id < f.clauses.size
h1 : some c ∈ f.clauses.data.set id none
i : Fin (f.clauses.data.set id none).length
h4 : (if id = ↑i then none else f.clauses.data.get ⟨↑i, ⋯⟩) = some c
⊢ some c ∈ f.clauses.data

State before:
case h_3.inl.h.isTrue.intro
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✝
h✝ : id < f.clauses.size
h1 : some c ∈ f.clauses.data.set id none
i : Fin (f.clauses.data.set id none).length
h4 : (if id = ↑i then none else f.clauses.data.get ⟨↑i, ⋯⟩) = some c
⊢ some c ∈ f.clauses.data
Tactic:
split at h4
State after:
case h_3.inl.h.isTrue.intro.isTrue
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✝
h✝¹ : id < f.clauses.size
h1 : some c ∈ f.clauses.data.set id none
i : Fin (f.clauses.data.set id none).length
h✝ : id = ↑i
h4 : False
⊢ some c ∈ f.clauses.data

case h_3.inl.h.isTrue.intro.isFalse
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✝
h✝¹ : id < f.clauses.size
h1 : some c ∈ f.clauses.data.set id none
i : Fin (f.clauses.data.set id none).length
h✝ : ¬id = ↑i
h4 : f.clauses.data.get ⟨↑i, ⋯⟩ = some c
⊢ some c ∈ f.clauses.data

State before:
case h_3.inl.h.isTrue.intro.isTrue
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✝
h✝¹ : id < f.clauses.size
h1 : some c ∈ f.clauses.data.set id none
i : Fin (f.clauses.data.set id none).length
h✝ : id = ↑i
h4 : False
⊢ some c ∈ f.clauses.data

case h_3.inl.h.isTrue.intro.isFalse
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✝
h✝¹ : id < f.clauses.size
h1 : some c ∈ f.clauses.data.set id none
i : Fin (f.clauses.data.set id none).length
h✝ : ¬id = ↑i
h4 : f.clauses.data.get ⟨↑i, ⋯⟩ = some c
⊢ some c ∈ f.clauses.data
Tactic:
. exact False.elim h4
State after:
case h_3.inl.h.isTrue.intro.isFalse
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✝
h✝¹ : id < f.clauses.size
h1 : some c ∈ f.clauses.data.set id none
i : Fin (f.clauses.data.set id none).length
h✝ : ¬id = ↑i
h4 : f.clauses.data.get ⟨↑i, ⋯⟩ = some c
⊢ some c ∈ f.clauses.data

State before:
case h_3.inl.h.isTrue.intro.isFalse
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✝
h✝¹ : id < f.clauses.size
h1 : some c ∈ f.clauses.data.set id none
i : Fin (f.clauses.data.set id none).length
h✝ : ¬id = ↑i
h4 : f.clauses.data.get ⟨↑i, ⋯⟩ = some c
⊢ some c ∈ f.clauses.data
Tactic:
. rw [← h4]
  apply List.get_mem
State after:
no goals

State before:
case h_3.inl.h.isTrue.intro.isTrue
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✝
h✝¹ : id < f.clauses.size
h1 : some c ∈ f.clauses.data.set id none
i : Fin (f.clauses.data.set id none).length
h✝ : id = ↑i
h4 : False
⊢ some c ∈ f.clauses.data
Tactic:
exact False.elim h4
State after:
no goals

State before:
case h_3.inl.h.isTrue.intro.isFalse
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✝
h✝¹ : id < f.clauses.size
h1 : some c ∈ f.clauses.data.set id none
i : Fin (f.clauses.data.set id none).length
h✝ : ¬id = ↑i
h4 : f.clauses.data.get ⟨↑i, ⋯⟩ = some c
⊢ some c ∈ f.clauses.data
Tactic:
rw [← h4]
State after:
case h_3.inl.h.isTrue.intro.isFalse
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✝
h✝¹ : id < f.clauses.size
h1 : some c ∈ f.clauses.data.set id none
i : Fin (f.clauses.data.set id none).length
h✝ : ¬id = ↑i
h4 : f.clauses.data.get ⟨↑i, ⋯⟩ = some c
⊢ f.clauses.data.get ⟨↑i, ⋯⟩ ∈ f.clauses.data

State before:
case h_3.inl.h.isTrue.intro.isFalse
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✝
h✝¹ : id < f.clauses.size
h1 : some c ∈ f.clauses.data.set id none
i : Fin (f.clauses.data.set id none).length
h✝ : ¬id = ↑i
h4 : f.clauses.data.get ⟨↑i, ⋯⟩ = some c
⊢ f.clauses.data.get ⟨↑i, ⋯⟩ ∈ f.clauses.data
Tactic:
apply List.get_mem
State after:
no goals

State before:
case h_3.inl.h.isFalse
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✝
h✝ : ¬id < f.clauses.size
h1 : some c ∈ f.clauses.data
⊢ some c ∈ f.clauses.data
Tactic:
exact h1
State after:
no goals

State before:
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
Tactic:
exact (Or.inr ∘ Or.inl) h1
State after:
no goals

State before:
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
Tactic:
exact (Or.inr ∘ Or.inr) h1
State after:
no goals