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

State before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z : ℕ
⊢ lMap Language.oringEmb (‘0’) = ‘0’
Tactic:
exact oringEmb_zero
State after:
no goals

State before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z : ℕ
⊢ lMap Language.oringEmb (‘1’) = ‘1’
Tactic:
exact oringEmb_one
State after:
no goals

State before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
⊢ lMap Language.oringEmb (Operator.const (Operator.numeral ℒₒᵣ (z + 2))) = Operator.const (Operator.numeral L (z + 2))
Tactic:
simp [Operator.numeral_add_two]
State after:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
⊢ (‘(!!(lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![])) + !!(Operator.const op(1)))’) =
    op(+).operator fun x => (![Operator.numeral L (z + 1), op(1)] x).operator ![]

State before:
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
⊢ (‘(!!(lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![])) + !!(Operator.const op(1)))’) =
    op(+).operator fun x => (![Operator.numeral L (z + 1), op(1)] x).operator ![]
Tactic:
congr
State after:
case e_v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
⊢ ![lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![]), Operator.const op(1)] = fun x =>
    (![Operator.numeral L (z + 1), op(1)] x).operator ![]

State before:
case e_v
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
⊢ ![lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![]), Operator.const op(1)] = fun x =>
    (![Operator.numeral L (z + 1), op(1)] x).operator ![]
Tactic:
funext i
State after:
case e_v.h
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
i : Fin (Nat.succ 1)
⊢ ![lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![]), Operator.const op(1)] i =
    (![Operator.numeral L (z + 1), op(1)] i).operator ![]

State before:
case e_v.h
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
i : Fin (Nat.succ 1)
⊢ ![lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![]), Operator.const op(1)] i =
    (![Operator.numeral L (z + 1), op(1)] i).operator ![]
Tactic:
cases i using Fin.cases
State after:
case e_v.h.zero
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
⊢ ![lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![]), Operator.const op(1)] 0 =
    (![Operator.numeral L (z + 1), op(1)] 0).operator ![]

case e_v.h.succ
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
i✝ : Fin 1
⊢ ![lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![]), Operator.const op(1)] i✝.succ =
    (![Operator.numeral L (z + 1), op(1)] i✝.succ).operator ![]

State before:
case e_v.h.zero
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
⊢ ![lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![]), Operator.const op(1)] 0 =
    (![Operator.numeral L (z + 1), op(1)] 0).operator ![]
Tactic:
exact oringEmb_numeral (z + 1)
State after:
no goals

State before:
case e_v.h.succ
L : Language
inst✝ : L.ORing
ξ : Type u_1
n z✝ z : ℕ
i✝ : Fin 1
⊢ ![lMap Language.oringEmb (Operator.operator (Operator.numeral ℒₒᵣ (z + 1)) ![]), Operator.const op(1)] i✝.succ =
    (![Operator.numeral L (z + 1), op(1)] i✝.succ).operator ![]
Tactic:
simp
State after:
no goals