internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.Lookup.weak'_iff
Proof state before:
l : Lift
Γ Γ' : List VExpr
i : Nat
A : VExpr
W : Ctx.Lift' l Γ Γ'
n : Nat
e : Lift.depth l = n
⊢ Lookup Γ' (Lift.liftVar l i) (lift' A l) ↔ Lookup Γ i A
Tactic:
induction n generalizing l Γ' with
| zero => rw [liftVar_depth_zero e, VExpr.lift'_depth_zero e, W.depth_zero e]
| succ n ih =>
  obtain ⟨l, k, rfl, rfl⟩ := Lift.depth_succ e
  have ⟨Γ₁, W1, W2⟩ := W.of_cons_skip
  rw [Lift.consN_skip_eq, liftVar_comp, liftVar_consN_skipN, lift'_comp, lift'_consN_skipN,
    weakN_iff W2, ih W1 Lift.depth_consN]
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.weak'_iff
Proof state before:
case zero
Γ : List VExpr
i : Nat
A : VExpr
l : Lift
Γ' : List VExpr
W : Ctx.Lift' l Γ Γ'
e : Lift.depth l = Nat.zero
⊢ Lookup Γ' (Lift.liftVar l i) (lift' A l) ↔ Lookup Γ i A
Tactic:
rw [liftVar_depth_zero e, VExpr.lift'_depth_zero e, W.depth_zero e]
Proof state after:
no goals
Theorem: Lean4Lean.Lookup.weak'_iff
Proof state before:
case succ
Γ : List VExpr
i : Nat
A : VExpr
n : Nat
ih :
  ∀ {l : Lift} {Γ' : List VExpr},
    Ctx.Lift' l Γ Γ' → Lift.depth l = n → (Lookup Γ' (Lift.liftVar l i) (lift' A l) ↔ Lookup Γ i A)
l : Lift
Γ' : List VExpr
W : Ctx.Lift' l Γ Γ'
e : Lift.depth l = Nat.succ n
⊢ Lookup Γ' (Lift.liftVar l i) (lift' A l) ↔ Lookup Γ i A
Tactic:
obtain ⟨l, k, rfl, rfl⟩ := Lift.depth_succ e
Proof state after:
case succ.intro.intro.intro
Γ : List VExpr
i : Nat
A : VExpr
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → (Lookup Γ' (Lift.liftVar l_1 i) (lift' A l_1) ↔ Lookup Γ i A)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
⊢ Lookup Γ' (Lift.liftVar (Lift.consN (Lift.skip l) k) i) (lift' A (Lift.consN (Lift.skip l) k)) ↔ Lookup Γ i A
Theorem: Lean4Lean.Lookup.weak'_iff
Proof state before:
case succ.intro.intro.intro
Γ : List VExpr
i : Nat
A : VExpr
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → (Lookup Γ' (Lift.liftVar l_1 i) (lift' A l_1) ↔ Lookup Γ i A)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
⊢ Lookup Γ' (Lift.liftVar (Lift.consN (Lift.skip l) k) i) (lift' A (Lift.consN (Lift.skip l) k)) ↔ Lookup Γ i A
Tactic:
have ⟨Γ₁, W1, W2⟩ := W.of_cons_skip
Proof state after:
case succ.intro.intro.intro
Γ : List VExpr
i : Nat
A : VExpr
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → (Lookup Γ' (Lift.liftVar l_1 i) (lift' A l_1) ↔ Lookup Γ i A)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
Γ₁ : List VExpr
W1 : Ctx.Lift' (Lift.consN l k) Γ Γ₁
W2 : Ctx.LiftN 1 k Γ₁ Γ'
⊢ Lookup Γ' (Lift.liftVar (Lift.consN (Lift.skip l) k) i) (lift' A (Lift.consN (Lift.skip l) k)) ↔ Lookup Γ i A
Theorem: Lean4Lean.Lookup.weak'_iff
Proof state before:
case succ.intro.intro.intro
Γ : List VExpr
i : Nat
A : VExpr
Γ' : List VExpr
l : Lift
k : Nat
ih :
  ∀ {l_1 : Lift} {Γ' : List VExpr},
    Ctx.Lift' l_1 Γ Γ' → Lift.depth l_1 = Lift.depth l → (Lookup Γ' (Lift.liftVar l_1 i) (lift' A l_1) ↔ Lookup Γ i A)
