-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/LRATCheckerSound.lean
theorem addEmptyCaseSound [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ)
    (f_readyForRupAdd : ReadyForRupAdd f) (rupHints : Array Nat)
    (rupAddSuccess : (Formula.performRupAdd f Clause.empty rupHints).snd = true) :
    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
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
f_liff_f' : performRupAdd f empty rupHints = (f', true) → Liff α f f'
⊢ Unsatisfiable α f

Tactic:
rw [← rupAddSuccess] at f_liff_f'

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
f_liff_f' : performRupAdd f empty rupHints = (f', (performRupAdd f empty rupHints).snd) → Liff α f 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
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
⊢ Unsatisfiable α f

Tactic:
have f'_def := rupAdd_result f empty rupHints f' 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
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : performRupAdd f empty rupHints = (f', true) → f' = Formula.insert f empty
⊢ 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
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
⊢ Unsatisfiable α f

Tactic:
let f' := (performRupAdd f empty rupHints).1

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
⊢ 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
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
p : α → Bool
pf : ∀ (c : β), c ∈ Formula.toList (Formula.insert f empty) → p ⊨ c
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
⊢ False

Tactic:
have empty_in_f' : empty ∈ toList (Formula.insert f empty) := by
  rw [Formula.insert_iff]
  exact Or.inl rfl

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
p : α → Bool
pf : ∀ (c : β), c ∈ Formula.toList (Formula.insert f empty) → p ⊨ c
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
empty_in_f' : empty ∈ Formula.toList (Formula.insert f empty)
⊢ 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
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
⊢ Unsatisfiable α f

Tactic:
have f_liff_f' := rupAdd_sound f empty rupHints f' 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
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
f_liff_f' : performRupAdd f empty rupHints = (f', true) → Liff α f 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
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
f_liff_f' : performRupAdd f empty rupHints = (f', (performRupAdd f empty rupHints).snd) → Liff α f f'
⊢ Unsatisfiable α f

Tactic:
specialize f_liff_f' rfl

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
f_liff_f' : Liff α f 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
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
f_liff_f' : Liff α f (Formula.insert f empty)
p : α → Bool
pf : p ⊨ f
⊢ False

Tactic:
specialize f_liff_f' p

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
p : α → Bool
pf : p ⊨ f
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
⊢ 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
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
p : α → Bool
pf : p ⊨ f
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
⊢ False

Tactic:
rw [f_liff_f', sat_iff_forall] at pf

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝³ : DecidableEq α
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
f : σ
f_readyForRupAdd : ReadyForRupAdd f
rupHints : Array Nat
rupAddSuccess : (performRupAdd f empty rupHints).snd = true
f' : σ := (performRupAdd f empty rupHints).fst
f'_def : f' = Formula.insert f empty
p : α → Bool
pf : ∀ (c : β), c ∈ Formula.toList (Formula.insert f empty) → p ⊨ c
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
⊢ False