rw [←vDashSingleton_iff_vDash_formula φ] at lhs
case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ ∀ φ_1 ∈ [φ], evaluate M w φ_1

case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ ψ✝ ∈ [ψ✝]
case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : (M, w)⊨[φ]
⊢ ∀ φ_1 ∈ [φ], evaluate M w φ_1

case a
φ ψ✝ : Formula
W : Type
M : KripkeModel W
w : W
ψ : Formula
impTaut : (∀ φ_1 ∈ [φ], evaluate M w φ_1) → ∀ ψ ∈ [ψ✝], evaluate M w ψ
psi_in_psi : ψ = ψ✝
lhs : evaluate M w φ
⊢ ψ✝ ∈ [ψ✝]