Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_invariant_helper
Proof state before:
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
hsize'✝ : (acc.fst.modify l.fst.val (addAssignment l.snd)).size = n :=
  Eq.mpr (id (congrArg (fun _a => _a = n) Array.modify_preserves_size)) hsize
i : Fin n
i_in_bounds : ↑i < acc.fst.size
l_in_bounds : l.fst.val < acc.fst.size
j1 j2 : Fin acc.snd.fst.length
j1_eq_i : (acc.snd.fst.get j1).fst.val = ↑i
j2_eq_i : (acc.snd.fst.get j2).fst.val = ↑i
j1_eq_true : (acc.snd.fst.get j1).snd = true
j2_eq_false : (acc.snd.fst.get j2).snd = false
h1 : acc.fst[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin acc.snd.fst.length), k ≠ j1 → k ≠ j2 → (acc.snd.fst.get k).fst.val ≠ ↑i
j1_succ_in_bounds : ↑j1 + 1 < (l :: acc.snd.fst).length
j2_succ_in_bounds : ↑j2 + 1 < (l :: acc.snd.fst).length
j1_succ : Fin (l :: acc.snd.fst).length := ⟨↑j1 + 1, j1_succ_in_bounds⟩
j2_succ : Fin (l :: acc.snd.fst).length := ⟨↑j2 + 1, j2_succ_in_bounds⟩
l_ne_i : l.fst.val ≠ ↑i
⊢ ∀ (k : Fin acc.snd.fst.length.succ), ¬k = j1_succ → ¬k = j2_succ → ¬((l :: acc.snd.fst).get k).fst.val = ↑i
Tactic:
. intro k k_ne_j1_succ k_ne_j2_succ
  have zero_in_bounds : 0 < (l :: acc.2.1).length := by
    simp only [List.length_cons]
    exact Nat.zero_lt_succ (List.length acc.snd.fst)
  by_cases k = ⟨0, zero_in_bounds⟩
  . next k_eq_zero =>
    simp only [k_eq_zero, List.length_cons, List.get, ne_eq]
    exact l_ne_i
  . next k_ne_zero =>
    have k_eq_succ : ∃ k' : Nat, ∃ k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length, k = ⟨k' + 1, k'_succ_in_bounds⟩ := by
      have k_val_ne_zero : k.1 ≠ 0 := by
        intro k_eq_zero
        simp only [List.length_cons, ← k_eq_zero, ne_eq, not_true] at k_ne_zero
      rcases Nat.exists_eq_succ_of_ne_zero k_val_ne_zero with ⟨k', k_eq_k'_succ⟩
      rw [Nat.succ_eq_add_one k'] at k_eq_k'_succ
      have k'_succ_in_bounds : k' + 1 < (l :: acc.2.1).length := by rw [← k_eq_k'_succ]; exact k.2
      apply Exists.intro k' ∘ Exists.intro k'_succ_in_bounds
      apply Fin.eq_of_val_eq
      exact k_eq_k'_succ
    rcases k_eq_succ with ⟨k', k'_succ_in_bounds, k_eq_succ⟩
    rw [k_eq_succ]
    simp only [List.get, Nat.add_eq, Nat.add_zero, ne_eq]
    have k'_in_bounds : k' < acc.2.1.length := by
      simp only [List.length_cons, Nat.succ_eq_add_one] at k'_succ_in_bounds
      exact Nat.lt_of_succ_lt_succ k'_succ_in_bounds
    have k'_ne_j1 : ⟨k', k'_in_bounds⟩ ≠ j1 := by
      simp only [List.length_cons, k_eq_succ, ne_eq, Fin.mk.injEq, Nat.succ.injEq, j1_succ] at k_ne_j1_succ
      exact Fin.ne_of_val_ne k_ne_j1_succ
    have k'_ne_j2 : ⟨k', k'_in_bounds⟩ ≠ j2 := by
      simp only [List.length_cons, k_eq_succ, ne_eq, Fin.mk.injEq, Nat.succ.injEq, j2_succ] at k_ne_j2_succ
      exact Fin.ne_of_val_ne k_ne_j2_succ
    exact h3 ⟨k', k'_in_bounds⟩ k'_ne_j1 k'_ne_j2
Proof state after:
no goals