-- Mathlib/ModelTheory/Satisfiability.lean
theorem isSatisfiable_iUnion_iff_isSatisfiable_iUnion_finset {ι : Type*} (T : ι → L.Theory) :
    IsSatisfiable (⋃ i, T i) ↔ ∀ s : Finset ι, IsSatisfiable (⋃ i ∈ s, T i)

Proof state:
L : Language
ι : Type u_1
T : ι → L.Theory
⊢ IsSatisfiable (⋃ i, T i) ↔ ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)

Tactic:
refine
  ⟨fun h s => h.mono (Set.iUnion_mono fun _ => Set.iUnion_subset_iff.2 fun _ => refl _),
    fun h => ?_⟩

Result:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
⊢ IsSatisfiable (⋃ i, T i)

Proof state:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
s : Finset L.Sentence
hs : ↑s ⊆ ⋃ t, ⋃ i ∈ t, T i
⊢ Directed (fun x1 x2 => x1 ⊆ x2) fun i => ⋃ i_1 ∈ i, T i_1

Tactic:
exact Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
  Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩

Result:
no goals

Proof state:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
s : Finset L.Sentence
hs : ↑s ⊆ ⋃ i, T i
⊢ IsSatisfiable ↑s

Tactic:
rw [Set.iUnion_eq_iUnion_finset] at hs

Result:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
s : Finset L.Sentence
hs : ↑s ⊆ ⋃ t, ⋃ i ∈ t, T i
⊢ IsSatisfiable ↑s

Proof state:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
s : Finset L.Sentence
hs : ↑s ⊆ ⋃ t, ⋃ i ∈ t, T i
⊢ IsSatisfiable ↑s

Tactic:
obtain ⟨t, ht⟩ := Directed.exists_mem_subset_of_finset_subset_biUnion (by
  exact Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
    Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩) hs

Result:
case intro
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
s : Finset L.Sentence
hs : ↑s ⊆ ⋃ t, ⋃ i ∈ t, T i
t : Finset ι
ht : ↑s ⊆ ⋃ i ∈ t, T i
⊢ IsSatisfiable ↑s

Proof state:
case intro
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
s : Finset L.Sentence
hs : ↑s ⊆ ⋃ t, ⋃ i ∈ t, T i
t : Finset ι
ht : ↑s ⊆ ⋃ i ∈ t, T i
⊢ IsSatisfiable ↑s

Tactic:
exact (h t).mono ht

Result:
no goals

Proof state:
L : Language
ι : Type u_1
T : ι → L.Theory
⊢ IsSatisfiable (⋃ i, T i) ↔ ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)

Tactic:
classical
  refine
    ⟨fun h s => h.mono (Set.iUnion_mono fun _ => Set.iUnion_subset_iff.2 fun _ => refl _),
      fun h => ?_⟩
  rw [isSatisfiable_iff_isFinitelySatisfiable]
  intro s hs
  rw [Set.iUnion_eq_iUnion_finset] at hs
  obtain ⟨t, ht⟩ := Directed.exists_mem_subset_of_finset_subset_biUnion (by
    exact Monotone.directed_le fun t1 t2 (h : ∀ ⦃x⦄, x ∈ t1 → x ∈ t2) =>
      Set.iUnion_mono fun _ => Set.iUnion_mono' fun h1 => ⟨h h1, refl _⟩) hs
  exact (h t).mono ht

Result:
no goals

Proof state:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
⊢ IsFinitelySatisfiable (⋃ i, T i)

Tactic:
intro s hs

Result:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
s : Finset L.Sentence
hs : ↑s ⊆ ⋃ i, T i
⊢ IsSatisfiable ↑s

Proof state:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
⊢ IsSatisfiable (⋃ i, T i)

Tactic:
rw [isSatisfiable_iff_isFinitelySatisfiable]

Result:
L : Language
ι : Type u_1
T : ι → L.Theory
h : ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
⊢ IsFinitelySatisfiable (⋃ i, T i)