Theorem: LO.FirstOrder.ultrafilter_exists (Logic/FirstOrder/Ultraproduct.lean)

State before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
⊢ ∀ (T_1 : Finset (Set (FinSubtheory T))), ↑T_1 ⊆ Semiformula.domain A '' T → (⋂₀ ↑T_1).Nonempty
Tactic:
haveI : DecidableEq (Set (FinSubtheory T)) := fun _ _ => Classical.propDecidable _
State after:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
⊢ ∀ (T_1 : Finset (Set (FinSubtheory T))), ↑T_1 ⊆ Semiformula.domain A '' T → (⋂₀ ↑T_1).Nonempty

State before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
⊢ ∀ (T_1 : Finset (Set (FinSubtheory T))), ↑T_1 ⊆ Semiformula.domain A '' T → (⋂₀ ↑T_1).Nonempty
Tactic:
simp[Finset.subset_image_iff, Semiformula.domain]
State after:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
⊢ ∀ (a : Finset (Sentence L)), ↑a ⊆ T → ∃ a_2, ∃ (h : ↑a_2 ⊆ T), ∀ a_3 ∈ a, A ⟨a_2, ⋯⟩ ⊧ₘ a_3

State before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
⊢ ∀ (a : Finset (Sentence L)), ↑a ⊆ T → ∃ a_2, ∃ (h : ↑a_2 ⊆ T), ∀ a_3 ∈ a, A ⟨a_2, ⋯⟩ ⊧ₘ a_3
Tactic:
intro t ht
State after:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ ∃ a, ∃ (h : ↑a ⊆ T), ∀ a_1 ∈ t, A ⟨a, ⋯⟩ ⊧ₘ a_1

State before:
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ ∃ a, ∃ (h : ↑a ⊆ T), ∀ a_1 ∈ t, A ⟨a, ⋯⟩ ⊧ₘ a_1
Tactic:
use t
State after:
case h
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ ∃ (h : ↑t ⊆ T), ∀ a ∈ t, A ⟨t, ⋯⟩ ⊧ₘ a

State before:
case h
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ ∃ (h : ↑t ⊆ T), ∀ a ∈ t, A ⟨t, ⋯⟩ ⊧ₘ a
Tactic:
use ht
State after:
case h
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ ∀ a ∈ t, A ⟨t, ⋯⟩ ⊧ₘ a

State before:
case h
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ ∀ a ∈ t, A ⟨t, ⋯⟩ ⊧ₘ a
Tactic:
intro σ hσ
State after:
case h
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
σ : Sentence L
hσ : σ ∈ t
⊢ A ⟨t, ⋯⟩ ⊧ₘ σ

State before:
case h
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
σ : Sentence L
hσ : σ ∈ t
⊢ A ⟨t, ⋯⟩ ⊧ₘ σ
Tactic:
exact (H ⟨t, ht⟩).RealizeSet hσ
State after:
no goals