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

State before:
case empty
env : VEnv
n : Name
ci : VConstant
h : ∅.constants n = some (some ci)
⊢ VConstant.WF ∅ ci
Tactic:
cases h
State after:
no goals

State before:
case const
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 : addConst env✝ n✝ oci✝ = some env'✝
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
h : env'✝.constants n = some (some ci)
⊢ VConstant.WF env'✝ ci
Tactic:
refine .mono (addConst_le h3) ?_
State after:
case const
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 : addConst env✝ n✝ oci✝ = some env'✝
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
h : env'✝.constants n = some (some ci)
⊢ VConstant.WF env✝ ci

State before:
case const
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 : addConst env✝ n✝ oci✝ = some env'✝
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
h : env'✝.constants n = some (some ci)
⊢ VConstant.WF env✝ ci
Tactic:
unfold addConst at h3
State after:
case const
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 :
  (match env✝.constants n✝ with
    | some val => none
    | none => some { constants := fun n => if n✝ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }) =
    some env'✝
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
h : env'✝.constants n = some (some ci)
⊢ VConstant.WF env✝ ci

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

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

State before:
case const.h_2.refl
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h : (if n✝ = n then some oci✝ else env✝.constants n) = some (some ci)
⊢ VConstant.WF env✝ ci
Tactic:
split at h
State after:
case const.h_2.refl.inl
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h✝ : n✝ = n
h : some oci✝ = some (some ci)
⊢ VConstant.WF env✝ ci

case const.h_2.refl.inr
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h✝ : ¬n✝ = n
h : env✝.constants n = some (some ci)
⊢ VConstant.WF env✝ ci

State before:
case const.h_2.refl.inl
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h✝ : n✝ = n
h : some oci✝ = some (some ci)
⊢ VConstant.WF env✝ ci
Tactic:
cases h
State after:
case const.h_2.refl.inl.refl
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
n✝ : Name
a✝ : Ordered env✝
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h✝ : n✝ = n
h2 : ∀ (ci_1 : VConstant), some ci = some ci_1 → VConstant.WF env✝ ci_1
⊢ VConstant.WF env✝ ci

State before:
case const.h_2.refl.inl.refl
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
n✝ : Name
a✝ : Ordered env✝
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h✝ : n✝ = n
h2 : ∀ (ci_1 : VConstant), some ci = some ci_1 → VConstant.WF env✝ ci_1
⊢ VConstant.WF env✝ ci
Tactic:
exact h2 _ rfl
State after:
no goals

State before:
case const.h_2.refl.inr
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
a✝ : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
h✝ : ¬n✝ = n
h : env✝.constants n = some (some ci)
⊢ VConstant.WF env✝ ci
Tactic:
exact ih h
State after:
no goals

State before:
case defeq
env : VEnv
n : Name
ci : VConstant
env✝ : VEnv
df✝ : VDefEq
a✝¹ : Ordered env✝
a✝ : VDefEq.WF env✝ df✝
ih : env✝.constants n = some (some ci) → VConstant.WF env✝ ci
h : (addDefEq env✝ df✝).constants n = some (some ci)
⊢ VConstant.WF (addDefEq env✝ df✝) ci
Tactic:
exact .mono addDefEq_le (ih h)
State after:
no goals