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

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

State before:
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
φ✝ : PropFun ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
φ : PropForm ν₁
hφ : ⟦φ⟧ = φ✝
⊢ τ ⊨ substL φ✝ f ↔ PropAssignment.subst (fun x => ⟦f x⟧) τ ⊨ φ✝
Tactic:
cases hφ
State after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
φ : PropForm ν₁
⊢ τ ⊨ substL ⟦φ⟧ f ↔ PropAssignment.subst (fun x => ⟦f x⟧) τ ⊨ ⟦φ⟧

State before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
φ : PropForm ν₁
⊢ τ ⊨ substL ⟦φ⟧ f ↔ PropAssignment.subst (fun x => ⟦f x⟧) τ ⊨ ⟦φ⟧
Tactic:
simp [substL]
State after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
φ : PropForm ν₁
⊢ τ ⊨ ⟦PropForm.subst φ f⟧ ↔ PropAssignment.subst (fun x => ⟦f x⟧) τ ⊨ ⟦φ⟧

State before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
φ : PropForm ν₁
⊢ τ ⊨ ⟦PropForm.subst φ f⟧ ↔ PropAssignment.subst (fun x => ⟦f x⟧) τ ⊨ ⟦φ⟧
Tactic:
rw [satisfies_mk, satisfies_mk, PropForm.satisfies_subst]
State after:
no goals