internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEq.const_inv'
Proof state before:
case symm
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V : VExpr
c : Name
ls : List VLevel
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ e✝ e'✝ A✝
ih :
  e✝ = VExpr.const c ls ∨ e'✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
eq : e'✝ = VExpr.const c ls ∨ e✝ = VExpr.const c ls
⊢ ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
Tactic:
exact ih eq.symm
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.const_inv'
Proof state before:
case extra
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V : VExpr
c : Name
ls : List VLevel
df✝ : VDefEq
ls✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
a✝⁸ : env.defeqs df✝
a✝⁷ : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝⁶ : List.length ls✝ = df✝.uvars
a✝⁵ : VLevel.WF U u✝
a✝⁴ : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.type) (VExpr.instL ls✝ df✝.type) (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
a✝² : IsDefEqStrong env U [] (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a✝¹ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.lhs) (VExpr.instL ls✝ df✝.type)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.rhs) (VExpr.instL ls✝ df✝.type)
a_ih✝² :
  VExpr.instL ls✝ df✝.type = VExpr.const c ls ∨ VExpr.instL ls✝ df✝.type = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝¹ :
  VExpr.instL ls✝ df✝.lhs = VExpr.const c ls ∨ VExpr.instL ls✝ df✝.lhs = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝ :
  VExpr.instL ls✝ df✝.rhs = VExpr.const c ls ∨ VExpr.instL ls✝ df✝.rhs = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
ih1 :
  VExpr.instL ls✝ df✝.lhs = VExpr.const c ls ∨ VExpr.instL ls✝ df✝.lhs = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
ih2 :
  VExpr.instL ls✝ df✝.rhs = VExpr.const c ls ∨ VExpr.instL ls✝ df✝.rhs = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
eq : VExpr.instL ls✝ df✝.lhs = VExpr.const c ls ∨ VExpr.instL ls✝ df✝.rhs = VExpr.const c ls
⊢ ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
Tactic:
obtain eq | eq := eq <;> [exact ih1 (.inl eq); exact ih2 (.inr eq)]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.const_inv'
Proof state before:
case constDF.inl.refl
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V : VExpr
c : Name
ls : List VLevel
ci✝ : VConstant
ls'✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h3 : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
a✝⁴ : VLevel.WF U u✝
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (VExpr.sort u✝)
a✝² : IsDefEqStrong env U Γ✝ (VExpr.instL ls'✝ ci✝.type) (VExpr.instL ls'✝ ci✝.type) (VExpr.sort u✝)
a_ih✝³ a_ih✝² :
  VExpr.instL ls'✝ ci✝.type = VExpr.const c ls ∨ VExpr.instL ls'✝ ci✝.type = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
h1 : env.constants c = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
h4 : List.length ls = ci✝.uvars
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls ls'✝
a✝¹ : IsDefEqStrong env U [] (VExpr.instL ls ci✝.type) (VExpr.instL ls ci✝.type) (VExpr.sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls ci✝.type) (VExpr.instL ls ci✝.type) (VExpr.sort u✝)
a_ih✝¹ a_ih✝ :
  VExpr.instL ls ci✝.type = VExpr.const c ls ∨ VExpr.instL ls ci✝.type = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
