Theorem: LO.Compact.compact_cumulative (Logic/Logic/Semantics.lean)

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
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)

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)
State after:
no goals

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
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)

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 : ∀ (s : ℕ), Semantics.Satisfiable M (T s)
⊢ Semantics.Satisfiable M (⋃ s, T s)
Tactic:
apply compact.mpr
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)
⊢ ∀ (u : Finset F), ↑u ⊆ ⋃ s, T s → Semantics.Satisfiable M ↑u

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 : ∀ (s : ℕ), Semantics.Satisfiable M (T s)
⊢ ∀ (u : Finset F), ↑u ⊆ ⋃ s, T s → Semantics.Satisfiable M ↑u
Tactic:
intro u hu
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)
u : Finset F
hu : ↑u ⊆ ⋃ s, T s
⊢ Semantics.Satisfiable M ↑u

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 : ∀ (s : ℕ), Semantics.Satisfiable M (T s)
u : Finset F
hu : ↑u ⊆ ⋃ s, T s
⊢ Semantics.Satisfiable M ↑u
Tactic:
rcases hT.finset_mem hu with ⟨s, hs⟩
State after:
case intro
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)
u : Finset F
hu : ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
⊢ Semantics.Satisfiable M ↑u

State before:
case intro
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)
u : Finset F
hu : ↑u ⊆ ⋃ s, T s
s : ℕ
hs : ↑u ⊆ T s
⊢ Semantics.Satisfiable M ↑u
Tactic:
exact (H s).of_subset hs
State after:
no goals