internlm/Lean-Github huggingface dataset:
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
⊢ ∃ x ∈ s, ¬x ⊧ f
Tactic:
exact ⟨𝓜, h𝓜, hf⟩
Proof state after:
no goals
Theorem: LO.Semantics.meaningful_iff_satisfiableSet
Proof state before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : ∀ (𝓜 : M), Meaningful 𝓜
⊢ Satisfiable M T ↔ Meaningful (models M T)
Tactic:
simp [set_meaningful_iff_nonempty, satisfiableSet_iff_models_nonempty]
Proof state after:
no goals
Theorem: LO.Semantics.consequence_iff_not_satisfiable
Proof state before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
⊢ T ⊨[M] f ↔ ¬Satisfiable M (insert (~f) T)
Tactic:
simp [consequence_iff, Satisfiable]
Proof state after:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
⊢ (∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f) ↔ ∀ (x : M), ¬x ⊧ f → ¬x ⊧* T
Theorem: LO.Semantics.consequence_iff_not_satisfiable
Proof state before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
⊢ (∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f) ↔ ∀ (x : M), ¬x ⊧ f → ¬x ⊧* T
Tactic:
constructor
Proof state after:
case mp
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
⊢ (∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f) → ∀ (x : M), ¬x ⊧ f → ¬x ⊧* T

case mpr
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
⊢ (∀ (x : M), ¬x ⊧ f → ¬x ⊧* T) → ∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f
Theorem: LO.Semantics.consequence_iff_not_satisfiable
Proof state before:
case mp
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
⊢ (∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f) → ∀ (x : M), ¬x ⊧ f → ¬x ⊧* T
Tactic:
intro h 𝓜 hf hT
Proof state after:
case mp
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
h : ∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f
𝓜 : M
hf : ¬𝓜 ⊧ f
hT : 𝓜 ⊧* T
⊢ False
Theorem: LO.Semantics.consequence_iff_not_satisfiable
Proof state before:
case mp
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
h : ∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f
𝓜 : M
hf : ¬𝓜 ⊧ f
hT : 𝓜 ⊧* T
⊢ False
Tactic:
have : 𝓜 ⊧ f := h hT
Proof state after:
case mp
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
h : ∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f
𝓜 : M
hf : ¬𝓜 ⊧ f
hT : 𝓜 ⊧* T
this : 𝓜 ⊧ f
⊢ False
Theorem: LO.Semantics.consequence_iff_not_satisfiable
Proof state before:
case mp
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
h : ∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f
𝓜 : M
hf : ¬𝓜 ⊧ f
hT : 𝓜 ⊧* T
this : 𝓜 ⊧ f
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Semantics.consequence_iff_not_satisfiable
Proof state before:
case mpr
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
T : Set F
inst✝ : Tarski M
f : F
⊢ (∀ (x : M), ¬x ⊧ f → ¬x ⊧* T) → ∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ f
Tactic:
intro h 𝓜
Proof state after:
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
Theorem: LO.Semantics.consequence_iff_not_satisfiable
Proof state before:
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
Tactic:
contrapose
Proof state after:
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
Theorem: LO.Semantics.consequence_iff_not_satisfiable
Proof state before:
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
Tactic:
exact h 𝓜
Proof state after:
no goals
Theorem: LO.Cumulative.subset_of_le
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
⊢ T s₁ ⊆ T s₂
Tactic:
suffices ∀ s d, T s ⊆ T (s + d) by
  simpa[Nat.add_sub_of_le h] using this s₁ (s₂ - s₁)
Proof state after:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
⊢ ∀ (s d : ℕ), T s ⊆ T (s + d)
Theorem: LO.Cumulative.subset_of_le
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
⊢ ∀ (s d : ℕ), T s ⊆ T (s + d)
Tactic:
intro s d
Proof state after:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
s d : ℕ
⊢ T s ⊆ T (s + d)
Theorem: LO.Cumulative.subset_of_le
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
s d : ℕ
⊢ T s ⊆ T (s + d)
Tactic:
induction' d with d ih
Proof state after:
case zero
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
s : ℕ
⊢ T s ⊆ T (s + 0)

