-- 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:
case right.intro
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)
hl :
  ∀ (acc : Array Assignment),
    ModifiedAssignmentsInvariant acc →
      ∀ (cOpt : Option (DefaultClause n)), cOpt ∈ arr.toList → ModifiedAssignmentsInvariant (ofArray_fold_fn acc cOpt)
_h_size : (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.toList).size = n
h' :
  ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.toList)[i.val] = true →
      unit (i, b) ∈ (ofArray arr).toList
i : PosFin n
b : Bool
h : hasAssignment b (ofArray arr).assignments[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList

Tactic:
simp only [ofArray, ← Array.foldl_toList] at h

Result:
case right.intro
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)
hl :
  ∀ (acc : Array Assignment),
    ModifiedAssignmentsInvariant acc →
      ∀ (cOpt : Option (DefaultClause n)), cOpt ∈ arr.toList → ModifiedAssignmentsInvariant (ofArray_fold_fn acc cOpt)
_h_size : (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.toList).size = n
h' :
  ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.toList)[i.val] = true →
      unit (i, b) ∈ (ofArray arr).toList
i : PosFin n
b : Bool
h : hasAssignment b (List.foldl ofArray_fold_fn (mkArray n unassigned) arr.toList)[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)
hsize : acc.size = n
i_eq_l : i.val = l.val
b_eq_true : b = true
h : acc[l.val].hasPosAssignment = true
ih : (if True then hasPosAssignment else hasNegAssignment) acc[l.val] = true → unit (l, true) ∈ (ofArray arr).toList
⊢ unit (l, true) ∈ (ofArray arr).toList

Tactic:
exact ih h

Result:
no goals

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
l : PosFin n
heq : c.isUnit = some (l, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList

Tactic:
rcases ih with ⟨hsize, ih⟩

Result:
case intro
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, true)
h : hasAssignment b (acc.modify l.val addPosAssignment)[i.val] = true
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
⊢ unit (i, b) ∈ (ofArray arr).toList

Proof state:
case neg
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)
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
h✝ : ¬b = true
⊢ unit (i, b) ∈ (ofArray arr).toList

Tactic:
next b_eq_false =>
rw [isUnit_iff, DefaultClause.toList] at heq
simp only [toList, ofArray, List.map, List.append_nil, List.mem_filterMap, id_eq, exists_eq_right]
have i_eq_l : i = l := Subtype.ext i_eq_l
simp only [unit, b_eq_false, i_eq_l]
have c_def : c = ⟨c.clause, c.nodupkey, c.nodup⟩ := rfl
simp only [heq] at c_def
rw [c_def] at cOpt_in_arr
exact cOpt_in_arr

Result:
no goals

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)
h : hasAssignment b (acc.modify l.val addNegAssignment)[i.val] = true
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
⊢ unit (i, b) ∈ (ofArray arr).toList

Tactic:
simp only [i_eq_l, Array.getElem_modify_self] 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
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)
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
⊢ unit (i, b) ∈ (ofArray arr).toList