exact
  ⟨ fun h => ⟨fun _ hf => h (Or.inl hf), fun _ hf => h (Or.inr hf)⟩,
    by rintro ⟨h₁, h₂⟩ f (h | h); exact h₁ h; exact h₂ h ⟩
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
⊢ (∀ ⦃f : F⦄, f ∈ T ∨ f ∈ U → 𝓜 ⊧ f) ↔ (∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f) ∧ ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f
no goals