Theorem: LeanSAT.Model.PropForm.satisfies_subst (LeanSAT/Model/Subst.lean)

State before:
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.10308
f✝ f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ✝ φ₁ φ₂ φ : PropForm ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ subst φ f ↔ PropAssignment.subst (fun x => ⟦f x⟧) τ ⊨ φ
Tactic:
induction φ <;> simp [subst, PropAssignment.subst, *]
State after:
case var
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.10308
f✝ f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁ φ₂ : PropForm ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
x✝ : ν₁
⊢ τ ⊨ f x✝ ↔ τ ⊨ ⟦f x✝⟧

State before:
case var
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.10308
f✝ f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁ φ₂ : PropForm ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
x✝ : ν₁
⊢ τ ⊨ f x✝ ↔ τ ⊨ ⟦f x✝⟧
Tactic:
rw [PropFun.satisfies_mk]
State after:
no goals