Theorem: LeanSAT.Clause.toPropFun_or (LeanSAT/Data/Cnf.lean)

State before:
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
⊢ toPropFun (or c1 c2) = toPropFun c1 ⊔ toPropFun c2
Tactic:
ext τ
State after:
case a
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (or c1 c2) ↔ τ ⊨ toPropFun c1 ⊔ toPropFun c2

State before:
case a
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (or c1 c2) ↔ τ ⊨ toPropFun c1 ⊔ toPropFun c2
Tactic:
simp [or, satisfies_iff]
State after:
case a
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ (∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l) ↔
    (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l

State before:
case a
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ (∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l) ↔
    (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l
Tactic:
apply Iff.intro
State after:
case a.mp
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ (∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l) →
    (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l

case a.mpr
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ ((∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l) →
    ∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l

State before:
case a.mp
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ (∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l) →
    (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l
Tactic:
rintro ⟨l,h1,h2⟩
State after:
case a.mp.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c1 ∨ l ∈ c2
h2 : τ ⊨ LitVar.toPropFun l
⊢ (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l

State before:
case a.mp.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c1 ∨ l ∈ c2
h2 : τ ⊨ LitVar.toPropFun l
⊢ (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l
Tactic:
cases h1
State after:
case a.mp.intro.intro.inl
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h2 : τ ⊨ LitVar.toPropFun l
h✝ : l ∈ c1
⊢ (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l

case a.mp.intro.intro.inr
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h2 : τ ⊨ LitVar.toPropFun l
h✝ : l ∈ c2
⊢ (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l

State before:
case a.mp.intro.intro.inl
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h2 : τ ⊨ LitVar.toPropFun l
h✝ : l ∈ c1
⊢ (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l
Tactic:
refine Or.inl ⟨l,?_⟩
State after:
case a.mp.intro.intro.inl
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h2 : τ ⊨ LitVar.toPropFun l
h✝ : l ∈ c1
⊢ l ∈ c1 ∧ τ ⊨ LitVar.toPropFun l

State before:
case a.mp.intro.intro.inl
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h2 : τ ⊨ LitVar.toPropFun l
h✝ : l ∈ c1
⊢ l ∈ c1 ∧ τ ⊨ LitVar.toPropFun l
Tactic:
simp [*]
State after:
no goals

State before:
case a.mp.intro.intro.inr
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h2 : τ ⊨ LitVar.toPropFun l
h✝ : l ∈ c2
⊢ (∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l
Tactic:
refine Or.inr ⟨l,?_⟩
State after:
case a.mp.intro.intro.inr
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h2 : τ ⊨ LitVar.toPropFun l
h✝ : l ∈ c2
⊢ l ∈ c2 ∧ τ ⊨ LitVar.toPropFun l

State before:
case a.mp.intro.intro.inr
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h2 : τ ⊨ LitVar.toPropFun l
h✝ : l ∈ c2
⊢ l ∈ c2 ∧ τ ⊨ LitVar.toPropFun l
Tactic:
simp [*]
State after:
no goals

State before:
case a.mpr
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
⊢ ((∃ l ∈ c1, τ ⊨ LitVar.toPropFun l) ∨ ∃ l ∈ c2, τ ⊨ LitVar.toPropFun l) →
    ∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l
Tactic:
rintro (⟨l,h1,h2⟩|⟨l,h1,h2⟩)
State after:
case a.mpr.inl.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c1
h2 : τ ⊨ LitVar.toPropFun l
⊢ ∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l

case a.mpr.inr.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c2
h2 : τ ⊨ LitVar.toPropFun l
⊢ ∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l

State before:
case a.mpr.inl.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c1
h2 : τ ⊨ LitVar.toPropFun l
⊢ ∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l
Tactic:
refine ⟨l,?_⟩
State after:
case a.mpr.inl.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c1
h2 : τ ⊨ LitVar.toPropFun l
⊢ (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l

State before:
case a.mpr.inl.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c1
h2 : τ ⊨ LitVar.toPropFun l
⊢ (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l
Tactic:
simp [*]
State after:
no goals

State before:
case a.mpr.inr.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c2
h2 : τ ⊨ LitVar.toPropFun l
⊢ ∃ l, (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l
Tactic:
refine ⟨l,?_⟩
State after:
case a.mpr.inr.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c2
h2 : τ ⊨ LitVar.toPropFun l
⊢ (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l

State before:
case a.mpr.inr.intro.intro
L : Type u
ν : Type v
inst✝ : LitVar L ν
c1 c2 : Clause L
τ : PropAssignment ν
l : L
h1 : l ∈ c2
h2 : τ ⊨ LitVar.toPropFun l
⊢ (l ∈ c1 ∨ l ∈ c2) ∧ τ ⊨ LitVar.toPropFun l
Tactic:
simp [*]
State after:
no goals