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

State before:
n : Nat
assignments : Array Assignment
cOpt : Option (DefaultClause n)
⊢ (ofArray_fold_fn assignments cOpt).size = assignments.size
Tactic:
rw [ofArray_fold_fn]
State after:
n : Nat
assignments : Array Assignment
cOpt : Option (DefaultClause n)
⊢ (match cOpt with
      | none => assignments
      | some c =>
        match c.isUnit with
        | none => assignments
        | some (l, true) => assignments.modify l.val addPosAssignment
        | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size

State before:
n : Nat
assignments : Array Assignment
cOpt : Option (DefaultClause n)
⊢ (match cOpt with
      | none => assignments
      | some c =>
        match c.isUnit with
        | none => assignments
        | some (l, true) => assignments.modify l.val addPosAssignment
        | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size
Tactic:
split
State after:
case h_1
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
⊢ assignments.size = assignments.size

case h_2
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
⊢ (match c✝.isUnit with
      | none => assignments
      | some (l, true) => assignments.modify l.val addPosAssignment
      | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size

State before:
case h_1
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
⊢ assignments.size = assignments.size

case h_2
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
⊢ (match c✝.isUnit with
      | none => assignments
      | some (l, true) => assignments.modify l.val addPosAssignment
      | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size
Tactic:
. rfl
State after:
case h_2
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
⊢ (match c✝.isUnit with
      | none => assignments
      | some (l, true) => assignments.modify l.val addPosAssignment
      | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size

State before:
case h_2
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
⊢ (match c✝.isUnit with
      | none => assignments
      | some (l, true) => assignments.modify l.val addPosAssignment
      | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size
Tactic:
. split <;> simp [Array.modify_preserves_size]
State after:
no goals

State before:
case h_1
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
⊢ assignments.size = assignments.size
Tactic:
rfl
State after:
no goals

State before:
case h_2
n : Nat
assignments : Array Assignment
cOpt✝ : Option (DefaultClause n)
c✝ : DefaultClause n
⊢ (match c✝.isUnit with
      | none => assignments
      | some (l, true) => assignments.modify l.val addPosAssignment
      | some (l, false) => assignments.modify l.val addNegAssignment).size =
    assignments.size
Tactic:
split <;> simp [Array.modify_preserves_size]
State after:
no goals