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

State before:
ν₁ : Type u_1
ν₂ : Type u_2
φ : PropFun ν₁
f : ν₁ → ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ map f φ ↔ PropAssignment.map f τ ⊨ φ
Tactic:
let ⟨ϕ,hϕ⟩ := φ.toTrunc.out
State after:
ν₁ : Type u_1
ν₂ : Type u_2
φ : PropFun ν₁
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
hϕ : ⟦ϕ⟧ = φ
⊢ τ ⊨ map f φ ↔ PropAssignment.map f τ ⊨ φ

State before:
ν₁ : Type u_1
ν₂ : Type u_2
φ : PropFun ν₁
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
hϕ : ⟦ϕ⟧ = φ
⊢ τ ⊨ map f φ ↔ PropAssignment.map f τ ⊨ φ
Tactic:
cases hϕ
State after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
⊢ τ ⊨ map f ⟦ϕ⟧ ↔ PropAssignment.map f τ ⊨ ⟦ϕ⟧

State before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
⊢ τ ⊨ map f ⟦ϕ⟧ ↔ PropAssignment.map f τ ⊨ ⟦ϕ⟧
Tactic:
simp [map]
State after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
⊢ τ ⊨ ⟦PropForm.map f ϕ⟧ ↔ PropAssignment.map f τ ⊨ ⟦ϕ⟧

State before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
⊢ τ ⊨ ⟦PropForm.map f ϕ⟧ ↔ PropAssignment.map f τ ⊨ ⟦ϕ⟧
Tactic:
rw [satisfies_mk, satisfies_mk]
State after:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
⊢ τ ⊨ PropForm.map f ϕ ↔ PropAssignment.map f τ ⊨ ϕ

State before:
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
⊢ τ ⊨ PropForm.map f ϕ ↔ PropAssignment.map f τ ⊨ ϕ
Tactic:
apply PropForm.satisfies_map
State after:
no goals