Theorem: LO.FirstOrder.Semiterm.lang_func_ss (Logic/FirstOrder/Completeness/SubLanguage.lean)

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

State before:
L L₁ L₂ : Language
inst✝ : (k : ℕ) → DecidableEq (L.Func k)
μ : Type u_1
n k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
⊢ x ∈ (v i).lang → x ∈ (func f v).lang
Tactic:
simp[lang]
State after:
L L₁ L₂ : Language
inst✝ : (k : ℕ) → DecidableEq (L.Func k)
μ : Type u_1
n k : ℕ
f : L.Func k
v : Fin k → Semiterm L μ n
i : Fin k
x : (k : ℕ) × L.Func k
⊢ x ∈ (v i).lang → x = ⟨k, f⟩ ∨ ∃ a, x ∈ (v a).lang

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

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