-- Mathlib/ModelTheory/Substructures.lean
theorem mem_iSup_of_directed {ι : Type*} [hι : Nonempty ι] {S : ι → L.Substructure M}
    (hS : Directed (· ≤ ·) S) {x : M} :
    x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Result:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
suffices x ∈ closure L (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by
  simpa only [closure_iUnion, closure_eq (S _)] using this

Result:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ (closure L).toFun (⋃ i, ↑(S i)) → ∃ i, x ∈ S i

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
hx : x ∈ (closure L).toFun (⋃ i, ↑(S i))
n✝ : ℕ
f : L.Functions n✝
v : Fin n✝ → M
hC : ∀ (i : Fin n✝), ∃ i_1, v i ∈ S i_1
⊢ ∃ i, funMap f v ∈ S i

Tactic:
have ⟨i, hi⟩ := hS.finite_le (fun i ↦ Classical.choose (hC i))

Result:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
hx : x ∈ (closure L).toFun (⋃ i, ↑(S i))
n✝ : ℕ
f : L.Functions n✝
v : Fin n✝ → M
hC : ∀ (i : Fin n✝), ∃ i_1, v i ∈ S i_1
i : ι
hi : ∀ (i_1 : Fin n✝), S (Classical.choose ⋯) ≤ S i
⊢ ∃ i, funMap f v ∈ S i

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
hx : x ∈ (closure L).toFun (⋃ i, ↑(S i))
n✝ : ℕ
f : L.Functions n✝
v : Fin n✝ → M
hC : ∀ (i : Fin n✝), v i ∈ {x | ∃ i, x ∈ S i}
⊢ funMap f v ∈ {x | ∃ i, x ∈ S i}

Tactic:
simp_rw [Set.mem_setOf] at *

Result:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
hx : x ∈ (closure L).toFun (⋃ i, ↑(S i))
n✝ : ℕ
f : L.Functions n✝
v : Fin n✝ → M
hC : ∀ (i : Fin n✝), ∃ i_1, v i ∈ S i_1
⊢ ∃ i, funMap f v ∈ S i

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
this : x ∈ (closure L).toFun (⋃ i, ↑(S i)) → ∃ i, x ∈ S i
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa only [closure_iUnion, closure_eq (S _)] using this

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ (closure L).toFun (⋃ i, ↑(S i)) → ∃ i, x ∈ S i

Tactic:
refine fun hx ↦ closure_induction hx (fun _ ↦ mem_iUnion.1) (fun f v hC ↦ ?_)

Result:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
hx : x ∈ (closure L).toFun (⋃ i, ↑(S i))
n✝ : ℕ
f : L.Functions n✝
v : Fin n✝ → M
hC : ∀ (i : Fin n✝), v i ∈ {x | ∃ i, x ∈ S i}
⊢ funMap f v ∈ {x | ∃ i, x ∈ S i}

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
ι : Type u_3
hι : Nonempty ι
S : ι → L.Substructure M
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : M
hx : x ∈ (closure L).toFun (⋃ i, ↑(S i))
n✝ : ℕ
f : L.Functions n✝
v : Fin n✝ → M
hC : ∀ (i : Fin n✝), ∃ i_1, v i ∈ S i_1
i : ι
hi : ∀ (i_1 : Fin n✝), S (Classical.choose ⋯) ≤ S i
⊢ ∃ i, funMap f v ∈ S i

Tactic:
refine ⟨i, (S i).fun_mem f v (fun j ↦ hi j (Classical.choose_spec (hC j)))⟩

Result:
no goals