L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ {p | S ⊆ ↑p} = Set.univ ↔ ∀ (φ : Sentence (L[[α]])), φ ∈ S → LHom.onTheory (lhomWithConstants L α) T ⊨ᵇ φ
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
⊢ {p | S ⊆ ↑p} = Set.univ ↔ ∀ (φ : Sentence (L[[α]])), φ ∈ S → LHom.onTheory (lhomWithConstants L α) T ⊨ᵇ φ
have h : { p : T.CompleteType α | S ⊆ ↑p } = ⋂₀ ((fun φ => { p | φ ∈ p }) '' S) := by
  ext
  simp [subset_def]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ (∀ (s : Set (CompleteType T α)), s ∈ (fun φ => {p | φ ∈ p}) '' S → s = Set.univ) ↔
    ∀ (φ : Sentence (L[[α]])), φ ∈ S → {p | φ ∈ p} = Set.univ
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ {p | S ⊆ ↑p} = Set.univ ↔ ∀ (φ : Sentence (L[[α]])), φ ∈ S → LHom.onTheory (lhomWithConstants L α) T ⊨ᵇ φ
simp_rw [h, sInter_eq_univ, ← setOf_mem_eq_univ_iff]
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ (∀ (φ : Sentence (L[[α]])), φ ∈ S → {p | φ ∈ p} = Set.univ) →
    ∀ (s : Set (CompleteType T α)), s ∈ (fun φ => {p | φ ∈ p}) '' S → s = Set.univ
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ (∀ (s : Set (CompleteType T α)), s ∈ (fun φ => {p | φ ∈ p}) '' S → s = Set.univ) ↔
    ∀ (φ : Sentence (L[[α]])), φ ∈ S → {p | φ ∈ p} = Set.univ
refine' ⟨fun h φ φS => h _ ⟨_, φS, rfl⟩, _⟩
case intro.intro
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
h✝ : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
h : ∀ (φ : Sentence (L[[α]])), φ ∈ S → {p | φ ∈ p} = Set.univ
φ : Sentence (L[[α]])
h1 : φ ∈ S
⊢ (fun φ => {p | φ ∈ p}) φ = Set.univ
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ (∀ (φ : Sentence (L[[α]])), φ ∈ S → {p | φ ∈ p} = Set.univ) →
    ∀ (s : Set (CompleteType T α)), s ∈ (fun φ => {p | φ ∈ p}) '' S → s = Set.univ
rintro h _ ⟨φ, h1, rfl⟩
no goals
case intro.intro
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
h✝ : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
h : ∀ (φ : Sentence (L[[α]])), φ ∈ S → {p | φ ∈ p} = Set.univ
φ : Sentence (L[[α]])
h1 : φ ∈ S
⊢ (fun φ => {p | φ ∈ p}) φ = Set.univ
exact h _ h1
case h
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
x✝ : CompleteType T α
⊢ x✝ ∈ {p | S ⊆ ↑p} ↔ x✝ ∈ ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
⊢ {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
ext
no goals
case h
L : Language
T : Theory L
α : Type w
S : Theory (L[[α]])
x✝ : CompleteType T α
⊢ x✝ ∈ {p | S ⊆ ↑p} ↔ x✝ ∈ ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
simp [subset_def]