internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.insert_iff
Proof state before:
case mpr.inr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2

case mpr.inr.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
. rw [insert_preserves_rupUnits]
  exact Or.inr $ Or.inl h
Proof state after:
case mpr.inr.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Theorem: LRAT.DefaultFormula.insert_iff
Proof state before:
case mpr.inr.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
. rw [insert_preserves_ratUnits]
  exact Or.inr $ Or.inr h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_iff
Proof state before:
case mpr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : c2 = c1
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
exact False.elim $ c2_ne_c1 h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_iff
Proof state before:
case mpr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
apply Or.inl
Proof state after:
case mpr.inr.inl.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
⊢ some c2 ∈ (f.insert c1).clauses.data
Theorem: LRAT.DefaultFormula.insert_iff
Proof state before:
case mpr.inr.inl.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
⊢ some c2 ∈ (f.insert c1).clauses.data
Tactic:
simp only [insert]
Proof state after:
case mpr.inr.inl.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
⊢ some c2 ∈
    (match c1.isUnit with
        | none =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }
        | some (l, true) =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addPosAssignment }
        | some (l, false) =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }).clauses.data
Theorem: LRAT.DefaultFormula.insert_iff
Proof state before:
case mpr.inr.inl.h
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
⊢ some c2 ∈
    (match c1.isUnit with
        | none =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }
        | some (l, true) =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addPosAssignment }
        | some (l, false) =>
          { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }).clauses.data
Tactic:
split
Proof state after:
case mpr.inr.inl.h.h_1
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
heq✝ : c1.isUnit = none
⊢ some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }.clauses.data

case mpr.inr.inl.h.h_2
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, true)
⊢ some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l✝.val addPosAssignment }.clauses.data

case mpr.inr.inl.h.h_3
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
⊢ some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l✝.val addNegAssignment }.clauses.data
Theorem: LRAT.DefaultFormula.insert_iff
Proof state before:
case mpr.inr.inl.h.h_1
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
heq✝ : c1.isUnit = none
⊢ some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments }.clauses.data

case mpr.inr.inl.h.h_2
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, true)
⊢ some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l✝.val addPosAssignment }.clauses.data

case mpr.inr.inl.h.h_3
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
⊢ some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l✝.val addNegAssignment }.clauses.data
Tactic:
all_goals
  simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq]
  exact Or.inl h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_iff
Proof state before:
case mpr.inr.inl.h.h_3
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
⊢ some c2 ∈
    { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := f.assignments.modify l✝.val addNegAssignment }.clauses.data
