-- Mathlib/ModelTheory/Satisfiability.lean
theorem isSatisfiable_union_distinctConstantsTheory_of_infinite (T : L.Theory) (s : Set α)
    (M : Type w') [L.Structure M] [M ⊨ T] [Infinite M] :
    ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable

Proof state:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable

Tactic:
rw [distinctConstantsTheory_eq_iUnion, Set.union_iUnion, isSatisfiable_directed_union_iff]

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

L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Directed (fun x1 x2 => x1 ⊆ x2) fun i =>
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)

Proof state:
case a
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i =>
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)

Tactic:
refine monotone_const.union (monotone_distinctConstantsTheory.comp ?_)

Result:
case a
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i => ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)

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

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

Result:
no goals

Proof state:
case a
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i => ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)

Tactic:
simp only [Finset.coe_map, Function.Embedding.coe_subtype]

Result:
case a
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i => (fun a => ↑a) '' ↑i

Proof state:
case a
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i => (fun a => ↑a) '' ↑i

Tactic:
exact Monotone.comp (g := Set.image ((↑) : s → α)) (f := ((↑) : Finset s → Set s))
  Set.monotone_image fun _ _ => Finset.coe_subset.2

Result:
no goals

Proof state:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Directed (fun x1 x2 => x1 ⊆ x2) fun i =>
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)

Tactic:
apply Monotone.directed_le

Result:
case a
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
⊢ Monotone fun i =>
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory ↑(Finset.map (Function.Embedding.subtype fun x => x ∈ s) i)