internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.consequence_iff_eq
Proof state before:
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
⊢ (∀ (M : Type v) (a : M) [inst : Structure L M], M ⊧ₘ* T → M ⊧ₘ σ) ↔
    ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
Tactic:
constructor
Proof state after:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
⊢ (∀ (M : Type v) (a : M) [inst : Structure L M], M ⊧ₘ* T → M ⊧ₘ σ) →
    ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ

case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
⊢ (∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ) →
    ∀ (M : Type v) (a : M) [inst : Structure L M], M ⊧ₘ* T → M ⊧ₘ σ
Theorem: LO.FirstOrder.consequence_iff_eq
Proof state before:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
⊢ (∀ (M : Type v) (a : M) [inst : Structure L M], M ⊧ₘ* T → M ⊧ₘ σ) →
    ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
Tactic:
intro h M x s _ hM
Proof state after:
case mp
L : Language
μ : Type u_1
inst✝² : Semiformula.Operator.Eq L
T : Theory L
inst✝¹ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
inst✝ : Structure.Eq L M
hM : M ⊧ₘ* T
⊢ M ⊧ₘ σ
Theorem: LO.FirstOrder.consequence_iff_eq
Proof state before:
case mp
L : Language
μ : Type u_1
inst✝² : Semiformula.Operator.Eq L
T : Theory L
inst✝¹ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
inst✝ : Structure.Eq L M
hM : M ⊧ₘ* T
⊢ M ⊧ₘ σ
Tactic:
exact h M x hM
Proof state after:
no goals
Theorem: LO.FirstOrder.consequence_iff_eq
Proof state before:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
⊢ (∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ) →
    ∀ (M : Type v) (a : M) [inst : Structure L M], M ⊧ₘ* T → M ⊧ₘ σ
Tactic:
intro h M x s hM
Proof state after:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
⊢ M ⊧ₘ σ
Theorem: LO.FirstOrder.consequence_iff_eq
Proof state before:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
⊢ M ⊧ₘ σ
Tactic:
haveI : Nonempty M := ⟨x⟩
Proof state after:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
⊢ M ⊧ₘ σ
Theorem: LO.FirstOrder.consequence_iff_eq
Proof state before:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
⊢ M ⊧ₘ σ
Tactic:
have H : M ⊧ₘ* (𝐄𝐐 : Theory L) := models_of_subtheory hM
Proof state after:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
H : M ⊧ₘ* 𝐄𝐐
⊢ M ⊧ₘ σ
Theorem: LO.FirstOrder.consequence_iff_eq
Proof state before:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
H : M ⊧ₘ* 𝐄𝐐
⊢ M ⊧ₘ σ
Tactic:
have e : Structure.Eq.QuotEq H ≡ₑ[L] M := Structure.Eq.QuotEq.elementaryEquiv H
Proof state after:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
H : M ⊧ₘ* 𝐄𝐐
e : Structure.Eq.QuotEq H ≡ₑ[L] M
⊢ M ⊧ₘ σ
Theorem: LO.FirstOrder.consequence_iff_eq
Proof state before:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
h : ∀ (M : Type v) (a : M) [inst : Structure L M] [inst_1 : Structure.Eq L M], M ⊧ₘ* T → M ⊧ₘ σ
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
H : M ⊧ₘ* 𝐄𝐐
e : Structure.Eq.QuotEq H ≡ₑ[L] M
⊢ M ⊧ₘ σ
Tactic:
exact e.models.mp $ h (Structure.Eq.QuotEq H) ⟦x⟧ (e.modelsTheory.mpr hM)
Proof state after:
no goals
Theorem: LO.FirstOrder.consequence_iff_eq'
Proof state before:
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
σ : Sentence L
⊢ T ⊨[Struc L] σ ↔
    ∀ (M : Type v) [inst : Nonempty M] [inst_1 : Structure L M] [inst_2 : Structure.Eq L M] [inst_3 : M ⊧ₘ* T], M ⊧ₘ σ
