-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))) :
    ReadyForRupAdd (ofArray arr)

Proof state:
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
ModifiedAssignmentsInvariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
⊢ (mkArray n unassigned).size = n

Tactic:
simp only [Array.size_mkArray]

Result:
no goals

Proof state:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList

Tactic:
let ModifiedAssignmentsInvariant (assignments : Array Assignment) : Prop :=
  ∃ hsize : assignments.size = n,
    ∀ i : PosFin n, ∀ b : Bool, hasAssignment b (assignments[i.1]'(by rw [hsize]; exact i.2.2)) →
    (unit (i, b)) ∈ toList (ofArray arr)

Result:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
ModifiedAssignmentsInvariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList

Proof state:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
ModifiedAssignmentsInvariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList

Tactic:
have hb : ModifiedAssignmentsInvariant (mkArray n unassigned) := by
  have hsize : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
  apply Exists.intro hsize
  intro i b h
  by_cases hb : b <;> simp [hasAssignment, hb, hasPosAssignment, hasNegAssignment] at h

Result:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
ModifiedAssignmentsInvariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : ModifiedAssignmentsInvariant (mkArray n unassigned)
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (ofArray arr).assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList

Proof state:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
ModifiedAssignmentsInvariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : ModifiedAssignmentsInvariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.toList
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq✝ : c.isUnit = some (l, false)
heq : c.clause = [(l, false)]
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
i_eq_l : i = l
c_def : c = { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ }
⊢ some { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.toList

Tactic:
rw [c_def] at cOpt_in_arr

Result:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
ModifiedAssignmentsInvariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : ModifiedAssignmentsInvariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq✝ : c.isUnit = some (l, false)
heq : c.clause = [(l, false)]
cOpt_in_arr : some { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.toList
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
i_eq_l : i = l
c_def : c = { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ }
⊢ some { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.toList

Proof state:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
ModifiedAssignmentsInvariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : ModifiedAssignmentsInvariant (mkArray n unassigned)
acc : Array Assignment
ih : ModifiedAssignmentsInvariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.toList
hsize : (ofArray_fold_fn acc (some c)).size = n
h :
  hasAssignment b
      (match c.isUnit with
        | none => acc
        | some (l, true) => acc.modify l.val addPosAssignment
        | some (l, false) => acc.modify l.val addNegAssignment)[i.val] =
    true
heq : c.isUnit = none
⊢ unit (i, b) ∈ (ofArray arr).toList

Tactic:
simp only [heq] at h

Result:
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝ : (ofArray arr).assignments.size = n
ModifiedAssignmentsInvariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : ModifiedAssignmentsInvariant (mkArray n unassigned)
acc : Array Assignment
ih : ModifiedAssignmentsInvariant acc
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.toList
hsize : (ofArray_fold_fn acc (some c)).size = n
heq : c.isUnit = none
h : hasAssignment b acc[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList

Proof state:
n : Nat
arr : Array (Option (DefaultClause n))
hb : (mkArray n unassigned).size = n
hl :
  ∀ (acc : Array Assignment),
    acc.size = n → ∀ (cOpt : Option (DefaultClause n)), cOpt ∈ arr.toList → (ofArray_fold_fn acc cOpt).size = n
⊢ (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.toList).size = n

Tactic:
exact List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl

Result:
no goals