-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Checker.lean
theorem check_sound (lratProof : Array IntAction) (cnf : CNF Nat) :
    check lratProof cnf → cnf.Unsat

Proof state:
lratProof : Array IntAction
cnf : CNF Nat
h1 :
  lratChecker (CNF.convertLRAT cnf)
      (List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (Action.addEmpty id rupHints) => some (Action.addEmpty id rupHints)
          | some (Action.addRup id c rupHints) => some (Action.addRup id c rupHints)
          | some (Action.del ids) => some (Action.del ids)
          | some (Action.addRat id c pivot rupHints ratHints) =>
            if pivot ∈ Clause.toList c then some (Action.addRat id c pivot rupHints ratHints) else none)
        (List.map (intActionToDefaultClauseAction (cnf.numLiterals + 1)) lratProof.toList)) =
    Result.success
⊢ cnf.Unsat

Tactic:
have h2 :=
  lratCheckerSound
    _
    (by apply CNF.convertLRAT_readyForRupAdd)
    (by apply CNF.convertLRAT_readyForRatAdd)
    _
    (by
      intro action h
      simp only [List.filterMap_map, List.mem_filterMap, Function.comp_apply] at h
      rcases h with ⟨WellFormedActions, _, h2⟩
      split at h2
      . contradiction
      . simp only [Option.some.injEq] at h2
        simp [← h2, WellFormedAction]
      . simp only [Option.some.injEq] at h2
        simp [← h2, WellFormedAction]
      . simp only [Option.some.injEq] at h2
        simp [← h2, WellFormedAction]
      . simp only [Option.ite_none_right_eq_some, Option.some.injEq] at h2
        rcases h2 with ⟨hleft, hright⟩
        simp [WellFormedAction, hleft, ← hright, Clause.limplies_iff_mem]
    )
    h1

Result:
lratProof : Array IntAction
cnf : CNF Nat
h1 :
  lratChecker (CNF.convertLRAT cnf)
      (List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (Action.addEmpty id rupHints) => some (Action.addEmpty id rupHints)
          | some (Action.addRup id c rupHints) => some (Action.addRup id c rupHints)
          | some (Action.del ids) => some (Action.del ids)
          | some (Action.addRat id c pivot rupHints ratHints) =>
            if pivot ∈ Clause.toList c then some (Action.addRat id c pivot rupHints ratHints) else none)
        (List.map (intActionToDefaultClauseAction (cnf.numLiterals + 1)) lratProof.toList)) =
    Result.success
h2 : Unsatisfiable (PosFin (cnf.numLiterals + 1)) (CNF.convertLRAT cnf)
⊢ cnf.Unsat

Proof state:
lratProof : Array IntAction
cnf : CNF Nat
h1 :
  (let internalFormula := CNF.convertLRAT cnf;
    let lratProof := lratProof.toList;
    let lratProof := List.map (intActionToDefaultClauseAction (cnf.numLiterals + 1)) lratProof;
    let lratProof :=
      List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (Action.addEmpty id rupHints) => some (Action.addEmpty id rupHints)
          | some (Action.addRup id c rupHints) => some (Action.addRup id c rupHints)
          | some (Action.del ids) => some (Action.del ids)
          | some (Action.addRat id c pivot rupHints ratHints) =>
            if pivot ∈ Clause.toList c then some (Action.addRat id c pivot rupHints ratHints) else none)
        lratProof;
    let checkerResult := lratChecker internalFormula lratProof;
    decide (checkerResult = Result.success)) =
    true
⊢ cnf.Unsat

Tactic:
simp only [decide_eq_true_eq] at h1

Result:
lratProof : Array IntAction
cnf : CNF Nat
h1 :
  lratChecker (CNF.convertLRAT cnf)
      (List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (Action.addEmpty id rupHints) => some (Action.addEmpty id rupHints)
          | some (Action.addRup id c rupHints) => some (Action.addRup id c rupHints)
          | some (Action.del ids) => some (Action.del ids)
          | some (Action.addRat id c pivot rupHints ratHints) =>
            if pivot ∈ Clause.toList c then some (Action.addRat id c pivot rupHints ratHints) else none)
        (List.map (intActionToDefaultClauseAction (cnf.numLiterals + 1)) lratProof.toList)) =
    Result.success
⊢ cnf.Unsat

Proof state:
lratProof : Array IntAction
cnf : CNF Nat
h1 : check lratProof cnf = true
⊢ cnf.Unsat

Tactic:
unfold check at h1

Result:
lratProof : Array IntAction
cnf : CNF Nat
h1 :
  (let internalFormula := CNF.convertLRAT cnf;
    let lratProof := lratProof.toList;
    let lratProof := List.map (intActionToDefaultClauseAction (cnf.numLiterals + 1)) lratProof;
    let lratProof :=
      List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (Action.addEmpty id rupHints) => some (Action.addEmpty id rupHints)
          | some (Action.addRup id c rupHints) => some (Action.addRup id c rupHints)
          | some (Action.del ids) => some (Action.del ids)
          | some (Action.addRat id c pivot rupHints ratHints) =>
            if pivot ∈ Clause.toList c then some (Action.addRat id c pivot rupHints ratHints) else none)
        lratProof;
    let checkerResult := lratChecker internalFormula lratProof;
    decide (checkerResult = Result.success)) =
    true
⊢ cnf.Unsat

Proof state:
case intro.intro.h_4
lratProof : Array IntAction
cnf : CNF Nat
h1 :
  lratChecker (CNF.convertLRAT cnf)
      (List.filterMap
        (fun actOpt =>
          match actOpt with
          | none => none
          | some (Action.addEmpty id rupHints) => some (Action.addEmpty id rupHints)
          | some (Action.addRup id c rupHints) => some (Action.addRup id c rupHints)
          | some (Action.del ids) => some (Action.del ids)
          | some (Action.addRat id c pivot rupHints ratHints) =>
            if pivot ∈ Clause.toList c then some (Action.addRat id c pivot rupHints ratHints) else none)
        (List.map (intActionToDefaultClauseAction (cnf.numLiterals + 1)) lratProof.toList)) =
    Result.success
action : Action (DefaultClause (cnf.numLiterals + 1)) (PosFin (cnf.numLiterals + 1))
WellFormedActions : IntAction
left✝ : WellFormedActions ∈ lratProof.toList
actOpt✝ : Option (DefaultClauseAction (cnf.numLiterals + 1))
ids✝ : Array Nat
heq✝ : intActionToDefaultClauseAction (cnf.numLiterals + 1) WellFormedActions = some (Action.del ids✝)
h2 : Action.del ids✝ = action
⊢ WellFormedAction action

Tactic:
simp [← h2, WellFormedAction]

Result:
no goals