-- Module: Mathlib.ModelTheory.Satisfiability
Goal:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst : L.Structure M
inst_1 : M ⊨ T
inst_2 : Infinite M
rw :
  ((L.lhomWithConstants α).onTheory T ∪
      ⋃ (t : Finset (↑s : Type w)),
        L.distinctConstantsTheory
          (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) t) : Set α)).IsSatisfiable
rw₁ :
  IsSatisfiable (L := L[[α]])
    (⋃ (i : Finset (↑s : Type w)),
      (L.lhomWithConstants α).onTheory T ∪
        L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))
rw₂ :
  ∀ (i : Finset (↑s : Type w)),
    IsSatisfiable
      ((L.lhomWithConstants α).onTheory T ∪
        L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))
rw₃ :
  Directed (fun (x1 x2 : L[[α]].Theory) ↦ x1 ⊆ x2) fun (i : Finset (↑s : Type w)) ↦
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)
rw₄ :
  ∀ (i : Finset (↑s : Type w)),
    IsSatisfiable
      ((L.lhomWithConstants α).onTheory T ∪
        L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))
rw₅ :
  Directed (fun (x1 x2 : L[[α]].Theory) ↦ x1 ⊆ x2) fun (i : Finset (↑s : Type w)) ↦
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)
rw₆ :
  ∀ (i : Finset (↑s : Type w)),
    IsSatisfiable
      ((L.lhomWithConstants α).onTheory T ∪
        L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α))
rw₇ rw₈ :
  Directed (fun (x1 x2 : L[[α]].Theory) ↦ x1 ⊆ x2) fun (i : Finset (↑s : Type w)) ↦
    (L.lhomWithConstants α).onTheory T ∪
      L.distinctConstantsTheory (↑(Finset.map (Function.Embedding.subtype fun (x : α) ↦ x ∈ s) i) : Set α)
⊢ ((L.lhomWithConstants α).onTheory T ∪ L.distinctConstantsTheory s).IsSatisfiable

Tactic:
classical
    rw [distinctConstantsTheory_eq_iUnion, Set.union_iUnion, isSatisfiable_directed_union_iff]
    · 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)))
    · apply Monotone.directed_le
      refine monotone_const.union (monotone_distinctConstantsTheory.comp ?_)
      simp only [Finset.coe_map, Function.Embedding.coe_subtype]
      exact Monotone.comp (g := Set.image ((↑) : s → α)) (f := ((↑) : Finset s → Set s))
        Set.monotone_image fun _ _ => Finset.coe_subset.2

Premises used: Iff.mpr, FirstOrder.Language.Theory.isSatisfiable_directed_union_iff, Cardinal.lift_le_aleph0, monotone_const, Monotone.union, Set.union_iUnion, Function.Embedding.coe_subtype, Monotone.comp, LT.lt.le, Cardinal.aleph0_le_lift, FirstOrder.Language.monotone_distinctConstantsTheory, SetLike.coe, FirstOrder.Language.distinctConstantsTheory_eq_iUnion, Finset.coe_map, LE.le.trans, Set.monotone_image, Monotone.directed_le, FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_card_le, Cardinal.finset_card_lt_aleph0, Cardinal.aleph0_le_mk, Finset.coe_subset