-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Basic.lean
theorem mem_append {v : α} {f1 f2 : CNF α} : Mem v (f1 ++ f2) ↔ Mem v f1 ∨ Mem v f2

Proof state:
case mp.intro.intro.inl.h
α : Type u_1
v : α
f1 f2 : CNF α
c : Clause α
mc : Clause.Mem v c
mf1 : c ∈ f1
⊢ ∃ c, c ∈ f1 ∧ Clause.Mem v c

Tactic:
exact ⟨c, mf1, mc⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
v : α
f1 f2 : CNF α
⊢ (∃ c, (c ∈ f1 ∨ c ∈ f2) ∧ Clause.Mem v c) → (∃ c, c ∈ f1 ∧ Clause.Mem v c) ∨ ∃ c, c ∈ f2 ∧ Clause.Mem v c

Tactic:
rintro ⟨c, (mf1 | mf2), mc⟩

Result:
case mp.intro.intro.inl
α : Type u_1
v : α
f1 f2 : CNF α
c : Clause α
mc : Clause.Mem v c
mf1 : c ∈ f1
⊢ (∃ c, c ∈ f1 ∧ Clause.Mem v c) ∨ ∃ c, c ∈ f2 ∧ Clause.Mem v c

case mp.intro.intro.inr
α : Type u_1
v : α
f1 f2 : CNF α
c : Clause α
mc : Clause.Mem v c
mf2 : c ∈ f2
⊢ (∃ c, c ∈ f1 ∧ Clause.Mem v c) ∨ ∃ c, c ∈ f2 ∧ Clause.Mem v c

Proof state:
α : Type u_1
v : α
f1 f2 : CNF α
⊢ (∃ c, (c ∈ f1 ∨ c ∈ f2) ∧ Clause.Mem v c) ↔ (∃ c, c ∈ f1 ∧ Clause.Mem v c) ∨ ∃ c, c ∈ f2 ∧ Clause.Mem v c

Tactic:
constructor

Result:
case mp
α : Type u_1
v : α
f1 f2 : CNF α
⊢ (∃ c, (c ∈ f1 ∨ c ∈ f2) ∧ Clause.Mem v c) → (∃ c, c ∈ f1 ∧ Clause.Mem v c) ∨ ∃ c, c ∈ f2 ∧ Clause.Mem v c

case mpr
α : Type u_1
v : α
f1 f2 : CNF α
⊢ ((∃ c, c ∈ f1 ∧ Clause.Mem v c) ∨ ∃ c, c ∈ f2 ∧ Clause.Mem v c) → ∃ c, (c ∈ f1 ∨ c ∈ f2) ∧ Clause.Mem v c

Proof state:
case mp.intro.intro.inr
α : Type u_1
v : α
f1 f2 : CNF α
c : Clause α
mc : Clause.Mem v c
mf2 : c ∈ f2
⊢ (∃ c, c ∈ f1 ∧ Clause.Mem v c) ∨ ∃ c, c ∈ f2 ∧ Clause.Mem v c

Tactic:
right

Result:
case mp.intro.intro.inr.h
α : Type u_1
v : α
f1 f2 : CNF α
c : Clause α
mc : Clause.Mem v c
mf2 : c ∈ f2
⊢ ∃ c, c ∈ f2 ∧ Clause.Mem v c

Proof state:
case mpr
α : Type u_1
v : α
f1 f2 : CNF α
⊢ ((∃ c, c ∈ f1 ∧ Clause.Mem v c) ∨ ∃ c, c ∈ f2 ∧ Clause.Mem v c) → ∃ c, (c ∈ f1 ∨ c ∈ f2) ∧ Clause.Mem v c

Tactic:
rintro (⟨c, mf1, mc⟩ | ⟨c, mf2, mc⟩)

Result:
case mpr.inl.intro.intro
α : Type u_1
v : α
f1 f2 : CNF α
c : Clause α
mf1 : c ∈ f1
mc : Clause.Mem v c
⊢ ∃ c, (c ∈ f1 ∨ c ∈ f2) ∧ Clause.Mem v c

case mpr.inr.intro.intro
α : Type u_1
v : α
f1 f2 : CNF α
c : Clause α
mf2 : c ∈ f2
mc : Clause.Mem v c
⊢ ∃ c, (c ∈ f1 ∨ c ∈ f2) ∧ Clause.Mem v c

Proof state:
case mpr.inl.intro.intro
α : Type u_1
v : α
f1 f2 : CNF α
c : Clause α
mf1 : c ∈ f1
mc : Clause.Mem v c
⊢ ∃ c, (c ∈ f1 ∨ c ∈ f2) ∧ Clause.Mem v c

Tactic:
exact ⟨c, Or.inl mf1, mc⟩

Result:
no goals

Proof state:
α : Type u_1
v : α
f1 f2 : CNF α
⊢ Mem v (f1 ++ f2) ↔ Mem v f1 ∨ Mem v f2

Tactic:
simp [Mem, List.mem_append]

Result:
α : Type u_1
v : α
f1 f2 : CNF α
⊢ (∃ c, (c ∈ f1 ∨ c ∈ f2) ∧ Clause.Mem v c) ↔ (∃ c, c ∈ f1 ∧ Clause.Mem v c) ∨ ∃ c, c ∈ f2 ∧ Clause.Mem v c

Proof state:
case mp.intro.intro.inl
α : Type u_1
v : α
f1 f2 : CNF α
c : Clause α
mc : Clause.Mem v c
mf1 : c ∈ f1
⊢ (∃ c, c ∈ f1 ∧ Clause.Mem v c) ∨ ∃ c, c ∈ f2 ∧ Clause.Mem v c

Tactic:
left

Result:
case mp.intro.intro.inl.h
α : Type u_1
v : α
f1 f2 : CNF α
c : Clause α
mc : Clause.Mem v c
mf1 : c ∈ f1
⊢ ∃ c, c ∈ f1 ∧ Clause.Mem v c

Proof state:
case mp.intro.intro.inr.h
α : Type u_1
v : α
f1 f2 : CNF α
c : Clause α
mc : Clause.Mem v c
mf2 : c ∈ f2
⊢ ∃ c, c ∈ f2 ∧ Clause.Mem v c

Tactic:
exact ⟨c, mf2, mc⟩

Result:
no goals

Proof state:
case mpr.inr.intro.intro
α : Type u_1
v : α
f1 f2 : CNF α
c : Clause α
mf2 : c ∈ f2
mc : Clause.Mem v c
⊢ ∃ c, (c ∈ f1 ∨ c ∈ f2) ∧ Clause.Mem v c

Tactic:
exact ⟨c, Or.inr mf2, mc⟩

Result:
no goals