-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
    (f_readyForRatAdd : ReadyForRatAdd f) (pivot : Literal (PosFin n))
    (ratHints : Array (Nat × Array Nat))
    (ratHintsExhaustive_eq_true : ratHintsExhaustive f pivot ratHints = true) (c' : DefaultClause n)
    (c'_in_f : c' ∈ toList f) (negPivot_in_c' : Literal.negate pivot ∈ Clause.toList c') :
    ∃ i : Fin ratHints.size, f.clauses[ratHints[i].1]! = some c'

Proof state:
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.negate ∈ Clause.toList c'
c'_in_f : some c' ∈ f.clauses.toList
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'

Tactic:
rw [List.mem_iff_getElem] at c'_in_f

Result:
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.negate ∈ Clause.toList c'
c'_in_f : ∃ i h, f.clauses.toList[i] = some c'
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'

Proof state:
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.negate ∈ Clause.toList c'
c'_in_f : ∃ i h, f.clauses.toList[i] = some c'
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'

Tactic:
rcases c'_in_f with ⟨i, hi, c'_in_f⟩

Result:
case intro.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.negate ∈ Clause.toList c'
i : Nat
hi : i < f.clauses.toList.length
c'_in_f : f.clauses.toList[i] = some c'
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'

Proof state:
case intro.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.negate)
          (Array.range f.clauses.size) =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negate ∈ Clause.toList c'
i : Nat
hi : i < f.clauses.toList.length
c'_in_f : f.clauses.toList[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).toList
j : Fin (Array.map (fun x => x.fst) ratHints).toList.length
h' : (Array.map (fun x => x.fst) ratHints).toList.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.toList_map, List.length_map] at j_property
  dsimp at *
  omega

Result:
case intro.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.negate)
          (Array.range f.clauses.size) =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negate ∈ Clause.toList c'
i : Nat
hi : i < f.clauses.toList.length
c'_in_f : f.clauses.toList[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).toList
j : Fin (Array.map (fun x => x.fst) ratHints).toList.length
h' : (Array.map (fun x => x.fst) ratHints).toList.get j = i
j_in_bounds : ↑j < ratHints.size
⊢ ∃ i, f.clauses[ratHints[i].fst]! = some c'

Proof state:
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.negate)
          (Array.range f.clauses.size) =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negate ∈ Clause.toList c'
i : Nat
hi : i < f.clauses.toList.length
c'_in_f : f.clauses.toList[i] = some c'
i_in_bounds : i < f.clauses.size
⊢ i < f.clauses.size

Tactic:
exact i_in_bounds

Result:
no goals

Proof state:
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.negate)
          (Array.range f.clauses.size) =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negate ∈ Clause.toList c'
i : Nat
hi : i < f.clauses.toList.length
c'_in_f : f.clauses.toList[i] = some c'
i_in_bounds : i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : i < f.clauses.size
i_eq_range_i : i = (Array.range f.clauses.size)[i]
⊢ (Array.range f.clauses.size)[i] ∈
    Array.filter
      (fun i =>
        match f.clauses[i]! with
        | none => false
        | some c => c.contains pivot.negate)
      (Array.range f.clauses.size)

Tactic:
rw [Array.mem_filter]

Result:
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.negate)
          (Array.range f.clauses.size) =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negate ∈ Clause.toList c'
i : Nat
hi : i < f.clauses.toList.length
c'_in_f : f.clauses.toList[i] = some c'
i_in_bounds : i < (Array.range f.clauses.size).size
i_lt_f_clauses_size : i < f.clauses.size
i_eq_range_i : i = (Array.range f.clauses.size)[i]
⊢ (Array.range f.clauses.size)[i] ∈ Array.range f.clauses.size ∧
    (match f.clauses[(Array.range f.clauses.size)[i]]! with
      | none => false
      | some c => c.contains pivot.negate) =
      true

Proof state:
case intro.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.negate)
          (Array.range f.clauses.size) =
        Array.map (fun x => x.fst) ratHints) =
    true
c' : DefaultClause n
negPivot_in_c' : pivot.negate ∈ Clause.toList c'
i : Nat
hi : i < f.clauses.toList.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).toList
j : Fin (Array.map (fun x => x.fst) ratHints).toList.length
j_in_bounds : ↑j < ratHints.size
h' : ratHints[↑j].fst = i
⊢ f.clauses[ratHints[⟨↑j, j_in_bounds⟩].fst]! = some c'

Tactic:
simp [getElem!, h', i_lt_f_clauses_size, dite_true, c'_in_f, decidableGetElem?]

Result:
no goals