unfold set
ν : Type ?u.19102
inst✝² : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
v : ν₂
b : Bool
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₂ → ν₁
τ : PropAssignment ν₁
finj : Function.Injective f
⊢ set τ (f v) b ∘ f = set (τ ∘ f) v b
ν : Type ?u.19102
inst✝² : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
v : ν₂
b : Bool
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
f : ν₂ → ν₁
τ : PropAssignment ν₁
finj : Function.Injective f
⊢ (fun y => if y = f v then b else τ y) ∘ f = fun y => if y = v then b else (τ ∘ f) y