-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem derivedLitsInvariant_performRupCheck {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n)
    (rupHints : Array Nat)
    (f'_assignments_size : (performRupCheck f rupHints).1.assignments.size = n) :
    let rupCheckRes := performRupCheck f rupHints
    DerivedLitsInvariant f f_assignments_size rupCheckRes.1.assignments f'_assignments_size rupCheckRes.2.1

Proof state:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ let_fun i_lt_assignments_size := ⋯;
  let_fun i_lt_f_assignments_size := ⋯;
  let assignments_i := (f.assignments, [], false, false).fst[↑i];
  let fassignments_i := f.assignments[↑i];
  (assignments_i = fassignments_i ∧
      ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i) ∨
    (∃ j,
        (List.get (f.assignments, [], false, false).snd.fst j).fst.val = ↑i ∧
          assignments_i = addAssignment (List.get (f.assignments, [], false, false).snd.fst j).snd fassignments_i ∧
            ¬hasAssignment (List.get (f.assignments, [], false, false).snd.fst j).snd fassignments_i = true ∧
              ∀ (k : Fin (List.length (f.assignments, [], false, false).snd.fst)),
                k ≠ j → (List.get (f.assignments, [], false, false).snd.fst k).fst.val ≠ ↑i) ∨
      ∃ j1 j2,
        (List.get (f.assignments, [], false, false).snd.fst j1).fst.val = ↑i ∧
          (List.get (f.assignments, [], false, false).snd.fst j2).fst.val = ↑i ∧
            (List.get (f.assignments, [], false, false).snd.fst j1).snd = true ∧
              (List.get (f.assignments, [], false, false).snd.fst j2).snd = false ∧
                assignments_i = both ∧
                  fassignments_i = unassigned ∧
                    ∀ (k : Fin (List.length (f.assignments, [], false, false).snd.fst)),
                      k ≠ j1 → k ≠ j2 → (List.get (f.assignments, [], false, false).snd.fst k).fst.val ≠ ↑i

Tactic:
apply Or.inl

Result:
case h
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ (f.assignments, [], false, false).fst[↑i] = f.assignments[↑i] ∧
    ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i

Proof state:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.DerivedLitsInvariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst

Tactic:
let motive := fun (_ : Nat) (acc : Array Assignment × CNF.Clause (PosFin n) × Bool × Bool) =>
  ∃ hsize : acc.1.size = n, DerivedLitsInvariant f f_assignments_size acc.1 hsize acc.2.1

Result:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.DerivedLitsInvariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst

Proof state:
case h.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i

Tactic:
intro l l_in_nil

Result:
case h.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
l : Literal (PosFin n)
l_in_nil : l ∈ (f.assignments, [], false, false).snd.fst
⊢ l.fst.val ≠ ↑i

Proof state:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
⊢ f.DerivedLitsInvariant f_assignments_size (f.assignments, [], false, false).fst f_assignments_size
    (f.assignments, [], false, false).snd.fst

Tactic:
intro i

Result:
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × CNF.Clause (PosFin n) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst
i : Fin n
⊢ let_fun i_lt_assignments_size := ⋯;
  let_fun i_lt_f_assignments_size := ⋯;
  let assignments_i := (f.assignments, [], false, false).fst[↑i];
  let fassignments_i := f.assignments[↑i];
  (assignments_i = fassignments_i ∧
      ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i) ∨
    (∃ j,
        (List.get (f.assignments, [], false, false).snd.fst j).fst.val = ↑i ∧
          assignments_i = addAssignment (List.get (f.assignments, [], false, false).snd.fst j).snd fassignments_i ∧
            ¬hasAssignment (List.get (f.assignments, [], false, false).snd.fst j).snd fassignments_i = true ∧
              ∀ (k : Fin (List.length (f.assignments, [], false, false).snd.fst)),
                k ≠ j → (List.get (f.assignments, [], false, false).snd.fst k).fst.val ≠ ↑i) ∨
      ∃ j1 j2,
        (List.get (f.assignments, [], false, false).snd.fst j1).fst.val = ↑i ∧
          (List.get (f.assignments, [], false, false).snd.fst j2).fst.val = ↑i ∧
            (List.get (f.assignments, [], false, false).snd.fst j1).snd = true ∧
              (List.get (f.assignments, [], false, false).snd.fst j2).snd = false ∧
                assignments_i = both ∧
                  fassignments_i = unassigned ∧
                    ∀ (k : Fin (List.length (f.assignments, [], false, false).snd.fst)),
                      k ≠ j1 → k ≠ j2 → (List.get (f.assignments, [], false, false).snd.fst k).fst.val ≠ ↑i