Theorem: Lean4Lean.VEnv.with_addConst (Lean4Lean/Theory/Typing/Meta.lean)

State before:
n : Name
ci : VConstant
f : VEnv → Option VEnv
P : Prop
env env' : VEnv
cis : List VObject
henv : Ordered env
hci : HasObjects env cis → VConstant.WF env ci
IH : ∀ {env1 : VEnv}, Ordered env1 → HasObjects env1 (VObject.const n (some ci) :: cis) → f env1 = some env' → P
hcis : HasObjects env cis
H : addConst env n (some ci) >>= f = some env'
⊢ P
Tactic:
let ⟨env1, h1, henv1⟩ := Option.bind_eq_some.1 H
State after:
n : Name
ci : VConstant
f : VEnv → Option VEnv
P : Prop
env env' : VEnv
cis : List VObject
henv : Ordered env
hci : HasObjects env cis → VConstant.WF env ci
IH : ∀ {env1 : VEnv}, Ordered env1 → HasObjects env1 (VObject.const n (some ci) :: cis) → f env1 = some env' → P
hcis : HasObjects env cis
H : addConst env n (some ci) >>= f = some env'
env1 : VEnv
h1 : addConst env n (some ci) = some env1
henv1 : f env1 = some env'
⊢ P

State before:
n : Name
ci : VConstant
f : VEnv → Option VEnv
P : Prop
env env' : VEnv
cis : List VObject
henv : Ordered env
hci : HasObjects env cis → VConstant.WF env ci
IH : ∀ {env1 : VEnv}, Ordered env1 → HasObjects env1 (VObject.const n (some ci) :: cis) → f env1 = some env' → P
hcis : HasObjects env cis
H : addConst env n (some ci) >>= f = some env'
env1 : VEnv
h1 : addConst env n (some ci) = some env1
henv1 : f env1 = some env'
⊢ P
Tactic:
refine IH (.const henv (by rintro _ ⟨⟩; exact hci hcis) h1) (hcis.const h1) henv1
State after:
no goals

State before:
n : Name
ci : VConstant
f : VEnv → Option VEnv
P : Prop
env env' : VEnv
cis : List VObject
henv : Ordered env
hci : HasObjects env cis → VConstant.WF env ci
IH : ∀ {env1 : VEnv}, Ordered env1 → HasObjects env1 (VObject.const n (some ci) :: cis) → f env1 = some env' → P
hcis : HasObjects env cis
H : addConst env n (some ci) >>= f = some env'
env1 : VEnv
h1 : addConst env n (some ci) = some env1
henv1 : f env1 = some env'
⊢ ∀ (ci_1 : VConstant), some ci = some ci_1 → VConstant.WF env ci_1
Tactic:
rintro _ ⟨⟩
State after:
case refl
n : Name
ci : VConstant
f : VEnv → Option VEnv
P : Prop
env env' : VEnv
cis : List VObject
henv : Ordered env
hci : HasObjects env cis → VConstant.WF env ci
IH : ∀ {env1 : VEnv}, Ordered env1 → HasObjects env1 (VObject.const n (some ci) :: cis) → f env1 = some env' → P
hcis : HasObjects env cis
H : addConst env n (some ci) >>= f = some env'
env1 : VEnv
h1 : addConst env n (some ci) = some env1
henv1 : f env1 = some env'
⊢ VConstant.WF env ci

State before:
case refl
n : Name
ci : VConstant
f : VEnv → Option VEnv
P : Prop
env env' : VEnv
cis : List VObject
henv : Ordered env
hci : HasObjects env cis → VConstant.WF env ci
IH : ∀ {env1 : VEnv}, Ordered env1 → HasObjects env1 (VObject.const n (some ci) :: cis) → f env1 = some env' → P
hcis : HasObjects env cis
H : addConst env n (some ci) >>= f = some env'
env1 : VEnv
h1 : addConst env n (some ci) = some env1
henv1 : f env1 = some env'
⊢ VConstant.WF env ci
Tactic:
exact hci hcis
State after:
no goals