Theorem: LeanSAT.Model.PropAssignment.agreeOn_setMany_of_disjoint (LeanSAT/Model/PropAssn.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
⊢ agreeOn xs (setMany τ xs' τ') τ
Tactic:
intro v hv
State after:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
v : ν
hv : v ∈ xs
⊢ setMany τ xs' τ' v = τ v

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
v : ν
hv : v ∈ xs
⊢ setMany τ xs' τ' v = τ v
Tactic:
simp [setMany]
State after:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
v : ν
hv : v ∈ xs
⊢ v ∈ xs' → τ' v = τ v

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
v : ν
hv : v ∈ xs
⊢ v ∈ xs' → τ' v = τ v
Tactic:
intro hv'
State after:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
v : ν
hv : v ∈ xs
hv' : v ∈ xs'
⊢ τ' v = τ v

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
v : ν
hv : v ∈ xs
hv' : v ∈ xs'
⊢ τ' v = τ v
Tactic:
exfalso
State after:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
v : ν
hv : v ∈ xs
hv' : v ∈ xs'
⊢ False

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
v : ν
hv : v ∈ xs
hv' : v ∈ xs'
⊢ False
Tactic:
apply h.ne_of_mem hv hv' rfl
State after:
no goals