internlm/Lean-Github huggingface dataset:
Theorem: LN.lc_at_instantiate
Proof state before:
case mp
X : String
vs : List Var
j : ℕ
zs : List String
v : Var
a2 : v ∈ vs
a1 :
  Var.openList j (List.map free_ zs) v ∈ List.map (Var.openList j (List.map free_ zs)) vs →
    Var.lc_at j (Var.openList j (List.map free_ zs) v)
⊢ Var.lc_at (j + zs.length) v
Tactic:
simp at a1
Proof state after:
case mp
X : String
vs : List Var
j : ℕ
zs : List String
v : Var
a2 : v ∈ vs
a1 :
  ∀ x ∈ vs,
    Var.openList j (List.map free_ zs) x = Var.openList j (List.map free_ zs) v →
      Var.lc_at j (Var.openList j (List.map free_ zs) v)
⊢ Var.lc_at (j + zs.length) v
Theorem: LN.lc_at_instantiate
Proof state before:
case mp
X : String
vs : List Var
j : ℕ
zs : List String
v : Var
a2 : v ∈ vs
a1 :
  ∀ x ∈ vs,
    Var.openList j (List.map free_ zs) x = Var.openList j (List.map free_ zs) v →
      Var.lc_at j (Var.openList j (List.map free_ zs) v)
⊢ Var.lc_at (j + zs.length) v
Tactic:
specialize a1 v a2
Proof state after:
case mp
X : String
vs : List Var
j : ℕ
zs : List String
v : Var
a2 : v ∈ vs
a1 :
  Var.openList j (List.map free_ zs) v = Var.openList j (List.map free_ zs) v →
    Var.lc_at j (Var.openList j (List.map free_ zs) v)
⊢ Var.lc_at (j + zs.length) v
Theorem: LN.lc_at_instantiate
Proof state before:
case mp
X : String
vs : List Var
j : ℕ
zs : List String
v : Var
a2 : v ∈ vs
a1 :
  Var.openList j (List.map free_ zs) v = Var.openList j (List.map free_ zs) v →
    Var.lc_at j (Var.openList j (List.map free_ zs) v)
⊢ Var.lc_at (j + zs.length) v
Tactic:
simp at a1
Proof state after:
case mp
X : String
vs : List Var
j : ℕ
zs : List String
v : Var
a2 : v ∈ vs
a1 : Var.lc_at j (Var.openList j (List.map free_ zs) v)
⊢ Var.lc_at (j + zs.length) v
Theorem: LN.lc_at_instantiate
Proof state before:
case mp
X : String
vs : List Var
j : ℕ
zs : List String
v : Var
a2 : v ∈ vs
a1 : Var.lc_at j (Var.openList j (List.map free_ zs) v)
⊢ Var.lc_at (j + zs.length) v
Tactic:
cases v
Proof state after:
case mp.free_
X : String
vs : List Var
j : ℕ
zs : List String
a✝ : String
a2 : free_ a✝ ∈ vs
a1 : Var.lc_at j (Var.openList j (List.map free_ zs) (free_ a✝))
⊢ Var.lc_at (j + zs.length) (free_ a✝)

case mp.bound_
X : String
vs : List Var
j : ℕ
zs : List String
a✝ : ℕ
a2 : bound_ a✝ ∈ vs
a1 : Var.lc_at j (Var.openList j (List.map free_ zs) (bound_ a✝))
⊢ Var.lc_at (j + zs.length) (bound_ a✝)
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
x : String
a2 : free_ x ∈ vs
a1 : Var.lc_at j (Var.openList j (List.map free_ zs) (free_ x))
⊢ Var.lc_at (j + zs.length) (free_ x)
Tactic:
case _ x =>
  simp only [Var.lc_at]
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
a1 : Var.lc_at j (Var.openList j (List.map free_ zs) (bound_ i))
⊢ Var.lc_at (j + zs.length) (bound_ i)
Tactic:
case _ i =>
  simp only [Var.lc_at]
  simp only [Var.openList] at a1
  split at a1
  case _ c1 =>
    linarith
  case _ c1 =>
    split at a1
    case _ c2 =>
      simp at c2
      exact lt_add_of_tsub_lt_left c2
    case _ c2 =>
      simp only [Var.lc_at] at a1
      simp at a1
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
x : String
a2 : free_ x ∈ vs
a1 : Var.lc_at j (Var.openList j (List.map free_ zs) (free_ x))
⊢ Var.lc_at (j + zs.length) (free_ x)
Tactic:
simp only [Var.lc_at]
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
a1 : Var.lc_at j (Var.openList j (List.map free_ zs) (bound_ i))
⊢ Var.lc_at (j + zs.length) (bound_ i)
Tactic:
simp only [Var.lc_at]
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
a1 : Var.lc_at j (Var.openList j (List.map free_ zs) (bound_ i))
⊢ i < j + zs.length
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
a1 : Var.lc_at j (Var.openList j (List.map free_ zs) (bound_ i))
⊢ i < j + zs.length
Tactic:
simp only [Var.openList] at a1
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
a1 :
  Var.lc_at j
    (if i < j then bound_ i
    else
      if x : i - j < (List.map free_ zs).length then (List.map free_ zs)[i - j]
      else bound_ (i - j - (List.map free_ zs).length + j))
