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

State before:
ν : 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
⊢ map f (set τ (f v) b) = set (map f τ) v b
Tactic:
unfold map
State after:
ν : 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

State before:
ν : 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
Tactic:
unfold set
State after:
ν : 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

State before:
ν : 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
Tactic:
ext
State after:
case h
ν : 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
x✝ : ν₂
⊢ ((fun y => if y = f v then b else τ y) ∘ f) x✝ = if x✝ = v then b else (τ ∘ f) x✝

State before:
case h
ν : 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
x✝ : ν₂
⊢ ((fun y => if y = f v then b else τ y) ∘ f) x✝ = if x✝ = v then b else (τ ∘ f) x✝
Tactic:
simp [finj.eq_iff]
State after:
no goals