Theorem: LO.FirstOrder.Semiterm.oringEmb_mul (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.Mul.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