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

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 => ?_
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'

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 => ?_
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'

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 => ?_
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'

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 => ?_
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'

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, _⟩ ⟨⟩
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)

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⟩
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals