Theorem: LeanSAT.Model.PropFun.var_ne_var_compl (LeanSAT/Model/PropFun.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
⊢ var v1 ≠ (var v2)ᶜ
Tactic:
intro h
State after:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : var v1 = (var v2)ᶜ
⊢ False

State before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : var v1 = (var v2)ᶜ
⊢ False
Tactic:
rw [ext_iff] at h
State after:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ var v1 ↔ τ ⊨ (var v2)ᶜ
⊢ False

State before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ var v1 ↔ τ ⊨ (var v2)ᶜ
⊢ False
Tactic:
have := h (fun v => v = v1 || v = v2)
State after:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ var v1 ↔ τ ⊨ (var v2)ᶜ
this :
  (fun v => decide (v = v1) || decide (v = v2)) ⊨ var v1 ↔ (fun v => decide (v = v1) || decide (v = v2)) ⊨ (var v2)ᶜ
⊢ False

State before:
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ var v1 ↔ τ ⊨ (var v2)ᶜ
this :
  (fun v => decide (v = v1) || decide (v = v2)) ⊨ var v1 ↔ (fun v => decide (v = v1) || decide (v = v2)) ⊨ (var v2)ᶜ
⊢ False
Tactic:
simp at this
State after:
no goals