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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x₁ : ν
b₁ : Bool
x₂ : ν
b₂ : Bool
h : x₁ ≠ x₂
⊢ set (set τ x₂ b₂) x₁ b₁ = set (set τ x₁ b₁) x₂ b₂
Tactic:
ext v
State after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x₁ : ν
b₁ : Bool
x₂ : ν
b₂ : Bool
h : x₁ ≠ x₂
v : ν
⊢ set (set τ x₂ b₂) x₁ b₁ v = set (set τ x₁ b₁) x₂ b₂ v

State before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x₁ : ν
b₁ : Bool
x₂ : ν
b₂ : Bool
h : x₁ ≠ x₂
v : ν
⊢ set (set τ x₂ b₂) x₁ b₁ v = set (set τ x₁ b₁) x₂ b₂ v
Tactic:
simp [set]
State after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x₁ : ν
b₁ : Bool
x₂ : ν
b₂ : Bool
h : x₁ ≠ x₂
v : ν
⊢ (if v = x₁ then b₁ else if v = x₂ then b₂ else τ v) = if v = x₂ then b₂ else if v = x₁ then b₁ else τ v

State before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x₁ : ν
b₁ : Bool
x₂ : ν
b₂ : Bool
h : x₁ ≠ x₂
v : ν
⊢ (if v = x₁ then b₁ else if v = x₂ then b₂ else τ v) = if v = x₂ then b₂ else if v = x₁ then b₁ else τ v
Tactic:
split <;> split <;> (subst_vars; simp at *)
State after:
no goals

State before:
case h.inr.inl
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x₁ : ν
b₁ : Bool
x₂ : ν
b₂ : Bool
h : x₁ ≠ x₂
v : ν
h✝¹ : ¬v = x₁
h✝ : v = x₂
⊢ b₂ = b₂
Tactic:
subst_vars
State after:
case h.inr.inl
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x₁ : ν
b₁ b₂ : Bool
v : ν
h✝ : ¬v = x₁
h : x₁ ≠ v
⊢ b₂ = b₂

State before:
case h.inr.inr
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x₁ : ν
b₁ : Bool
x₂ : ν
b₂ : Bool
h : x₁ ≠ x₂
v : ν
h✝¹ : ¬v = x₁
h✝ : ¬v = x₂
⊢ τ v = τ v
Tactic:
simp at *
State after:
no goals