internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.performRatCheck_success_entails_c_without_negPivot
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
negPivot : Literal (PosFin n)
ratHint : Nat × Array Nat
c : DefaultClause n
hc : f.clauses[ratHint.fst]! = some c
p : PosFin n → Bool
pf : p ⊨ f
h :
  ({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits, assignments := f.assignments }.insertRatUnits
        (c.delete negPivot).negate).snd =
    true
performRatCheck_success :
  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                  assignments := f.assignments }.insertRatUnits
              (c.delete negPivot).negate).fst.clearRatUnits,
        true).snd =
    true
⊢ p ⊨ c.delete negPivot
Tactic:
exact insertRat_entails_hsat f hf (DefaultClause.delete c negPivot) p pf h
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRatCheck_success_entails_c_without_negPivot
Proof state before:
case isFalse.isTrue
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
negPivot : Literal (PosFin n)
ratHint : Nat × Array Nat
c : DefaultClause n
hc : f.clauses[ratHint.fst]! = some c
p : PosFin n → Bool
pf : p ⊨ f
h✝¹ :
  ¬({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments }.insertRatUnits
          (c.delete negPivot).negate).snd =
      true
h✝ :
  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                        assignments := f.assignments }.insertRatUnits
                    (c.delete negPivot).negate).fst.performRupCheck
              ratHint.snd).2.2.snd =
      true ∨
    (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                        assignments := f.assignments }.insertRatUnits
                    (c.delete negPivot).negate).fst.performRupCheck
              ratHint.snd).2.2.fst =
      false
performRatCheck_success : False
⊢ p ⊨ c.delete negPivot
Tactic:
exact False.elim performRatCheck_success
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRatCheck_success_entails_c_without_negPivot
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
negPivot : Literal (PosFin n)
ratHint : Nat × Array Nat
c : DefaultClause n
hc : f.clauses[ratHint.fst]! = some c
p : PosFin n → Bool
pf : p ⊨ f
h✝ :
  ¬({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments }.insertRatUnits
          (c.delete negPivot).negate).snd =
      true
performRatCheck_success :
  ({
            clauses :=
              (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                              assignments := f.assignments }.insertRatUnits
                          (c.delete negPivot).negate).fst.performRupCheck
                    ratHint.snd).1.clauses,
            rupUnits :=
              (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                              assignments := f.assignments }.insertRatUnits
                          (c.delete negPivot).negate).fst.performRupCheck
                    ratHint.snd).1.rupUnits,
            ratUnits :=
              (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                              assignments := f.assignments }.insertRatUnits
                          (c.delete negPivot).negate).fst.performRupCheck
                    ratHint.snd).1.ratUnits,
            assignments :=
              restoreAssignments
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete negPivot).negate).fst.performRupCheck
                      ratHint.snd).1.assignments
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete negPivot).negate).fst.performRupCheck
                      ratHint.snd).2.fst }.clearRatUnits,
        true).snd =
    true
h :
  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                        assignments := f.assignments }.insertRatUnits
                    (c.delete negPivot).negate).fst.performRupCheck
              ratHint.snd).2.2.snd =
      false ∧
    (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                        assignments := f.assignments }.insertRatUnits
                    (c.delete negPivot).negate).fst.performRupCheck
              ratHint.snd).2.2.fst =
      true
pfc : ∀ (x : DefaultClause n), x ∈ (f.insert (c.delete negPivot)).toList → decide (Clause.instHSat.1 p x) = true
c_negPivot_in_fc : c.delete negPivot ∈ (f.insert (c.delete negPivot)).toList
⊢ p ⊨ c.delete negPivot
Tactic:
exact of_decide_eq_true $ pfc (DefaultClause.delete c negPivot) c_negPivot_in_fc
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRatCheck_success_entails_c_without_negPivot
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
negPivot : Literal (PosFin n)
ratHint : Nat × Array Nat
c : DefaultClause n
hc : f.clauses[ratHint.fst]! = some c
p : PosFin n → Bool
pf : p ⊨ f
h✝ :
  ¬({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
              assignments := f.assignments }.insertRatUnits
          (c.delete negPivot).negate).snd =
      true
performRatCheck_success :
  ({
            clauses :=
              (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                              assignments := f.assignments }.insertRatUnits
                          (c.delete negPivot).negate).fst.performRupCheck
                    ratHint.snd).1.clauses,
            rupUnits :=
              (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                              assignments := f.assignments }.insertRatUnits
                          (c.delete negPivot).negate).fst.performRupCheck
                    ratHint.snd).1.rupUnits,
            ratUnits :=
              (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                              assignments := f.assignments }.insertRatUnits
                          (c.delete negPivot).negate).fst.performRupCheck
                    ratHint.snd).1.ratUnits,
            assignments :=
              restoreAssignments
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete negPivot).negate).fst.performRupCheck
                      ratHint.snd).1.assignments
                (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                                assignments := f.assignments }.insertRatUnits
                            (c.delete negPivot).negate).fst.performRupCheck
                      ratHint.snd).2.fst }.clearRatUnits,
        true).snd =
    true
h :
  (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                        assignments := f.assignments }.insertRatUnits
                    (c.delete negPivot).negate).fst.performRupCheck
              ratHint.snd).2.2.snd =
      false ∧
    (({ clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                        assignments := f.assignments }.insertRatUnits
                    (c.delete negPivot).negate).fst.performRupCheck
              ratHint.snd).2.2.fst =
      true
