internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VLCtx.IsDefEq.fvars
Proof state before:
env : VEnv
U : Nat
Δ₁ Δ₂ : VLCtx
⊢ VLCtx.fvars [] = VLCtx.fvars []
Tactic:
simp
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.IsDefEq.fvars
Proof state before:
env : VEnv
U : Nat
Δ₁ Δ₂ : VLCtx
fv : FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
h1 : IsDefEq env U Δ₁✝ Δ₂✝
h2 : ∀ (fv_1 : FVarId), some fv = some fv_1 → ¬fv_1 ∈ VLCtx.fvars Δ₁✝
a✝ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
⊢ VLCtx.fvars ((some fv, d₁✝) :: Δ₁✝) = VLCtx.fvars ((some fv, d₂✝) :: Δ₂✝)
Tactic:
simp [h1.fvars]
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.IsDefEq.symm
Proof state before:
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
h1 : IsDefEq env U Δ₁✝ Δ₂✝
h2 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h3 : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
⊢ ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₂✝
Tactic:
simpa [h1.fvars] using h2
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq
Proof state before:
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁ e₂ A₂ : VExpr
hΔ : IsDefEq env U Δ₁ Δ₂
H1 : find? Δ₁ v = some (e₁, A₁)
H2 : find? Δ₂ v = some (e₂, A₂)
⊢ IsDefEqU env U (toCtx Δ₁) A₁ A₂ ∧ VEnv.IsDefEq env U (toCtx Δ₁) e₁ e₂ A₁
Tactic:
let .cons hΔ h1 h2 := hΔ
Proof state after:
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁ e₂ A₂ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2 : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
H1 : find? ((ofv✝, d₁✝) :: Δ₁✝) v = some (e₁, A₁)
H2 : find? ((ofv✝, d₂✝) :: Δ₂✝) v = some (e₂, A₂)
⊢ IsDefEqU env U (toCtx ((ofv✝, d₁✝) :: Δ₁✝)) A₁ A₂ ∧ VEnv.IsDefEq env U (toCtx ((ofv✝, d₁✝) :: Δ₁✝)) e₁ e₂ A₁
Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq
Proof state before:
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁✝ e₂ A₂✝ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2✝ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
A₁ A₂ : VExpr
u✝ : VLevel
h2 : VEnv.IsDefEq env U (toCtx Δ₁✝) A₁ A₂ (VExpr.sort u✝)
H1 : find? ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝) v = some (e₁, A₁✝)
H2 : find? ((ofv✝, VLocalDecl.vlam A₂) :: Δ₂✝) v = some (e₂, A₂✝)
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) A₁✝ A₂✝ ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) e₁ e₂ A₁✝
Tactic:
revert H1 H2
Proof state after:
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁✝ e₂ A₂✝ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2✝ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
A₁ A₂ : VExpr
u✝ : VLevel
h2 : VEnv.IsDefEq env U (toCtx Δ₁✝) A₁ A₂ (VExpr.sort u✝)
⊢ find? ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝) v = some (e₁, A₁✝) →
    find? ((ofv✝, VLocalDecl.vlam A₂) :: Δ₂✝) v = some (e₂, A₂✝) →
      IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) A₁✝ A₂✝ ∧
        VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) e₁ e₂ A₁✝
Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq
Proof state before:
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁✝ e₂ A₂✝ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2✝ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
A₁ A₂ : VExpr
u✝ : VLevel
h2 : VEnv.IsDefEq env U (toCtx Δ₁✝) A₁ A₂ (VExpr.sort u✝)
⊢ find? ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝) v = some (e₁, A₁✝) →
    find? ((ofv✝, VLocalDecl.vlam A₂) :: Δ₂✝) v = some (e₂, A₂✝) →
      IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) A₁✝ A₂✝ ∧
        VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) e₁ e₂ A₁✝
