internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
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
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
l_eq_i : l.val = i.val
⊢ b = false
Tactic:
by_cases b = true
Proof state after:
case pos
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
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
l_eq_i : l.val = i.val
h✝ : b = true
⊢ b = false

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
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
l_eq_i : l.val = i.val
h✝ : ¬b = true
⊢ b = false
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
case pos
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
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
l_eq_i : l.val = i.val
h✝ : b = true
⊢ b = false

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
l_in_bounds : l.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_true =>
  simp only [b_eq_true, Subtype.ext l_eq_i, not_true] at ib_ne_c
Proof state after:
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
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
l_eq_i : l.val = i.val
h✝ : ¬b = true
⊢ b = false
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
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
l_in_bounds : l.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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
case pos
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
l_in_bounds : l.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_true =>
simp only [b_eq_true, Subtype.ext l_eq_i, not_true] at ib_ne_c
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
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
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
l_eq_i : l.val = i.val
b_eq_true : b = true
⊢ b = false
Tactic:
simp only [b_eq_true, Subtype.ext l_eq_i, not_true] at ib_ne_c
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
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
l_in_bounds : l.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
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
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
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
l_eq_i : l.val = i.val
b_eq_false : ¬b = true
⊢ b = false
Tactic:
simp only [Bool.not_eq_true] at b_eq_false
Proof state after:
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
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
l_eq_i : l.val = i.val
b_eq_false : b = false
⊢ b = false
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
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
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
l_eq_i : l.val = i.val
b_eq_false : b = false
⊢ b = false
Tactic:
exact b_eq_false
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
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
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
h✝ : ¬l.val = i.val
⊢ hasAssignment b f.assignments[i.val] = true
Tactic:
next l_ne_i =>
simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i] at hb
exact hb
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
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
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
l_ne_i : ¬l.val = i.val
⊢ hasAssignment b f.assignments[i.val] = true
Tactic:
simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i] at hb
Proof state after:
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
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
l_ne_i : ¬l.val = i.val
hb : hasAssignment b f.assignments[i.val] = true
⊢ hasAssignment b f.assignments[i.val] = true
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
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
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
l_in_bounds : l.val < f.assignments.size
ib_ne_c : ¬(i, b) = (l, true)
l_ne_i : ¬l.val = i.val
hb : hasAssignment b f.assignments[i.val] = true
⊢ hasAssignment b f.assignments[i.val] = true
Tactic:
exact hb
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
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
l_in_bounds : l.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.data
⊢ (some (unit (i, b)) ∈ f.clauses.data ∨ unit (i, b) = c) ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
Tactic:
exact Or.inl $ Or.inl hf
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
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
l_in_bounds : l.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.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
    ∃ a,
      (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
        (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ (some (unit (i, b)) ∈ f.clauses.data ∨ unit (i, b) = c) ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
Tactic:
exact Or.inr hf
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
case h_3
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c.isUnit = some (l✝, false)
⊢ { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := f.assignments.modify l✝.val addNegAssignment }.readyForRupAdd
Tactic:
next l hc =>
have hsize : (Array.modify f.assignments l.1 addNegAssignment).size = n := by
  rw [Array.modify_preserves_size, f_readyForRupAdd.2.1]
refine ⟨f_readyForRupAdd.1, hsize, ?_⟩
intro i b hb
have hf := f_readyForRupAdd.2.2 i b
have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
have l_in_bounds : l.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact l.2.2
simp only at hb
by_cases (i, b) = (l, false)
. next ib_eq_c =>
  simp only [toList, Array.toList_eq, Array.push_data, 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]
  apply Or.inl ∘ Or.inr
  rw [isUnit_iff, DefaultClause.toList, ← ib_eq_c] at hc
  apply DefaultClause.ext
  simp only [unit, hc]
. next ib_ne_c =>
  have hb' : hasAssignment b (f.assignments[i.1]'i_in_bounds) := by
    by_cases l.1 = i.1
    . next l_eq_i =>
      have b_eq_false : b = true := by
        by_cases b = true
        . assumption
        . next b_eq_false =>
          simp only [b_eq_false, Subtype.ext l_eq_i, not_true] at ib_ne_c
      simp only [hasAssignment, b_eq_false, l_eq_i, Array.get_modify_at_idx i_in_bounds, ite_true, hasPos_of_addNeg] at hb
      simp only [hasAssignment, b_eq_false, ite_true, hb]
    . next l_ne_i =>
      simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i] at hb
      exact hb
  specialize hf hb'
  simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
    exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
  simp only [toList, Array.toList_eq, Array.push_data, 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]
  rcases hf with hf | hf
  . exact Or.inl $ Or.inl hf
  . exact Or.inr hf
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
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)
⊢ { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := f.assignments.modify l.val addNegAssignment }.readyForRupAdd
Tactic:
have hsize : (Array.modify f.assignments l.1 addNegAssignment).size = n := by
  rw [Array.modify_preserves_size, f_readyForRupAdd.2.1]
Proof state after:
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
⊢ { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := f.assignments.modify l.val addNegAssignment }.readyForRupAdd
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
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
⊢ { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := f.assignments.modify l.val addNegAssignment }.readyForRupAdd
Tactic:
refine ⟨f_readyForRupAdd.1, hsize, ?_⟩
Proof state after:
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),
    hasAssignment b
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                assignments := f.assignments.modify l.val addNegAssignment }.assignments[i.val] =
        true →
      unit (i, b) ∈
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }.toList
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
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),
    hasAssignment b
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                assignments := f.assignments.modify l.val addNegAssignment }.assignments[i.val] =
        true →
      unit (i, b) ∈
        { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }.toList
Tactic:
intro i b hb
Proof state after:
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
      { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }.assignments[i.val] =
    true
⊢ unit (i, b) ∈
    { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addNegAssignment }.toList
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
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
      { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }.assignments[i.val] =
    true
⊢ unit (i, b) ∈
    { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addNegAssignment }.toList
Tactic:
have hf := f_readyForRupAdd.2.2 i b
Proof state after:
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
      { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }.assignments[i.val] =
    true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ unit (i, b) ∈
    { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addNegAssignment }.toList
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
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
      { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }.assignments[i.val] =
    true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ unit (i, b) ∈
    { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addNegAssignment }.toList
Tactic:
have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
Proof state after:
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
      { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }.assignments[i.val] =
    true
hf : hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i_in_bounds : i.val < f.assignments.size
⊢ unit (i, b) ∈
    { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addNegAssignment }.toList