internlm/Lean-Github huggingface dataset:
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'
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
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'
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)]
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'
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
Proof 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)]
Theorem: Lean4Lean.VEnv.addQuot_objs
Proof 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
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.DefInv.symm
Proof state before:
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 : VExpr
h : DefInv env U Γ e1 e2
⊢ DefInv env U Γ e2 e1
Tactic:
cases e1 <;> cases e2 <;> try trivial
Proof state after:
case sort.sort
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
u✝¹ u✝ : VLevel
h : DefInv env U Γ (sort u✝¹) (sort u✝)
⊢ DefInv env U Γ (sort u✝) (sort u✝¹)

case forallE.forallE
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
binderType✝¹ body✝¹ binderType✝ body✝ : VExpr
h : DefInv env U Γ (forallE binderType✝¹ body✝¹) (forallE binderType✝ body✝)
⊢ DefInv env U Γ (forallE binderType✝ body✝) (forallE binderType✝¹ body✝¹)
Theorem: Lean4Lean.VEnv.DefInv.symm
Proof state before:
case forallE.lam
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
binderType✝¹ body✝¹ binderType✝ body✝ : VExpr
h : DefInv env U Γ (forallE binderType✝¹ body✝¹) (lam binderType✝ body✝)
⊢ DefInv env U Γ (lam binderType✝ body✝) (forallE binderType✝¹ body✝¹)
Tactic:
trivial
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.DefInv.symm
Proof state before:
case sort.sort
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
u✝¹ u✝ : VLevel
h : DefInv env U Γ (sort u✝¹) (sort u✝)
⊢ DefInv env U Γ (sort u✝) (sort u✝¹)
Tactic:
exact h.symm
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.DefInv.symm
Proof state before:
case forallE.forallE
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
binderType✝¹ body✝¹ binderType✝ body✝ : VExpr
h : DefInv env U Γ (forallE binderType✝¹ body✝¹) (forallE binderType✝ body✝)
⊢ DefInv env U Γ (forallE binderType✝ body✝) (forallE binderType✝¹ body✝¹)
Tactic:
let ⟨u, v, h1, h2⟩ := h
Proof state after:
case forallE.forallE
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
binderType✝¹ body✝¹ binderType✝ body✝ : VExpr
h : DefInv env U Γ (forallE binderType✝¹ body✝¹) (forallE binderType✝ body✝)
u v : VLevel
h1 : IsDefEq env U Γ binderType✝¹ binderType✝ (sort u)
h2 : IsDefEq env U (binderType✝¹ :: Γ) body✝¹ body✝ (sort v)
⊢ DefInv env U Γ (forallE binderType✝ body✝) (forallE binderType✝¹ body✝¹)
Theorem: Lean4Lean.VEnv.DefInv.symm
Proof state before:
case forallE.forallE
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
binderType✝¹ body✝¹ binderType✝ body✝ : VExpr
h : DefInv env U Γ (forallE binderType✝¹ body✝¹) (forallE binderType✝ body✝)
u v : VLevel
h1 : IsDefEq env U Γ binderType✝¹ binderType✝ (sort u)
h2 : IsDefEq env U (binderType✝¹ :: Γ) body✝¹ body✝ (sort v)
⊢ DefInv env U Γ (forallE binderType✝ body✝) (forallE binderType✝¹ body✝¹)
Tactic:
exact ⟨u, v, h1.symm, h1.defeqDF_l henv h2.symm⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
H : IsDefEq env U Γ e1 e2 A
⊢ HasType1 env U defEq Γ e1 A ∧ HasType1 env U defEq Γ e2 A ∧ IsDefEq1 env U hasType defEq Γ e1 e2 A
Tactic:
have H' := H.strong henv hΓ
Proof state after:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
H : IsDefEq env U Γ e1 e2 A
H' : IsDefEqStrong env U Γ e1 e2 A
⊢ HasType1 env U defEq Γ e1 A ∧ HasType1 env U defEq Γ e2 A ∧ IsDefEq1 env U hasType defEq Γ e1 e2 A
Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
H : IsDefEq env U Γ e1 e2 A
H' : IsDefEqStrong env U Γ e1 e2 A
⊢ HasType1 env U defEq Γ e1 A ∧ HasType1 env U defEq Γ e2 A ∧ IsDefEq1 env U hasType defEq Γ e1 e2 A
Tactic:
clear hΓ H
Proof state after:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
H' : IsDefEqStrong env U Γ e1 e2 A
⊢ HasType1 env U defEq Γ e1 A ∧ HasType1 env U defEq Γ e2 A ∧ IsDefEq1 env U hasType defEq Γ e1 e2 A
Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
H' : IsDefEqStrong env U Γ e1 e2 A
⊢ HasType1 env U defEq Γ e1 A ∧ HasType1 env U defEq Γ e2 A ∧ IsDefEq1 env U hasType defEq Γ e1 e2 A
Tactic:
induction H' with
| bvar h => exact ⟨.bvar h, .bvar h, .refl (hty (.bvar h))⟩
| symm _ ih => exact ⟨ih.2.1, ih.1, .symm ih.2.2⟩
| trans _ _ ih1 ih2 => exact ⟨ih1.1, ih2.2.1, .trans ih1.2.2 ih2.2.2⟩
| @constDF _ _ ls₁ ls₂ u _ h1 h2 h3 h4 h5 =>
  exact ⟨.const h1 h2 h4,
    .defeq (u := u.inst ls₁) sorry <| .const h1 h3 (h5.length_eq.symm.trans h4),
    .constDF h1 h2 h3 h4 h5⟩