⊢ i < j + zs.length
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
a1 :
  Var.lc_at j
    (if i < j then bound_ i
    else
      if x : i - j < (List.map free_ zs).length then (List.map free_ zs)[i - j]
      else bound_ (i - j - (List.map free_ zs).length + j))
⊢ i < j + zs.length
Tactic:
split at a1
Proof state after:
case inl
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
h✝ : i < j
a1 : Var.lc_at j (bound_ i)
⊢ i < j + zs.length

case inr
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
h✝ : ¬i < j
a1 :
  Var.lc_at j
    (if x : i - j < (List.map free_ zs).length then (List.map free_ zs)[i - j]
    else bound_ (i - j - (List.map free_ zs).length + j))
⊢ i < j + zs.length
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
c1 : i < j
a1 : Var.lc_at j (bound_ i)
⊢ i < j + zs.length
Tactic:
case _ c1 =>
  linarith
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
c1 : ¬i < j
a1 :
  Var.lc_at j
    (if x : i - j < (List.map free_ zs).length then (List.map free_ zs)[i - j]
    else bound_ (i - j - (List.map free_ zs).length + j))
⊢ i < j + zs.length
Tactic:
case _ c1 =>
  split at a1
  case _ c2 =>
    simp at c2
    exact lt_add_of_tsub_lt_left c2
  case _ c2 =>
    simp only [Var.lc_at] at a1
    simp at a1
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
c1 : i < j
a1 : Var.lc_at j (bound_ i)
⊢ i < j + zs.length
Tactic:
linarith
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
c1 : ¬i < j
a1 :
  Var.lc_at j
    (if x : i - j < (List.map free_ zs).length then (List.map free_ zs)[i - j]
    else bound_ (i - j - (List.map free_ zs).length + j))
⊢ i < j + zs.length
Tactic:
split at a1
Proof state after:
case inl
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
c1 : ¬i < j
h✝ : i - j < (List.map free_ zs).length
a1 : Var.lc_at j (List.map free_ zs)[i - j]
⊢ i < j + zs.length

case inr
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
c1 : ¬i < j
h✝ : ¬i - j < (List.map free_ zs).length
a1 : Var.lc_at j (bound_ (i - j - (List.map free_ zs).length + j))
⊢ i < j + zs.length
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
c1 : ¬i < j
c2 : i - j < (List.map free_ zs).length
a1 : Var.lc_at j (List.map free_ zs)[i - j]
⊢ i < j + zs.length
Tactic:
case _ c2 =>
  simp at c2
  exact lt_add_of_tsub_lt_left c2
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
c1 : ¬i < j
c2 : ¬i - j < (List.map free_ zs).length
a1 : Var.lc_at j (bound_ (i - j - (List.map free_ zs).length + j))
⊢ i < j + zs.length
Tactic:
case _ c2 =>
  simp only [Var.lc_at] at a1
  simp at a1
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
c1 : ¬i < j
c2 : i - j < (List.map free_ zs).length
a1 : Var.lc_at j (List.map free_ zs)[i - j]
⊢ i < j + zs.length
Tactic:
simp at c2
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
c1 : ¬i < j
c2✝ : i - j < (List.map free_ zs).length
a1 : Var.lc_at j (List.map free_ zs)[i - j]
c2 : i - j < zs.length
⊢ i < j + zs.length
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
c1 : ¬i < j
c2✝ : i - j < (List.map free_ zs).length
a1 : Var.lc_at j (List.map free_ zs)[i - j]
c2 : i - j < zs.length
⊢ i < j + zs.length
Tactic:
exact lt_add_of_tsub_lt_left c2
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
c1 : ¬i < j
c2 : ¬i - j < (List.map free_ zs).length
a1 : Var.lc_at j (bound_ (i - j - (List.map free_ zs).length + j))
⊢ i < j + zs.length
Tactic:
simp only [Var.lc_at] at a1
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
c1 : ¬i < j
c2 : ¬i - j < (List.map free_ zs).length
a1 : i - j - (List.map free_ zs).length + j < j
⊢ i < j + zs.length
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a2 : bound_ i ∈ vs
c1 : ¬i < j
c2 : ¬i - j < (List.map free_ zs).length
a1 : i - j - (List.map free_ zs).length + j < j
⊢ i < j + zs.length
Tactic:
simp at a1
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
case mpr
X : String
vs : List Var
j : ℕ
zs : List String
⊢ (∀ v ∈ vs, Var.lc_at (j + zs.length) v) → ∀ v ∈ List.map (Var.openList j (List.map free_ zs)) vs, Var.lc_at j v
Tactic:
intro a1 v a2
Proof state after:
case mpr
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
v : Var
a2 : v ∈ List.map (Var.openList j (List.map free_ zs)) vs
⊢ Var.lc_at j v
Theorem: LN.lc_at_instantiate
Proof state before:
case mpr
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
v : Var
a2 : v ∈ List.map (Var.openList j (List.map free_ zs)) vs
⊢ Var.lc_at j v
Tactic:
cases v
Proof state after:
case mpr.free_
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
a✝ : String
a2 : free_ a✝ ∈ List.map (Var.openList j (List.map free_ zs)) vs
⊢ Var.lc_at j (free_ a✝)

