-- 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
⊢ ∀ (a : Action (DefaultClause (cnf.numLiterals + 1)) (PosFin (cnf.numLiterals + 1))),
    a ∈
        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) →
      WellFormedAction a

Tactic:
intro action h

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
action : Action (DefaultClause (cnf.numLiterals + 1)) (PosFin (cnf.numLiterals + 1))
h :
  action ∈
    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)
⊢ WellFormedAction action

Proof state:
case a
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)
⊢ Unsatisfiable (PosFin (cnf.numLiterals + 1)) (CNF.convertLRAT cnf)

Tactic:
assumption

Result:
no goals