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

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
C : Clause L
⊢ x ∈ PropFun.semVars (toPropFun C) → ∃ l ∈ C, LitVar.toVar l = x
Tactic:
intro h
State after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
C : Clause L
h : x ∈ PropFun.semVars (toPropFun C)
⊢ ∃ l ∈ C, LitVar.toVar l = x

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
C : Clause L
h : x ∈ PropFun.semVars (toPropFun C)
⊢ ∃ l ∈ C, LitVar.toVar l = x
Tactic:
rcases C with ⟨data⟩
State after:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
h : x ∈ PropFun.semVars (toPropFun { data := data })
⊢ ∃ l ∈ { data := data }, LitVar.toVar l = x

State before:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
h : x ∈ PropFun.semVars (toPropFun { data := data })
⊢ ∃ l ∈ { data := data }, LitVar.toVar l = x
Tactic:
have ⟨τ,hpos,hneg⟩ := (PropFun.mem_semVars _ _).mp h
State after:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
h : x ∈ PropFun.semVars (toPropFun { data := data })
τ : PropAssignment ν
hpos : τ ⊨ toPropFun { data := data }
hneg : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) (toPropFun { data := data })
⊢ ∃ l ∈ { data := data }, LitVar.toVar l = x

State before:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
h : x ∈ PropFun.semVars (toPropFun { data := data })
τ : PropAssignment ν
hpos : τ ⊨ toPropFun { data := data }
hneg : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) (toPropFun { data := data })
⊢ ∃ l ∈ { data := data }, LitVar.toVar l = x
Tactic:
clear h
State after:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hpos : τ ⊨ toPropFun { data := data }
hneg : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) (toPropFun { data := data })
⊢ ∃ l ∈ { data := data }, LitVar.toVar l = x

State before:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hpos : τ ⊨ toPropFun { data := data }
hneg : (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) (toPropFun { data := data })
⊢ ∃ l ∈ { data := data }, LitVar.toVar l = x
Tactic:
simp_all [toPropFun, Array.mem_def]
State after:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hpos : ∃ a ∈ data, τ ⊨ LitVar.toPropFun a
hneg : ∀ x_1 ∈ data, ¬(PropAssignment.set τ x !τ x) ⊨ LitVar.toPropFun x_1
⊢ ∃ l ∈ data, LitVar.toVar l = x

State before:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hpos : ∃ a ∈ data, τ ⊨ LitVar.toPropFun a
hneg : ∀ x_1 ∈ data, ¬(PropAssignment.set τ x !τ x) ⊨ LitVar.toPropFun x_1
⊢ ∃ l ∈ data, LitVar.toVar l = x
Tactic:
rcases hpos with ⟨l,hl,h⟩
State after:
case mk.intro.intro
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hneg : ∀ x_1 ∈ data, ¬(PropAssignment.set τ x !τ x) ⊨ LitVar.toPropFun x_1
l : L
hl : l ∈ data
h : τ ⊨ LitVar.toPropFun l
⊢ ∃ l ∈ data, LitVar.toVar l = x

State before:
case mk.intro.intro
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hneg : ∀ x_1 ∈ data, ¬(PropAssignment.set τ x !τ x) ⊨ LitVar.toPropFun x_1
l : L
hl : l ∈ data
h : τ ⊨ LitVar.toPropFun l
⊢ ∃ l ∈ data, LitVar.toVar l = x
Tactic:
have := (PropFun.mem_semVars _ _).mpr ⟨τ,h,hneg l hl⟩
State after:
case mk.intro.intro
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hneg : ∀ x_1 ∈ data, ¬(PropAssignment.set τ x !τ x) ⊨ LitVar.toPropFun x_1
l : L
hl : l ∈ data
h : τ ⊨ LitVar.toPropFun l
this : x ∈ PropFun.semVars (LitVar.toPropFun l)
⊢ ∃ l ∈ data, LitVar.toVar l = x

State before:
case mk.intro.intro
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
hneg : ∀ x_1 ∈ data, ¬(PropAssignment.set τ x !τ x) ⊨ LitVar.toPropFun x_1
l : L
hl : l ∈ data
h : τ ⊨ LitVar.toPropFun l
this : x ∈ PropFun.semVars (LitVar.toPropFun l)
⊢ ∃ l ∈ data, LitVar.toVar l = x
Tactic:
clear hneg h
State after:
case mk.intro.intro
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
l : L
hl : l ∈ data
this : x ∈ PropFun.semVars (LitVar.toPropFun l)
⊢ ∃ l ∈ data, LitVar.toVar l = x

State before:
case mk.intro.intro
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
x : ν
data : List L
τ : PropAssignment ν
l : L
hl : l ∈ data
this : x ∈ PropFun.semVars (LitVar.toPropFun l)
⊢ ∃ l ∈ data, LitVar.toVar l = x
Tactic:
aesop
State after:
no goals