Tactic:
rw [consequence_iff_eq]
Proof state after:
no goals
Theorem: LO.FirstOrder.consequence_iff_add_eq
Proof state before:
L : Language
μ : Type u_1
inst✝ : Semiformula.Operator.Eq L
T : Theory L
σ : Sentence L
M : Type v
x✝² : Nonempty M
x✝¹ : Structure L M
x✝ : Structure.Eq L M
⊢ M ⊧ₘ* T⁼ → M ⊧ₘ σ ↔ M ⊧ₘ* T → M ⊧ₘ σ
Tactic:
simp
Proof state after:
no goals
Theorem: LO.FirstOrder.satisfiable_iff_eq
Proof state before:
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
⊢ Semantics.Satisfiable (Struc L) T ↔ ∃ M, ∃ (x : Nonempty M), ∃ x_1, ∃ (_ : Structure.Eq L M), M ⊧ₘ* T
Tactic:
simp [satisfiable_iff]
Proof state after:
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
⊢ (∃ M a x, M ⊧ₘ* T) ↔ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T
Theorem: LO.FirstOrder.satisfiable_iff_eq
Proof state before:
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
⊢ (∃ M a x, M ⊧ₘ* T) ↔ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T
Tactic:
constructor
Proof state after:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
⊢ (∃ M a x, M ⊧ₘ* T) → ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T

