Theorem: LO.FirstOrder.Semiformula.langFunc_rel_ss (Logic/FirstOrder/Completeness/SubLanguage.lean)

State before:
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
⊢ (v i).lang ⊆ (rel r v).langFunc
Tactic:
intros x
State after:
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
⊢ x ∈ (v i).lang → x ∈ (rel r v).langFunc

State before:
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
⊢ x ∈ (v i).lang → x ∈ (rel r v).langFunc
Tactic:
simp[langFunc]
State after:
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
⊢ x ∈ (v i).lang → ∃ a, x ∈ (v a).lang

State before:
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
⊢ x ∈ (v i).lang → ∃ a, x ∈ (v a).lang
Tactic:
intros h
State after:
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
h : x ∈ (v i).lang
⊢ ∃ a, x ∈ (v a).lang

State before:
L L₁ L₂ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L.Func k)
inst✝ : (k : ℕ) → DecidableEq (L.Rel k)
μ : Type u_1
n k : ℕ
r : L.Rel k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
h : x ∈ (v i).lang
⊢ ∃ a, x ∈ (v a).lang
Tactic:
exact ⟨i, h⟩
State after:
no goals