-- 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
⊢ Formula.ReadyForRupAdd (CNF.convertLRAT cnf)

Tactic:
apply CNF.convertLRAT_readyForRupAdd

Result:
no goals

Proof state:
case intro.intro.h_3
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))
id✝ : Nat
c✝ : DefaultClause (cnf.numLiterals + 1)
rupHints✝ : Array Nat
heq✝ : intActionToDefaultClauseAction (cnf.numLiterals + 1) WellFormedActions = some (Action.addRup id✝ c✝ rupHints✝)
h2 : some (Action.addRup id✝ c✝ rupHints✝) = some action
⊢ WellFormedAction action

Tactic:
simp only [Option.some.injEq] at h2

Result:
case intro.intro.h_3
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))
id✝ : Nat
c✝ : DefaultClause (cnf.numLiterals + 1)
rupHints✝ : Array Nat
heq✝ : intActionToDefaultClauseAction (cnf.numLiterals + 1) WellFormedActions = some (Action.addRup id✝ c✝ rupHints✝)
h2 : Action.addRup id✝ c✝ rupHints✝ = action
⊢ WellFormedAction action

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
action : Action (DefaultClause (cnf.numLiterals + 1)) (PosFin (cnf.numLiterals + 1))
h :
  ∃ a,
    a ∈ lratProof.toList ∧
      (match intActionToDefaultClauseAction (cnf.numLiterals + 1) a 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) =
        some action
⊢ WellFormedAction action

Tactic:
rcases h with ⟨WellFormedActions, _, h2⟩

Result:
case intro.intro
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
h2 :
  (match intActionToDefaultClauseAction (cnf.numLiterals + 1) WellFormedActions 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) =
    some action
⊢ WellFormedAction action