-- 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 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

Tactic:
by_cases i = l.1

Result:
case pos
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
h✝ : i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList

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, 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
h✝ : ¬i.val = l.val
⊢ 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, true)
hsize : acc.size = n
i_eq_l : i.val = l.val
b_eq_false : b = false
h : acc[l.val].hasNegAssignment = true
ih : hasAssignment false acc[l.val] = true → unit (l, false) ∈ (ofArray arr).toList
⊢ unit (i, b) ∈ (ofArray arr).toList

Tactic:
simp only [hasAssignment, ite_false] at ih

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, true)
hsize : acc.size = n
i_eq_l : i.val = l.val
b_eq_false : b = false
h : acc[l.val].hasNegAssignment = true
ih :
  (if false = true then hasPosAssignment else hasNegAssignment) acc[l.val] = true →
    unit (l, false) ∈ (ofArray arr).toList
⊢ unit (i, b) ∈ (ofArray arr).toList

Proof state:
case right
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).StrongAssignmentsInvariant

Tactic:
have hsize : (ofArray arr).assignments.size = n := by
  simp only [ofArray, ← Array.foldl_toList]
  have hb : (mkArray n unassigned).size = n := by simp only [Array.size_mkArray]
  have hl (acc : Array Assignment) (ih : acc.size = n) (cOpt : Option (DefaultClause n)) (_cOpt_in_arr : cOpt ∈ arr.toList) :
    (ofArray_fold_fn acc cOpt).size = n := by rw [size_ofArray_fold_fn acc cOpt, ih]
  exact List.foldlRecOn arr.toList ofArray_fold_fn (mkArray n unassigned) hb hl

Result:
case right
n : Nat
arr : Array (Option (DefaultClause n))
hsize : (ofArray arr).assignments.size = n
⊢ (ofArray arr).StrongAssignmentsInvariant

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, 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
i_ne_l : ¬i.val = l.val
⊢ unit (i, b) ∈ (ofArray arr).toList

Tactic:
simp only [Array.getElem_modify_of_ne (Ne.symm i_ne_l)] 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, true)
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_ne_l : ¬i.val = l.val
h : hasAssignment b acc[i.val] = true
⊢ unit (i, b) ∈ (ofArray arr).toList