-- 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
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

Tactic:
specialize pf empty empty_in_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
p : α → Bool
f_liff_f' : p ⊨ f ↔ p ⊨ Formula.insert f empty
empty_in_f' : empty ∈ Formula.toList (Formula.insert f empty)
pf : p ⊨ 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
f_liff_f' : Liff α f (Formula.insert f empty)
⊢ 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
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

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 : performRupAdd f empty rupHints = (f', true) → f' = Formula.insert f empty
⊢ Unsatisfiable α f

Tactic:
rw [← rupAddSuccess] at f'_def

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

Tactic:
specialize f'_def 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
⊢ 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 f'
⊢ Unsatisfiable α f

Tactic:
rw [f'_def] 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' : Liff α 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
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 = empty ∨ empty ∈ Formula.toList f

Tactic:
exact Or.inl rfl

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
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 ∈ Formula.toList (Formula.insert f empty)

Tactic:
rw [Formula.insert_iff]

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 = empty ∨ empty ∈ Formula.toList f