Tactic:
unfold VLCtx.find?
Proof state after:
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁✝ e₂ A₂✝ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2✝ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
A₁ A₂ : VExpr
u✝ : VLevel
h2 : VEnv.IsDefEq env U (toCtx Δ₁✝) A₁ A₂ (VExpr.sort u✝)
⊢ (match next ofv✝ v with
      | none => some (VLocalDecl.value (VLocalDecl.vlam A₁), VLocalDecl.type (VLocalDecl.vlam A₁))
      | some v => do
        let __discr ← find? Δ₁✝ v
        match __discr with
          | (e, A) =>
            some
              (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) e,
                VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) A)) =
      some (e₁, A₁✝) →
    (match next ofv✝ v with
        | none => some (VLocalDecl.value (VLocalDecl.vlam A₂), VLocalDecl.type (VLocalDecl.vlam A₂))
        | some v => do
          let __discr ← find? Δ₂✝ v
          match __discr with
            | (e, A) =>
              some
                (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) e,
                  VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) A)) =
        some (e₂, A₂✝) →
      IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) A₁✝ A₂✝ ∧
        VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) e₁ e₂ A₁✝
Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq
Proof state before:
case h_1
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁✝ e₂ A₂✝ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2✝ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
A₁ A₂ : VExpr
u✝ : VLevel
h2 : VEnv.IsDefEq env U (toCtx Δ₁✝) A₁ A₂ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
heq✝ : next ofv✝ v = none
⊢ some (VLocalDecl.value (VLocalDecl.vlam A₁), VLocalDecl.type (VLocalDecl.vlam A₁)) = some (e₁, A₁✝) →
    some (VLocalDecl.value (VLocalDecl.vlam A₂), VLocalDecl.type (VLocalDecl.vlam A₂)) = some (e₂, A₂✝) →
      IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) A₁✝ A₂✝ ∧
        VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) e₁ e₂ A₁✝
Tactic:
rintro ⟨⟩ ⟨⟩
Proof state after:
case h_1.refl.refl
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2✝ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
A₁ A₂ : VExpr
u✝ : VLevel
h2 : VEnv.IsDefEq env U (toCtx Δ₁✝) A₁ A₂ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
heq✝ : next ofv✝ v = none
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) (VLocalDecl.type (VLocalDecl.vlam A₁))
      (VLocalDecl.type (VLocalDecl.vlam A₂)) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) (VLocalDecl.value (VLocalDecl.vlam A₁))
      (VLocalDecl.value (VLocalDecl.vlam A₂)) (VLocalDecl.type (VLocalDecl.vlam A₁))
Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq
Proof state before:
case h_1.refl.refl
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2✝ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
A₁ A₂ : VExpr
u✝ : VLevel
h2 : VEnv.IsDefEq env U (toCtx Δ₁✝) A₁ A₂ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
heq✝ : next ofv✝ v = none
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) (VLocalDecl.type (VLocalDecl.vlam A₁))
      (VLocalDecl.type (VLocalDecl.vlam A₂)) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) (VLocalDecl.value (VLocalDecl.vlam A₁))
      (VLocalDecl.value (VLocalDecl.vlam A₂)) (VLocalDecl.type (VLocalDecl.vlam A₁))
Tactic:
exact ⟨⟨_, h2.weak henv⟩, .bvar .zero⟩
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq
Proof state before:
case h_2
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁✝ e₂ A₂✝ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2✝ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
A₁ A₂ : VExpr
u✝ : VLevel
h2 : VEnv.IsDefEq env U (toCtx Δ₁✝) A₁ A₂ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv✝ v = some v✝
⊢ (do
        let __discr ← find? Δ₁✝ v✝
        match __discr with
          | (e, A) =>
            some
              (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) e,
                VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) A)) =
      some (e₁, A₁✝) →
    (do
          let __discr ← find? Δ₂✝ v✝
          match __discr with
            | (e, A) =>
              some
                (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) e,
                  VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) A)) =
        some (e₂, A₂✝) →
      IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) A₁✝ A₂✝ ∧
        VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) e₁ e₂ A₁✝
