-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem derivedLitsInvariant_confirmRupHint {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n)
    (rupHints : Array Nat) (i : Fin rupHints.size)
    (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool)
    (ih : ∃ hsize : acc.1.size = n, DerivedLitsInvariant f f_assignments_size acc.1 hsize acc.2.1) :
    let rupHint_res := (confirmRupHint f.clauses) acc rupHints[i]
    ∃ hsize : rupHint_res.1.size = n, DerivedLitsInvariant f f_assignments_size rupHint_res.1 hsize rupHint_res.2.1

Proof state:
case intro.isFalse.inr.inr.intro.inr.inr.inr
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hreducedToNonunit : c.reduce acc.fst = ReduceResult.reducedToNonunit
⊢ f.DerivedLitsInvariant f_assignments_size acc.fst ⋯ acc.2.fst

Tactic:
exact ih

Result:
no goals

Proof state:
case intro.isFalse.inr.inr.intro.inr.inr.inl.intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
⊢ f.DerivedLitsInvariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), (l.fst, l.snd) :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), (l.fst, l.snd) :: acc.2.fst, false, false)).snd.fst

Tactic:
by_cases h : hasAssignment l.snd acc.fst[l.fst.val]!

Result:
case pos
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.DerivedLitsInvariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), (l.fst, l.snd) :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), (l.fst, l.snd) :: acc.2.fst, false, false)).snd.fst

case neg
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
l : Literal (PosFin n)
hreducedToUnit : c.reduce acc.fst = ReduceResult.reducedToUnit l
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ f.DerivedLitsInvariant f_assignments_size
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.fst.val (addAssignment l.snd), (l.fst, l.snd) :: acc.2.fst, false, false)).fst
    ⋯
    (if hasAssignment l.snd acc.fst[l.fst.val]! = true then (acc.fst, acc.2.fst, false, false)
        else (acc.fst.modify l.fst.val (addAssignment l.snd), (l.fst, l.snd) :: acc.2.fst, false, false)).snd.fst

Proof state:
case intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
⊢ let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
  ∃ hsize, f.DerivedLitsInvariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst

Tactic:
apply Exists.intro hsize'

Result:
case intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
⊢ f.DerivedLitsInvariant f_assignments_size (confirmRupHint f.clauses acc rupHints[i]).fst hsize'
    (confirmRupHint f.clauses acc rupHints[i]).snd.fst

Proof state:
case intro.isFalse.inr.inr.intro.inl
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : ¬(acc.2.2.snd || acc.2.2.fst) = true
c : DefaultClause n
rupHint_clause_eq_c : f.clauses[rupHints[↑i]]? = some (some c)
hencounteredBoth : c.reduce acc.fst = ReduceResult.encounteredBoth
⊢ f.DerivedLitsInvariant f_assignments_size acc.fst ⋯ acc.2.fst

Tactic:
exact ih

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ (confirmRupHint f.clauses acc rupHints[i]).fst.size = n

Tactic:
rw [size_assignemnts_confirmRupHint]

Result:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ acc.fst.size = n

Proof state:
case intro.isTrue
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
i : Fin rupHints.size
acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool
hsize : acc.fst.size = n
ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
hsize' : (confirmRupHint f.clauses acc rupHints[i]).fst.size = n
h✝ : (acc.2.2.snd || acc.2.2.fst) = true
⊢ f.DerivedLitsInvariant f_assignments_size (acc.fst, acc.2.fst, acc.2.2.fst, acc.2.2.snd).fst ⋯
    (acc.fst, acc.2.fst, acc.2.2.fst, acc.2.2.snd).snd.fst

Tactic:
exact ih

Result:
no goals