-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
theorem limplies_insert [Clause α β] [Entails α σ] [Formula α β σ] {c : β} {f : σ} :
    Limplies α (insert f c) f

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
h : ∀ (x : β), x ∈ toList (insert f c) → p ⊨ x
c' : β
c'_in_f : c' ∈ toList f
c'_in_fc : c' ∈ toList (insert f c)
⊢ p ⊨ c'

Tactic:
exact h c' c'_in_fc

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
c : β
f : σ
⊢ Limplies α (insert f c) f

Tactic:
intro p

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
⊢ p ⊨ insert f c → p ⊨ f

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
h : ∀ (x : β), x ∈ toList (insert f c) → p ⊨ x
c' : β
c'_in_f : c' ∈ toList f
⊢ c' = c ∨ c' ∈ toList f

Tactic:
exact Or.inr c'_in_f

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
h : ∀ (x : β), x ∈ toList (insert f c) → p ⊨ x
c' : β
c'_in_f : c' ∈ toList f
⊢ p ⊨ c'

Tactic:
have c'_in_fc : c' ∈ toList (insert f c) := by
  simp only [insert_iff, Array.toList_toArray, List.mem_singleton]
  exact Or.inr c'_in_f

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
h : ∀ (x : β), x ∈ toList (insert f c) → p ⊨ x
c' : β
c'_in_f : c' ∈ toList f
c'_in_fc : c' ∈ toList (insert f c)
⊢ p ⊨ c'

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
h : ∀ (x : β), x ∈ toList (insert f c) → p ⊨ x
c' : β
c'_in_f : c' ∈ toList f
⊢ c' ∈ toList (insert f c)

Tactic:
simp only [insert_iff, Array.toList_toArray, List.mem_singleton]

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
h : ∀ (x : β), x ∈ toList (insert f c) → p ⊨ x
c' : β
c'_in_f : c' ∈ toList f
⊢ c' = c ∨ c' ∈ toList f

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
⊢ p ⊨ insert f c → p ⊨ f

Tactic:
simp only [formulaEntails_def, List.all_eq_true, decide_eq_true_eq]

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
⊢ (∀ (x : β), x ∈ toList (insert f c) → p ⊨ x) → ∀ (x : β), x ∈ toList f → p ⊨ x

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
⊢ (∀ (x : β), x ∈ toList (insert f c) → p ⊨ x) → ∀ (x : β), x ∈ toList f → p ⊨ x

Tactic:
intro h c' c'_in_f

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Clause α β
inst✝¹ : Entails α σ
inst✝ : Formula α β σ
c : β
f : σ
p : α → Bool
h : ∀ (x : β), x ∈ toList (insert f c) → p ⊨ x
c' : β
c'_in_f : c' ∈ toList f
⊢ p ⊨ c'