Theorem: LO.Semantics.set_meaningful_iff_nonempty (Logic/Logic/Semantics.lean)

State before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
s : Set M
⊢ Meaningful s → s.Nonempty
Tactic:
rintro ⟨f, hf⟩
State after:
case mk.intro
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
s : Set M
f : F
hf : ¬s ⊧ f
⊢ s.Nonempty

State before:
case mk.intro
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
s : Set M
f : F
hf : ¬s ⊧ f
⊢ s.Nonempty
Tactic:
by_contra A
State after:
case mk.intro
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
s : Set M
f : F
hf : ¬s ⊧ f
A : ¬s.Nonempty
⊢ False

State before:
case mk.intro
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
s : Set M
f : F
hf : ¬s ⊧ f
A : ¬s.Nonempty
⊢ False
Tactic:
rcases Set.not_nonempty_iff_eq_empty.mp A
State after:
case mk.intro.refl
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
f : F
hf : ¬∅ ⊧ f
A : ¬∅.Nonempty
⊢ False

State before:
case mk.intro.refl
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
f : F
hf : ¬∅ ⊧ f
A : ¬∅.Nonempty
⊢ False
Tactic:
simp at hf
State after:
no goals

State before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
s : Set M
⊢ s.Nonempty → Meaningful s
Tactic:
rintro ⟨𝓜, h𝓜⟩
State after:
case intro
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
s : Set M
𝓜 : M
h𝓜 : 𝓜 ∈ s
⊢ Meaningful s

State before:
case intro
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
s : Set M
𝓜 : M
h𝓜 : 𝓜 ∈ s
⊢ Meaningful s
Tactic:
rcases Meaningful.exists_unrealize (𝓜 := 𝓜) with ⟨f, hf⟩
State after:
case intro.intro
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
s : Set M
𝓜 : M
h𝓜 : 𝓜 ∈ s
f : F
hf : ¬𝓜 ⊧ f
⊢ Meaningful s

State before:
case intro.intro
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
s : Set M
𝓜 : M
h𝓜 : 𝓜 ∈ s
f : F
hf : ¬𝓜 ⊧ f
⊢ Meaningful s
Tactic:
exact ⟨f, by simp [set_models_iff]; exact ⟨𝓜, h𝓜, hf⟩⟩
State after:
no goals

State before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
s : Set M
𝓜 : M
h𝓜 : 𝓜 ∈ s
f : F
hf : ¬𝓜 ⊧ f
⊢ ¬s ⊧ f
Tactic:
simp [set_models_iff]
State after:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
s : Set M
𝓜 : M
h𝓜 : 𝓜 ∈ s
f : F
hf : ¬𝓜 ⊧ f
⊢ ∃ x ∈ s, ¬x ⊧ f

State before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
s : Set M
𝓜 : M
h𝓜 : 𝓜 ∈ s
f : F
hf : ¬𝓜 ⊧ f
⊢ ∃ x ∈ s, ¬x ⊧ f
Tactic:
exact ⟨𝓜, h𝓜, hf⟩
State after:
no goals