-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem deleteOne_subset (f : DefaultFormula n) (id : Nat) (c : DefaultClause n) :
    c ∈ toList (deleteOne f id) → c ∈ toList f

Proof state:
case h_3.inl.h.isTrue.intro.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.toList.set id none
i : Nat
h : i < (f.clauses.toList.set id none).length
h4 : (if id = i then none else f.clauses.toList[i]) = some c
⊢ some c ∈ f.clauses.toList

Tactic:
split at h4

Result:
case h_3.inl.h.isTrue.intro.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.toList.set id none
i : Nat
h : i < (f.clauses.toList.set id none).length
h✝ : id = i
h4 : none = some c
⊢ some c ∈ f.clauses.toList

case h_3.inl.h.isTrue.intro.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.toList.set id none
i : Nat
h : i < (f.clauses.toList.set id none).length
h✝ : ¬id = i
h4 : f.clauses.toList[i] = some c
⊢ some c ∈ f.clauses.toList

Proof state:
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

Result:
no goals

Proof state:
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).toList
⊢ some c ∈ f.clauses.toList

Tactic:
rw [Array.set!, Array.setIfInBounds] at h1

Result:
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 none h else f.clauses).toList
⊢ some c ∈ f.clauses.toList

Proof state:
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

Result:
no goals

Proof state:
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).toList
⊢ c ∈ List.filterMap _root_.id f.clauses.toList

Tactic:
simp only [List.mem_filterMap, id_eq, exists_eq_right]

Result:
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).toList
⊢ some c ∈ f.clauses.toList

Proof state:
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 [List.mem_filterMap, id_eq, exists_eq_right] at h1

Result:
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).toList
⊢ c ∈ List.filterMap _root_.id f.clauses.toList