Tactic:
simp [bind, Option.bind_eq_some]
Proof state after:
case h_2
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁✝ e₂ A₂✝ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2✝ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
A₁ A₂ : VExpr
u✝ : VLevel
h2 : VEnv.IsDefEq env U (toCtx Δ₁✝) A₁ A₂ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv✝ v = some v✝
⊢ ∀ (x : VExpr × VExpr),
    find? Δ₁✝ v✝ = some x →
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) x.fst = e₁ →
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) x.snd = A₁✝ →
          ∀ (x : VExpr × VExpr),
            find? Δ₂✝ v✝ = some x →
              VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) x.fst = e₂ →
                VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) x.snd = A₂✝ →
                  IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) A₁✝ A₂✝ ∧
                    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) e₁ e₂ A₁✝
Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq
Proof state before:
case h_2
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁✝ e₂ A₂✝ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2✝ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
A₁ A₂ : VExpr
u✝ : VLevel
h2 : VEnv.IsDefEq env U (toCtx Δ₁✝) A₁ A₂ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv✝ v = some v✝
⊢ ∀ (x : VExpr × VExpr),
    find? Δ₁✝ v✝ = some x →
      VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) x.fst = e₁ →
        VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) x.snd = A₁✝ →
          ∀ (x : VExpr × VExpr),
            find? Δ₂✝ v✝ = some x →
              VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) x.fst = e₂ →
                VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) x.snd = A₂✝ →
                  IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) A₁✝ A₂✝ ∧
                    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝)) e₁ e₂ A₁✝
Tactic:
rintro ⟨d₁', n₁'⟩ H1' rfl rfl ⟨d₂', n₂'⟩ H2' rfl rfl
Proof state after:
case h_2.mk.mk
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2✝ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
A₁ A₂ : VExpr
u✝ : VLevel
h2 : VEnv.IsDefEq env U (toCtx Δ₁✝) A₁ A₂ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv✝ v = some v✝
d₁' n₁' : VExpr
H1' : find? Δ₁✝ v✝ = some (d₁', n₁')
d₂' n₂' : VExpr
H2' : find? Δ₂✝ v✝ = some (d₂', n₂')
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').snd)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) (d₂', n₂').snd) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) (d₂', n₂').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').snd)
Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq
Proof state before:
case h_2.mk.mk
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2✝ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
A₁ A₂ : VExpr
u✝ : VLevel
h2 : VEnv.IsDefEq env U (toCtx Δ₁✝) A₁ A₂ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv✝ v = some v✝
d₁' n₁' : VExpr
H1' : find? Δ₁✝ v✝ = some (d₁', n₁')
d₂' n₂' : VExpr
H2' : find? Δ₂✝ v✝ = some (d₂', n₂')
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').snd)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) (d₂', n₂').snd) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) (d₂', n₂').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').snd)
Tactic:
obtain ⟨h2, h3⟩ := find?_uniq hΔ H1' H2'
Proof state after:
case h_2.mk.mk.intro
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2✝¹ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
A₁ A₂ : VExpr
u✝ : VLevel
h2✝ : VEnv.IsDefEq env U (toCtx Δ₁✝) A₁ A₂ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv✝ v = some v✝
d₁' n₁' : VExpr
H1' : find? Δ₁✝ v✝ = some (d₁', n₁')
d₂' n₂' : VExpr
H2' : find? Δ₂✝ v✝ = some (d₂', n₂')
h2 : IsDefEqU env U (toCtx Δ₁✝) n₁' n₂'
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) d₁' d₂' n₁'
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').snd)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) (d₂', n₂').snd) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) (d₂', n₂').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').snd)
Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq
Proof state before:
case h_2.mk.mk.intro
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2✝¹ : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
A₁ A₂ : VExpr
u✝ : VLevel
h2✝ : VEnv.IsDefEq env U (toCtx Δ₁✝) A₁ A₂ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
v✝ : Nat ⊕ FVarId
heq✝ : next ofv✝ v = some v✝
d₁' n₁' : VExpr
H1' : find? Δ₁✝ v✝ = some (d₁', n₁')
d₂' n₂' : VExpr
H2' : find? Δ₂✝ v✝ = some (d₂', n₂')
h2 : IsDefEqU env U (toCtx Δ₁✝) n₁' n₂'
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) d₁' d₂' n₁'
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').snd)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) (d₂', n₂').snd) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlam A₁) :: Δ₁✝))
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₂)) (d₂', n₂').fst)
      (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlam A₁)) (d₁', n₁').snd)