| @sortDF l l' _ h1 h2 h3 =>
  refine ⟨.sort h1, ?_, .sortDF h1 h2 h3⟩
  exact .defeq (hdf <| .symm <| .sortDF (l' := l'.succ) h1 h2 (VLevel.succ_congr h3)) (.sort h2)
| appDF _ _ _ _ _ _ _ _ _ ihf iha ihBa =>
  let ⟨hf, hf', ff⟩ := ihf; let ⟨ha, ha', aa⟩ := iha
  exact ⟨.app hf ha, .defeq (hdf ihBa.2.2.symm) (.app hf' ha'), .appDF ff aa⟩
| lamDF _ _ _ _ _ _ _ ihA ihB _ ihb ihb' =>
  refine ⟨.lam ihA.1 ihb.1, ?_, .lamDF ihA.2.2 ihb.2.2⟩
  exact .defeq (hdf <| .symm <| .forallEDF ihA.2.2 ihB.2.2) <| .lam ihA.2.1 ihb'.2.1
| forallEDF _ _ _ _ _ ih1 ih2 ih3 =>
  exact ⟨.forallE ih1.1 ih2.1, .forallE ih1.2.1 ih3.2.1, .forallEDF ih1.2.2 ih2.2.2⟩
| defeqDF _ _ _ ih1 ih2 =>
  exact ⟨.defeq (hdf ih1.2.2) ih2.1, .defeq (hdf ih1.2.2) ih2.2.1, .defeqDF (hdf ih1.2.2) ih2.2.2⟩
| beta _ _ _ _ _ _ _ _ ihA _ ihe ihe' _ ihee =>
  exact ⟨.app (.lam ihA.1 ihe.1) ihe'.1, ihee.1, .beta (hty ihe.1) (hty ihe'.1)⟩
| eta _ _ _ _ _ _ _ ihA _ _ ihe ihe' =>
  have := HasType1.app ihe'.1 (.bvar .zero)
  rw [instN_bvar0] at this
  exact ⟨.lam ihA.1 this, ihe.1, .eta (hty ihe.1)⟩
| proofIrrel _ _ _ ih1 ih2 ih3 =>
  exact ⟨ih2.1, ih3.1, .proofIrrel (hty ih1.1) (hty ih2.1) (hty ih3.1)⟩
| extra h1 h2 h3 _ _ _ _ _ _ _ _ _ ihl' ihr' =>
  exact ⟨ihl'.1, ihr'.1, .extra h1 h2 h3⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
case bvar
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
Γ✝ : List VExpr
i✝ : Nat
A✝ : VExpr
u✝ : VLevel
h : Lookup Γ✝ i✝ A✝
a✝¹ : VLevel.WF U u✝
a✝ : IsDefEqStrong env U Γ✝ A✝ A✝ (VExpr.sort u✝)
a_ih✝ :
  HasType1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasType1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEq1 env U hasType defEq Γ✝ A✝ A✝ (VExpr.sort u✝)
⊢ HasType1 env U defEq Γ✝ (VExpr.bvar i✝) A✝ ∧
    HasType1 env U defEq Γ✝ (VExpr.bvar i✝) A✝ ∧ IsDefEq1 env U hasType defEq Γ✝ (VExpr.bvar i✝) (VExpr.bvar i✝) A✝
