-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean
theorem delCaseSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ)
    (f_readyForRupAdd : ReadyForRupAdd f) (f_readyForRatAdd : ReadyForRatAdd f) (ids : Array Nat)
    (restPrf : List (Action β α))
    (restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a)
    (ih : ∀ (f : σ),
      ReadyForRupAdd f → ReadyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) →
      lratChecker f restPrf = success → Unsatisfiable α f)
    (h : 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 α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
ids : Array Nat
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
h : lratChecker (Formula.delete f ids) restPrf = success
p : α → Bool
pf : p ⊨ f
f_del_readyForRupAdd : ReadyForRupAdd (Formula.delete f ids)
⊢ False

Tactic:
have f_del_readyForRatAdd : ReadyForRatAdd (Formula.delete f ids) := readyForRatAdd_delete f ids f_readyForRatAdd

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
ids : Array Nat
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
h : lratChecker (Formula.delete f ids) restPrf = success
p : α → Bool
pf : p ⊨ f
f_del_readyForRupAdd : ReadyForRupAdd (Formula.delete f ids)
f_del_readyForRatAdd : ReadyForRatAdd (Formula.delete f ids)
⊢ False

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
ids : Array Nat
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
h : lratChecker (Formula.delete f ids) restPrf = success
p : α → Bool
pf : p ⊨ f
f_del_readyForRupAdd : ReadyForRupAdd (Formula.delete f ids)
f_del_readyForRatAdd : ReadyForRatAdd (Formula.delete f ids)
⊢ False

Tactic:
exact ih (delete f ids) f_del_readyForRupAdd f_del_readyForRatAdd restPrfWellFormed h p (limplies_delete p pf)

Result:
no goals

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

Tactic:
intro p pf

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
ids : Array Nat
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
h : lratChecker (Formula.delete f ids) restPrf = success
p : α → Bool
pf : p ⊨ f
⊢ False

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
ids : Array Nat
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
h : lratChecker (Formula.delete f ids) restPrf = success
p : α → Bool
pf : p ⊨ f
⊢ False

Tactic:
have f_del_readyForRupAdd : ReadyForRupAdd (Formula.delete f ids) := readyForRupAdd_delete f ids f_readyForRupAdd

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
f_readyForRatAdd : ReadyForRatAdd f
ids : Array Nat
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
ih :
  ∀ (f : σ),
    ReadyForRupAdd f →
      ReadyForRatAdd f →
        (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = success → Unsatisfiable α f
h : lratChecker (Formula.delete f ids) restPrf = success
p : α → Bool
pf : p ⊨ f
f_del_readyForRupAdd : ReadyForRupAdd (Formula.delete f ids)
⊢ False