case mpr.bound_
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
a✝ : ℕ
a2 : bound_ a✝ ∈ List.map (Var.openList j (List.map free_ zs)) vs
⊢ Var.lc_at j (bound_ a✝)
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
x : String
a2 : free_ x ∈ List.map (Var.openList j (List.map free_ zs)) vs
⊢ Var.lc_at j (free_ x)
Tactic:
case _ x =>
  simp only [Var.lc_at]
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
i : ℕ
a2 : bound_ i ∈ List.map (Var.openList j (List.map free_ zs)) vs
⊢ Var.lc_at j (bound_ i)
Tactic:
case _ i =>
  simp only [Var.lc_at]
  simp at a2
  apply Exists.elim a2
  intro z a3
  clear a2
  cases a3
  case _ a3_left a3_right =>
    specialize a1 z a3_left
    cases z
    case _ x =>
      simp only [Var.openList] at a3_right
    case _ i' =>
      simp only [Var.lc_at] at a1
      simp only [Var.openList] at a3_right
      split at a3_right
      case _ c1 =>
        simp at a3_right
        subst a3_right
        exact c1
      case _ c1 =>
        simp at c1
        simp at a3_right
        split at a3_right
        case _ c2 =>
          contradiction
        case _ c2 =>
          exfalso
          apply c2
          exact Nat.sub_lt_left_of_lt_add c1 a1
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
x : String
a2 : free_ x ∈ List.map (Var.openList j (List.map free_ zs)) vs
⊢ Var.lc_at j (free_ x)
Tactic:
simp only [Var.lc_at]
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
i : ℕ
a2 : bound_ i ∈ List.map (Var.openList j (List.map free_ zs)) vs
⊢ Var.lc_at j (bound_ i)
Tactic:
simp only [Var.lc_at]
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
i : ℕ
a2 : bound_ i ∈ List.map (Var.openList j (List.map free_ zs)) vs
⊢ i < j
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
i : ℕ
a2 : bound_ i ∈ List.map (Var.openList j (List.map free_ zs)) vs
⊢ i < j
Tactic:
simp at a2
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
i : ℕ
a2 : ∃ a ∈ vs, Var.openList j (List.map free_ zs) a = bound_ i
⊢ i < j
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
i : ℕ
a2 : ∃ a ∈ vs, Var.openList j (List.map free_ zs) a = bound_ i
⊢ i < j
Tactic:
apply Exists.elim a2
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
i : ℕ
a2 : ∃ a ∈ vs, Var.openList j (List.map free_ zs) a = bound_ i
⊢ ∀ (a : Var), a ∈ vs ∧ Var.openList j (List.map free_ zs) a = bound_ i → i < j
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
i : ℕ
a2 : ∃ a ∈ vs, Var.openList j (List.map free_ zs) a = bound_ i
⊢ ∀ (a : Var), a ∈ vs ∧ Var.openList j (List.map free_ zs) a = bound_ i → i < j
Tactic:
intro z a3
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
i : ℕ
a2 : ∃ a ∈ vs, Var.openList j (List.map free_ zs) a = bound_ i
z : Var
a3 : z ∈ vs ∧ Var.openList j (List.map free_ zs) z = bound_ i
⊢ i < j
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
i : ℕ
a2 : ∃ a ∈ vs, Var.openList j (List.map free_ zs) a = bound_ i
z : Var
a3 : z ∈ vs ∧ Var.openList j (List.map free_ zs) z = bound_ i
⊢ i < j
Tactic:
clear a2
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
i : ℕ
z : Var
a3 : z ∈ vs ∧ Var.openList j (List.map free_ zs) z = bound_ i
⊢ i < j
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
i : ℕ
z : Var
a3 : z ∈ vs ∧ Var.openList j (List.map free_ zs) z = bound_ i
⊢ i < j
Tactic:
cases a3
Proof state after:
case intro
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
i : ℕ
z : Var
left✝ : z ∈ vs
right✝ : Var.openList j (List.map free_ zs) z = bound_ i
⊢ i < j
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
i : ℕ
z : Var
a3_left : z ∈ vs
a3_right : Var.openList j (List.map free_ zs) z = bound_ i
⊢ i < j
Tactic:
case _ a3_left a3_right =>
  specialize a1 z a3_left
  cases z
  case _ x =>
    simp only [Var.openList] at a3_right
  case _ i' =>
    simp only [Var.lc_at] at a1
    simp only [Var.openList] at a3_right
    split at a3_right
    case _ c1 =>
      simp at a3_right
      subst a3_right
      exact c1
    case _ c1 =>
      simp at c1
      simp at a3_right
      split at a3_right
      case _ c2 =>
        contradiction
      case _ c2 =>
        exfalso
        apply c2
        exact Nat.sub_lt_left_of_lt_add c1 a1
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ vs, Var.lc_at (j + zs.length) v
i : ℕ
z : Var
a3_left : z ∈ vs
a3_right : Var.openList j (List.map free_ zs) z = bound_ i
⊢ i < j
Tactic:
specialize a1 z a3_left
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
z : Var
a3_left : z ∈ vs
a3_right : Var.openList j (List.map free_ zs) z = bound_ i
a1 : Var.lc_at (j + zs.length) z
⊢ i < j
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
z : Var
a3_left : z ∈ vs
a3_right : Var.openList j (List.map free_ zs) z = bound_ i
a1 : Var.lc_at (j + zs.length) z
⊢ i < j
Tactic:
cases z
Proof state after:
case free_
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
a✝ : String
a3_left : free_ a✝ ∈ vs
a3_right : Var.openList j (List.map free_ zs) (free_ a✝) = bound_ i
a1 : Var.lc_at (j + zs.length) (free_ a✝)
⊢ i < j

