Theorem: LeanSAT.Model.PropFun.semVars_var (LeanSAT/Model/PropVars.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
⊢ semVars (var x) = {x}
Tactic:
ext y
State after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ y ∈ semVars (var x) ↔ y ∈ {x}

State before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ y ∈ semVars (var x) ↔ y ∈ {x}
Tactic:
simp only [Finset.mem_singleton, mem_semVars, satisfies_var]
State after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ (∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true) ↔ y = x

State before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ (∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true) ↔ y = x
Tactic:
refine ⟨?mp, ?mpr⟩
State after:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ (∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true) → y = x

case mpr
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ y = x → ∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true

State before:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ (∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true) → y = x
Tactic:
case mp =>
  intro ⟨τ, hτ, hτ'⟩
  by_contra h
  have := τ.set_get_of_ne (!τ y) h
  exact hτ' (hτ ▸ this)
State after:
no goals

State before:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ y = x → ∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true
Tactic:
case mpr =>
  intro h; cases h
  use (fun _ => true)
  simp
State after:
no goals

State before:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ (∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true) → y = x
Tactic:
intro ⟨τ, hτ, hτ'⟩
State after:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ x = true
hτ' : ¬PropAssignment.set τ y (!τ y) x = true
⊢ y = x

State before:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ x = true
hτ' : ¬PropAssignment.set τ y (!τ y) x = true
⊢ y = x
Tactic:
by_contra h
State after:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ x = true
hτ' : ¬PropAssignment.set τ y (!τ y) x = true
h : ¬y = x
⊢ False

State before:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ x = true
hτ' : ¬PropAssignment.set τ y (!τ y) x = true
h : ¬y = x
⊢ False
Tactic:
have := τ.set_get_of_ne (!τ y) h
State after:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ x = true
hτ' : ¬PropAssignment.set τ y (!τ y) x = true
h : ¬y = x
this : PropAssignment.set τ y (!τ y) x = τ x
⊢ False

State before:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
τ : PropAssignment ν
hτ : τ x = true
hτ' : ¬PropAssignment.set τ y (!τ y) x = true
h : ¬y = x
this : PropAssignment.set τ y (!τ y) x = τ x
⊢ False
Tactic:
exact hτ' (hτ ▸ this)
State after:
no goals

State before:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
⊢ y = x → ∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true
Tactic:
intro h
State after:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
h : y = x
⊢ ∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true

State before:
ν : Type u_1
inst✝ : DecidableEq ν
x y : ν
h : y = x
⊢ ∃ τ, τ x = true ∧ ¬PropAssignment.set τ y (!τ y) x = true
Tactic:
cases h
State after:
case refl
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
⊢ ∃ τ, τ x = true ∧ ¬PropAssignment.set τ x (!τ x) x = true

State before:
case refl
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
⊢ ∃ τ, τ x = true ∧ ¬PropAssignment.set τ x (!τ x) x = true
Tactic:
use (fun _ => true)
State after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
⊢ true = true ∧ ¬PropAssignment.set (fun x => true) x (!true) x = true

State before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
⊢ true = true ∧ ¬PropAssignment.set (fun x => true) x (!true) x = true
Tactic:
simp
State after:
no goals