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

Proof state:
case a.inl.h
α : Type u_1
a1 a2 : α → Bool
i : Literal α
c : List (Literal α)
ih : (∀ (i : α), Mem i c → a1 i = a2 i) → eval a1 c = eval a2 c
hw : ∀ (i_1 : α), Mem i_1 (i :: c) → a1 i_1 = a2 i_1
j : α
h : (j, false) ∈ c
⊢ (j, false) ∈ i :: c

Tactic:
apply List.mem_cons_of_mem _ h

Result:
no goals

Proof state:
α : Type u_1
a1 a2 : α → Bool
i : Literal α
c : List (Literal α)
ih : (∀ (i : α), Mem i c → a1 i = a2 i) → eval a1 c = eval a2 c
hw : ∀ (i_1 : α), Mem i_1 (i :: c) → a1 i_1 = a2 i_1
⊢ (a1 i.fst == i.snd || eval a1 c) = (a2 i.fst == i.snd || eval a2 c)

Tactic:
rw [ih, hw]

Result:
case a
α : Type u_1
a1 a2 : α → Bool
i : Literal α
c : List (Literal α)
ih : (∀ (i : α), Mem i c → a1 i = a2 i) → eval a1 c = eval a2 c
hw : ∀ (i_1 : α), Mem i_1 (i :: c) → a1 i_1 = a2 i_1
⊢ Mem i.fst (i :: c)

α : Type u_1
a1 a2 : α → Bool
i : Literal α
c : List (Literal α)
ih : (∀ (i : α), Mem i c → a1 i = a2 i) → eval a1 c = eval a2 c
hw : ∀ (i_1 : α), Mem i_1 (i :: c) → a1 i_1 = a2 i_1
⊢ ∀ (i : α), Mem i c → a1 i = a2 i

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

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

Tactic:
case nil => rfl

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

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

Tactic:
rcases h with h | h

Result:
case a.inl
α : Type u_1
a1 a2 : α → Bool
i : Literal α
c : List (Literal α)
ih : (∀ (i : α), Mem i c → a1 i = a2 i) → eval a1 c = eval a2 c
hw : ∀ (i_1 : α), Mem i_1 (i :: c) → a1 i_1 = a2 i_1
j : α
h : (j, false) ∈ c
⊢ Mem j (i :: c)

case a.inr
α : Type u_1
a1 a2 : α → Bool
i : Literal α
c : List (Literal α)
ih : (∀ (i : α), Mem i c → a1 i = a2 i) → eval a1 c = eval a2 c
hw : ∀ (i_1 : α), Mem i_1 (i :: c) → a1 i_1 = a2 i_1
j : α
h : (j, true) ∈ c
⊢ Mem j (i :: c)

Proof state:
case a.inr
α : Type u_1
a1 a2 : α → Bool
i : Literal α
c : List (Literal α)
ih : (∀ (i : α), Mem i c → a1 i = a2 i) → eval a1 c = eval a2 c
hw : ∀ (i_1 : α), Mem i_1 (i :: c) → a1 i_1 = a2 i_1
j : α
h : (j, true) ∈ c
⊢ Mem j (i :: c)

Tactic:
right

Result:
case a.inr.h
α : Type u_1
a1 a2 : α → Bool
i : Literal α
c : List (Literal α)
ih : (∀ (i : α), Mem i c → a1 i = a2 i) → eval a1 c = eval a2 c
hw : ∀ (i_1 : α), Mem i_1 (i :: c) → a1 i_1 = a2 i_1
j : α
h : (j, true) ∈ c
⊢ (j, true) ∈ i :: c

Proof state:
α : Type u_1
a1 a2 : α → Bool
i : Literal α
c : List (Literal α)
ih : (∀ (i : α), Mem i c → a1 i = a2 i) → eval a1 c = eval a2 c
hw : ∀ (i_1 : α), Mem i_1 (i :: c) → a1 i_1 = a2 i_1
⊢ eval a1 (i :: c) = eval a2 (i :: c)

Tactic:
simp only [eval_cons]

Result:
α : Type u_1
a1 a2 : α → Bool
i : Literal α
c : List (Literal α)
ih : (∀ (i : α), Mem i c → a1 i = a2 i) → eval a1 c = eval a2 c
hw : ∀ (i_1 : α), Mem i_1 (i :: c) → a1 i_1 = a2 i_1
⊢ (a1 i.fst == i.snd || eval a1 c) = (a2 i.fst == i.snd || eval a2 c)

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

Tactic:
induction c

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

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

Proof state:
case a.inr.h
α : Type u_1
a1 a2 : α → Bool
i : Literal α
c : List (Literal α)
ih : (∀ (i : α), Mem i c → a1 i = a2 i) → eval a1 c = eval a2 c
hw : ∀ (i_1 : α), Mem i_1 (i :: c) → a1 i_1 = a2 i_1
j : α
h : (j, true) ∈ c
⊢ (j, true) ∈ i :: c

Tactic:
apply List.mem_cons_of_mem _ h

Result:
no goals

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

Tactic:
apply hw

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

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

Tactic:
rfl

Result:
no goals

Proof state:
case a.inl
α : Type u_1
a1 a2 : α → Bool
i : Literal α
c : List (Literal α)
ih : (∀ (i : α), Mem i c → a1 i = a2 i) → eval a1 c = eval a2 c
hw : ∀ (i_1 : α), Mem i_1 (i :: c) → a1 i_1 = a2 i_1
j : α
h : (j, false) ∈ c
⊢ Mem j (i :: c)

Tactic:
left

Result:
case a.inl.h
α : Type u_1
a1 a2 : α → Bool
i : Literal α
c : List (Literal α)
ih : (∀ (i : α), Mem i c → a1 i = a2 i) → eval a1 c = eval a2 c
hw : ∀ (i_1 : α), Mem i_1 (i :: c) → a1 i_1 = a2 i_1
j : α
h : (j, false) ∈ c
⊢ (j, false) ∈ i :: c

Proof state:
case a
α : Type u_1
a1 a2 : α → Bool
i : Literal α
c : List (Literal α)
ih : (∀ (i : α), Mem i c → a1 i = a2 i) → eval a1 c = eval a2 c
hw : ∀ (i_1 : α), Mem i_1 (i :: c) → a1 i_1 = a2 i_1
⊢ Mem i.fst (i :: c)

Tactic:
rcases i with ⟨b, (_|_)⟩ <;> simp [Mem]

Result:
no goals

Proof state:
α : Type u_1
a1 a2 : α → Bool
i : Literal α
c : List (Literal α)
ih : (∀ (i : α), Mem i c → a1 i = a2 i) → eval a1 c = eval a2 c
hw : ∀ (i_1 : α), Mem i_1 (i :: c) → a1 i_1 = a2 i_1
⊢ ∀ (i : α), Mem i c → a1 i = a2 i

Tactic:
intro j h

Result:
α : Type u_1
a1 a2 : α → Bool
i : Literal α
c : List (Literal α)
ih : (∀ (i : α), Mem i c → a1 i = a2 i) → eval a1 c = eval a2 c
hw : ∀ (i_1 : α), Mem i_1 (i :: c) → a1 i_1 = a2 i_1
j : α
h : Mem j c
⊢ a1 j = a2 j