-- 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:
case intro.intro.h_5
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)
pivot✝ : Literal (PosFin (cnf.numLiterals + 1))
rupHints✝ : Array Nat
ratHints✝ : Array (Nat × Array Nat)
heq✝ :
  intActionToDefaultClauseAction (cnf.numLiterals + 1) WellFormedActions =
    some (Action.addRat id✝ c✝ pivot✝ rupHints✝ ratHints✝)
h2 : pivot✝ ∈ Clause.toList c✝ ∧ Action.addRat id✝ c✝ pivot✝ rupHints✝ ratHints✝ = action
⊢ WellFormedAction action

Tactic:
rcases h2 with ⟨hleft, hright⟩

Result:
case intro.intro.h_5.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
actOpt✝ : Option (DefaultClauseAction (cnf.numLiterals + 1))
id✝ : Nat
c✝ : DefaultClause (cnf.numLiterals + 1)
pivot✝ : Literal (PosFin (cnf.numLiterals + 1))
rupHints✝ : Array Nat
ratHints✝ : Array (Nat × Array Nat)
heq✝ :
  intActionToDefaultClauseAction (cnf.numLiterals + 1) WellFormedActions =
    some (Action.addRat id✝ c✝ pivot✝ rupHints✝ ratHints✝)
hleft : pivot✝ ∈ Clause.toList c✝
hright : Action.addRat id✝ c✝ pivot✝ rupHints✝ ratHints✝ = action
⊢ WellFormedAction action

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

Tactic:
simp [← h2, WellFormedAction]

Result:
no goals

Proof state:
case intro.intro.h_5
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)
pivot✝ : Literal (PosFin (cnf.numLiterals + 1))
rupHints✝ : Array Nat
ratHints✝ : Array (Nat × Array Nat)
heq✝ :
  intActionToDefaultClauseAction (cnf.numLiterals + 1) WellFormedActions =
    some (Action.addRat id✝ c✝ pivot✝ rupHints✝ ratHints✝)
h2 : (if pivot✝ ∈ Clause.toList c✝ then some (Action.addRat id✝ c✝ pivot✝ rupHints✝ ratHints✝) else none) = some action
⊢ WellFormedAction action

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

Result:
case intro.intro.h_5
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)
pivot✝ : Literal (PosFin (cnf.numLiterals + 1))
rupHints✝ : Array Nat
ratHints✝ : Array (Nat × Array Nat)
heq✝ :
  intActionToDefaultClauseAction (cnf.numLiterals + 1) WellFormedActions =
    some (Action.addRat id✝ c✝ pivot✝ rupHints✝ ratHints✝)
h2 : pivot✝ ∈ Clause.toList c✝ ∧ Action.addRat id✝ c✝ pivot✝ rupHints✝ ratHints✝ = action
⊢ WellFormedAction action