-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFormula n) (id : Nat) :
    StrongAssignmentsInvariant f → StrongAssignmentsInvariant (deleteOne f id)

Proof state:
case neg.h_3.inl.h.isTrue.intro.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.toList
h✝ : id < f.clauses.size
idx : Nat
hbound : idx < f.clauses.toList.length
hidx : f.clauses.toList[idx] = some (unit (i, b))
idx_in_bounds : idx < (f.clauses.toList.set id none).length
⊢ ∃ n_1, (f.clauses.toList.set id none).get n_1 = f.clauses.toList[idx]

Tactic:
apply Exists.intro ⟨idx, idx_in_bounds⟩

Result:
case neg.h_3.inl.h.isTrue.intro.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.toList
h✝ : id < f.clauses.size
idx : Nat
hbound : idx < f.clauses.toList.length
hidx : f.clauses.toList[idx] = some (unit (i, b))
idx_in_bounds : idx < (f.clauses.toList.set id none).length
⊢ (f.clauses.toList.set id none).get ⟨idx, idx_in_bounds⟩ = f.clauses.toList[idx]

Proof state:
n : Nat
f : DefaultFormula n
id : Nat
⊢ f.StrongAssignmentsInvariant → (f.deleteOne id).StrongAssignmentsInvariant

Tactic:
intro hf

Result:
n : Nat
f : DefaultFormula n
id : Nat
hf : f.StrongAssignmentsInvariant
⊢ (f.deleteOne id).StrongAssignmentsInvariant

Proof state:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
hl :
  ∀ (x : PosFin n),
    ¬c = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬c = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.toList
h✝ : id < f.clauses.size
idx : Nat
hbound : idx < f.clauses.toList.length
hidx : f.clauses.toList[idx] = some (unit (i, b))
idx_in_bounds : idx < (f.clauses.toList.set id none).length
id_eq_idx : id = idx
idx_in_bounds2 : idx < f.clauses.size
heq : unit (i, b) = c
⊢ False

Tactic:
rw [← heq] at hl

Result:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
hl :
  ∀ (x : PosFin n),
    ¬unit (i, b) = { clause := [(x, false)], nodupkey := ⋯, nodup := ⋯ } ∧
      ¬unit (i, b) = { clause := [(x, true)], nodupkey := ⋯, nodup := ⋯ }
x✝¹ : Option (DefaultClause n)
val✝ : DefaultClause n
x✝ :
  ∀ (l : Literal (PosFin n)) (nodupkey : ∀ (l_1 : PosFin n), ¬(l_1, true) ∈ [l] ∨ ¬(l_1, false) ∈ [l])
    (nodup : [l].Nodup), val✝ = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False
heq✝ : some c = some val✝
deleteOne_f_rw :
  f.deleteOne id =
    { clauses := f.clauses.set! id none, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.toList
h✝ : id < f.clauses.size
idx : Nat
hbound : idx < f.clauses.toList.length
hidx : f.clauses.toList[idx] = some (unit (i, b))
idx_in_bounds : idx < (f.clauses.toList.set id none).length
id_eq_idx : id = idx
idx_in_bounds2 : idx < f.clauses.size
heq : unit (i, b) = c
⊢ False

Proof state:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
l_ne_b : l.snd = !b
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.toList
h✝ : id < f.clauses.size
idx : Nat
hbound : idx < f.clauses.toList.length
hidx : f.clauses.toList[idx] = some (unit (i, b))
idx_in_bounds : idx < (f.clauses.toList.set id none).length
id_eq_idx : id = idx
⊢ False

Tactic:
have idx_in_bounds2 : idx < f.clauses.size := by
  conv => rhs; rw [Array.size_toArray]
  exact hbound

Result:
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
l_ne_b : l.snd = !b
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.toList
h✝ : id < f.clauses.size
idx : Nat
hbound : idx < f.clauses.toList.length
hidx : f.clauses.toList[idx] = some (unit (i, b))
idx_in_bounds : idx < (f.clauses.toList.set id none).length
id_eq_idx : id = idx
idx_in_bounds2 : idx < f.clauses.size
⊢ False