-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem size_assignemnts_confirmRupHint {n : Nat} (clauses : Array (Option (DefaultClause n)))
    (assignments : Array Assignment) (derivedLits : CNF.Clause (PosFin n)) (b1 b2 : Bool) (id : Nat) :
    (confirmRupHint clauses (assignments, derivedLits, b1, b2) id).1.size = assignments.size

Proof state:
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : CNF.Clause (PosFin n)
b1 b2 : Bool
id : Nat
⊢ (if (b2 || b1) = true then (assignments, derivedLits, b1, b2)
        else
          match clauses[id]? with
          | some (some c) =>
            match c.reduce assignments with
            | ReduceResult.encounteredBoth => (assignments, derivedLits, true, false)
            | ReduceResult.reducedToEmpty => (assignments, derivedLits, true, false)
            | ReduceResult.reducedToUnit (l, b) =>
              if hasAssignment b assignments[l.val]! = true then (assignments, derivedLits, false, false)
              else (assignments.modify l.val (addAssignment b), (l, b) :: derivedLits, false, false)
            | ReduceResult.reducedToNonunit => (assignments, derivedLits, false, true)
          | some none => (assignments, derivedLits, false, true)
          | none => (assignments, derivedLits, false, true)).fst.size =
    assignments.size

Tactic:
repeat first
  | rfl
  | simp only [Array.size_modify]
  | split

Result:
no goals

Proof state:
case isFalse.h_1.h_3.isFalse
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : CNF.Clause (PosFin n)
b1 b2 : Bool
id : Nat
h✝¹ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
l✝ : PosFin n
b✝ : Bool
heq✝ : c✝.reduce assignments = ReduceResult.reducedToUnit (l✝, b✝)
h✝ : ¬hasAssignment b✝ assignments[l✝.val]! = true
⊢ (assignments.modify l✝.val (addAssignment b✝), (l✝, b✝) :: derivedLits, false, false).fst.size = assignments.size

case isFalse.h_1.h_4
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : CNF.Clause (PosFin n)
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
heq✝ : c✝.reduce assignments = ReduceResult.reducedToNonunit
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_2
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : CNF.Clause (PosFin n)
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = some none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_3
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : CNF.Clause (PosFin n)
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

Tactic:
simp only [Array.size_modify]

Result:
case isFalse.h_1.h_4
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : CNF.Clause (PosFin n)
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
heq✝ : c✝.reduce assignments = ReduceResult.reducedToNonunit
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_2
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : CNF.Clause (PosFin n)
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = some none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_3
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : CNF.Clause (PosFin n)
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

Proof state:
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : CNF.Clause (PosFin n)
b1 b2 : Bool
id : Nat
⊢ (confirmRupHint clauses (assignments, derivedLits, b1, b2) id).fst.size = assignments.size

Tactic:
simp only [confirmRupHint]

Result:
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : CNF.Clause (PosFin n)
b1 b2 : Bool
id : Nat
⊢ (if (b2 || b1) = true then (assignments, derivedLits, b1, b2)
        else
          match clauses[id]? with
          | some (some c) =>
            match c.reduce assignments with
            | ReduceResult.encounteredBoth => (assignments, derivedLits, true, false)
            | ReduceResult.reducedToEmpty => (assignments, derivedLits, true, false)
            | ReduceResult.reducedToUnit (l, b) =>
              if hasAssignment b assignments[l.val]! = true then (assignments, derivedLits, false, false)
              else (assignments.modify l.val (addAssignment b), (l, b) :: derivedLits, false, false)
            | ReduceResult.reducedToNonunit => (assignments, derivedLits, false, true)
          | some none => (assignments, derivedLits, false, true)
          | none => (assignments, derivedLits, false, true)).fst.size =
    assignments.size

Proof state:
case isFalse.h_3
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : CNF.Clause (PosFin n)
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

Tactic:
first
| rfl
| simp only [Array.size_modify]
| split

Result:
no goals