Theorem: LO.FirstOrder.Semiterm.oringEmb_add (Logic/FirstOrder/Arith/Basic.lean)

State before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ lMap Language.oringEmb (op(+).operator v) = (‘(!!(lMap Language.oringEmb (v 0)) + !!(lMap Language.oringEmb (v 1)))’)
Tactic:
simp [lMap_func, Rew.func, Operator.operator, Operator.Add.term_eq, Matrix.empty_eq]
State after:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ (fun i => lMap Language.oringEmb (v i)) = fun i => ![lMap Language.oringEmb (v 0), lMap Language.oringEmb (v 1)] i

State before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ (fun i => lMap Language.oringEmb (v i)) = fun i => ![lMap Language.oringEmb (v 0), lMap Language.oringEmb (v 1)] i
Tactic:
funext i
State after:
case h
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
i : Fin 2
⊢ lMap Language.oringEmb (v i) = ![lMap Language.oringEmb (v 0), lMap Language.oringEmb (v 1)] i

State before:
case h
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
i : Fin 2
⊢ lMap Language.oringEmb (v i) = ![lMap Language.oringEmb (v 0), lMap Language.oringEmb (v 1)] i
Tactic:
cases i using Fin.cases <;> simp [Fin.eq_zero]
State after:
no goals