internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof state before:
case inr.inl
e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this : j < Nat.succ (k + j)
⊢ liftN (k + j + 1) e2 = liftN 1 (liftN (k + j) e2) j
Tactic:
exact (liftN'_liftN' (Nat.zero_le _) (Nat.le_add_left j k)).symm
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof state before:
e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this✝ : j < Nat.succ (k + j)
this : liftN (k + j + 1) ?m.117762 = ?m.117771
⊢ inst (liftN (k + j + 1) e2) e3 j = liftN (k + j) e2
Tactic:
rw [this]
Proof state after:
e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this✝ : j < Nat.succ (k + j)
this : liftN (k + j + 1) e2 = ?m.117771
⊢ inst ?m.117771 e3 j = liftN (k + j) e2

e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this : j < Nat.succ (k + j)
⊢ VExpr
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof state before:
e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this✝ : j < Nat.succ (k + j)
this : liftN (k + j + 1) e2 = ?m.117771
⊢ inst ?m.117771 e3 j = liftN (k + j) e2

e2 e3 : VExpr
k j : Nat
h : ¬k + j + 1 < k + j + 1
this : j < Nat.succ (k + j)
⊢ VExpr
Tactic:
exact inst_liftN ..
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof state before:
case inr.inr
i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬i < k + j + 1
h' : ¬i = k + j + 1
⊢ inst (bvar (i - 1)) e3 j =
    inst (if i < j then bvar i else if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)
Tactic:
have hk := Nat.lt_of_le_of_ne (Nat.not_lt.1 h) (Ne.symm h')
Proof state after:
case inr.inr
i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬i < k + j + 1
h' : ¬i = k + j + 1
hk : k + j + 1 < i
⊢ inst (bvar (i - 1)) e3 j =
    inst (if i < j then bvar i else if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof state before:
case inr.inr
i : Nat
e2 e3 : VExpr
k j : Nat
h : ¬i < k + j + 1
h' : ¬i = k + j + 1
hk : k + j + 1 < i
⊢ inst (bvar (i - 1)) e3 j =
    inst (if i < j then bvar i else if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)
Tactic:
let i+1 := i
Proof state after:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk : k + j + 1 < i + 1
⊢ inst (bvar (i + 1 - 1)) e3 j =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar (i + 1 - 1)) e2 (k + j)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof state before:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk : k + j + 1 < i + 1
⊢ inst (bvar (i + 1 - 1)) e3 j =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar (i + 1 - 1)) e2 (k + j)
Tactic:
have hk := Nat.lt_of_add_lt_add_right hk
Proof state after:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
⊢ inst (bvar (i + 1 - 1)) e3 j =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar (i + 1 - 1)) e2 (k + j)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof state before:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
⊢ inst (bvar (i + 1 - 1)) e3 j =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar (i + 1 - 1)) e2 (k + j)
Tactic:
simp [inst, instVar, hk]
Proof state after:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
⊢ (if i < j then bvar i else if i = j then liftN j e3 else bvar (i - 1)) =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar i) e2 (k + j)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof state before:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
⊢ (if i < j then bvar i else if i = j then liftN j e3 else bvar (i - 1)) =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar i) e2 (k + j)
Tactic:
have := Nat.lt_of_le_of_lt (Nat.le_add_left ..) hk
Proof state after:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this : j < i
⊢ (if i < j then bvar i else if i = j then liftN j e3 else bvar (i - 1)) =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar i) e2 (k + j)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof state before:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this : j < i
⊢ (if i < j then bvar i else if i = j then liftN j e3 else bvar (i - 1)) =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar i) e2 (k + j)
Tactic:
rw [if_neg (Nat.lt_asymm this), if_neg (Nat.ne_of_gt this)]
Proof state after:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this : j < i
⊢ bvar (i - 1) =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar i) e2 (k + j)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof state before:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this : j < i
⊢ bvar (i - 1) =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar i) e2 (k + j)
Tactic:
have := Nat.lt_succ_of_lt this
Proof state after:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this✝ : j < i
this : j < Nat.succ i
⊢ bvar (i - 1) =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar i) e2 (k + j)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof state before:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this✝ : j < i
this : j < Nat.succ i
⊢ bvar (i - 1) =
    inst (if i + 1 < j then bvar (i + 1) else if i + 1 = j then liftN j (liftN 1 e3 k) else bvar i) e2 (k + j)
