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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x : ν
⊢ set τ x (τ x) = τ
Tactic:
ext x'
State after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x x' : ν
⊢ set τ x (τ x) x' = τ x'

State before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x x' : ν
⊢ set τ x (τ x) x' = τ x'
Tactic:
dsimp [set]
State after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x x' : ν
⊢ (if x' = x then τ x else τ x') = τ x'

State before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x x' : ν
⊢ (if x' = x then τ x else τ x') = τ x'
Tactic:
split <;> simp_all
State after:
no goals