Tactic:
simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq]
Proof state after:
case mpr.inr.inl.h.h_3
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
⊢ some c2 ∈ f.clauses.data ∨ c2 = c1
Theorem: LRAT.DefaultFormula.insert_iff
Proof state before:
case mpr.inr.inl.h.h_3
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : some c2 ∈ f.clauses.data
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c1.isUnit = some (l✝, false)
⊢ some c2 ∈ f.clauses.data ∨ c2 = c1
Tactic:
exact Or.inl h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_iff
Proof state before:
case mpr.inr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
rw [insert_preserves_rupUnits]
Proof state after:
case mpr.inr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Theorem: LRAT.DefaultFormula.insert_iff
Proof state before:
case mpr.inr.inr.inl
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
exact Or.inr $ Or.inl h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_iff
Proof state before:
case mpr.inr.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a,
        (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2
Tactic:
rw [insert_preserves_ratUnits]
Proof state after:
case mpr.inr.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Theorem: LRAT.DefaultFormula.insert_iff
Proof state before:
case mpr.inr.inr.inr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_ne_c1 : ¬c2 = c1
h : ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
⊢ some c2 ∈ (f.insert c1).clauses.data ∨
    (∃ a,
        (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
          (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
      ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
Tactic:
exact Or.inr $ Or.inr h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.limplies_of_insert
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ limplies (PosFin n) (f.insert c) f
Tactic:
intro p
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
⊢ p ⊨ f.insert c → p ⊨ f
Theorem: LRAT.DefaultFormula.limplies_of_insert
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
⊢ p ⊨ f.insert c → p ⊨ f
Tactic:
simp only [formulaHSat_def, List.all_eq_true, decide_eq_true_eq]
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
⊢ (∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x) → ∀ (x : DefaultClause n), x ∈ f.toList → p ⊨ x
Theorem: LRAT.DefaultFormula.limplies_of_insert
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
⊢ (∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x) → ∀ (x : DefaultClause n), x ∈ f.toList → p ⊨ x
Tactic:
intro h c' c'_in_f
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'
Theorem: LRAT.DefaultFormula.limplies_of_insert
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'
Tactic:
have c'_in_fc : c' ∈ toList (insert f c) := by
  simp only [insert_iff, Array.toList_eq, Array.data_toArray, List.mem_singleton]
  exact Or.inr c'_in_f
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
c'_in_fc : c' ∈ (f.insert c).toList
⊢ p ⊨ c'
Theorem: LRAT.DefaultFormula.limplies_of_insert
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
c'_in_fc : c' ∈ (f.insert c).toList
⊢ p ⊨ c'
Tactic:
exact h c' c'_in_fc
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.limplies_of_insert
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ c' ∈ (f.insert c).toList
Tactic:
simp only [insert_iff, Array.toList_eq, Array.data_toArray, List.mem_singleton]
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ c' = c ∨ c' ∈ f.toList
Theorem: LRAT.DefaultFormula.limplies_of_insert
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : PosFin n → Bool
h : ∀ (x : DefaultClause n), x ∈ (f.insert c).toList → p ⊨ x
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ c' = c ∨ c' ∈ f.toList
Tactic:
exact Or.inr c'_in_f
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_preserves_assignments_size
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (f.insert c).assignments.size = f.assignments.size
Tactic:
simp only [insert]
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (match c.isUnit with
        | none =>
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }
        | some (l, true) =>
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addPosAssignment }
        | some (l, false) =>
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }).assignments.size =
    f.assignments.size
Theorem: LRAT.DefaultFormula.insert_preserves_assignments_size
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ (match c.isUnit with
        | none =>
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }
        | some (l, true) =>
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addPosAssignment }
        | some (l, false) =>
          { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments.modify l.val addNegAssignment }).assignments.size =
    f.assignments.size
Tactic:
split <;> simp only [Array.modify_preserves_size]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
⊢ f.readyForRupAdd → (f.insert c).readyForRupAdd
Tactic:
intro f_readyForRupAdd
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
⊢ (f.insert c).readyForRupAdd
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
⊢ (f.insert c).readyForRupAdd
Tactic:
simp only [insert]
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
⊢ (match c.isUnit with
    | none =>
      { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments }
    | some (l, true) =>
      { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addPosAssignment }
    | some (l, false) =>
      { 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
⊢ (match c.isUnit with
    | none =>
      { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments }
    | some (l, true) =>
      { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addPosAssignment }
    | some (l, false) =>
      { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments.modify l.val addNegAssignment }).readyForRupAdd
Tactic:
split
Proof state after:
case h_1
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
heq✝ : c.isUnit = none
⊢ { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := f.assignments }.readyForRupAdd

case h_2
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✝, true)
⊢ { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := f.assignments.modify l✝.val addPosAssignment }.readyForRupAdd

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
Theorem: LRAT.DefaultFormula.insert_readyForRupAdd
Proof state before:
case h_1
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
heq✝ : c.isUnit = none
⊢ { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := f.assignments }.readyForRupAdd

case h_2
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✝, true)
⊢ { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := f.assignments.modify l✝.val addPosAssignment }.readyForRupAdd

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:
. refine ⟨f_readyForRupAdd.1, f_readyForRupAdd.2.1, ?_⟩
  intro i b hb
  have hf := f_readyForRupAdd.2.2 i b 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:
case h_2
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✝, true)
⊢ { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := f.assignments.modify l✝.val addPosAssignment }.readyForRupAdd

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