Theorem: LeanSAT.Model.PropFun.subst_neg (LeanSAT/Model/Subst.lean)

State before:
ν₁ : Type u_2
ν₂ : Type u_1
φ φ₁ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
⊢ subst (neg φ) f = neg (subst φ f)
Tactic:
have ⟨φ, hφ⟩ := φ.exists_rep
State after:
ν₁ : Type u_2
ν₂ : Type u_1
φ✝ φ₁ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ : PropForm ν₁
hφ : ⟦φ⟧ = φ✝
⊢ subst (neg φ✝) f = neg (subst φ✝ f)

State before:
ν₁ : Type u_2
ν₂ : Type u_1
φ✝ φ₁ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ : PropForm ν₁
hφ : ⟦φ⟧ = φ✝
⊢ subst (neg φ✝) f = neg (subst φ✝ f)
Tactic:
cases hφ
State after:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
φ₁ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ : PropForm ν₁
⊢ subst (neg ⟦φ⟧) f = neg (subst ⟦φ⟧ f)

State before:
case refl
ν₁ : Type u_2
ν₂ : Type u_1
φ₁ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ : PropForm ν₁
⊢ subst (neg ⟦φ⟧) f = neg (subst ⟦φ⟧ f)
Tactic:
rfl
State after:
no goals