Theorem: LO.FirstOrder.Semiformula.oringEmb_eq (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) =
    (“!!(Semiterm.lMap Language.oringEmb (v 0)) = !!(Semiterm.lMap Language.oringEmb (v 1))”)
Tactic:
simp [lMap_rel, Rew.rel, Operator.operator, Operator.Eq.sentence_eq]
State after:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n : ℕ
v : Fin 2 → Semiterm ℒₒᵣ ξ n
⊢ (fun i => Semiterm.lMap Language.oringEmb (v i)) = fun i =>
    ![Semiterm.lMap Language.oringEmb (v 0), Semiterm.lMap Language.oringEmb (v 1)] i

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