case succ
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
s d : ℕ
ih : T s ⊆ T (s + d)
⊢ T s ⊆ T (s + (d + 1))
Theorem: LO.Cumulative.subset_of_le
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
this : ∀ (s d : ℕ), T s ⊆ T (s + d)
⊢ T s₁ ⊆ T s₂
Tactic:
simpa[Nat.add_sub_of_le h] using this s₁ (s₂ - s₁)
Proof state after:
no goals
Theorem: LO.Cumulative.subset_of_le
Proof state before:
case zero
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
s : ℕ
⊢ T s ⊆ T (s + 0)
Tactic:
simp
Proof state after:
case zero
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
s : ℕ
⊢ T s ⊆ T s
Theorem: LO.Cumulative.subset_of_le
Proof state before:
case zero
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
s : ℕ
⊢ T s ⊆ T s
Tactic:
rfl
Proof state after:
no goals
Theorem: LO.Cumulative.subset_of_le
Proof state before:
case succ
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
s₁ s₂ : ℕ
h : s₁ ≤ s₂
s d : ℕ
ih : T s ⊆ T (s + d)
⊢ T s ⊆ T (s + (d + 1))
Tactic:
simpa only [Nat.add_succ, add_zero] using subset_trans ih (H (s + d))
Proof state after:
no goals
Theorem: LO.Cumulative.finset_mem
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
u : Finset F
hu : ↑u ⊆ ⋃ s, T s
⊢ ∃ s, ↑u ⊆ T s
Tactic:
haveI := Classical.decEq
Proof state after:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
u : Finset F
hu : ↑u ⊆ ⋃ s, T s
this : (α : Sort ?u.87136) → DecidableEq α
⊢ ∃ s, ↑u ⊆ T s
Theorem: LO.Cumulative.finset_mem
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
u : Finset F
hu : ↑u ⊆ ⋃ s, T s
this : (α : Sort ?u.87136) → DecidableEq α
⊢ ∃ s, ↑u ⊆ T s
Tactic:
induction u using Finset.induction
Proof state after:
case empty
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
hu : ↑∅ ⊆ ⋃ s, T s
⊢ ∃ s, ↑∅ ⊆ T s