case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
⊢ (∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T) → ∃ M a x, M ⊧ₘ* T
Theorem: LO.FirstOrder.satisfiable_iff_eq
Proof state before:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
⊢ (∃ M a x, M ⊧ₘ* T) → ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T
Tactic:
intro ⟨M, x, s, hM⟩
Proof state after:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
⊢ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T
Theorem: LO.FirstOrder.satisfiable_iff_eq
Proof state before:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
⊢ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T
Tactic:
haveI : Nonempty M := ⟨x⟩
Proof state after:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
⊢ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T
Theorem: LO.FirstOrder.satisfiable_iff_eq
Proof state before:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
⊢ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T
Tactic:
have H : M ⊧ₘ* (𝐄𝐐 : Theory L) := models_of_subtheory hM
Proof state after:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
H : M ⊧ₘ* 𝐄𝐐
⊢ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T
Theorem: LO.FirstOrder.satisfiable_iff_eq
Proof state before:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
H : M ⊧ₘ* 𝐄𝐐
⊢ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T
Tactic:
have e : Structure.Eq.QuotEq H ≡ₑ[L] M := Structure.Eq.QuotEq.elementaryEquiv H
Proof state after:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
H : M ⊧ₘ* 𝐄𝐐
e : Structure.Eq.QuotEq H ≡ₑ[L] M
⊢ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T
Theorem: LO.FirstOrder.satisfiable_iff_eq
Proof state before:
case mp
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
x : M
s : Structure L M
hM : M ⊧ₘ* T
this : Nonempty M
H : M ⊧ₘ* 𝐄𝐐
e : Structure.Eq.QuotEq H ≡ₑ[L] M
⊢ ∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T
Tactic:
exact ⟨Structure.Eq.QuotEq H, ⟦x⟧, inferInstance, inferInstance, e.modelsTheory.mpr hM⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.satisfiable_iff_eq
Proof state before:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
⊢ (∃ M a x, Structure.Eq L M ∧ M ⊧ₘ* T) → ∃ M a x, M ⊧ₘ* T
Tactic:
intro ⟨M, i, s, _, hM⟩
Proof state after:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
i : M
s : Structure L M
left✝ : Structure.Eq L M
hM : M ⊧ₘ* T
⊢ ∃ M a x, M ⊧ₘ* T
Theorem: LO.FirstOrder.satisfiable_iff_eq
Proof state before:
case mpr
L : Language
μ : Type u_1
inst✝¹ : Semiformula.Operator.Eq L
T : Theory L
inst✝ : 𝐄𝐐 ≼ T
M : Type v
i : M
s : Structure L M
left✝ : Structure.Eq L M
hM : M ⊧ₘ* T
⊢ ∃ M a x, M ⊧ₘ* T
Tactic:
exact ⟨M, i, s, hM⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Semiformula.eval_existsUnique
Proof state before:
L : Language
μ : Type u_1
inst✝¹ : Operator.Eq L
M : Type u_2
s : Structure L M
inst✝ : Structure.Eq L M
n : ℕ
e : Fin n → M
ε : μ → M
p : Semiformula L μ (n + 1)
⊢ (Eval s e ε) (∃'! p) ↔ ∃! x, (Eval s (x :> e) ε) p
Tactic:
simp [existsUnique, Semiformula.eval_substs, Matrix.comp_vecCons', ExistsUnique]
Proof state after:
no goals
Theorem: LO.Semantics.realize_iff
Proof state before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Tarski M
𝓜 : M
p q : F
⊢ 𝓜 ⊧ p ⟷ q ↔ (𝓜 ⊧ p ↔ 𝓜 ⊧ q)
Tactic:
simp [LogicalConnective.iff, iff_iff_implies_and_implies]
Proof state after:
no goals
Theorem: LO.Semantics.realize_list_conj
Proof state before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Tarski M
𝓜 : M
l : List F
⊢ 𝓜 ⊧ l.conj ↔ ∀ p ∈ l, 𝓜 ⊧ p
Tactic:
induction l <;> simp [*]
Proof state after:
no goals
Theorem: LO.Semantics.realize_finset_conj
Proof state before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Tarski M
𝓜 : M
s : Finset F
⊢ 𝓜 ⊧ ⋀s ↔ ∀ p ∈ s, 𝓜 ⊧ p
Tactic:
simp [Finset.conj]
Proof state after:
no goals
Theorem: LO.Semantics.realize_list_disj
Proof state before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Tarski M
𝓜 : M
l : List F
⊢ 𝓜 ⊧ l.disj ↔ ∃ p ∈ l, 𝓜 ⊧ p
Tactic:
induction l <;> simp [*]
Proof state after:
no goals
Theorem: LO.Semantics.realize_finset_disj
Proof state before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Tarski M
𝓜 : M
s : Finset F
⊢ 𝓜 ⊧ ⋁s ↔ ∃ p ∈ s, 𝓜 ⊧ p
Tactic:
simp [Finset.disj]
Proof state after:
no goals
Theorem: LO.Semantics.meaningful_iff
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
𝓜 : M
⊢ Meaningful 𝓜 → ∃ f, ¬𝓜 ⊧ f
Tactic:
rintro ⟨h⟩
Proof state after:
case mk
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
𝓜 : M
h : ∃ f, ¬𝓜 ⊧ f
⊢ ∃ f, ¬𝓜 ⊧ f
Theorem: LO.Semantics.meaningful_iff
Proof state before:
case mk
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
𝓜 : M
h : ∃ f, ¬𝓜 ⊧ f
⊢ ∃ f, ¬𝓜 ⊧ f
Tactic:
exact h
Proof state after:
no goals
Theorem: LO.Semantics.not_meaningful_iff
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
𝓜 : M
⊢ ¬Meaningful 𝓜 ↔ ∀ (f : F), 𝓜 ⊧ f
Tactic:
simp [meaningful_iff]
Proof state after:
no goals
Theorem: LO.Semantics.realizeSet_iff
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
𝓜 : M
T : Set F
⊢ 𝓜 ⊧* T → ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
Tactic:
rintro ⟨h⟩ f hf
Proof state after:
case mk
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
𝓜 : M
T : Set F
h : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
f : F
hf : f ∈ T
⊢ 𝓜 ⊧ f
Theorem: LO.Semantics.realizeSet_iff
Proof state before:
case mk
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
𝓜 : M
T : Set F
h : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
f : F
hf : f ∈ T
⊢ 𝓜 ⊧ f
Tactic:
exact h hf
Proof state after:
no goals
Theorem: LO.Semantics.realizeSet_iff
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
𝓜 : M
T : Set F
⊢ (∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f) → 𝓜 ⊧* T
Tactic:
intro h
Proof state after:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
𝓜 : M
T : Set F
h : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
⊢ 𝓜 ⊧* T
Theorem: LO.Semantics.realizeSet_iff
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
𝓜 : M
T : Set F
h : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
⊢ 𝓜 ⊧* T
Tactic:
exact ⟨h⟩
Proof state after:
no goals
Theorem: LO.Semantics.not_satisfiable_finset
Proof state before:
M : Type u_1
F : Type u_2
inst✝² : LogicalConnective F
𝓢 : Semantics F M
inst✝¹ : Tarski M
inst✝ : DecidableEq F
t : Finset F
⊢ ¬Satisfiable M ↑t ↔ Valid M (⋁Finset.image (fun x => ~x) t)
Tactic:
simp [Satisfiable, realizeSet_iff, Valid, Finset.map_disj]
Proof state after:
no goals
Theorem: LO.Semantics.satisfiableSet_iff_models_nonempty
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
⊢ Satisfiable M T → (models M T).Nonempty
Tactic:
rintro ⟨𝓜, h𝓜⟩
Proof state after:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
𝓜 : M
h𝓜 : 𝓜 ⊧* T
⊢ (models M T).Nonempty
Theorem: LO.Semantics.satisfiableSet_iff_models_nonempty
Proof state before:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
𝓜 : M
h𝓜 : 𝓜 ⊧* T
⊢ (models M T).Nonempty
Tactic:
exact ⟨𝓜, h𝓜⟩
Proof state after:
no goals
Theorem: LO.Semantics.satisfiableSet_iff_models_nonempty
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
⊢ (models M T).Nonempty → Satisfiable M T
Tactic:
rintro ⟨𝓜, h𝓜⟩
Proof state after:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
𝓜 : M
h𝓜 : 𝓜 ∈ models M T
⊢ Satisfiable M T
Theorem: LO.Semantics.satisfiableSet_iff_models_nonempty
Proof state before:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
𝓜 : M
h𝓜 : 𝓜 ∈ models M T
⊢ Satisfiable M T
Tactic:
exact ⟨𝓜, h𝓜⟩
Proof state after:
no goals
Theorem: LO.Semantics.RealizeSet.empty
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
𝓜 : M
⊢ ∀ ⦃f : F⦄, f ∈ ∅ → 𝓜 ⊧ f
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Semantics.RealizeSet.singleton_iff
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
f : F
𝓜 : M
⊢ 𝓜 ⊧* {f} ↔ 𝓜 ⊧ f
Tactic:
simp [realizeSet_iff]
Proof state after:
no goals
Theorem: LO.Semantics.RealizeSet.insert_iff
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
f : F
𝓜 : M
⊢ 𝓜 ⊧* insert f T ↔ 𝓜 ⊧ f ∧ 𝓜 ⊧* T
Tactic:
simp [realizeSet_iff]
Proof state after:
no goals
Theorem: LO.Semantics.RealizeSet.union_iff
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
⊢ 𝓜 ⊧* T ∪ U ↔ 𝓜 ⊧* T ∧ 𝓜 ⊧* U
Tactic:
simp [realizeSet_iff]
Proof state after:
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
Theorem: LO.Semantics.RealizeSet.union_iff
Proof state before:
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
Tactic:
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 ⟩
Proof state after:
no goals
Theorem: LO.Semantics.RealizeSet.union_iff
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
⊢ ((∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f) ∧ ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f) → ∀ ⦃f : F⦄, f ∈ T ∨ f ∈ U → 𝓜 ⊧ f
Tactic:
rintro ⟨h₁, h₂⟩ f (h | h)
Proof state after:
case intro.inl
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
h₁ : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
h₂ : ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f
f : F
h : f ∈ T
⊢ 𝓜 ⊧ f

case intro.inr
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
h₁ : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
h₂ : ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f
f : F
h : f ∈ U
⊢ 𝓜 ⊧ f
Theorem: LO.Semantics.RealizeSet.union_iff
Proof state before:
case intro.inl
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
h₁ : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
h₂ : ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f
f : F
h : f ∈ T
⊢ 𝓜 ⊧ f

case intro.inr
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
h₁ : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
h₂ : ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f
f : F
h : f ∈ U
⊢ 𝓜 ⊧ f
Tactic:
exact h₁ h
Proof state after:
case intro.inr
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
h₁ : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
h₂ : ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f
f : F
h : f ∈ U
⊢ 𝓜 ⊧ f
Theorem: LO.Semantics.RealizeSet.union_iff
Proof state before:
case intro.inr
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
𝓜 : M
h₁ : ∀ ⦃f : F⦄, f ∈ T → 𝓜 ⊧ f
h₂ : ∀ ⦃f : F⦄, f ∈ U → 𝓜 ⊧ f
f : F
h : f ∈ U
⊢ 𝓜 ⊧ f
Tactic:
exact h₂ h
Proof state after:
no goals
Theorem: LO.Semantics.RealizeSet.image_iff
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
ι : Type u_3
f : ι → F
A : Set ι
𝓜 : M
⊢ 𝓜 ⊧* f '' A ↔ ∀ i ∈ A, 𝓜 ⊧ f i
Tactic:
simp [realizeSet_iff]
Proof state after:
no goals
Theorem: LO.Semantics.RealizeSet.range_iff
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
ι : Sort u_3
f : ι → F
𝓜 : M
⊢ 𝓜 ⊧* Set.range f ↔ ∀ (i : ι), 𝓜 ⊧ f i
Tactic:
simp [realizeSet_iff]
Proof state after:
no goals
Theorem: LO.Semantics.RealizeSet.setOf_iff
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
P : F → Prop
𝓜 : M
⊢ 𝓜 ⊧* setOf P ↔ ∀ (f : F), P f → 𝓜 ⊧ f
Tactic:
simp [realizeSet_iff]
Proof state after:
no goals
Theorem: LO.Semantics.valid_neg_iff
Proof state before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Tarski M
f : F
⊢ Valid M (~f) ↔ ¬Satisfiable M {f}
Tactic:
simp [Valid, Satisfiable]
Proof state after:
no goals
Theorem: LO.Semantics.Satisfiable.of_subset
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
h : Satisfiable M U
ss : T ⊆ U
⊢ Satisfiable M T
Tactic:
rcases h with ⟨𝓜, h⟩
Proof state after:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
ss : T ⊆ U
𝓜 : M
h : 𝓜 ⊧* U
⊢ Satisfiable M T
Theorem: LO.Semantics.Satisfiable.of_subset
Proof state before:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T U : Set F
ss : T ⊆ U
𝓜 : M
h : 𝓜 ⊧* U
⊢ Satisfiable M T
Tactic:
exact ⟨𝓜, RealizeSet.of_subset h ss⟩
Proof state after:
no goals
Theorem: LO.Semantics.empty_models
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
f : F
⊢ ∅ ⊧ f
Tactic:
rintro h
Proof state after:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
f : F
h : M
⊢ h ∈ ∅ → h ⊧ f
Theorem: LO.Semantics.empty_models
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
f : F
h : M
⊢ h ∈ ∅ → h ⊧ f
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Semantics.set_meaningful_iff_nonempty
Proof 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⟩
Proof 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
Theorem: LO.Semantics.set_meaningful_iff_nonempty
Proof 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
Proof 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
Theorem: LO.Semantics.set_meaningful_iff_nonempty
Proof 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
Proof 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
Theorem: LO.Semantics.set_meaningful_iff_nonempty
Proof 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
Proof state after:
no goals
Theorem: LO.Semantics.set_meaningful_iff_nonempty
Proof 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𝓜⟩
Proof 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
Theorem: LO.Semantics.set_meaningful_iff_nonempty
Proof 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⟩
Proof 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
Theorem: LO.Semantics.set_meaningful_iff_nonempty
Proof 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⟩⟩
Proof state after:
no goals
Theorem: LO.Semantics.set_meaningful_iff_nonempty
Proof 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]
Proof 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