W : Ctx.Lift' (Lift.consN (Lift.skip l) k) Γ Γ'
e : Lift.depth (Lift.consN (Lift.skip l) k) = Nat.succ (Lift.depth l)
Γ₁ : List VExpr
W1 : Ctx.Lift' (Lift.consN l k) Γ Γ₁
W2 : Ctx.LiftN 1 k Γ₁ Γ'
⊢ Lookup Γ' (Lift.liftVar (Lift.consN (Lift.skip l) k) i) (lift' A (Lift.consN (Lift.skip l) k)) ↔ Lookup Γ i A
Tactic:
rw [Lift.consN_skip_eq, liftVar_comp, liftVar_consN_skipN, lift'_comp, lift'_consN_skipN,
  weakN_iff W2, ih W1 Lift.depth_consN]
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.LiftN.right
Proof state before:
Γ : List VExpr
h : CtxClosed Γ
Γ' : List VExpr
x✝ : CtxClosed []
⊢ LiftN (List.length Γ') (List.length []) [] ([] ++ Γ')
Tactic:
simpa using LiftN.zero (Γ := []) Γ'
Proof state after:
no goals
Theorem: Lean4Lean.Ctx.LiftN.right
Proof state before:
Γ✝ : List VExpr
h : CtxClosed Γ✝
Γ' : List VExpr
A : VExpr
Γ : List VExpr
h1 : OnCtx Γ fun Γ A => ClosedN A (List.length Γ)
h2 : (fun Γ A => ClosedN A (List.length Γ)) Γ A
⊢ LiftN (List.length Γ') (List.length (A :: Γ)) (A :: Γ) (A :: Γ ++ Γ')
Tactic:
simpa [h2.liftN_eq (Nat.le_refl _)] using LiftN.succ (LiftN.right h1 Γ') (A := A)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.addConst_le
Proof state before:
n : Name
oci : Option VConstant
env env' : VEnv
h : addConst env n oci = some env'
⊢ env ≤ env'
Tactic:
unfold addConst at h
Proof 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'
Theorem: Lean4Lean.VEnv.addConst_le
Proof 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
Proof 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 }
Theorem: Lean4Lean.VEnv.addConst_le
Proof 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⟩
Proof 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
Theorem: Lean4Lean.VEnv.addConst_le
Proof 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
Proof 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
Theorem: Lean4Lean.VEnv.addConst_le
Proof 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]
Proof 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
Theorem: Lean4Lean.VEnv.addConst_le
Proof 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
Proof 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
Theorem: Lean4Lean.VEnv.addConst_le
Proof 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›
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.addConst_self
Proof 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
Proof 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
Theorem: Lean4Lean.VEnv.addConst_self
Proof 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
Proof 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
Theorem: Lean4Lean.VEnv.addConst_self
Proof 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
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.addDefEq_le
Proof state before:
df✝ : VDefEq
env : VEnv
df : VDefEq
h : env.defeqs df
⊢ (addDefEq env df✝).defeqs df
Tactic:
simp [addDefEq, h]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.Ordered.induction
Proof state before:
case empty
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
⊢ OnTypes ∅ (motive ∅)
Tactic:
exact ⟨nofun, nofun⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.Ordered.induction
Proof state before:
case const
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 : addConst env✝ n✝ oci✝ = some env'✝
ih : OnTypes env✝ (motive env✝)
⊢ OnTypes env'✝ (motive env'✝)
Tactic:
apply OnTypes.mono .rfl (mono (addConst_le h3))
Proof state after:
case const
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 : addConst env✝ n✝ oci✝ = some env'✝
ih : OnTypes env✝ (motive env✝)
⊢ OnTypes env'✝ fun {U} {e A} => motive env✝ U e A
Theorem: Lean4Lean.VEnv.Ordered.induction
Proof state before:
case const
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
h3 : addConst env✝ n✝ oci✝ = some env'✝
ih : OnTypes env✝ (motive env✝)
⊢ OnTypes env'✝ fun {U} {e A} => motive env✝ U e A
Tactic:
unfold addConst at h3
Proof state after:
case const
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
h1 : 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 : OnTypes env✝ (motive env✝)
⊢ OnTypes env'✝ fun {U} {e A} => motive env✝ U e A
Theorem: Lean4Lean.VEnv.Ordered.induction
Proof state before:
case const
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
env'✝ : VEnv
h1 : 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 : OnTypes env✝ (motive env✝)
⊢ OnTypes env'✝ fun {U} {e A} => motive env✝ U e A
Tactic:
split at h3 <;> cases h3
Proof state after:
case const.h_2.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
⊢ OnTypes { constants := fun n => if n✝ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }
    fun {U} {e A} => motive env✝ U e A
