contrapose
case mpr
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
h : ∀ (x : M), ¬x ⊧ f → ¬x ⊧* T
𝓜 : M
⊢ 𝓜 ⊧* T → 𝓜 ⊧ f
case mpr
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
h : ∀ (x : M), ¬x ⊧ f → ¬x ⊧* T
𝓜 : M
⊢ ¬𝓜 ⊧ f → ¬𝓜 ⊧* T