Tactic:
exact ⟨h2.weakN henv .one, h3.weak henv⟩
Proof state after:
no goals
Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq
Proof state before:
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁ e₂ A₂ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2 : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
value₁✝ value₂✝ type₁✝ type₂✝ : VExpr
u✝ : VLevel
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) value₁✝ value₂✝ type₁✝
h4 : VEnv.IsDefEq env U (toCtx Δ₁✝) type₁✝ type₂✝ (VExpr.sort u✝)
H1 : find? ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝) v = some (e₁, A₁)
H2 : find? ((ofv✝, VLocalDecl.vlet type₂✝ value₂✝) :: Δ₂✝) v = some (e₂, A₂)
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) A₁ A₂ ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) e₁ e₂ A₁
Tactic:
revert H1 H2
Proof state after:
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁ e₂ A₂ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2 : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
value₁✝ value₂✝ type₁✝ type₂✝ : VExpr
u✝ : VLevel
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) value₁✝ value₂✝ type₁✝
h4 : VEnv.IsDefEq env U (toCtx Δ₁✝) type₁✝ type₂✝ (VExpr.sort u✝)
⊢ find? ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝) v = some (e₁, A₁) →
    find? ((ofv✝, VLocalDecl.vlet type₂✝ value₂✝) :: Δ₂✝) v = some (e₂, A₂) →
      IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) A₁ A₂ ∧
        VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) e₁ e₂ A₁
Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq
Proof state before:
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁ e₂ A₂ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2 : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
value₁✝ value₂✝ type₁✝ type₂✝ : VExpr
u✝ : VLevel
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) value₁✝ value₂✝ type₁✝
h4 : VEnv.IsDefEq env U (toCtx Δ₁✝) type₁✝ type₂✝ (VExpr.sort u✝)
⊢ find? ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝) v = some (e₁, A₁) →
    find? ((ofv✝, VLocalDecl.vlet type₂✝ value₂✝) :: Δ₂✝) v = some (e₂, A₂) →
      IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) A₁ A₂ ∧
        VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) e₁ e₂ A₁
Tactic:
unfold VLCtx.find?
Proof state after:
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁ e₂ A₂ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2 : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
value₁✝ value₂✝ type₁✝ type₂✝ : VExpr
u✝ : VLevel
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) value₁✝ value₂✝ type₁✝
h4 : VEnv.IsDefEq env U (toCtx Δ₁✝) type₁✝ type₂✝ (VExpr.sort u✝)
⊢ (match next ofv✝ v with
      | none =>
        some (VLocalDecl.value (VLocalDecl.vlet type₁✝ value₁✝), VLocalDecl.type (VLocalDecl.vlet type₁✝ value₁✝))
      | some v => do
        let __discr ← find? Δ₁✝ v
        match __discr with
          | (e, A) =>
            some
              (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) e,
                VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₁✝ value₁✝)) A)) =
      some (e₁, A₁) →
    (match next ofv✝ v with
        | none =>
          some (VLocalDecl.value (VLocalDecl.vlet type₂✝ value₂✝), VLocalDecl.type (VLocalDecl.vlet type₂✝ value₂✝))
        | some v => do
          let __discr ← find? Δ₂✝ v
          match __discr with
            | (e, A) =>
              some
                (VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) e,
                  VExpr.liftN (VLocalDecl.depth (VLocalDecl.vlet type₂✝ value₂✝)) A)) =
        some (e₂, A₂) →
      IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) A₁ A₂ ∧
        VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) e₁ e₂ A₁
Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq
Proof state before:
case h_1
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
e₁ A₁ e₂ A₂ : VExpr
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2 : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
value₁✝ value₂✝ type₁✝ type₂✝ : VExpr
u✝ : VLevel
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) value₁✝ value₂✝ type₁✝
h4 : VEnv.IsDefEq env U (toCtx Δ₁✝) type₁✝ type₂✝ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
heq✝ : next ofv✝ v = none
⊢ some (VLocalDecl.value (VLocalDecl.vlet type₁✝ value₁✝), VLocalDecl.type (VLocalDecl.vlet type₁✝ value₁✝)) =
      some (e₁, A₁) →
    some (VLocalDecl.value (VLocalDecl.vlet type₂✝ value₂✝), VLocalDecl.type (VLocalDecl.vlet type₂✝ value₂✝)) =
        some (e₂, A₂) →
      IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) A₁ A₂ ∧
        VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝)) e₁ e₂ A₁