Theorem: Lean4Lean.VEnv.Ordered.induction
Proof state before:
case const.h_2.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝ = none
⊢ OnTypes { constants := fun n => if n✝ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }
    fun {U} {e A} => motive env✝ U e A
Tactic:
refine ⟨fun h => ?_, ih.2⟩
Proof state after:
case const.h_2.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝¹ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h :
  { constants := fun n => if n✝¹ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }.constants n✝ =
    some (some ci✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A
Theorem: Lean4Lean.VEnv.Ordered.induction
Proof state before:
case const.h_2.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝¹ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h :
  { constants := fun n => if n✝¹ = n then some oci✝ else env✝.constants n, defeqs := env✝.defeqs }.constants n✝ =
    some (some ci✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A
Tactic:
simp at h
Proof state after:
case const.h_2.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝¹ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h : (if n✝¹ = n✝ then some oci✝ else env✝.constants n✝) = some (some ci✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A
Theorem: Lean4Lean.VEnv.Ordered.induction
Proof state before:
case const.h_2.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝¹ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h : (if n✝¹ = n✝ then some oci✝ else env✝.constants n✝) = some (some ci✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A
Tactic:
split at h
Proof state after:
case const.h_2.refl.inl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝¹ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h✝ : n✝¹ = n✝
h : some oci✝ = some (some ci✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A

case const.h_2.refl.inr
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝¹ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h✝ : ¬n✝¹ = n✝
h : env✝.constants n✝ = some (some ci✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A
Theorem: Lean4Lean.VEnv.Ordered.induction
Proof state before:
case const.h_2.refl.inl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝¹ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h✝ : n✝¹ = n✝
h : some oci✝ = some (some ci✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A
Tactic:
cases h
Proof state after:
case const.h_2.refl.inl.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
n✝¹ : Name
h1 : Ordered env✝
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h✝ : n✝¹ = n✝
h2 : ∀ (ci : VConstant), some ci✝ = some ci → VConstant.WF env✝ ci
⊢ Exists fun u {U} {e A} => motive env✝ U e A
Theorem: Lean4Lean.VEnv.Ordered.induction
Proof state before:
case const.h_2.refl.inl.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
n✝¹ : Name
h1 : Ordered env✝
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h✝ : n✝¹ = n✝
h2 : ∀ (ci : VConstant), some ci✝ = some ci → VConstant.WF env✝ ci
⊢ Exists fun u {U} {e A} => motive env✝ U e A
Tactic:
let ⟨_, ht⟩ := h2 _ rfl
Proof state after:
case const.h_2.refl.inl.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
n✝¹ : Name
h1 : Ordered env✝
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h✝ : n✝¹ = n✝
h2 : ∀ (ci : VConstant), some ci✝ = some ci → VConstant.WF env✝ ci
w✝ : VLevel
ht : HasType env✝ ci✝.uvars [] ci✝.type (sort w✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A
Theorem: Lean4Lean.VEnv.Ordered.induction
Proof state before:
case const.h_2.refl.inl.refl
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
n✝¹ : Name
h1 : Ordered env✝
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h✝ : n✝¹ = n✝
h2 : ∀ (ci : VConstant), some ci✝ = some ci → VConstant.WF env✝ ci
w✝ : VLevel
ht : HasType env✝ ci✝.uvars [] ci✝.type (sort w✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A
Tactic:
exact ⟨_, type h1 ih ht⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.Ordered.induction
Proof state before:
case const.h_2.refl.inr
env : VEnv
motive : VEnv → Nat → VExpr → VExpr → Prop
mono : ∀ {env env' : VEnv} {U : Nat} {e A : VExpr}, env ≤ env' → motive env U e A → motive env' U e A
type :
  ∀ {env : VEnv} {U : Nat} {e A : VExpr},
    Ordered env → OnTypes env (motive env) → HasType env U [] e A → motive env U e A
env✝ : VEnv
oci✝ : Option VConstant
n✝¹ : Name
h1 : Ordered env✝
h2 : ∀ (ci : VConstant), oci✝ = some ci → VConstant.WF env✝ ci
ih : OnTypes env✝ (motive env✝)
x✝ : Option (Option VConstant)
heq✝ : env✝.constants n✝¹ = none
n✝ : Name
ci✝ : VConstant
h✝ : ¬n✝¹ = n✝
h : env✝.constants n✝ = some (some ci✝)
⊢ Exists fun u {U} {e A} => motive env✝ U e A
Tactic:
exact ih.1 h
Proof state after:
no goals