pfc : ∀ (x : DefaultClause n), x ∈ (f.insert (c.delete negPivot)).toList → decide (Clause.instHSat.1 p x) = true
⊢ c.delete negPivot = c.delete negPivot ∨ c.delete negPivot ∈ f.toList
Tactic:
exact Or.inl rfl
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Tactic:
simp only [toList, Array.toList_eq, f_readyForRatAdd.2.1, Array.data_toArray, List.map, List.append_nil, f_readyForRatAdd.1,
  List.mem_filterMap, id_eq, exists_eq_right] at c'_in_f
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
c'_in_f : some c' ∈ f.clauses.data
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
c'_in_f : some c' ∈ f.clauses.data
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Tactic:
rw [List.mem_iff_get] at c'_in_f
Proof state after:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
c'_in_f : ∃ n_1, f.clauses.data.get n_1 = some c'
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
c'_in_f : ∃ n_1, f.clauses.data.get n_1 = some c'
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Tactic:
rcases c'_in_f with ⟨i, c'_in_f⟩
Proof state after:
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses.data.get i = some c'
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses.data.get i = some c'
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Tactic:
rw [← Array.getElem_eq_data_get] at c'_in_f
Proof state after:
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Tactic:
simp only [ratHintsExhaustive, getRatClauseIndices] at ratHintsExhaustive_eq_true
Proof state after:
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Tactic:
have i_in_bounds : i.val < Array.size (Array.range (Array.size f.clauses)) := by
  rw [Array.range_size]
  dsimp
  omega
Proof state after:
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Tactic:
have i_lt_f_clauses_size : i.1 < f.clauses.size := by
  rw [Array.range_size] at i_in_bounds
  exact i_in_bounds
Proof state after:
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Tactic:
have h : i.1 ∈ (ratHints.map (fun x => x.1)).data := by
  rw [← of_decide_eq_true ratHintsExhaustive_eq_true]
  have i_eq_range_i : i.1 = (Array.range f.clauses.size)[i.1]'i_in_bounds := by
    have f_clauses_rw : f.clauses = { data := f.clauses.data } := rfl
    rw [Array.range_idx]
    conv => rhs; rw [f_clauses_rw, Array.size]
    exact i.2
  rw [i_eq_range_i]
  apply Misc.Array.mem_filter i.1 i_in_bounds
  simp only [getElem!, Array.range_idx i_lt_f_clauses_size, i_lt_f_clauses_size, dite_true,
    c'_in_f, DefaultClause.contains_iff, Array.get_eq_getElem]
  simp only [Clause.toList] at negPivot_in_c'
  exact negPivot_in_c'
Proof state after:
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
h : ↑i ∈ (Array.map (fun x => x.fst) ratHints).data
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
case intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
h : ↑i ∈ (Array.map (fun x => x.fst) ratHints).data
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Tactic:
rcases List.get_of_mem h with ⟨j, h'⟩
Proof state after:
case intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
h : ↑i ∈ (Array.map (fun x => x.fst) ratHints).data
j : Fin (Array.map (fun x => x.fst) ratHints).data.length
h' : (Array.map (fun x => x.fst) ratHints).data.get j = ↑i
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
case intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
h : ↑i ∈ (Array.map (fun x => x.fst) ratHints).data
j : Fin (Array.map (fun x => x.fst) ratHints).data.length
h' : (Array.map (fun x => x.fst) ratHints).data.get j = ↑i
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Tactic:
have j_in_bounds : j < ratHints.size := by
  have j_property := j.2
  simp only [Array.map_data, List.length_map] at j_property
  dsimp at *
  omega
Proof state after:
case intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
h : ↑i ∈ (Array.map (fun x => x.fst) ratHints).data
j : Fin (Array.map (fun x => x.fst) ratHints).data.length
h' : (Array.map (fun x => x.fst) ratHints).data.get j = ↑i
j_in_bounds : ↑j < ratHints.size
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Theorem: LRAT.DefaultFormula.existsRatHint_of_ratHintsExhaustive
Proof state before:
case intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
h : ↑i ∈ (Array.map (fun x => x.fst) ratHints).data
j : Fin (Array.map (fun x => x.fst) ratHints).data.length
h' : (Array.map (fun x => x.fst) ratHints).data.get j = ↑i
j_in_bounds : ↑j < ratHints.size
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'
Tactic:
rw [← Array.getElem_eq_data_get] at h'
Proof state after:
case intro.intro
n : Nat
f : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
pivot : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
ratHintsExhaustive_eq_true :
  decide
      (Array.filter
          (fun i =>
            match f.clauses[i]! with
            | none => false
            | some c => c.contains pivot.negateLiteral)
          (Array.range f.clauses.size) 0 =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negateLiteral ∈ Clause.toList c'
i : Fin f.clauses.data.length
c'_in_f : f.clauses[↑i] = some c'
i_in_bounds : ↑i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : ↑i < f.clauses.size
h : ↑i ∈ (Array.map (fun x => x.fst) ratHints).data
j : Fin (Array.map (fun x => x.fst) ratHints).data.length
h' : (Array.map (fun x => x.fst) ratHints)[↑j] = ↑i
j_in_bounds : ↑j < ratHints.size
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'