Tactic:
rintro ⟨⟩ ⟨⟩
Proof state after:
case h_1.refl.refl
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2 : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
value₁✝ value₂✝ type₁✝ type₂✝ : VExpr
u✝ : VLevel
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) value₁✝ value₂✝ type₁✝
h4 : VEnv.IsDefEq env U (toCtx Δ₁✝) type₁✝ type₂✝ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
heq✝ : next ofv✝ v = none
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝))
      (VLocalDecl.type (VLocalDecl.vlet type₁✝ value₁✝)) (VLocalDecl.type (VLocalDecl.vlet type₂✝ value₂✝)) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝))
      (VLocalDecl.value (VLocalDecl.vlet type₁✝ value₁✝)) (VLocalDecl.value (VLocalDecl.vlet type₂✝ value₂✝))
      (VLocalDecl.type (VLocalDecl.vlet type₁✝ value₁✝))
Theorem: Lean4Lean.VLCtx.IsDefEq.find?_uniq
Proof state before:
case h_1.refl.refl
env : VEnv
henv : Ordered env
U : Nat
Δ₁ Δ₂ : VLCtx
v : Nat ⊕ FVarId
hΔ✝ : IsDefEq env U Δ₁ Δ₂
ofv✝ : Option FVarId
d₁✝ d₂✝ : VLocalDecl
Δ₁✝ Δ₂✝ : VLCtx
hΔ : IsDefEq env U Δ₁✝ Δ₂✝
h1 : ∀ (fv : FVarId), ofv✝ = some fv → ¬fv ∈ VLCtx.fvars Δ₁✝
h2 : VLocalDecl.IsDefEq env U (toCtx Δ₁✝) d₁✝ d₂✝
value₁✝ value₂✝ type₁✝ type₂✝ : VExpr
u✝ : VLevel
h3 : VEnv.IsDefEq env U (toCtx Δ₁✝) value₁✝ value₂✝ type₁✝
h4 : VEnv.IsDefEq env U (toCtx Δ₁✝) type₁✝ type₂✝ (VExpr.sort u✝)
x✝ : Option (Nat ⊕ FVarId)
heq✝ : next ofv✝ v = none
⊢ IsDefEqU env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝))
      (VLocalDecl.type (VLocalDecl.vlet type₁✝ value₁✝)) (VLocalDecl.type (VLocalDecl.vlet type₂✝ value₂✝)) ∧
    VEnv.IsDefEq env U (toCtx ((ofv✝, VLocalDecl.vlet type₁✝ value₁✝) :: Δ₁✝))
      (VLocalDecl.value (VLocalDecl.vlet type₁✝ value₁✝)) (VLocalDecl.value (VLocalDecl.vlet type₂✝ value₂✝))
      (VLocalDecl.type (VLocalDecl.vlet type₁✝ value₁✝))
Tactic:
exact ⟨⟨_, h4⟩, h3⟩
Proof state after:
no goals