Theorem: Lean4Lean.VEnv.addConst_self (Lean4Lean/Theory/Typing/Lemmas.lean)

State before:
n : Name
oci : Option VConstant
env env' : VEnv
h : addConst env n oci = some env'
⊢ env'.constants n = some oci
Tactic:
unfold addConst at h
State after:
n : Name
oci : Option VConstant
env env' : VEnv
h :
  (match env.constants n with
    | some val => none
    | none => some { constants := fun n_1 => if n = n_1 then some oci else env.constants n_1, defeqs := env.defeqs }) =
    some env'
⊢ env'.constants n = some oci

State before:
n : Name
oci : Option VConstant
env env' : VEnv
h :
  (match env.constants n with
    | some val => none
    | none => some { constants := fun n_1 => if n = n_1 then some oci else env.constants n_1, defeqs := env.defeqs }) =
    some env'
⊢ env'.constants n = some oci
Tactic:
split at h <;> cases h
State after:
case h_2.refl
n : Name
oci : Option VConstant
env : VEnv
x✝ : Option (Option VConstant)
heq✝ : env.constants n = none
⊢ { constants := fun n_1 => if n = n_1 then some oci else env.constants n_1, defeqs := env.defeqs }.constants n =
    some oci

State before:
case h_2.refl
n : Name
oci : Option VConstant
env : VEnv
x✝ : Option (Option VConstant)
heq✝ : env.constants n = none
⊢ { constants := fun n_1 => if n = n_1 then some oci else env.constants n_1, defeqs := env.defeqs }.constants n =
    some oci
Tactic:
simp
State after:
no goals