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

State before:
n : Name
oci : Option VConstant
env env' : VEnv
h : addConst env n oci = some env'
⊢ env ≤ env'
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 ≤ env'

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 ≤ env'
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
⊢ env ≤ { constants := fun n_1 => if n = n_1 then some oci else env.constants n_1, defeqs := env.defeqs }

State before:
case h_2.refl
n : Name
oci : Option VConstant
env : VEnv
x✝ : Option (Option VConstant)
heq✝ : env.constants n = none
⊢ env ≤ { constants := fun n_1 => if n = n_1 then some oci else env.constants n_1, defeqs := env.defeqs }
Tactic:
refine ⟨fun n ci h => ?_, fun _ => id⟩
State after:
case h_2.refl
n✝ : Name
oci : Option VConstant
env : VEnv
x✝ : Option (Option VConstant)
heq✝ : env.constants n✝ = none
n : Name
ci : Option VConstant
h : env.constants n = some ci
⊢ { constants := fun n => if n✝ = n then some oci else env.constants n, defeqs := env.defeqs }.constants n = some ci

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

State before:
case h_2.refl
n✝ : Name
oci : Option VConstant
env : VEnv
x✝ : Option (Option VConstant)
heq✝ : env.constants n✝ = none
n : Name
ci : Option VConstant
h : env.constants n = some ci
⊢ (if n✝ = n then some oci else env.constants n) = some ci
Tactic:
rwa [if_neg]
State after:
case h_2.refl.hnc
n✝ : Name
oci : Option VConstant
env : VEnv
x✝ : Option (Option VConstant)
heq✝ : env.constants n✝ = none
n : Name
ci : Option VConstant
h : env.constants n = some ci
⊢ ¬n✝ = n

State before:
case h_2.refl.hnc
n✝ : Name
oci : Option VConstant
env : VEnv
x✝ : Option (Option VConstant)
heq✝ : env.constants n✝ = none
n : Name
ci : Option VConstant
h : env.constants n = some ci
⊢ ¬n✝ = n
Tactic:
rintro rfl
State after:
case h_2.refl.hnc
n : Name
oci : Option VConstant
env : VEnv
x✝ : Option (Option VConstant)
heq✝ : env.constants n = none
ci : Option VConstant
h : env.constants n = some ci
⊢ False

State before:
case h_2.refl.hnc
n : Name
oci : Option VConstant
env : VEnv
x✝ : Option (Option VConstant)
heq✝ : env.constants n = none
ci : Option VConstant
h : env.constants n = some ci
⊢ False
Tactic:
cases h.symm.trans ‹_ = none›
State after:
no goals