Tactic:
rw [if_neg (Nat.lt_asymm this), if_neg (Nat.ne_of_gt this)]
Proof state after:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this✝ : j < i
this : j < Nat.succ i
⊢ bvar (i - 1) = inst (bvar i) e2 (k + j)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof state before:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this✝ : j < i
this : j < Nat.succ i
⊢ bvar (i - 1) = inst (bvar i) e2 (k + j)
Tactic:
simp [inst, instVar]
Proof state after:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this✝ : j < i
this : j < Nat.succ i
⊢ bvar (i - 1) = if i < k + j then bvar i else if i = k + j then liftN (k + j) e2 else bvar (i - 1)
Theorem: Lean4Lean.VExpr.inst_instVar_lo
Proof state before:
case inr.inr
i✝ : Nat
e2 e3 : VExpr
k j i : Nat
h : ¬i + 1 < k + j + 1
h' : ¬i + 1 = k + j + 1
hk✝ : k + j + 1 < i + 1
hk : k + j < i
this✝ : j < i
this : j < Nat.succ i
⊢ bvar (i - 1) = if i < k + j then bvar i else if i = k + j then liftN (k + j) e2 else bvar (i - 1)
Tactic:
rw [if_neg (Nat.lt_asymm hk), if_neg (Nat.ne_of_gt hk)]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_inst_lo
Proof state before:
e1 e2 e3 : VExpr
k j : Nat
⊢ inst (inst e1 e2 (k + j + 1)) e3 j = inst (inst e1 (liftN 1 e3 k) j) e2 (k + j)
Tactic:
induction e1 generalizing j with simp [liftN, inst, instVar, *]
| bvar i => apply inst_instVar_lo
| _ => rename_i IH; exact IH (j+1)
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_inst_lo
Proof state before:
case bvar
e2 e3 : VExpr
k i j : Nat
⊢ inst (if i < k + j + 1 then bvar i else if i = k + j + 1 then liftN (k + j + 1) e2 else bvar (i - 1)) e3 j =
    inst (if i < j then bvar i else if i = j then liftN j (liftN 1 e3 k) else bvar (i - 1)) e2 (k + j)
Tactic:
apply inst_instVar_lo
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.inst_inst_lo
Proof state before:
case forallE
e2 e3 : VExpr
k : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ :
  ∀ (j : Nat), inst (inst binderType✝ e2 (k + j + 1)) e3 j = inst (inst binderType✝ (liftN 1 e3 k) j) e2 (k + j)
body_ih✝ : ∀ (j : Nat), inst (inst body✝ e2 (k + j + 1)) e3 j = inst (inst body✝ (liftN 1 e3 k) j) e2 (k + j)
j : Nat
⊢ inst (inst body✝ e2 (k + j + 1 + 1)) e3 (j + 1) = inst (inst body✝ (liftN 1 e3 k) (j + 1)) e2 (k + j + 1)
Tactic:
rename_i IH
Proof state after:
case forallE
e2 e3 : VExpr
k : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ :
  ∀ (j : Nat), inst (inst binderType✝ e2 (k + j + 1)) e3 j = inst (inst binderType✝ (liftN 1 e3 k) j) e2 (k + j)
IH : ∀ (j : Nat), inst (inst body✝ e2 (k + j + 1)) e3 j = inst (inst body✝ (liftN 1 e3 k) j) e2 (k + j)
j : Nat
⊢ inst (inst body✝ e2 (k + j + 1 + 1)) e3 (j + 1) = inst (inst body✝ (liftN 1 e3 k) (j + 1)) e2 (k + j + 1)
Theorem: Lean4Lean.VExpr.inst_inst_lo
Proof state before:
case forallE
e2 e3 : VExpr
k : Nat
binderType✝ body✝ : VExpr
binderType_ih✝ :
  ∀ (j : Nat), inst (inst binderType✝ e2 (k + j + 1)) e3 j = inst (inst binderType✝ (liftN 1 e3 k) j) e2 (k + j)
