-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
    ReadyForRupAdd f → ReadyForRupAdd (insert f c)

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.ReadyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
hb' : hasAssignment b f.assignments[i.val] = true
hf :
  some (unit (i, b)) ∈ f.clauses.toList ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.toList ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.toList ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = unit (i, b)
⊢ (some (unit (i, b)) ∈ f.clauses.toList ∨ unit (i, b) = c) ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.toList ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.toList ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = unit (i, b)

Tactic:
rcases hf with hf | hf

Result:
case inl
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.ReadyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
hb' : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.toList
⊢ (some (unit (i, b)) ∈ f.clauses.toList ∨ unit (i, b) = c) ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.toList ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.toList ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = unit (i, b)

case inr
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.ReadyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
hb' : hasAssignment b f.assignments[i.val] = true
hf :
  (∃ a,
      (a, false) ∈ f.rupUnits.toList ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = unit (i, b)) ∨
    ∃ a,
      (a, false) ∈ f.ratUnits.toList ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = unit (i, b)
⊢ (some (unit (i, b)) ∈ f.clauses.toList ∨ unit (i, b) = c) ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.toList ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.toList ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = unit (i, b)

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.ReadyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
ib_eq_c : (i, b) = (l, false)
⊢ unit (i, b) ∈
    { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addNegAssignment }.toList

Tactic:
simp only [toList, Array.push_toList, List.append_assoc, List.mem_append, List.mem_filterMap,
  List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]

Result:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.ReadyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
ib_eq_c : (i, b) = (l, false)
⊢ (some (unit (i, b)) ∈ f.clauses.toList ∨ unit (i, b) = c) ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.toList ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.toList ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = unit (i, b)

Proof state:
case inl
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.ReadyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[i.val] = true
i_in_bounds : i.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
hb' : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.toList
⊢ (some (unit (i, b)) ∈ f.clauses.toList ∨ unit (i, b) = c) ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.toList ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.toList ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.toList ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.toList ∧ unit (a, true) = unit (i, b)

Tactic:
exact Or.inl <| Or.inl hf

Result:
no goals

Proof state:
case neg
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.ReadyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, true)
hsize : (f.assignments.modify l.val addPosAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addPosAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
l_eq_i : l.val = i.val
h✝ : ¬b = true
⊢ b = false

Tactic:
next b_eq_false =>
simp only [Bool.not_eq_true] at b_eq_false
exact b_eq_false

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.ReadyForRupAdd
x✝ : Option (Literal (PosFin n))
l : PosFin n
hc : c.isUnit = some (l, false)
hsize : (f.assignments.modify l.val addNegAssignment).size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.assignments.modify l.val addNegAssignment)[i.val] = true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, false)
l_eq_i : l.val = i.val
b_eq_false : ¬b = true
⊢ b = true

Tactic:
simp only [b_eq_false, Subtype.ext l_eq_i, not_true] at ib_ne_c

Result:
no goals