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

State before:
case empty
env : VEnv
df : VDefEq
h : ∅.defeqs df
⊢ VDefEq.WF ∅ df
Tactic:
cases h
State after:
no goals

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

State before:
case const
env : VEnv
df : VDefEq
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
a✝¹ : Ordered env✝
a✝ : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 : addConst env✝ n✝ oci✝ = some env'✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
h : env'✝.defeqs df
⊢ env✝.defeqs df
Tactic:
unfold addConst at h3
State after:
case const
env : VEnv
df : VDefEq
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
a✝¹ : Ordered env✝
a✝ : ∀ (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✝.defeqs df → VDefEq.WF env✝ df
h : env'✝.defeqs df
⊢ env✝.defeqs df

State before:
case const
env : VEnv
df : VDefEq
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
a✝¹ : Ordered env✝
a✝ : ∀ (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✝.defeqs df → VDefEq.WF env✝ df
h : env'✝.defeqs df
⊢ env✝.defeqs df
Tactic:
split at h3 <;> cases h3
State after:
case const.h_2.refl
env : VEnv
df : VDefEq
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
a✝¹ : Ordered env✝
a✝ : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : env✝.defeqs df → VDefEq.WF env✝ df
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 }.defeqs df
⊢ env✝.defeqs df

State before:
case const.h_2.refl
env : VEnv
df : VDefEq
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
a✝¹ : Ordered env✝
a✝ : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : env✝.defeqs df → VDefEq.WF env✝ df
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 }.defeqs df
⊢ env✝.defeqs df
Tactic:
exact h
State after:
no goals

State before:
case defeq
env : VEnv
df : VDefEq
env✝ : VEnv
df✝ : VDefEq
a✝¹ : Ordered env✝
a✝ : VDefEq.WF env✝ df✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
h : (addDefEq env✝ df✝).defeqs df
⊢ VDefEq.WF (addDefEq env✝ df✝) df
Tactic:
refine .mono addDefEq_le ?_
State after:
case defeq
env : VEnv
df : VDefEq
env✝ : VEnv
df✝ : VDefEq
a✝¹ : Ordered env✝
a✝ : VDefEq.WF env✝ df✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
h : (addDefEq env✝ df✝).defeqs df
⊢ VDefEq.WF env✝ df

State before:
case defeq
env : VEnv
df : VDefEq
env✝ : VEnv
df✝ : VDefEq
a✝¹ : Ordered env✝
a✝ : VDefEq.WF env✝ df✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
h : (addDefEq env✝ df✝).defeqs df
⊢ VDefEq.WF env✝ df
Tactic:
obtain rfl | h := h
State after:
case defeq.inl
env : VEnv
df : VDefEq
env✝ : VEnv
a✝¹ : Ordered env✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
a✝ : VDefEq.WF env✝ df
⊢ VDefEq.WF env✝ df

case defeq.inr
env : VEnv
df : VDefEq
env✝ : VEnv
df✝ : VDefEq
a✝¹ : Ordered env✝
a✝ : VDefEq.WF env✝ df✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
h : env✝.defeqs df
⊢ VDefEq.WF env✝ df

State before:
case defeq.inl
env : VEnv
df : VDefEq
env✝ : VEnv
a✝¹ : Ordered env✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
a✝ : VDefEq.WF env✝ df
⊢ VDefEq.WF env✝ df
Tactic:
assumption
State after:
no goals

State before:
case defeq.inr
env : VEnv
df : VDefEq
env✝ : VEnv
df✝ : VDefEq
a✝¹ : Ordered env✝
a✝ : VDefEq.WF env✝ df✝
ih : env✝.defeqs df → VDefEq.WF env✝ df
h : env✝.defeqs df
⊢ VDefEq.WF env✝ df
Tactic:
exact ih h
State after:
no goals