⊢ ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
Tactic:
exact ⟨_, h1, h2, h4⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.const_inv'
Proof state before:
case constDF.inr.refl
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V : VExpr
c : Name
ls : List VLevel
ci✝ : VConstant
ls✝ : List VLevel
u✝ : VLevel
Γ✝ : List VExpr
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
h4 : List.length ls✝ = ci✝.uvars
a✝⁴ : VLevel.WF U u✝
a✝³ : IsDefEqStrong env U [] (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (VExpr.sort u✝)
a✝² : IsDefEqStrong env U Γ✝ (VExpr.instL ls✝ ci✝.type) (VExpr.instL ls✝ ci✝.type) (VExpr.sort u✝)
a_ih✝³ a_ih✝² :
  VExpr.instL ls✝ ci✝.type = VExpr.const c ls ∨ VExpr.instL ls✝ ci✝.type = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
h1 : env.constants c = some (some ci✝)
h3 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
h5 : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls
a✝¹ : IsDefEqStrong env U [] (VExpr.instL ls ci✝.type) (VExpr.instL ls ci✝.type) (VExpr.sort u✝)
a✝ : IsDefEqStrong env U Γ✝ (VExpr.instL ls ci✝.type) (VExpr.instL ls ci✝.type) (VExpr.sort u✝)
a_ih✝¹ a_ih✝ :
  VExpr.instL ls ci✝.type = VExpr.const c ls ∨ VExpr.instL ls ci✝.type = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
⊢ ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
Tactic:
exact ⟨_, h1, h3, h5.length_eq.symm.trans h4⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.const_inv'
Proof state before:
case defeqDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V : VExpr
c : Name
ls : List VLevel
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
a✝² : VLevel.WF U u✝
a✝¹ : IsDefEqStrong env U Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : IsDefEqStrong env U Γ✝ e1✝ e2✝ A✝
a_ih✝ :
  A✝ = VExpr.const c ls ∨ B✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
ih2 :
  e1✝ = VExpr.const c ls ∨ e2✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
eq : e1✝ = VExpr.const c ls ∨ e2✝ = VExpr.const c ls
⊢ ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
Tactic:
exact ih2 eq
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.const_inv'
Proof state before:
case beta.inr
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V : VExpr
c : Name
ls : List VLevel
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ e'✝ : VExpr
a✝⁷ : VLevel.WF U u✝
a✝⁶ : VLevel.WF U v✝
a✝⁵ : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝⁴ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) e✝ e✝ B✝
a✝² : IsDefEqStrong env U Γ✝ e'✝ e'✝ A✝
a✝¹ : IsDefEqStrong env U Γ✝ (inst B✝ e'✝) (inst B✝ e'✝) (VExpr.sort v✝)
a✝ : IsDefEqStrong env U Γ✝ (inst e✝ e'✝) (inst e✝ e'✝) (inst B✝ e'✝)
a_ih✝⁴ :
  A✝ = VExpr.const c ls ∨ A✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝³ :
  B✝ = VExpr.const c ls ∨ B✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝² :
  e✝ = VExpr.const c ls ∨ e✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝¹ :
  e'✝ = VExpr.const c ls ∨ e'✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝ :
  inst B✝ e'✝ = VExpr.const c ls ∨ inst B✝ e'✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
ihee :
  inst e✝ e'✝ = VExpr.const c ls ∨ inst e✝ e'✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
eq : inst e✝ e'✝ = VExpr.const c ls
⊢ ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
Tactic:
exact ihee (.inl eq)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.const_inv'
Proof state before:
case eta.inr
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V : VExpr
c : Name
ls : List VLevel
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
e✝ : VExpr
a✝⁶ : VLevel.WF U u✝
a✝⁵ : VLevel.WF U v✝
a✝⁴ : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a✝³ : IsDefEqStrong env U (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
a✝² : IsDefEqStrong env U (lift A✝ :: A✝ :: Γ✝) (liftN 1 B✝ 1) (liftN 1 B✝ 1) (VExpr.sort v✝)
a✝¹ : IsDefEqStrong env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
a✝ : IsDefEqStrong env U (A✝ :: Γ✝) (lift e✝) (lift e✝) (VExpr.forallE (lift A✝) (liftN 1 B✝ 1))
a_ih✝³ :
  A✝ = VExpr.const c ls ∨ A✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝² :
  B✝ = VExpr.const c ls ∨ B✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝¹ :
  liftN 1 B✝ 1 = VExpr.const c ls ∨ liftN 1 B✝ 1 = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
ih :
  e✝ = VExpr.const c ls ∨ e✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝ :
  lift e✝ = VExpr.const c ls ∨ lift e✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
eq : e✝ = VExpr.const c ls
⊢ ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
Tactic:
exact ih (.inl eq)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.const_inv'
Proof state before:
case forallEDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 V : VExpr
c : Name
ls : List VLevel
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝⁴ : VLevel.WF U u✝
a✝³ : VLevel.WF U v✝
a✝² : IsDefEqStrong env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝¹ : IsDefEqStrong env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
a✝ : IsDefEqStrong env U (A'✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
a_ih✝² :
  A✝ = VExpr.const c ls ∨ A'✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
a_ih✝¹ a_ih✝ :
  body✝ = VExpr.const c ls ∨ body'✝ = VExpr.const c ls →
    ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
eq : VExpr.forallE A✝ body✝ = VExpr.const c ls ∨ VExpr.forallE A'✝ body'✝ = VExpr.const c ls
⊢ ∃ ci, env.constants c = some (some ci) ∧ (∀ (l : VLevel), l ∈ ls → VLevel.WF U l) ∧ List.length ls = ci.uvars
Tactic:
nomatch eq
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.addQuot_WF
Proof state before:
env env' : VEnv
henv : Ordered env
hq : QuotReady env
⊢ addQuot env = some env' → Ordered env'
Tactic:
refine with_addConst (cis := [.const _ eqConst]) (hcis := ⟨hq, ⟨⟩⟩) henv
  (fun _ => ⟨_, by type_tac⟩) fun henv => ?_
Proof state after:
env env' : VEnv
henv✝ : Ordered env
hq : QuotReady env
env1✝ : VEnv
henv : Ordered env1✝
⊢ HasObjects env1✝ [VObject.const `Quot (some quotConst), VObject.const `Eq (some eqConst)] →
    (do
          let env ← addConst env1✝ `Quot.mk (some quotMkConst)
          let env ← addConst env `Quot.ind (some quotIndConst)
          let env ← addConst env `Quot.lift (some quotLiftConst)
          some (addDefEq env quotDefEq)) =
        some env' →
      Ordered env'
Theorem: Lean4Lean.VEnv.addQuot_WF
Proof state before:
env env' : VEnv
henv✝ : Ordered env
hq : QuotReady env
env1✝ : VEnv
henv : Ordered env1✝
⊢ HasObjects env1✝ [VObject.const `Quot (some quotConst), VObject.const `Eq (some eqConst)] →
    (do
          let env ← addConst env1✝ `Quot.mk (some quotMkConst)
          let env ← addConst env `Quot.ind (some quotIndConst)
          let env ← addConst env `Quot.lift (some quotLiftConst)
          some (addDefEq env quotDefEq)) =
        some env' →
      Ordered env'
Tactic:
refine with_addConst henv (fun ⟨quot, _⟩ => ⟨_, by type_tac⟩) fun henv => ?_
Proof state after:
env env' : VEnv
henv✝¹ : Ordered env
hq : QuotReady env
env1✝¹ : VEnv
henv✝ : Ordered env1✝¹
env1✝ : VEnv
henv : Ordered env1✝
⊢ HasObjects env1✝
      [VObject.const `Quot.mk (some quotMkConst), VObject.const `Quot (some quotConst),
        VObject.const `Eq (some eqConst)] →
    (do
          let env ← addConst env1✝ `Quot.ind (some quotIndConst)
          let env ← addConst env `Quot.lift (some quotLiftConst)
          some (addDefEq env quotDefEq)) =
        some env' →
      Ordered env'
Theorem: Lean4Lean.VEnv.addQuot_WF
Proof state before:
env env' : VEnv
henv✝¹ : Ordered env
hq : QuotReady env
env1✝¹ : VEnv
henv✝ : Ordered env1✝¹
env1✝ : VEnv
henv : Ordered env1✝
⊢ HasObjects env1✝
      [VObject.const `Quot.mk (some quotMkConst), VObject.const `Quot (some quotConst),
        VObject.const `Eq (some eqConst)] →
    (do
          let env ← addConst env1✝ `Quot.ind (some quotIndConst)
          let env ← addConst env `Quot.lift (some quotLiftConst)
          some (addDefEq env quotDefEq)) =
        some env' →
      Ordered env'
Tactic:
refine with_addConst henv (fun ⟨_, quot, _⟩ => ⟨_, by type_tac⟩) fun henv => ?_
Proof state after:
env env' : VEnv
henv✝² : Ordered env
hq : QuotReady env
env1✝² : VEnv
henv✝¹ : Ordered env1✝²
env1✝¹ : VEnv
henv✝ : Ordered env1✝¹
env1✝ : VEnv
henv : Ordered env1✝
⊢ HasObjects env1✝
      [VObject.const `Quot.ind (some quotIndConst), VObject.const `Quot.mk (some quotMkConst),
        VObject.const `Quot (some quotConst), VObject.const `Eq (some eqConst)] →
    (do
          let env ← addConst env1✝ `Quot.lift (some quotLiftConst)
          some (addDefEq env quotDefEq)) =
        some env' →
      Ordered env'
Theorem: Lean4Lean.VEnv.addQuot_WF
Proof state before:
env env' : VEnv
henv✝² : Ordered env
hq : QuotReady env
env1✝² : VEnv
henv✝¹ : Ordered env1✝²
env1✝¹ : VEnv
henv✝ : Ordered env1✝¹
env1✝ : VEnv
henv : Ordered env1✝
⊢ HasObjects env1✝
      [VObject.const `Quot.ind (some quotIndConst), VObject.const `Quot.mk (some quotMkConst),
        VObject.const `Quot (some quotConst), VObject.const `Eq (some eqConst)] →
    (do
          let env ← addConst env1✝ `Quot.lift (some quotLiftConst)
          some (addDefEq env quotDefEq)) =
        some env' →
      Ordered env'
Tactic:
refine with_addConst henv (fun ⟨_, _, quot, eq, _⟩ => ⟨_, by type_tac⟩) fun henv => ?_
Proof state after:
env env' : VEnv
henv✝³ : Ordered env
hq : QuotReady env
env1✝³ : VEnv
henv✝² : Ordered env1✝³
env1✝² : VEnv
henv✝¹ : Ordered env1✝²
env1✝¹ : VEnv
henv✝ : Ordered env1✝¹
env1✝ : VEnv
henv : Ordered env1✝
⊢ HasObjects env1✝
      [VObject.const `Quot.lift (some quotLiftConst), VObject.const `Quot.ind (some quotIndConst),
        VObject.const `Quot.mk (some quotMkConst), VObject.const `Quot (some quotConst),
        VObject.const `Eq (some eqConst)] →
    some (addDefEq env1✝ quotDefEq) = some env' → Ordered env'
Theorem: Lean4Lean.VEnv.addQuot_WF
Proof state before:
env env' : VEnv
henv✝³ : Ordered env
hq : QuotReady env
env1✝³ : VEnv
henv✝² : Ordered env1✝³
env1✝² : VEnv
henv✝¹ : Ordered env1✝²
env1✝¹ : VEnv
henv✝ : Ordered env1✝¹
env1✝ : VEnv
henv : Ordered env1✝
⊢ HasObjects env1✝
      [VObject.const `Quot.lift (some quotLiftConst), VObject.const `Quot.ind (some quotIndConst),
        VObject.const `Quot.mk (some quotMkConst), VObject.const `Quot (some quotConst),
        VObject.const `Eq (some eqConst)] →
    some (addDefEq env1✝ quotDefEq) = some env' → Ordered env'
Tactic:
rintro ⟨_, _, _, _, eq, _⟩ ⟨⟩
Proof state after:
case intro.intro.intro.intro.intro.refl
env : VEnv
henv✝³ : Ordered env
hq : QuotReady env
env1✝³ : VEnv
henv✝² : Ordered env1✝³
env1✝² : VEnv
henv✝¹ : Ordered env1✝²
env1✝¹ : VEnv
henv✝ : Ordered env1✝¹
env1✝ : VEnv
henv : Ordered env1✝
left✝³ : env1✝.constants `Quot.lift = some (some quotLiftConst)
left✝² : env1✝.constants `Quot.ind = some (some quotIndConst)
left✝¹ : env1✝.constants `Quot.mk = some (some quotMkConst)
left✝ : env1✝.constants `Quot = some (some quotConst)
eq : env1✝.constants `Eq = some (some eqConst)
right✝ : HasObjects env1✝ []
⊢ Ordered (addDefEq env1✝ quotDefEq)
Theorem: Lean4Lean.VEnv.addQuot_WF
Proof state before:
case intro.intro.intro.intro.intro.refl
env : VEnv
henv✝³ : Ordered env
hq : QuotReady env
env1✝³ : VEnv
henv✝² : Ordered env1✝³
env1✝² : VEnv
henv✝¹ : Ordered env1✝²
env1✝¹ : VEnv
henv✝ : Ordered env1✝¹
env1✝ : VEnv
henv : Ordered env1✝
left✝³ : env1✝.constants `Quot.lift = some (some quotLiftConst)
left✝² : env1✝.constants `Quot.ind = some (some quotIndConst)
left✝¹ : env1✝.constants `Quot.mk = some (some quotMkConst)
left✝ : env1✝.constants `Quot = some (some quotConst)
eq : env1✝.constants `Eq = some (some eqConst)
right✝ : HasObjects env1✝ []
⊢ Ordered (addDefEq env1✝ quotDefEq)
Tactic:
exact .defeq henv ⟨by type_tac, by type_tac⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.addQuot_WF
Proof state before:
env env' : VEnv
henv : Ordered env
hq : QuotReady env
x✝ : HasObjects env [VObject.const `Eq (some eqConst)]
⊢ HasType env quotConst.uvars [] quotConst.type (VExpr.sort (?m.204 x✝))
Tactic:
type_tac
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.addQuot_WF
Proof state before:
env env' : VEnv
henv✝ : Ordered env
hq : QuotReady env
env1✝ : VEnv
henv : Ordered env1✝
x✝ : HasObjects env1✝ [VObject.const `Quot (some quotConst), VObject.const `Eq (some eqConst)]
quot : env1✝.constants `Quot = some (some quotConst)
right✝ : HasObjects env1✝ [VObject.const `Eq (some eqConst)]
⊢ HasType env1✝ quotMkConst.uvars [] quotMkConst.type (VExpr.sort (?m.743 x✝ quot right✝))
Tactic:
type_tac
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.addQuot_WF
Proof state before:
env env' : VEnv
henv✝¹ : Ordered env
hq : QuotReady env
env1✝¹ : VEnv
henv✝ : Ordered env1✝¹
env1✝ : VEnv
henv : Ordered env1✝
x✝ :
  HasObjects env1✝
    [VObject.const `Quot.mk (some quotMkConst), VObject.const `Quot (some quotConst), VObject.const `Eq (some eqConst)]
left✝ : env1✝.constants `Quot.mk = some (some quotMkConst)
quot : env1✝.constants `Quot = some (some quotConst)
right✝ : HasObjects env1✝ [VObject.const `Eq (some eqConst)]
⊢ HasType env1✝ quotIndConst.uvars [] quotIndConst.type (VExpr.sort (?m.2200 x✝ left✝ quot right✝))
Tactic:
type_tac
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.addQuot_WF
Proof state before:
env env' : VEnv
henv✝² : Ordered env
hq : QuotReady env
env1✝² : VEnv
henv✝¹ : Ordered env1✝²
env1✝¹ : VEnv
henv✝ : Ordered env1✝¹
env1✝ : VEnv
henv : Ordered env1✝
x✝ :
  HasObjects env1✝
    [VObject.const `Quot.ind (some quotIndConst), VObject.const `Quot.mk (some quotMkConst),
      VObject.const `Quot (some quotConst), VObject.const `Eq (some eqConst)]
left✝¹ : env1✝.constants `Quot.ind = some (some quotIndConst)
left✝ : env1✝.constants `Quot.mk = some (some quotMkConst)
quot : env1✝.constants `Quot = some (some quotConst)
eq : env1✝.constants `Eq = some (some eqConst)
right✝ : HasObjects env1✝ []
⊢ HasType env1✝ quotLiftConst.uvars [] quotLiftConst.type (VExpr.sort (?m.5951 x✝ left✝¹ left✝ quot eq right✝))
Tactic:
type_tac
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.addQuot_WF
Proof state before:
env : VEnv
henv✝³ : Ordered env
hq : QuotReady env
env1✝³ : VEnv
henv✝² : Ordered env1✝³
env1✝² : VEnv
henv✝¹ : Ordered env1✝²
env1✝¹ : VEnv
henv✝ : Ordered env1✝¹
env1✝ : VEnv
henv : Ordered env1✝
left✝³ : env1✝.constants `Quot.lift = some (some quotLiftConst)
left✝² : env1✝.constants `Quot.ind = some (some quotIndConst)
left✝¹ : env1✝.constants `Quot.mk = some (some quotMkConst)
left✝ : env1✝.constants `Quot = some (some quotConst)
eq : env1✝.constants `Eq = some (some eqConst)
right✝ : HasObjects env1✝ []
⊢ HasType env1✝ quotDefEq.uvars [] quotDefEq.lhs quotDefEq.type
Tactic:
type_tac
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.addQuot_WF
Proof state before:
env : VEnv
henv✝³ : Ordered env
hq : QuotReady env
env1✝³ : VEnv
henv✝² : Ordered env1✝³
env1✝² : VEnv
henv✝¹ : Ordered env1✝²
env1✝¹ : VEnv
henv✝ : Ordered env1✝¹
env1✝ : VEnv
henv : Ordered env1✝
left✝³ : env1✝.constants `Quot.lift = some (some quotLiftConst)
left✝² : env1✝.constants `Quot.ind = some (some quotIndConst)
left✝¹ : env1✝.constants `Quot.mk = some (some quotMkConst)
left✝ : env1✝.constants `Quot = some (some quotConst)
eq : env1✝.constants `Eq = some (some eqConst)
right✝ : HasObjects env1✝ []
⊢ HasType env1✝ quotDefEq.uvars [] quotDefEq.rhs quotDefEq.type
Tactic:
type_tac
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.addQuot_objs
Proof state before:
env env' : VEnv
henv : addQuot env = some env'
⊢ HasObjects env'
    [VObject.defeq quotDefEq, VObject.const `Quot.lift (some quotLiftConst),
      VObject.const `Quot.ind (some quotIndConst), VObject.const `Quot.mk (some quotMkConst),
      VObject.const `Quot (some quotConst)]
Tactic:
let ⟨env, h, henv⟩ := HasObjects.bind_const (ls := []) trivial henv
Proof state after:
env✝ env' : VEnv
henv✝ : addQuot env✝ = some env'
env : VEnv
h : HasObjects env [VObject.const `Quot (some quotConst)]
henv :
  (do
      let env ← addConst env `Quot.mk (some quotMkConst)
      let env ← addConst env `Quot.ind (some quotIndConst)
      let env ← addConst env `Quot.lift (some quotLiftConst)
      some (addDefEq env quotDefEq)) =
    some env'
⊢ HasObjects env'
    [VObject.defeq quotDefEq, VObject.const `Quot.lift (some quotLiftConst),
      VObject.const `Quot.ind (some quotIndConst), VObject.const `Quot.mk (some quotMkConst),
      VObject.const `Quot (some quotConst)]
Theorem: Lean4Lean.VEnv.addQuot_objs
Proof state before:
env✝ env' : VEnv
henv✝ : addQuot env✝ = some env'
env : VEnv
h : HasObjects env [VObject.const `Quot (some quotConst)]
henv :
  (do
      let env ← addConst env `Quot.mk (some quotMkConst)
      let env ← addConst env `Quot.ind (some quotIndConst)
      let env ← addConst env `Quot.lift (some quotLiftConst)
      some (addDefEq env quotDefEq)) =
    some env'
⊢ HasObjects env'
    [VObject.defeq quotDefEq, VObject.const `Quot.lift (some quotLiftConst),
      VObject.const `Quot.ind (some quotIndConst), VObject.const `Quot.mk (some quotMkConst),
      VObject.const `Quot (some quotConst)]
Tactic:
let ⟨env, h, henv⟩ := HasObjects.bind_const h henv
Proof state after:
env✝¹ env' : VEnv
henv✝¹ : addQuot env✝¹ = some env'
env✝ : VEnv
h✝ : HasObjects env✝ [VObject.const `Quot (some quotConst)]
henv✝ :
  (do
      let env ← addConst env✝ `Quot.mk (some quotMkConst)
      let env ← addConst env `Quot.ind (some quotIndConst)
      let env ← addConst env `Quot.lift (some quotLiftConst)
      some (addDefEq env quotDefEq)) =
    some env'
env : VEnv
h : HasObjects env [VObject.const `Quot.mk (some quotMkConst), VObject.const `Quot (some quotConst)]
henv :
  (do
      let env ← addConst env `Quot.ind (some quotIndConst)
      let env ← addConst env `Quot.lift (some quotLiftConst)
      some (addDefEq env quotDefEq)) =
    some env'
⊢ HasObjects env'
    [VObject.defeq quotDefEq, VObject.const `Quot.lift (some quotLiftConst),
      VObject.const `Quot.ind (some quotIndConst), VObject.const `Quot.mk (some quotMkConst),
      VObject.const `Quot (some quotConst)]