IH : ∀ (j : Nat), inst (inst body✝ e2 (k + j + 1)) e3 j = inst (inst body✝ (liftN 1 e3 k) j) e2 (k + j)
j : Nat
⊢ inst (inst body✝ e2 (k + j + 1 + 1)) e3 (j + 1) = inst (inst body✝ (liftN 1 e3 k) (j + 1)) e2 (k + j + 1)
Tactic:
exact IH (j+1)
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.instN_bvar0
Proof state before:
e : VExpr
k : Nat
⊢ inst (liftN 1 e (k + 1)) (bvar 0) k = e
Tactic:
induction e generalizing k with simp [liftN, inst, *]
| bvar i => induction i generalizing k <;> cases k <;> simp [*, lift, liftN]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.instN_bvar0
Proof state before:
case bvar
i k : Nat
⊢ instVar (liftVar 1 i (k + 1)) (bvar 0) k = bvar i
Tactic:
induction i generalizing k <;> cases k <;> simp [*, lift, liftN]
Proof state after:
no goals
Theorem: Lean4Lean.Lift.depth_consN
Proof state before:
l : Lift
n : Nat
⊢ depth (consN l n) = depth l
Tactic:
induction n <;> simp [*]
Proof state after:
no goals
Theorem: Lean4Lean.Lift.consN_consN
Proof state before:
l : Lift
a b : Nat
⊢ consN (consN l a) b = consN l (a + b)
Tactic:
induction b <;> simp [*]
Proof state after:
no goals
Theorem: Lean4Lean.Lift.consN_comp
Proof state before:
l₁ l₂ : Lift
n : Nat
⊢ consN (comp l₁ l₂) n = comp (consN l₁ n) (consN l₂ n)
Tactic:
induction n <;> simp [*]
Proof state after:
no goals
Theorem: Lean4Lean.Lift.depth_skipN
Proof state before:
n : Nat
⊢ depth (skipN n) = n
Tactic:
induction n <;> simp [*]
Proof state after:
no goals
Theorem: Lean4Lean.Lift.consN_skip_eq
Proof state before:
l : Lift
k : Nat
⊢ consN (skip l) k = comp (consN l k) (consN (skipN 1) k)
Tactic:
rw [← consN_comp]
Proof state after:
l : Lift
k : Nat
⊢ consN (skip l) k = consN (comp l (skipN 1)) k
Theorem: Lean4Lean.Lift.consN_skip_eq
Proof state before:
l : Lift
k : Nat
⊢ consN (skip l) k = consN (comp l (skipN 1)) k
Tactic:
rfl
Proof state after:
no goals
Theorem: Lean4Lean.Lift.depth_succ
Proof state before:
n : Nat
l : Lift
H : depth l = n + 1
⊢ ∃ l' k, depth l' = n ∧ l = consN (skip l') k
Tactic:
match l with
| .skip l => cases H; exact ⟨l, 0, rfl, rfl⟩
| .cons l =>
  obtain ⟨l, k, rfl, ⟨⟩⟩ := depth_succ (l := l) H
  exact ⟨l, k+1, rfl, rfl⟩
Proof state after:
no goals
Theorem: Lean4Lean.Lift.depth_succ
Proof state before:
n : Nat
l✝ l : Lift
H : depth (skip l) = n + 1
⊢ ∃ l' k, depth l' = n ∧ skip l = consN (skip l') k
Tactic:
cases H
Proof state after:
case refl
l✝ l : Lift
⊢ ∃ l' k, depth l' = depth l ∧ skip l = consN (skip l') k
Theorem: Lean4Lean.Lift.depth_succ
Proof state before:
case refl
l✝ l : Lift
⊢ ∃ l' k, depth l' = depth l ∧ skip l = consN (skip l') k
Tactic:
exact ⟨l, 0, rfl, rfl⟩
Proof state after:
no goals
Theorem: Lean4Lean.Lift.depth_succ
Proof state before:
n : Nat
l✝ l : Lift
H : depth (cons l) = n + 1
⊢ ∃ l' k, depth l' = n ∧ cons l = consN (skip l') k
Tactic:
obtain ⟨l, k, rfl, ⟨⟩⟩ := depth_succ (l := l) H
Proof state after:
case intro.intro.intro.refl
l✝ l : Lift
k : Nat
H : depth (cons (consN (skip l) k)) = depth l + 1
⊢ ∃ l' k_1, depth l' = depth l ∧ cons (consN (skip l) k) = consN (skip l') k_1
Theorem: Lean4Lean.Lift.depth_succ
Proof state before:
case intro.intro.intro.refl
l✝ l : Lift
k : Nat
H : depth (cons (consN (skip l) k)) = depth l + 1
⊢ ∃ l' k_1, depth l' = depth l ∧ cons (consN (skip l) k) = consN (skip l') k_1
Tactic:
exact ⟨l, k+1, rfl, rfl⟩
Proof state after:
no goals
Theorem: Lean4Lean.Lift.depth_succ'
Proof state before:
n : Nat
l : Lift
H : depth l = n + 1
⊢ ∃ l' k, depth l' = n ∧ l = comp l' (consN (skipN 1) k)
Tactic:
let ⟨l', k, h1, h2⟩ := depth_succ H
Proof state after:
n : Nat
l : Lift
H : depth l = n + 1
l' : Lift
k : Nat
h1 : depth l' = n
h2 : l = consN (skip l') k
⊢ ∃ l' k, depth l' = n ∧ l = comp l' (consN (skipN 1) k)
Theorem: Lean4Lean.Lift.depth_succ'
Proof state before:
n : Nat
l : Lift
H : depth l = n + 1
l' : Lift
k : Nat
h1 : depth l' = n
h2 : l = consN (skip l') k
⊢ ∃ l' k, depth l' = n ∧ l = comp l' (consN (skipN 1) k)
Tactic:
exact ⟨.consN l' k, k, by simp [h1], by rwa [← consN_skip_eq]⟩
Proof state after:
no goals
Theorem: Lean4Lean.Lift.depth_succ'
Proof state before:
n : Nat
l : Lift
H : depth l = n + 1
l' : Lift
k : Nat
h1 : depth l' = n
h2 : l = consN (skip l') k
⊢ depth (consN l' k) = n
Tactic:
simp [h1]
Proof state after:
no goals
Theorem: Lean4Lean.Lift.depth_succ'
Proof state before:
n : Nat
l : Lift
H : depth l = n + 1
l' : Lift
k : Nat
h1 : depth l' = n
h2 : l = consN (skip l') k
⊢ l = comp (consN l' k) (consN (skipN 1) k)
Tactic:
rwa [← consN_skip_eq]
Proof state after:
no goals
Theorem: Lean4Lean.liftVar_comp
Proof state before:
l₁ l₂ : Lift
n : Nat
⊢ Lift.liftVar (Lift.comp l₁ l₂) n = Lift.liftVar l₂ (Lift.liftVar l₁ n)
Tactic:
induction l₂ generalizing l₁ n <;> [skip; skip; cases l₁ <;> [skip; skip; cases n]] <;> simp [*]
Proof state after:
no goals
Theorem: Lean4Lean.liftVar_skipN
Proof state before:
n i : Nat
⊢ Lift.liftVar (Lift.skipN n) i = i + n
Tactic:
induction n generalizing i with
| zero => rfl
| succ _ ih => simp [ih, Nat.add_right_comm]; rfl
Proof state after:
no goals
Theorem: Lean4Lean.liftVar_skipN
Proof state before:
case zero
i : Nat
⊢ Lift.liftVar (Lift.skipN Nat.zero) i = i + Nat.zero
Tactic:
rfl
Proof state after:
no goals
Theorem: Lean4Lean.liftVar_skipN
Proof state before:
case succ
n✝ : Nat
ih : ∀ {i : Nat}, Lift.liftVar (Lift.skipN n✝) i = i + n✝
i : Nat
⊢ Lift.liftVar (Lift.skipN (Nat.succ n✝)) i = i + Nat.succ n✝
Tactic:
simp [ih, Nat.add_right_comm]
Proof state after:
case succ
n✝ : Nat
ih : ∀ {i : Nat}, Lift.liftVar (Lift.skipN n✝) i = i + n✝
i : Nat
⊢ i + n✝ + 1 = i + Nat.succ n✝
Theorem: Lean4Lean.liftVar_skipN
Proof state before:
case succ
n✝ : Nat
ih : ∀ {i : Nat}, Lift.liftVar (Lift.skipN n✝) i = i + n✝
i : Nat
⊢ i + n✝ + 1 = i + Nat.succ n✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Lean4Lean.liftVar_consN_skipN
Proof state before:
n k i : Nat
⊢ Lift.liftVar (Lift.consN (Lift.skipN n) k) i = liftVar n i k
Tactic:
induction k generalizing i with
| zero => simp [liftVar_skipN]
| succ k ih =>
  cases i with simp [liftVar, Nat.succ_lt_succ_iff, ih]
  | succ i => split <;> rfl
Proof state after:
no goals
Theorem: Lean4Lean.liftVar_consN_skipN
Proof state before:
case zero
n i : Nat
⊢ Lift.liftVar (Lift.consN (Lift.skipN n) Nat.zero) i = liftVar n i Nat.zero
Tactic:
simp [liftVar_skipN]
Proof state after:
no goals
Theorem: Lean4Lean.liftVar_consN_skipN
Proof state before:
case succ
n k : Nat
ih : ∀ {i : Nat}, Lift.liftVar (Lift.consN (Lift.skipN n) k) i = liftVar n i k
i : Nat
⊢ Lift.liftVar (Lift.consN (Lift.skipN n) (Nat.succ k)) i = liftVar n i (Nat.succ k)
Tactic:
cases i with simp [liftVar, Nat.succ_lt_succ_iff, ih]
| succ i => split <;> rfl
Proof state after:
no goals
Theorem: Lean4Lean.liftVar_consN_skipN
Proof state before:
case succ.succ
n k : Nat
ih : ∀ {i : Nat}, Lift.liftVar (Lift.consN (Lift.skipN n) k) i = liftVar n i k
i : Nat
⊢ (if i < k then i else n + i) + 1 = if i < k then Nat.succ i else n + Nat.succ i
Tactic:
split <;> rfl
Proof state after:
no goals
Theorem: Lean4Lean.liftVar_depth_zero
Proof state before:
l : Lift
n : Nat
H : Lift.depth l = 0
⊢ Lift.liftVar l n = n
Tactic:
induction l generalizing n <;> [skip; skip; cases n] <;> simp_all [Lift.depth]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.lift'_consN_skipN
Proof state before:
n : Nat
e : VExpr
k : Nat
⊢ liftN n e k = lift' e (Lift.consN (Lift.skipN n) k)
Tactic:
induction e generalizing k <;> simp [liftN, liftVar_consN_skipN, *]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.lift'_comp
Proof state before:
l₁ l₂ : Lift
e : VExpr
⊢ lift' (lift' e l₁) l₂ = lift' e (Lift.comp l₁ l₂)
Tactic:
induction e generalizing l₁ l₂ <;> simp [liftVar_comp, *]
Proof state after:
no goals
Theorem: Lean4Lean.VExpr.lift'_depth_zero
Proof state before:
l : Lift
e : VExpr
H : Lift.depth l = 0
⊢ lift' e l = e
Tactic:
induction e generalizing l <;> simp_all [liftVar_depth_zero]
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.inductionU1
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
H : IsDefEq env U Γ e1 e2 A
⊢ HasTypeU1 env U defEq Γ e1 A ∧ HasTypeU1 env U defEq Γ e2 A ∧ IsDefEqU1 env U hasType Γ e1 e2
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 hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
H : IsDefEq env U Γ e1 e2 A
H' : IsDefEqStrong env U Γ e1 e2 A
⊢ HasTypeU1 env U defEq Γ e1 A ∧ HasTypeU1 env U defEq Γ e2 A ∧ IsDefEqU1 env U hasType Γ e1 e2
Theorem: Lean4Lean.VEnv.IsDefEq.inductionU1
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
hΓ : OnCtx Γ (IsType env U)
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
H : IsDefEq env U Γ e1 e2 A
H' : IsDefEqStrong env U Γ e1 e2 A
⊢ HasTypeU1 env U defEq Γ e1 A ∧ HasTypeU1 env U defEq Γ e2 A ∧ IsDefEqU1 env U hasType Γ e1 e2
Tactic:
clear hΓ H
Proof state after:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
H' : IsDefEqStrong env U Γ e1 e2 A
⊢ HasTypeU1 env U defEq Γ e1 A ∧ HasTypeU1 env U defEq Γ e2 A ∧ IsDefEqU1 env U hasType Γ e1 e2
Theorem: Lean4Lean.VEnv.IsDefEq.inductionU1
Proof state before:
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
H' : IsDefEqStrong env U Γ e1 e2 A
⊢ HasTypeU1 env U defEq Γ e1 A ∧ HasTypeU1 env U defEq Γ e2 A ∧ IsDefEqU1 env U hasType Γ e1 e2
Tactic:
induction H' with
| bvar h => exact ⟨.bvar h, .bvar h, .refl⟩
| 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₂ _ _ h1 h2 h3 h4 h5 =>
  exact ⟨.const h1 h2 h4, .defeq sorry <| .const h1 h3 (h5.length_eq.symm.trans h4), .constDF h5⟩
| @sortDF l l' _ h1 h2 h3 =>
  refine ⟨.sort h1, ?_, .sortDF h3⟩
  exact .defeq (hdf (.sort (l := l'.succ) h2) (.sort (l := l.succ) h1)
    (.sortDF <| VLevel.succ_congr h3.symm)) (.sort h2)
| appDF _ _ _ _ _ _ _ _ _ ihf iha ihBa =>
  let ⟨hf, hf', ff⟩ := ihf; let ⟨ha, ha', aa⟩ := iha
  exact ⟨.app hf ha, .defeq (hdf ihBa.2.1 ihBa.1 (.symm ihBa.2.2)) (.app hf' ha'), .appDF ff aa⟩
| lamDF _ _ _ _ _ _ _ ihA ihB ihB' ihb ihb' =>
  refine ⟨.lam ihA.1 ihb.1, .defeq ?_ <| .lam ihA.2.1 ihb'.2.1, .lamDF ihA.2.2 ihb.2.2⟩
  exact hdf (.forallE ihA.2.1 ihB'.1) (.forallE ihA.1 ihB.1) <|
    .symm <| .forallEDF ihA.2.2 ihB.2.2
| 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 =>
  have h := hdf ih1.1 ih1.2.1 ih1.2.2; exact ⟨.defeq h ih2.1, .defeq h ih2.2.1, 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 := HasTypeU1.app ihe'.1 (.bvar .zero)
  rw [instN_bvar0] at this
  exact ⟨.lam ihA.1 this, ihe.1, .eta⟩
| 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.inductionU1
Proof state before:
case bvar
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : 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✝ :
  HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧
    HasTypeU1 env U defEq Γ✝ A✝ (VExpr.sort u✝) ∧ IsDefEqU1 env U hasType Γ✝ A✝ A✝
⊢ HasTypeU1 env U defEq Γ✝ (VExpr.bvar i✝) A✝ ∧
    HasTypeU1 env U defEq Γ✝ (VExpr.bvar i✝) A✝ ∧ IsDefEqU1 env U hasType Γ✝ (VExpr.bvar i✝) (VExpr.bvar i✝)
Tactic:
exact ⟨.bvar h, .bvar h, .refl⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.inductionU1
Proof state before:
case symm
env : VEnv
Γ : List VExpr
U : Nat
henv : Ordered env
e1 e2 A : VExpr
defEq hasType : List VExpr → VExpr → VExpr → Prop
hty : ∀ {Γ : List VExpr} {e A : VExpr}, HasTypeU1 env U defEq Γ e A → hasType Γ e A
hdf :
  ∀ {Γ : List VExpr} {e1 e2 A1 A2 : VExpr},
    HasTypeU1 env U defEq Γ e1 A1 → HasTypeU1 env U defEq Γ e2 A2 → IsDefEqU1 env U hasType Γ e1 e2 → defEq Γ e1 e2
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEqStrong env U Γ✝ e✝ e'✝ A✝
ih : HasTypeU1 env U defEq Γ✝ e✝ A✝ ∧ HasTypeU1 env U defEq Γ✝ e'✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ e✝ e'✝
⊢ HasTypeU1 env U defEq Γ✝ e'✝ A✝ ∧ HasTypeU1 env U defEq Γ✝ e✝ A✝ ∧ IsDefEqU1 env U hasType Γ✝ e'✝ e✝
Tactic:
exact ⟨ih.2.1, ih.1, .symm ih.2.2⟩
Proof state after:
no goals