Theorem: LO.FirstOrder.Structure.extendStructure.eval_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
p : Semiformula L₁ μ n
⊢ (Eval (extendStructure Φ s₁) e ε) ((lMap Φ) p) ↔ (Eval s₁ e ε) p
Tactic:
induction p using Semiformula.rec' <;> simp[*, val_lMap Φ e ε injf s₁, Semiformula.lMap_rel, Semiformula.lMap_nrel, eval_rel, eval_nrel]
State after:
case hrel
μ : 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 : ℕ
ε : μ → M
n✝ k✝ : ℕ
r✝ : L₁.Rel k✝
v✝ : Fin k✝ → Semiterm L₁ μ n✝
e : Fin n✝ → M
⊢ (rel (Φ.rel r✝) fun i => Semiterm.val s₁ e ε (v✝ i)) ↔ rel r✝ fun i => Semiterm.val s₁ e ε (v✝ i)

case hnrel
μ : 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 : ℕ
ε : μ → M
n✝ k✝ : ℕ
r✝ : L₁.Rel k✝
v✝ : Fin k✝ → Semiterm L₁ μ n✝
e : Fin n✝ → M
⊢ (¬rel (Φ.rel r✝) fun i => Semiterm.val s₁ e ε (v✝ i)) ↔ ¬rel r✝ fun i => Semiterm.val s₁ e ε (v✝ 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 : ℕ
ε : μ → M
n✝ k : ℕ
r : L₁.Rel k
v : Fin k → Semiterm L₁ μ n✝
e : Fin n✝ → M
⊢ (rel (Φ.rel r) fun i => Semiterm.val s₁ e ε (v i)) ↔ rel r fun i => Semiterm.val s₁ e ε (v i)
Tactic:
case hrel k r v =>
exact extendStructure.rel Φ s₁ (injr k) r (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 : ℕ
ε : μ → M
n✝ k : ℕ
r : L₁.Rel k
v : Fin k → Semiterm L₁ μ n✝
e : Fin n✝ → M
⊢ (rel (Φ.rel r) fun i => Semiterm.val s₁ e ε (v i)) ↔ rel r fun i => Semiterm.val s₁ e ε (v i)
Tactic:
exact extendStructure.rel Φ s₁ (injr k) r (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 : ℕ
ε : μ → M
n✝ k : ℕ
r : L₁.Rel k
v : Fin k → Semiterm L₁ μ n✝
e : Fin n✝ → M
⊢ (¬rel (Φ.rel r) fun i => Semiterm.val s₁ e ε (v i)) ↔ ¬rel r fun i => Semiterm.val s₁ e ε (v i)
Tactic:
case hnrel k r v =>
simpa[not_iff_not] using
  extendStructure.rel Φ s₁ (injr k) r (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 : ℕ
ε : μ → M
n✝ k : ℕ
r : L₁.Rel k
v : Fin k → Semiterm L₁ μ n✝
e : Fin n✝ → M
⊢ (¬rel (Φ.rel r) fun i => Semiterm.val s₁ e ε (v i)) ↔ ¬rel r fun i => Semiterm.val s₁ e ε (v i)
Tactic:
simpa[not_iff_not] using
  extendStructure.rel Φ s₁ (injr k) r (fun i => Semiterm.val s₁ e ε (v i))
State after:
no goals