Theorem: LO.FirstOrder.Structure.extendStructure.val_lMap (Logic/FirstOrder/Completeness/SubLanguage.lean)

State before:
μ : Type u_1
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf✝ : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁✝ : Structure L₁ M
n : ℕ
e : Fin n → M
ε : μ → M
injf : ∀ (k : ℕ), Function.Injective Φ.func
s₁ : Structure L₁ M
t : Semiterm L₁ μ n
⊢ Semiterm.val (extendStructure Φ s₁) e ε (Semiterm.lMap Φ t) = Semiterm.val s₁ e ε t
Tactic:
induction t <;> simp[*, Semiterm.lMap_func, Semiterm.val_func]
State after:
case func
μ : Type u_1
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf✝ : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁✝ : Structure L₁ M
n : ℕ
e : Fin n → M
ε : μ → M
injf : ∀ (k : ℕ), Function.Injective Φ.func
s₁ : Structure L₁ M
arity✝ : ℕ
a✝¹ : L₁.Func arity✝
a✝ : Fin arity✝ → Semiterm L₁ μ n
a_ih✝ :
  ∀ (a : Fin arity✝), Semiterm.val (extendStructure Φ s₁) e ε (Semiterm.lMap Φ (a✝ a)) = Semiterm.val s₁ e ε (a✝ a)
⊢ (func (Φ.func a✝¹) fun i => Semiterm.val s₁ e ε (a✝ i)) = func a✝¹ fun i => Semiterm.val s₁ e ε (a✝ i)

State before:
μ : Type u_1
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf✝ : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁✝ : Structure L₁ M
n : ℕ
e : Fin n → M
ε : μ → M
injf : ∀ (k : ℕ), Function.Injective Φ.func
s₁ : Structure L₁ M
k : ℕ
f : L₁.Func k
v : Fin k → Semiterm L₁ μ n
ih : ∀ (a : Fin k), Semiterm.val (extendStructure Φ s₁) e ε (Semiterm.lMap Φ (v a)) = Semiterm.val s₁ e ε (v a)
⊢ (func (Φ.func f) fun i => Semiterm.val s₁ e ε (v i)) = func f fun i => Semiterm.val s₁ e ε (v i)
Tactic:
case func k f v ih =>
  exact extendStructure.func Φ s₁ (injf k) f (fun i => Semiterm.val s₁ e ε (v i))
State after:
no goals

State before:
μ : Type u_1
L L₁ L₂ : Language
Φ : L₁ →ᵥ L₂
injf✝ : ∀ (k : ℕ), Function.Injective Φ.func
injr : ∀ (k : ℕ), Function.Injective Φ.rel
M : Type u
inst✝ : Nonempty M
s₁✝ : Structure L₁ M
n : ℕ
e : Fin n → M
ε : μ → M
injf : ∀ (k : ℕ), Function.Injective Φ.func
s₁ : Structure L₁ M
k : ℕ
f : L₁.Func k
v : Fin k → Semiterm L₁ μ n
ih : ∀ (a : Fin k), Semiterm.val (extendStructure Φ s₁) e ε (Semiterm.lMap Φ (v a)) = Semiterm.val s₁ e ε (v a)
⊢ (func (Φ.func f) fun i => Semiterm.val s₁ e ε (v i)) = func f fun i => Semiterm.val s₁ e ε (v i)
Tactic:
exact extendStructure.func Φ s₁ (injf k) f (fun i => Semiterm.val s₁ e ε (v i))
State after:
no goals