Theorem: LN.lc_at_instantiate (FOL/LN/Paper.lean)

State before:
F : Formula
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) F) ↔ Formula.lc_at (j + zs.length) F
Tactic:
induction F generalizing j zs
State after:
case pred_
a✝¹ : String
a✝ : List Var
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (pred_ a✝¹ a✝)) ↔ Formula.lc_at (j + zs.length) (pred_ a✝¹ a✝)

case not_
a✝ : Formula
a_ih✝ :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) a✝) ↔ Formula.lc_at (j + zs.length) a✝
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) a✝.not_) ↔ Formula.lc_at (j + zs.length) a✝.not_

case imp_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) a✝¹) ↔ Formula.lc_at (j + zs.length) a✝¹
a_ih✝ :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) a✝) ↔ Formula.lc_at (j + zs.length) a✝
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (a✝¹.imp_ a✝)) ↔ Formula.lc_at (j + zs.length) (a✝¹.imp_ a✝)

case forall_
a✝¹ : String
a✝ : Formula
a_ih✝ :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) a✝) ↔ Formula.lc_at (j + zs.length) a✝
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (forall_ a✝¹ a✝)) ↔
    Formula.lc_at (j + zs.length) (forall_ a✝¹ a✝)

State before:
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi.not_) ↔ Formula.lc_at (j + zs.length) phi.not_
Tactic:
case not_ phi phi_ih =>
  simp only [Formula.openList]
  simp only [Formula.lc_at]
  apply phi_ih
State after:
no goals

State before:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (forall_ a✝ phi)) ↔
    Formula.lc_at (j + zs.length) (forall_ a✝ phi)
Tactic:
case forall_ _ phi phi_ih =>
  simp only [Formula.openList]
  simp only [Formula.lc_at]
  simp only [phi_ih]
  have s1 : j + 1 + List.length zs = j + List.length zs + 1
  linarith;
  simp only [s1]
State after:
no goals

State before:
X : String
vs : List Var
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (pred_ X vs)) ↔ Formula.lc_at (j + zs.length) (pred_ X vs)
Tactic:
simp only [Formula.openList]
State after:
X : String
vs : List Var
j : ℕ
zs : List String
⊢ Formula.lc_at j (pred_ X (List.map (Var.openList j (List.map free_ zs)) vs)) ↔
    Formula.lc_at (j + zs.length) (pred_ X vs)

State before:
X : String
vs : List Var
j : ℕ
zs : List String
⊢ Formula.lc_at j (pred_ X (List.map (Var.openList j (List.map free_ zs)) vs)) ↔
    Formula.lc_at (j + zs.length) (pred_ X vs)
Tactic:
simp only [Formula.lc_at]
State after:
X : String
vs : List Var
j : ℕ
zs : List String
⊢ (∀ v ∈ List.map (Var.openList j (List.map free_ zs)) vs, Var.lc_at j v) ↔ ∀ v ∈ vs, Var.lc_at (j + zs.length) v

State before:
X : String
vs : List Var
j : ℕ
zs : List String
⊢ (∀ v ∈ List.map (Var.openList j (List.map free_ zs)) vs, Var.lc_at j v) ↔ ∀ v ∈ vs, Var.lc_at (j + zs.length) v
Tactic:
constructor
State after:
case mp
X : String
vs : List Var
j : ℕ
zs : List String
⊢ (∀ v ∈ List.map (Var.openList j (List.map free_ zs)) vs, Var.lc_at j v) → ∀ v ∈ vs, Var.lc_at (j + zs.length) v

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

State before:
case mp
X : String
vs : List Var
j : ℕ
zs : List String
⊢ (∀ v ∈ List.map (Var.openList j (List.map free_ zs)) vs, Var.lc_at j v) → ∀ v ∈ vs, Var.lc_at (j + zs.length) v
Tactic:
intro a1 v a2
State after:
case mp
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ List.map (Var.openList j (List.map free_ zs)) vs, Var.lc_at j v
v : Var
a2 : v ∈ vs
⊢ Var.lc_at (j + zs.length) v

