Theorem: LO.FirstOrder.Structure.Eq.eqv_funcExt (Logic/FirstOrder/Basic/Eq.lean)

State before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
f : L.Func k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
⊢ eqv L (func f v) (func f w)
Tactic:
have : M ⊧ₘ ∀* (Semiformula.vecEq varSumInL varSumInR ⟶ op(=).operator ![Semiterm.func f varSumInL, Semiterm.func f varSumInR]) :=
  H.realize (eqAxiom.funcExt f (L := L))
State after:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
f : L.Func k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
this : M ⊧ₘ ∀* (“(!(vecEq varSumInL varSumInR) → !!(Semiterm.func f varSumInL) = !!(Semiterm.func f varSumInR))”)
⊢ eqv L (func f v) (func f w)

State before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
f : L.Func k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
this : M ⊧ₘ ∀* (“(!(vecEq varSumInL varSumInR) → !!(Semiterm.func f varSumInL) = !!(Semiterm.func f varSumInR))”)
⊢ eqv L (func f v) (func f w)
Tactic:
simp [varSumInL, varSumInR, models_def, vecEq, Semiterm.val_func] at this
State after:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
f : L.Func k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
this :
  ∀ (e : Fin (k + k) → M),
    (∀ (i : Fin k), op(=).val ![e (Fin.castLE ⋯ i), e (Fin.natAdd k i)]) →
      op(=).val ![func f fun i => e (Fin.castLE ⋯ i), func f fun i => e (Fin.natAdd k i)]
⊢ eqv L (func f v) (func f w)

State before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
f : L.Func k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
this :
  ∀ (e : Fin (k + k) → M),
    (∀ (i : Fin k), op(=).val ![e (Fin.castLE ⋯ i), e (Fin.natAdd k i)]) →
      op(=).val ![func f fun i => e (Fin.castLE ⋯ i), func f fun i => e (Fin.natAdd k i)]
⊢ eqv L (func f v) (func f w)
Tactic:
simpa [Matrix.vecAppend_eq_ite] using this (Matrix.vecAppend rfl v w) (fun i => by simpa [Matrix.vecAppend_eq_ite] using h i)
State after:
no goals

State before:
L : Language
μ : Type u_1
inst✝² : Operator.Eq L
M : Type u
inst✝¹ : Nonempty M
inst✝ : Structure L M
H : M ⊧ₘ* 𝐄𝐐
k : ℕ
f : L.Func k
v w : Fin k → M
h : ∀ (i : Fin k), eqv L (v i) (w i)
this :
  ∀ (e : Fin (k + k) → M),
    (∀ (i : Fin k), op(=).val ![e (Fin.castLE ⋯ i), e (Fin.natAdd k i)]) →
      op(=).val ![func f fun i => e (Fin.castLE ⋯ i), func f fun i => e (Fin.natAdd k i)]
i : Fin k
⊢ op(=).val ![Matrix.vecAppend ⋯ v w (Fin.castLE ⋯ i), Matrix.vecAppend ⋯ v w (Fin.natAdd k i)]
Tactic:
simpa [Matrix.vecAppend_eq_ite] using h i
State after:
no goals