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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
x y : ν
τ : PropAssignment ν
v : Bool
⊢ x ≠ y → set τ x v y = τ y
Tactic:
intro h
State after:
ν : Type u_1
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
x y : ν
τ : PropAssignment ν
v : Bool
h : x ≠ y
⊢ set τ x v y = τ y

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
x y : ν
τ : PropAssignment ν
v : Bool
h : x ≠ y
⊢ set τ x v y = τ y
Tactic:
simp [set, h.symm]
State after:
no goals