-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Basic.lean
theorem eval_congr (a1 a2 : α → Bool) (f : CNF α) (hw : ∀ v, Mem v f → a1 v = a2 v) :
    eval a1 f = eval a2 f

Proof state:
α : Type u_1
a1 a2 : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (v : α), Mem v x → a1 v = a2 v) → eval a1 x = eval a2 x
hw : ∀ (v : α), Mem v (c :: x) → a1 v = a2 v
⊢ eval a1 (c :: x) = eval a2 (c :: x)

Tactic:
simp only [eval_cons]

Result:
α : Type u_1
a1 a2 : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (v : α), Mem v x → a1 v = a2 v) → eval a1 x = eval a2 x
hw : ∀ (v : α), Mem v (c :: x) → a1 v = a2 v
⊢ (Clause.eval a1 c && eval a1 x) = (Clause.eval a2 c && eval a2 x)

Proof state:
α : Type u_1
a1 a2 : α → Bool
hw : ∀ (v : α), Mem v [] → a1 v = a2 v
⊢ eval a1 [] = eval a2 []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
a1 a2 : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (v : α), Mem v x → a1 v = a2 v) → eval a1 x = eval a2 x
hw : ∀ (v : α), Mem v (c :: x) → a1 v = a2 v
i : α
h : Mem i x
⊢ a1 i = a2 i

Tactic:
apply hw

Result:
case a
α : Type u_1
a1 a2 : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (v : α), Mem v x → a1 v = a2 v) → eval a1 x = eval a2 x
hw : ∀ (v : α), Mem v (c :: x) → a1 v = a2 v
i : α
h : Mem i x
⊢ Mem i (c :: x)

Proof state:
case nil
α : Type u_1
a1 a2 : α → Bool
hw : ∀ (v : α), Mem v [] → a1 v = a2 v
⊢ eval a1 [] = eval a2 []

case cons
α : Type u_1
a1 a2 : α → Bool
head✝ : Clause α
tail✝ : List (Clause α)
tail_ih✝ : (∀ (v : α), Mem v tail✝ → a1 v = a2 v) → eval a1 tail✝ = eval a2 tail✝
hw : ∀ (v : α), Mem v (head✝ :: tail✝) → a1 v = a2 v
⊢ eval a1 (head✝ :: tail✝) = eval a2 (head✝ :: tail✝)

Tactic:
case nil => rfl

Result:
case cons
α : Type u_1
a1 a2 : α → Bool
head✝ : Clause α
tail✝ : List (Clause α)
tail_ih✝ : (∀ (v : α), Mem v tail✝ → a1 v = a2 v) → eval a1 tail✝ = eval a2 tail✝
hw : ∀ (v : α), Mem v (head✝ :: tail✝) → a1 v = a2 v
⊢ eval a1 (head✝ :: tail✝) = eval a2 (head✝ :: tail✝)

Proof state:
case a
α : Type u_1
a1 a2 : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (v : α), Mem v x → a1 v = a2 v) → eval a1 x = eval a2 x
hw : ∀ (v : α), Mem v (c :: x) → a1 v = a2 v
i : α
h : Mem i x
⊢ Mem i (c :: x)

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
a1 a2 : α → Bool
f : CNF α
hw : ∀ (v : α), Mem v f → a1 v = a2 v
⊢ eval a1 f = eval a2 f

Tactic:
induction f

Result:
case nil
α : Type u_1
a1 a2 : α → Bool
hw : ∀ (v : α), Mem v [] → a1 v = a2 v
⊢ eval a1 [] = eval a2 []

case cons
α : Type u_1
a1 a2 : α → Bool
head✝ : Clause α
tail✝ : List (Clause α)
tail_ih✝ : (∀ (v : α), Mem v tail✝ → a1 v = a2 v) → eval a1 tail✝ = eval a2 tail✝
hw : ∀ (v : α), Mem v (head✝ :: tail✝) → a1 v = a2 v
⊢ eval a1 (head✝ :: tail✝) = eval a2 (head✝ :: tail✝)

Proof state:
α : Type u_1
a1 a2 : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (v : α), Mem v x → a1 v = a2 v) → eval a1 x = eval a2 x
hw : ∀ (v : α), Mem v (c :: x) → a1 v = a2 v
⊢ ∀ (v : α), Mem v x → a1 v = a2 v

Tactic:
intro i h

Result:
α : Type u_1
a1 a2 : α → Bool
c : Clause α
x : List (Clause α)
ih : (∀ (v : α), Mem v x → a1 v = a2 v) → eval a1 x = eval a2 x
hw : ∀ (v : α), Mem v (c :: x) → a1 v = a2 v
i : α
h : Mem i x
⊢ a1 i = a2 i