case insert
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
a✝² : F
s✝ : Finset F
a✝¹ : a✝² ∉ s✝
a✝ : ↑s✝ ⊆ ⋃ s, T s → ∃ s, ↑s✝ ⊆ T s
hu : ↑(insert a✝² s✝) ⊆ ⋃ s, T s
⊢ ∃ s, ↑(insert a✝² s✝) ⊆ T s
Theorem: LO.Cumulative.finset_mem
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
hu : ↑∅ ⊆ ⋃ s, T s
⊢ ∃ s, ↑∅ ⊆ T s
Tactic:
case empty => exact ⟨0, by simp⟩
Proof state after:
no goals
Theorem: LO.Cumulative.finset_mem
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : ↑(insert f u) ⊆ ⋃ s, T s
⊢ ∃ s, ↑(insert f u) ⊆ T s
Tactic:
case insert f u _ ih =>
  simp at hu
  have : ∃ s, ↑u ⊆ T s := ih (subset_trans (Set.subset_insert _ _) hu)
  rcases this with ⟨s, hs⟩
  have : ∃ s', f ∈ T s' := by simpa using (Set.insert_subset_iff.mp hu).1
  rcases this with ⟨s', hs'⟩
  exact ⟨max s s', by
    simp; exact Set.insert_subset
      (subset_of_le H (Nat.le_max_right s s') hs')
      (subset_trans hs (subset_of_le H $ Nat.le_max_left s s'))⟩
Proof state after:
no goals
Theorem: LO.Cumulative.finset_mem
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
hu : ↑∅ ⊆ ⋃ s, T s
⊢ ∃ s, ↑∅ ⊆ T s
Tactic:
exact ⟨0, by simp⟩
Proof state after:
no goals
Theorem: LO.Cumulative.finset_mem
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
hu : ↑∅ ⊆ ⋃ s, T s
⊢ ↑∅ ⊆ T 0
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Cumulative.finset_mem
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : ↑(insert f u) ⊆ ⋃ s, T s
⊢ ∃ s, ↑(insert f u) ⊆ T s
Tactic:
simp at hu
Proof state after:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
⊢ ∃ s, ↑(insert f u) ⊆ T s
Theorem: LO.Cumulative.finset_mem
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
⊢ ∃ s, ↑(insert f u) ⊆ T s
Tactic:
have : ∃ s, ↑u ⊆ T s := ih (subset_trans (Set.subset_insert _ _) hu)
Proof state after:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this✝ : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
this : ∃ s, ↑u ⊆ T s
⊢ ∃ s, ↑(insert f u) ⊆ T s
Theorem: LO.Cumulative.finset_mem
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this✝ : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
this : ∃ s, ↑u ⊆ T s
⊢ ∃ s, ↑(insert f u) ⊆ T s
Tactic:
rcases this with ⟨s, hs⟩
Proof state after:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
⊢ ∃ s, ↑(insert f u) ⊆ T s
Theorem: LO.Cumulative.finset_mem
Proof state before:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
⊢ ∃ s, ↑(insert f u) ⊆ T s
Tactic:
have : ∃ s', f ∈ T s' := by simpa using (Set.insert_subset_iff.mp hu).1
Proof state after:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this✝ : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
this : ∃ s', f ∈ T s'
⊢ ∃ s, ↑(insert f u) ⊆ T s
Theorem: LO.Cumulative.finset_mem
Proof state before:
case intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this✝ : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
this : ∃ s', f ∈ T s'
⊢ ∃ s, ↑(insert f u) ⊆ T s
Tactic:
rcases this with ⟨s', hs'⟩
Proof state after:
case intro.intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
s' : ℕ
hs' : f ∈ T s'
⊢ ∃ s, ↑(insert f u) ⊆ T s
Theorem: LO.Cumulative.finset_mem
Proof state before:
case intro.intro
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
s' : ℕ
hs' : f ∈ T s'
⊢ ∃ s, ↑(insert f u) ⊆ T s
Tactic:
exact ⟨max s s', by
  simp; exact Set.insert_subset
    (subset_of_le H (Nat.le_max_right s s') hs')
    (subset_trans hs (subset_of_le H $ Nat.le_max_left s s'))⟩
Proof state after:
no goals
Theorem: LO.Cumulative.finset_mem
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
⊢ ∃ s', f ∈ T s'
Tactic:
simpa using (Set.insert_subset_iff.mp hu).1
Proof state after:
no goals
Theorem: LO.Cumulative.finset_mem
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
s' : ℕ
hs' : f ∈ T s'
⊢ ↑(insert f u) ⊆ T (max s s')
Tactic:
simp
Proof state after:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
s' : ℕ
hs' : f ∈ T s'
⊢ insert f ↑u ⊆ T (max s s')
Theorem: LO.Cumulative.finset_mem
Proof state before:
M : Type u_1
F : Type u_2
inst✝ : LogicalConnective F
𝓢 : Semantics F M
T : ℕ → Set F
H : Cumulative T
this : (α : Type u_2) → DecidableEq α
f : F
u : Finset F
a✝ : f ∉ u
ih : ↑u ⊆ ⋃ s, T s → ∃ s, ↑u ⊆ T s
hu : insert f ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
s' : ℕ
hs' : f ∈ T s'
⊢ insert f ↑u ⊆ T (max s s')
Tactic:
exact Set.insert_subset
(subset_of_le H (Nat.le_max_right s s') hs')
(subset_trans hs (subset_of_le H $ Nat.le_max_left s s'))
Proof state after:
no goals
Theorem: LO.Compact.conseq_compact
Proof state before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
⊢ T ⊨[M] f ↔ ∃ u, ↑u ⊆ T ∧ ↑u ⊨[M] f
Tactic:
simp [Semantics.consequence_iff_not_satisfiable, compact (T := insert (~f) T)]
Proof state after:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
⊢ (∃ x, ↑x ⊆ insert (~f) T ∧ ¬Semantics.Satisfiable M ↑x) ↔ ∃ u, ↑u ⊆ T ∧ ¬Semantics.Satisfiable M (insert (~f) ↑u)
Theorem: LO.Compact.conseq_compact
Proof state before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
⊢ (∃ x, ↑x ⊆ insert (~f) T ∧ ¬Semantics.Satisfiable M ↑x) ↔ ∃ u, ↑u ⊆ T ∧ ¬Semantics.Satisfiable M (insert (~f) ↑u)
Tactic:
constructor
Proof state after:
case mp
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
⊢ (∃ x, ↑x ⊆ insert (~f) T ∧ ¬Semantics.Satisfiable M ↑x) → ∃ u, ↑u ⊆ T ∧ ¬Semantics.Satisfiable M (insert (~f) ↑u)

case mpr
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
⊢ (∃ u, ↑u ⊆ T ∧ ¬Semantics.Satisfiable M (insert (~f) ↑u)) → ∃ x, ↑x ⊆ insert (~f) T ∧ ¬Semantics.Satisfiable M ↑x
Theorem: LO.Compact.conseq_compact
Proof state before:
case mp
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
⊢ (∃ x, ↑x ⊆ insert (~f) T ∧ ¬Semantics.Satisfiable M ↑x) → ∃ u, ↑u ⊆ T ∧ ¬Semantics.Satisfiable M (insert (~f) ↑u)
Tactic:
intro ⟨u, ss, hu⟩
Proof state after:
case mp
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
⊢ ∃ u, ↑u ⊆ T ∧ ¬Semantics.Satisfiable M (insert (~f) ↑u)
Theorem: LO.Compact.conseq_compact
Proof state before:
case mp
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
⊢ ∃ u, ↑u ⊆ T ∧ ¬Semantics.Satisfiable M (insert (~f) ↑u)
Tactic:
exact ⟨Finset.erase u (~f), by simp [ss],
  by simp; intro h; exact hu (Semantics.Satisfiable.of_subset h (by simp))⟩
Proof state after:
no goals
Theorem: LO.Compact.conseq_compact
Proof state before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
⊢ ↑(u.erase (~f)) ⊆ T
Tactic:
simp [ss]
Proof state after:
no goals
Theorem: LO.Compact.conseq_compact
Proof state before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
⊢ ¬Semantics.Satisfiable M (insert (~f) ↑(u.erase (~f)))
Tactic:
simp
Proof state after:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
⊢ ¬Semantics.Satisfiable M (insert (~f) ↑u)
Theorem: LO.Compact.conseq_compact
Proof state before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
⊢ ¬Semantics.Satisfiable M (insert (~f) ↑u)
Tactic:
intro h
Proof state after:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
h : Semantics.Satisfiable M (insert (~f) ↑u)
⊢ False
Theorem: LO.Compact.conseq_compact
Proof state before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
h : Semantics.Satisfiable M (insert (~f) ↑u)
⊢ False
Tactic:
exact hu (Semantics.Satisfiable.of_subset h (by simp))
Proof state after:
no goals
Theorem: LO.Compact.conseq_compact
Proof state before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ insert (~f) T
hu : ¬Semantics.Satisfiable M ↑u
h : Semantics.Satisfiable M (insert (~f) ↑u)
⊢ ↑u ⊆ insert (~f) ↑u
Tactic:
simp
Proof state after:
no goals
Theorem: LO.Compact.conseq_compact
Proof state before:
case mpr
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
⊢ (∃ u, ↑u ⊆ T ∧ ¬Semantics.Satisfiable M (insert (~f) ↑u)) → ∃ x, ↑x ⊆ insert (~f) T ∧ ¬Semantics.Satisfiable M ↑x
Tactic:
intro ⟨u, ss, hu⟩
Proof state after:
case mpr
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ T
hu : ¬Semantics.Satisfiable M (insert (~f) ↑u)
⊢ ∃ x, ↑x ⊆ insert (~f) T ∧ ¬Semantics.Satisfiable M ↑x
Theorem: LO.Compact.conseq_compact
Proof state before:
case mpr
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ T
hu : ¬Semantics.Satisfiable M (insert (~f) ↑u)
⊢ ∃ x, ↑x ⊆ insert (~f) T ∧ ¬Semantics.Satisfiable M ↑x
Tactic:
exact ⟨insert (~f) u,
  by simpa using Set.insert_subset_insert ss, by simpa using hu⟩
Proof state after:
no goals
Theorem: LO.Compact.conseq_compact
Proof state before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ T
hu : ¬Semantics.Satisfiable M (insert (~f) ↑u)
⊢ ↑(insert (~f) u) ⊆ insert (~f) T
Tactic:
simpa using Set.insert_subset_insert ss
Proof state after:
no goals
Theorem: LO.Compact.conseq_compact
Proof state before:
M : Type u_1
F : Type u_2
inst✝³ : LogicalConnective F
𝓢 : Semantics F M
inst✝² : Compact M
𝓜 : M
T : Set F
inst✝¹ : Semantics.Tarski M
inst✝ : DecidableEq F
f : F
u : Finset F
ss : ↑u ⊆ T
hu : ¬Semantics.Satisfiable M (insert (~f) ↑u)
⊢ ¬Semantics.Satisfiable M ↑(insert (~f) u)
Tactic:
simpa using hu
Proof state after:
no goals
Theorem: LO.Compact.compact_cumulative
Proof state before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Compact M
𝓜 : M
T : ℕ → Set F
hT : Cumulative T
⊢ Semantics.Satisfiable M (⋃ s, T s) → ∀ (s : ℕ), Semantics.Satisfiable M (T s)
Tactic:
intro H s
Proof state after:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Compact M
𝓜 : M
T : ℕ → Set F
hT : Cumulative T
H : Semantics.Satisfiable M (⋃ s, T s)
s : ℕ
⊢ Semantics.Satisfiable M (T s)
Theorem: LO.Compact.compact_cumulative
Proof state before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Compact M
𝓜 : M
T : ℕ → Set F
hT : Cumulative T
H : Semantics.Satisfiable M (⋃ s, T s)
s : ℕ
⊢ Semantics.Satisfiable M (T s)
Tactic:
exact H.of_subset (Set.subset_iUnion T s)
Proof state after:
no goals
Theorem: LO.Compact.compact_cumulative
Proof state before:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Compact M
𝓜 : M
T : ℕ → Set F
hT : Cumulative T
⊢ (∀ (s : ℕ), Semantics.Satisfiable M (T s)) → Semantics.Satisfiable M (⋃ s, T s)
Tactic:
intro H
Proof state after:
M : Type u_1
F : Type u_2
inst✝¹ : LogicalConnective F
𝓢 : Semantics F M
inst✝ : Compact M
𝓜 : M
T : ℕ → Set F
hT : Cumulative T
H : ∀ (s : ℕ), Semantics.Satisfiable M (T s)
⊢ Semantics.Satisfiable M (⋃ s, T s)