-- 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:
case isFalse.h_1.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))
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✝)
⊢ (if hasAssignment b✝ assignments[l✝.val]! = true then (assignments, derivedLits, false, false)
        else (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:
split

Result:
case isFalse.h_1.h_3.isTrue
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, derivedLits, false, false).fst.size = assignments.size

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

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

Result:
no goals