State before:
case mp
X : String
vs : List Var
j : ℕ
zs : List String
a1 : ∀ v ∈ List.map (Var.openList j (List.map free_ zs)) vs, Var.lc_at j v
v : Var
a2 : v ∈ vs
⊢ Var.lc_at (j + zs.length) v
Tactic:
specialize a1 (Var.openList j (List.map free_ zs) v)
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 ∈ 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 : bound_ (i' - j - zs.length + j) = bound_ i
⊢ i < j
Tactic:
case _ c2 =>
  exfalso
  apply c2
  exact Nat.sub_lt_left_of_lt_add c1 a1
State after:
no goals

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

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 : bound_ (i' - j - zs.length + j) = bound_ i
⊢ i < j
Tactic:
exfalso
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'
c2 : ¬i' - j < zs.length
a3_right : bound_ (i' - j - zs.length + j) = bound_ i
⊢ False

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 : bound_ (i' - j - zs.length + j) = bound_ i
⊢ False
Tactic:
apply c2
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'
c2 : ¬i' - j < zs.length
a3_right : bound_ (i' - j - zs.length + j) = bound_ i
⊢ i' - j < zs.length

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 : bound_ (i' - j - zs.length + j) = bound_ i
⊢ i' - j < zs.length
Tactic:
exact Nat.sub_lt_left_of_lt_add c1 a1
State after:
no goals

State before:
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi.not_) ↔ Formula.lc_at (j + zs.length) phi.not_
Tactic:
simp only [Formula.openList]
State after:
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi).not_ ↔ Formula.lc_at (j + zs.length) phi.not_

State before:
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi).not_ ↔ Formula.lc_at (j + zs.length) phi.not_
Tactic:
simp only [Formula.lc_at]
State after:
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi

State before:
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
Tactic:
apply phi_ih
State after:
no goals

State before:
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (phi.imp_ psi)) ↔ Formula.lc_at (j + zs.length) (phi.imp_ psi)
Tactic:
simp only [Formula.openList]
State after:
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j ((Formula.openList j (List.map free_ zs) phi).imp_ (Formula.openList j (List.map free_ zs) psi)) ↔
    Formula.lc_at (j + zs.length) (phi.imp_ psi)

State before:
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j ((Formula.openList j (List.map free_ zs) phi).imp_ (Formula.openList j (List.map free_ zs) psi)) ↔
    Formula.lc_at (j + zs.length) (phi.imp_ psi)
Tactic:
simp only [Formula.lc_at]
State after:
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ∧
      Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔
    Formula.lc_at (j + zs.length) phi ∧ Formula.lc_at (j + zs.length) psi

State before:
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ∧
      Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔
    Formula.lc_at (j + zs.length) phi ∧ Formula.lc_at (j + zs.length) psi
Tactic:
congr! 1
State after:
case a.h.e'_1.a
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi

case a.h.e'_2.a
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi

State before:
case a.h.e'_1.a
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
Tactic:
apply phi_ih
State after:
no goals

State before:
case a.h.e'_2.a
phi psi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
psi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) psi) ↔ Formula.lc_at (j + zs.length) psi
Tactic:
apply psi_ih
State after:
no goals

State before:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (Formula.openList j (List.map free_ zs) (forall_ a✝ phi)) ↔
    Formula.lc_at (j + zs.length) (forall_ a✝ phi)
Tactic:
simp only [Formula.openList]
State after:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (forall_ a✝ (Formula.openList (j + 1) (List.map free_ zs) phi)) ↔
    Formula.lc_at (j + zs.length) (forall_ a✝ phi)

State before:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at j (forall_ a✝ (Formula.openList (j + 1) (List.map free_ zs) phi)) ↔
    Formula.lc_at (j + zs.length) (forall_ a✝ phi)
Tactic:
simp only [Formula.lc_at]
State after:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at (j + 1) (Formula.openList (j + 1) (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length + 1) phi

State before:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at (j + 1) (Formula.openList (j + 1) (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length + 1) phi
Tactic:
simp only [phi_ih]
State after:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at (j + 1 + zs.length) phi ↔ Formula.lc_at (j + zs.length + 1) phi

State before:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ Formula.lc_at (j + 1 + zs.length) phi ↔ Formula.lc_at (j + zs.length + 1) phi
Tactic:
have s1 : j + 1 + List.length zs = j + List.length zs + 1
State after:
case s1
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ j + 1 + zs.length = j + zs.length + 1

a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
s1 : j + 1 + zs.length = j + zs.length + 1
⊢ Formula.lc_at (j + 1 + zs.length) phi ↔ Formula.lc_at (j + zs.length + 1) phi

State before:
case s1
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
⊢ j + 1 + zs.length = j + zs.length + 1

a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
s1 : j + 1 + zs.length = j + zs.length + 1
⊢ Formula.lc_at (j + 1 + zs.length) phi ↔ Formula.lc_at (j + zs.length + 1) phi
Tactic:
linarith
State after:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
s1 : j + 1 + zs.length = j + zs.length + 1
⊢ Formula.lc_at (j + 1 + zs.length) phi ↔ Formula.lc_at (j + zs.length + 1) phi

State before:
a✝ : String
phi : Formula
phi_ih :
  ∀ (j : ℕ) (zs : List String),
    Formula.lc_at j (Formula.openList j (List.map free_ zs) phi) ↔ Formula.lc_at (j + zs.length) phi
j : ℕ
zs : List String
s1 : j + 1 + zs.length = j + zs.length + 1
⊢ Formula.lc_at (j + 1 + zs.length) phi ↔ Formula.lc_at (j + zs.length + 1) phi
Tactic:
simp only [s1]
State after:
no goals