Tactic:
exact ⟨.bvar h, .bvar h, .refl (hty (.bvar h))⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
case symm
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ e✝ e'✝ A✝
ih : HasType1 env U defEq Γ✝ e✝ A✝ ∧ HasType1 env U defEq Γ✝ e'✝ A✝ ∧ IsDefEq1 env U hasType defEq Γ✝ e✝ e'✝ A✝
⊢ HasType1 env U defEq Γ✝ e'✝ A✝ ∧ HasType1 env U defEq Γ✝ e✝ A✝ ∧ IsDefEq1 env U hasType defEq Γ✝ e'✝ e✝ A✝
Tactic:
exact ⟨ih.2.1, ih.1, .symm ih.2.2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
case trans
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
Γ✝ : List VExpr
e₁✝ e₂✝ A✝ e₃✝ : VExpr
a✝¹ : IsDefEqStrong env U Γ✝ e₁✝ e₂✝ A✝
a✝ : IsDefEqStrong env U Γ✝ e₂✝ e₃✝ A✝
ih1 : HasType1 env U defEq Γ✝ e₁✝ A✝ ∧ HasType1 env U defEq Γ✝ e₂✝ A✝ ∧ IsDefEq1 env U hasType defEq Γ✝ e₁✝ e₂✝ A✝
ih2 : HasType1 env U defEq Γ✝ e₂✝ A✝ ∧ HasType1 env U defEq Γ✝ e₃✝ A✝ ∧ IsDefEq1 env U hasType defEq Γ✝ e₂✝ e₃✝ A✝
⊢ HasType1 env U defEq Γ✝ e₁✝ A✝ ∧ HasType1 env U defEq Γ✝ e₃✝ A✝ ∧ IsDefEq1 env U hasType defEq Γ✝ e₁✝ e₃✝ A✝
Tactic:
exact ⟨ih1.1, ih2.2.1, .trans ih1.2.2 ih2.2.2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
case constDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
c✝ : Name
ci✝ : VConstant
ls₁ ls₂ : List VLevel
u : VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls₁ → VLevel.WF U l
h3 : ∀ (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✝⁴ : 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✝¹ : 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✝³ :
  HasType1 env U defEq [] (VExpr.instL ls₁ ci✝.type) (VExpr.sort u) ∧
    HasType1 env U defEq [] (VExpr.instL ls₁ ci✝.type) (VExpr.sort u) ∧
      IsDefEq1 env U hasType defEq [] (VExpr.instL ls₁ ci✝.type) (VExpr.instL ls₁ ci✝.type) (VExpr.sort u)
a_ih✝² :
  HasType1 env U defEq [] (VExpr.instL ls₂ ci✝.type) (VExpr.sort u) ∧
    HasType1 env U defEq [] (VExpr.instL ls₂ ci✝.type) (VExpr.sort u) ∧
      IsDefEq1 env U hasType defEq [] (VExpr.instL ls₂ ci✝.type) (VExpr.instL ls₂ ci✝.type) (VExpr.sort u)
a_ih✝¹ :
  HasType1 env U defEq Γ✝ (VExpr.instL ls₁ ci✝.type) (VExpr.sort u) ∧
    HasType1 env U defEq Γ✝ (VExpr.instL ls₁ ci✝.type) (VExpr.sort u) ∧
      IsDefEq1 env U hasType defEq Γ✝ (VExpr.instL ls₁ ci✝.type) (VExpr.instL ls₁ ci✝.type) (VExpr.sort u)
a_ih✝ :
  HasType1 env U defEq Γ✝ (VExpr.instL ls₂ ci✝.type) (VExpr.sort u) ∧
    HasType1 env U defEq Γ✝ (VExpr.instL ls₂ ci✝.type) (VExpr.sort u) ∧
      IsDefEq1 env U hasType defEq Γ✝ (VExpr.instL ls₂ ci✝.type) (VExpr.instL ls₂ ci✝.type) (VExpr.sort u)
⊢ HasType1 env U defEq Γ✝ (VExpr.const c✝ ls₁) (VExpr.instL ls₁ ci✝.type) ∧
    HasType1 env U defEq Γ✝ (VExpr.const c✝ ls₂) (VExpr.instL ls₁ ci✝.type) ∧
      IsDefEq1 env U hasType defEq Γ✝ (VExpr.const c✝ ls₁) (VExpr.const c✝ ls₂) (VExpr.instL ls₁ ci✝.type)
Tactic:
exact ⟨.const h1 h2 h4,
  .defeq (u := u.inst ls₁) sorry <| .const h1 h3 (h5.length_eq.symm.trans h4),
  .constDF h1 h2 h3 h4 h5⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
case sortDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
l l' : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF U l
h2 : VLevel.WF U l'
h3 : l ≈ l'
⊢ HasType1 env U defEq Γ✝ (VExpr.sort l) (VExpr.sort (VLevel.succ l)) ∧
    HasType1 env U defEq Γ✝ (VExpr.sort l') (VExpr.sort (VLevel.succ l)) ∧
      IsDefEq1 env U hasType defEq Γ✝ (VExpr.sort l) (VExpr.sort l') (VExpr.sort (VLevel.succ l))
Tactic:
refine ⟨.sort h1, ?_, .sortDF h1 h2 h3⟩
Proof state after:
case sortDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
l l' : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF U l
h2 : VLevel.WF U l'
h3 : l ≈ l'
⊢ HasType1 env U defEq Γ✝ (VExpr.sort l') (VExpr.sort (VLevel.succ l))
Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
case sortDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
l l' : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF U l
h2 : VLevel.WF U l'
h3 : l ≈ l'
⊢ HasType1 env U defEq Γ✝ (VExpr.sort l') (VExpr.sort (VLevel.succ l))
Tactic:
exact .defeq (hdf <| .symm <| .sortDF (l' := l'.succ) h1 h2 (VLevel.succ_congr h3)) (.sort h2)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.induction1
Proof state before:
case appDF
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq : List VExpr → VExpr → VExpr → VExpr → Prop
hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasType1 env U defEq Γ e A → hasType Γ e A
hdf : ∀ {Γ : List VExpr} {e1 e2 A : VExpr}, IsDefEq1 env U hasType defEq Γ e1 e2 A → defEq Γ e1 e2 A
Γ✝ : List VExpr
A✝ : VExpr
u✝ : VLevel
B✝ : VExpr
v✝ : VLevel
f✝ f'✝ a✝⁷ a'✝ : 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 Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
a✝¹ : IsDefEqStrong env U Γ✝ a✝⁷ a'✝ A✝
a✝ : IsDefEqStrong env U Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝) (VExpr.sort v✝)
a_ih✝¹ :
  HasType1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasType1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEq1 env U hasType defEq Γ✝ A✝ A✝ (VExpr.sort u✝)
a_ih✝ :
  HasType1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧
    HasType1 env U defEq (A✝ :: Γ✝) B✝ (VExpr.sort v✝) ∧ IsDefEq1 env U hasType defEq (A✝ :: Γ✝) B✝ B✝ (VExpr.sort v✝)
ihf :
  HasType1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝) ∧
    HasType1 env U defEq Γ✝ f'✝ (VExpr.forallE A✝ B✝) ∧ IsDefEq1 env U hasType defEq Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
iha : HasType1 env U defEq Γ✝ a✝⁷ A✝ ∧ HasType1 env U defEq Γ✝ a'✝ A✝ ∧ IsDefEq1 env U hasType defEq Γ✝ a✝⁷ a'✝ A✝
ihBa :
  HasType1 env U defEq Γ✝ (inst B✝ a✝⁷) (VExpr.sort v✝) ∧
    HasType1 env U defEq Γ✝ (inst B✝ a'✝) (VExpr.sort v✝) ∧
      IsDefEq1 env U hasType defEq Γ✝ (inst B✝ a✝⁷) (inst B✝ a'✝) (VExpr.sort v✝)
hf : HasType1 env U defEq Γ✝ f✝ (VExpr.forallE A✝ B✝)
hf' : HasType1 env U defEq Γ✝ f'✝ (VExpr.forallE A✝ B✝)
ff : IsDefEq1 env U hasType defEq Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
ha : HasType1 env U defEq Γ✝ a✝⁷ A✝
ha' : HasType1 env U defEq Γ✝ a'✝ A✝
aa : IsDefEq1 env U hasType defEq Γ✝ a✝⁷ a'✝ A✝
⊢ HasType1 env U defEq Γ✝ (app f✝ a✝⁷) (inst B✝ a✝⁷) ∧
    HasType1 env U defEq Γ✝ (app f'✝ a'✝) (inst B✝ a✝⁷) ∧
      IsDefEq1 env U hasType defEq Γ✝ (app f✝ a✝⁷) (app f'✝ a'✝) (inst B✝ a✝⁷)
Tactic:
exact ⟨.app hf ha, .defeq (hdf ihBa.2.2.symm) (.app hf' ha'), .appDF ff aa⟩
Proof state after:
no goals