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

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

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

State before:
case mk
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
data : List (Clause L)
h : x ∈ PropFun.semVars (toPropFun { data := data })
⊢ ∃ C ∈ { data := data }, x ∈ PropFun.semVars (Clause.toPropFun C)
Tactic:
simp [Array.mem_def]
State after:
case mk
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
data : List (Clause L)
h : x ∈ PropFun.semVars (toPropFun { data := data })
⊢ ∃ C ∈ data, x ∈ PropFun.semVars (Clause.toPropFun C)

State before:
case mk
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
data : List (Clause L)
h : x ∈ PropFun.semVars (toPropFun { data := data })
⊢ ∃ C ∈ data, x ∈ PropFun.semVars (Clause.toPropFun C)
Tactic:
induction data <;> simp_all [toPropFun, PropFun.all]
State after:
case mk.cons
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
head✝ : Clause L
tail✝ : List (Clause L)
tail_ih✝ :
  x ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝)) →
    ∃ C ∈ tail✝, x ∈ PropFun.semVars (Clause.toPropFun C)
h : x ∈ PropFun.semVars (Clause.toPropFun head✝ ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝))
⊢ x ∈ PropFun.semVars (Clause.toPropFun head✝) ∨ ∃ a ∈ tail✝, x ∈ PropFun.semVars (Clause.toPropFun a)

State before:
case mk.cons
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
head✝ : Clause L
tail✝ : List (Clause L)
tail_ih✝ :
  x ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝)) →
    ∃ C ∈ tail✝, x ∈ PropFun.semVars (Clause.toPropFun C)
h : x ∈ PropFun.semVars (Clause.toPropFun head✝ ⊓ List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝))
⊢ x ∈ PropFun.semVars (Clause.toPropFun head✝) ∨ ∃ a ∈ tail✝, x ∈ PropFun.semVars (Clause.toPropFun a)
Tactic:
replace h := PropFun.semVars_conj _ _ h
State after:
case mk.cons
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
head✝ : Clause L
tail✝ : List (Clause L)
tail_ih✝ :
  x ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝)) →
    ∃ C ∈ tail✝, x ∈ PropFun.semVars (Clause.toPropFun C)
h :
  x ∈
    PropFun.semVars (Clause.toPropFun head✝) ∪
      PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝))
⊢ x ∈ PropFun.semVars (Clause.toPropFun head✝) ∨ ∃ a ∈ tail✝, x ∈ PropFun.semVars (Clause.toPropFun a)

State before:
case mk.cons
L : Type u
ν : Type v
inst✝² : LitVar L ν
inst✝¹ inst✝ : DecidableEq ν
x : ν
head✝ : Clause L
tail✝ : List (Clause L)
tail_ih✝ :
  x ∈ PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝)) →
    ∃ C ∈ tail✝, x ∈ PropFun.semVars (Clause.toPropFun C)
h :
  x ∈
    PropFun.semVars (Clause.toPropFun head✝) ∪
      PropFun.semVars (List.foldr (fun x x_1 => x ⊓ x_1) ⊤ (List.map Clause.toPropFun tail✝))
⊢ x ∈ PropFun.semVars (Clause.toPropFun head✝) ∨ ∃ a ∈ tail✝, x ∈ PropFun.semVars (Clause.toPropFun a)
Tactic:
aesop
State after:
no goals