L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ ∀ (i : Finset ↑s),
    IsSatisfiable
      (LHom.onTheory (lhomWithConstants L α) T ∪
        distinctConstantsTheory L ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i))

L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Directed (fun x x_1 => x ⊆ x_1) fun i =>
    LHom.onTheory (lhomWithConstants L α) T ∪
      distinctConstantsTheory L ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ IsSatisfiable (LHom.onTheory (lhomWithConstants L α) T ∪ distinctConstantsTheory L s)
rw [distinctConstantsTheory_eq_iUnion, Set.union_iUnion, isSatisfiable_directed_union_iff]
no goals
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ ∀ (i : Finset ↑s),
    IsSatisfiable
      (LHom.onTheory (lhomWithConstants L α) T ∪
        distinctConstantsTheory L ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i))
exact fun t =>
  isSatisfiable_union_distinctConstantsTheory_of_card_le T _ M
    ((lift_le_aleph0.2 (finset_card_lt_aleph0 _).le).trans
      (aleph0_le_lift.2 (aleph0_le_mk M)))
case a
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i =>
    LHom.onTheory (lhomWithConstants L α) T ∪
      distinctConstantsTheory L ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Directed (fun x x_1 => x ⊆ x_1) fun i =>
    LHom.onTheory (lhomWithConstants L α) T ∪
      distinctConstantsTheory L ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
apply Monotone.directed_le
case a
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i => ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
case a
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i =>
    LHom.onTheory (lhomWithConstants L α) T ∪
      distinctConstantsTheory L ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
refine' monotone_const.union (monotone_distinctConstantsTheory.comp _)
case a
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i => (fun a => ↑a) '' ↑i
case a
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i => ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)
simp only [Finset.coe_map, Function.Embedding.coe_subtype]
no goals
case a
L : Language
T✝ : Theory L
α : Type w
n : ℕ
T' T : Theory L
s : Set α
M : Type w'
inst✝² : Structure L M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i => (fun a => ↑a) '' ↑i
exact Monotone.comp (g := Set.image ((↑) : s → α)) (f := ((↑) : Finset s → Set s))
  Set.monotone_image fun _ _ => Finset.coe_subset.2