-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean
theorem lratCheckerSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ)
    (f_readyForRupAdd : ReadyForRupAdd f) (f_readyForRatAdd : ReadyForRatAdd f)
    (prf : List (Action β α)) (prfWellFormed : ∀ a : Action β α, a ∈ prf → WellFormedAction a) :
    lratChecker f prf = success → Unsatisfiable α f

Proof state:
case intro
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
action : Action β α
restPrf : List (Action β α)
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
actionWellFormed : WellFormedAction action
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
⊢ (match action :: restPrf with
      | [] => outOfProof
      | Action.addEmpty id rupHints :: tail =>
        match performRupAdd f empty rupHints with
        | (fst, checkSuccess) => if checkSuccess = true then success else rupFailure
      | Action.addRup id c rupHints :: restPrf =>
        match performRupAdd f c rupHints with
        | (f, checkSuccess) => if checkSuccess = true then lratChecker f restPrf else rupFailure
      | Action.addRat id c pivot rupHints ratHints :: restPrf =>
        match performRatAdd f c pivot rupHints ratHints with
        | (f, checkSuccess) => if checkSuccess = true then lratChecker f restPrf else rupFailure
      | Action.del ids :: restPrf => lratChecker (Formula.delete f ids) restPrf) =
      success →
    Unsatisfiable α f

Tactic:
split

Result:
case intro.h_1
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
action : Action β α
restPrf : List (Action β α)
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
actionWellFormed : WellFormedAction action
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
prf✝ : List (Action β α)
heq✝ : action :: restPrf = []
⊢ outOfProof = success → Unsatisfiable α f

case intro.h_2
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
action : Action β α
restPrf : List (Action β α)
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
actionWellFormed : WellFormedAction action
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
prf✝ : List (Action β α)
id✝ : Nat
rupHints✝ : Array Nat
tail✝ : List (Action β α)
heq✝ : action :: restPrf = Action.addEmpty id✝ rupHints✝ :: tail✝
⊢ (match performRupAdd f empty rupHints✝ with
      | (fst, checkSuccess) => if checkSuccess = true then success else rupFailure) =
      success →
    Unsatisfiable α f

case intro.h_3
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
action : Action β α
restPrf : List (Action β α)
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
actionWellFormed : WellFormedAction action
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
prf✝ : List (Action β α)
id✝ : Nat
c✝ : β
rupHints✝ : Array Nat
restPrf✝ : List (Action β α)
heq✝ : action :: restPrf = Action.addRup id✝ c✝ rupHints✝ :: restPrf✝
⊢ (match performRupAdd f c✝ rupHints✝ with
      | (f, checkSuccess) => if checkSuccess = true then lratChecker f restPrf✝ else rupFailure) =
      success →
    Unsatisfiable α f

case intro.h_4
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
action : Action β α
restPrf : List (Action β α)
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
actionWellFormed : WellFormedAction action
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
prf✝ : List (Action β α)
id✝ : Nat
c✝ : β
pivot✝ : Literal α
rupHints✝ : Array Nat
ratHints✝ : Array (Nat × Array Nat)
restPrf✝ : List (Action β α)
heq✝ : action :: restPrf = Action.addRat id✝ c✝ pivot✝ rupHints✝ ratHints✝ :: restPrf✝
⊢ (match performRatAdd f c✝ pivot✝ rupHints✝ ratHints✝ with
      | (f, checkSuccess) => if checkSuccess = true then lratChecker f restPrf✝ else rupFailure) =
      success →
    Unsatisfiable α f

case intro.h_5
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
action : Action β α
restPrf : List (Action β α)
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
actionWellFormed : WellFormedAction action
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
prf✝ : List (Action β α)
ids✝ : Array Nat
restPrf✝ : List (Action β α)
heq✝ : action :: restPrf = Action.del ids✝ :: restPrf✝
⊢ lratChecker (Formula.delete f ids✝) restPrf✝ = success → Unsatisfiable α f

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
action : Action β α
restPrf : List (Action β α)
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
prfWellFormed : WellFormedAction action ∧ ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
⊢ lratChecker f (action :: restPrf) = success → Unsatisfiable α f

Tactic:
rcases prfWellFormed with ⟨actionWellFormed, restPrfWellFormed⟩

Result:
case intro
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
action : Action β α
restPrf : List (Action β α)
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
actionWellFormed : WellFormedAction action
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
⊢ lratChecker f (action :: restPrf) = success → Unsatisfiable α f