-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean
theorem addRatCaseSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ)
    (f_readyForRupAdd : ReadyForRupAdd f) (f_readyForRatAdd : ReadyForRatAdd f) (c : β)
    (pivot : Literal α) (f' : σ) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat))
    (pivot_limplies_c : Limplies α pivot c) (heq : performRatAdd f c pivot rupHints ratHints = (f', true))
    (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)
    (f'_success : lratChecker f' 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
c : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
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
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
⊢ Unsatisfiable α f

Tactic:
have f'_readyForRupAdd : ReadyForRupAdd f' := by
  rw [f'_def]
  exact readyForRupAdd_insert f c 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
c : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
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
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : ReadyForRupAdd f'
⊢ 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
c : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : ReadyForRupAdd f'
f'_readyForRatAdd : ReadyForRatAdd f'
ih : Unsatisfiable α f'
f_equisat_f' : Equisat α f f'
p : α → Bool
pf : p ⊨ f
⊢ False

Tactic:
rw [Equisat] at f_equisat_f'

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
c : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : ReadyForRupAdd f'
f'_readyForRatAdd : ReadyForRatAdd f'
ih : Unsatisfiable α f'
f_equisat_f' : Unsatisfiable α f ↔ Unsatisfiable α f'
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
c : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : Limplies α pivot c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
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
f'_success : lratChecker f' restPrf = success
⊢ Unsatisfiable α f

Tactic:
rw [limplies_iff_mem] at pivot_limplies_c

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
c : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
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
f'_success : lratChecker f' 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
c : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : ReadyForRupAdd f'
f'_readyForRatAdd : ReadyForRatAdd f'
ih : Unsatisfiable α f'
⊢ Unsatisfiable α f

Tactic:
have f_equisat_f' : Equisat α f f' := ratAdd_sound f c pivot rupHints ratHints f' f_readyForRatAdd pivot_limplies_c heq

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
c : β
pivot : Literal α
f' : σ
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
pivot_limplies_c : pivot ∈ Clause.toList c
heq : performRatAdd f c pivot rupHints ratHints = (f', true)
restPrf : List (Action β α)
restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a
f'_success : lratChecker f' restPrf = success
f'_def : f' = Formula.insert f c
f'_readyForRupAdd : ReadyForRupAdd f'
f'_readyForRatAdd : ReadyForRatAdd f'
ih : Unsatisfiable α f'
f_equisat_f' : Equisat α f f'
⊢ Unsatisfiable α f