Theorem: Lean4Lean.VEnv.addQuot_objs (Lean4Lean/Theory/Typing/QuotLemmas.lean)

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
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)]

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
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)]

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'
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)]
Tactic:
let ⟨env, h, henv⟩ := HasObjects.bind_const h henv
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'
env : VEnv
h :
  HasObjects env
    [VObject.const `Quot.ind (some quotIndConst), VObject.const `Quot.mk (some quotMkConst),
      VObject.const `Quot (some quotConst)]
henv :
  (do
      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)]

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'
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'
env : VEnv
h :
  HasObjects env
    [VObject.const `Quot.ind (some quotIndConst), VObject.const `Quot.mk (some quotMkConst),
      VObject.const `Quot (some quotConst)]
henv :
  (do
      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:
obtain ⟨env, h, ⟨⟩⟩ := HasObjects.bind_const h henv
State after:
case intro.intro.refl
env✝³ env✝² : VEnv
h✝² : HasObjects env✝² [VObject.const `Quot (some quotConst)]
env✝¹ : VEnv
h✝¹ : HasObjects env✝¹ [VObject.const `Quot.mk (some quotMkConst), VObject.const `Quot (some quotConst)]
env✝ : VEnv
h✝ :
  HasObjects env✝
    [VObject.const `Quot.ind (some quotIndConst), VObject.const `Quot.mk (some quotMkConst),
      VObject.const `Quot (some quotConst)]
env : VEnv
h :
  HasObjects env
    [VObject.const `Quot.lift (some quotLiftConst), VObject.const `Quot.ind (some quotIndConst),
      VObject.const `Quot.mk (some quotMkConst), VObject.const `Quot (some quotConst)]
henv✝² : addQuot env✝³ = some (addDefEq env quotDefEq)
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 (addDefEq env quotDefEq)
henv✝ :
  (do
      let env ← addConst env✝¹ `Quot.ind (some quotIndConst)
      let env ← addConst env `Quot.lift (some quotLiftConst)
      some (addDefEq env quotDefEq)) =
    some (addDefEq env quotDefEq)
henv :
  (do
      let env ← addConst env✝ `Quot.lift (some quotLiftConst)
      some (addDefEq env quotDefEq)) =
    some (addDefEq env quotDefEq)
⊢ HasObjects (addDefEq env quotDefEq)
    [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)]

State before:
case intro.intro.refl
env✝³ env✝² : VEnv
h✝² : HasObjects env✝² [VObject.const `Quot (some quotConst)]
env✝¹ : VEnv
h✝¹ : HasObjects env✝¹ [VObject.const `Quot.mk (some quotMkConst), VObject.const `Quot (some quotConst)]
env✝ : VEnv
h✝ :
  HasObjects env✝
    [VObject.const `Quot.ind (some quotIndConst), VObject.const `Quot.mk (some quotMkConst),
      VObject.const `Quot (some quotConst)]
env : VEnv
h :
  HasObjects env
    [VObject.const `Quot.lift (some quotLiftConst), VObject.const `Quot.ind (some quotIndConst),
      VObject.const `Quot.mk (some quotMkConst), VObject.const `Quot (some quotConst)]
henv✝² : addQuot env✝³ = some (addDefEq env quotDefEq)
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 (addDefEq env quotDefEq)
henv✝ :
  (do
      let env ← addConst env✝¹ `Quot.ind (some quotIndConst)
      let env ← addConst env `Quot.lift (some quotLiftConst)
      some (addDefEq env quotDefEq)) =
    some (addDefEq env quotDefEq)
henv :
  (do
      let env ← addConst env✝ `Quot.lift (some quotLiftConst)
      some (addDefEq env quotDefEq)) =
    some (addDefEq env quotDefEq)
⊢ HasObjects (addDefEq env quotDefEq)
    [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:
exact HasObjects.defeq (df := quotDefEq) h
State after:
no goals