rw [PropFun.satisfies_mk] at hpos hneg
case a.mpr.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
τ : PropAssignment ν₁
hpos : τ ⊨ ⟦φ⟧
hneg : ¬(PropAssignment.set τ v1 !τ v1) ⊨ ⟦φ⟧
⊢ ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧
case a.mpr.intro.intro.intro.intro
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
τ : PropAssignment ν₁
hpos : τ ⊨ φ
hneg : ¬(PropAssignment.set τ v1 !τ v1) ⊨ φ
⊢ ∃ τ, τ ⊨ ⟦map f φ⟧ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ (f v1) !τ (f v1)) ⟦map f φ⟧