case bound_
X : String
vs : List Var
j : ℕ
zs : List String
i a✝ : ℕ
a3_left : bound_ a✝ ∈ vs
a3_right : Var.openList j (List.map free_ zs) (bound_ a✝) = bound_ i
a1 : Var.lc_at (j + zs.length) (bound_ a✝)
⊢ i < j
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
x : String
a3_left : free_ x ∈ vs
a3_right : Var.openList j (List.map free_ zs) (free_ x) = bound_ i
a1 : Var.lc_at (j + zs.length) (free_ x)
⊢ i < j
Tactic:
case _ x =>
  simp only [Var.openList] at a3_right
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a3_right : Var.openList j (List.map free_ zs) (bound_ i') = bound_ i
a1 : Var.lc_at (j + zs.length) (bound_ i')
⊢ i < j
Tactic:
case _ i' =>
  simp only [Var.lc_at] at a1
  simp only [Var.openList] at a3_right
  split at a3_right
  case _ c1 =>
    simp at a3_right
    subst a3_right
    exact c1
  case _ c1 =>
    simp at c1
    simp at a3_right
    split at a3_right
    case _ c2 =>
      contradiction
    case _ c2 =>
      exfalso
      apply c2
      exact Nat.sub_lt_left_of_lt_add c1 a1
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i : ℕ
x : String
a3_left : free_ x ∈ vs
a3_right : Var.openList j (List.map free_ zs) (free_ x) = bound_ i
a1 : Var.lc_at (j + zs.length) (free_ x)
⊢ i < j
Tactic:
simp only [Var.openList] at a3_right
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a3_right : Var.openList j (List.map free_ zs) (bound_ i') = bound_ i
a1 : Var.lc_at (j + zs.length) (bound_ i')
⊢ i < j
Tactic:
simp only [Var.lc_at] at a1
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a3_right : Var.openList j (List.map free_ zs) (bound_ i') = bound_ i
a1 : i' < j + zs.length
⊢ i < j
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a3_right : Var.openList j (List.map free_ zs) (bound_ i') = bound_ i
a1 : i' < j + zs.length
⊢ i < j
Tactic:
simp only [Var.openList] at a3_right
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
a3_right :
  (if i' < j then bound_ i'
    else
      if x : i' - j < (List.map free_ zs).length then (List.map free_ zs)[i' - j]
      else bound_ (i' - j - (List.map free_ zs).length + j)) =
    bound_ i
⊢ i < j
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
a3_right :
  (if i' < j then bound_ i'
    else
      if x : i' - j < (List.map free_ zs).length then (List.map free_ zs)[i' - j]
      else bound_ (i' - j - (List.map free_ zs).length + j)) =
    bound_ i
⊢ i < j
Tactic:
split at a3_right
Proof state after:
case inl
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
h✝ : i' < j
a3_right : bound_ i' = bound_ i
⊢ i < j

case inr
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
h✝ : ¬i' < j
a3_right :
  (if x : i' - j < (List.map free_ zs).length then (List.map free_ zs)[i' - j]
    else bound_ (i' - j - (List.map free_ zs).length + j)) =
    bound_ i
⊢ i < j
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : i' < j
a3_right : bound_ i' = bound_ i
⊢ i < j
Tactic:
case _ c1 =>
  simp at a3_right
  subst a3_right
  exact c1
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : ¬i' < j
a3_right :
  (if x : i' - j < (List.map free_ zs).length then (List.map free_ zs)[i' - j]
    else bound_ (i' - j - (List.map free_ zs).length + j)) =
    bound_ i
⊢ i < j
Tactic:
case _ c1 =>
  simp at c1
  simp at a3_right
  split at a3_right
  case _ c2 =>
    contradiction
  case _ c2 =>
    exfalso
    apply c2
    exact Nat.sub_lt_left_of_lt_add c1 a1
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : i' < j
a3_right : bound_ i' = bound_ i
⊢ i < j
Tactic:
simp at a3_right
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : i' < j
a3_right : i' = i
⊢ i < j
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : i' < j
a3_right : i' = i
⊢ i < j
Tactic:
subst a3_right
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : i' < j
⊢ i' < j
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : i' < j
⊢ i' < j
Tactic:
exact c1
Proof state after:
no goals
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : ¬i' < j
a3_right :
  (if x : i' - j < (List.map free_ zs).length then (List.map free_ zs)[i' - j]
    else bound_ (i' - j - (List.map free_ zs).length + j)) =
    bound_ i
⊢ i < j
Tactic:
simp at c1
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
a3_right :
  (if x : i' - j < (List.map free_ zs).length then (List.map free_ zs)[i' - j]
    else bound_ (i' - j - (List.map free_ zs).length + j)) =
    bound_ i
c1 : j ≤ i'
⊢ i < j
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
a3_right :
  (if x : i' - j < (List.map free_ zs).length then (List.map free_ zs)[i' - j]
    else bound_ (i' - j - (List.map free_ zs).length + j)) =
    bound_ i
c1 : j ≤ i'
⊢ i < j
Tactic:
simp at a3_right
Proof state after:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : j ≤ i'
a3_right : (if h : i' - j < zs.length then free_ (zs.get ⟨i' - j, ⋯⟩) else bound_ (i' - j - zs.length + j)) = bound_ i
⊢ i < j
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : j ≤ i'
a3_right : (if h : i' - j < zs.length then free_ (zs.get ⟨i' - j, ⋯⟩) else bound_ (i' - j - zs.length + j)) = bound_ i
⊢ i < j
Tactic:
split at a3_right
Proof state after:
case inl
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : j ≤ i'
h✝ : i' - j < zs.length
a3_right : False
⊢ i < j

case inr
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : j ≤ i'
h✝ : ¬i' - j < zs.length
a3_right : bound_ (i' - j - zs.length + j) = bound_ i
⊢ i < j
Theorem: LN.lc_at_instantiate
Proof state before:
X : String
vs : List Var
j : ℕ
zs : List String
i i' : ℕ
a3_left : bound_ i' ∈ vs
a1 : i' < j + zs.length
c1 : j ≤ i'
c2 : i' - j < zs.length
a3_right : False
⊢ i < j
Tactic:
case _ c2 =>
  contradiction
Proof state after:
no goals