internlm/Lean-Github huggingface dataset:
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
X : String
vs : List Var
⊢ (pred_ X vs).freeVarSet \ {free_ z} ⊆ (pred_ X (List.map ((free_ z).subst t) vs)).freeVarSet
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
z : String
t : Var
X : String
vs : List Var
⊢ vs.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) vs).toFinset.biUnion Var.freeVarSet
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
X : String
vs : List Var
⊢ vs.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) vs).toFinset.biUnion Var.freeVarSet
Tactic:
induction vs
Proof state after:
case nil
z : String
t : Var
X : String
⊢ [].toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) []).toFinset.biUnion Var.freeVarSet

case cons
z : String
t : Var
X : String
head✝ : Var
tail✝ : List Var
tail_ih✝ :
  tail✝.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆
    (List.map ((free_ z).subst t) tail✝).toFinset.biUnion Var.freeVarSet
⊢ (head✝ :: tail✝).toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆
    (List.map ((free_ z).subst t) (head✝ :: tail✝)).toFinset.biUnion Var.freeVarSet
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
X : String
⊢ [].toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) []).toFinset.biUnion Var.freeVarSet
Tactic:
case nil =>
  simp
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
⊢ (hd :: tl).toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆
    (List.map ((free_ z).subst t) (hd :: tl)).toFinset.biUnion Var.freeVarSet
Tactic:
case cons hd tl ih =>
  simp
  have s1 : (Var.freeVarSet hd ∪ Finset.biUnion (List.toFinset tl) Var.freeVarSet) \ {free_ z} = (Var.freeVarSet hd \ {free_ z}) ∪ ((Finset.biUnion (List.toFinset tl) Var.freeVarSet) \ {free_ z})
  exact Finset.union_sdiff_distrib (Var.freeVarSet hd) (Finset.biUnion (List.toFinset tl) Var.freeVarSet) {free_ z}
  simp only [s1]
  exact Finset.union_subset_union (VarSubstFreeVarSet' z t hd) ih
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
X : String
⊢ [].toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) []).toFinset.biUnion Var.freeVarSet
Tactic:
simp
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
⊢ (hd :: tl).toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆
    (List.map ((free_ z).subst t) (hd :: tl)).toFinset.biUnion Var.freeVarSet
Tactic:
simp
Proof state after:
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
⊢ (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} ⊆
    ((free_ z).subst t hd).freeVarSet ∪ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
⊢ (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} ⊆
    ((free_ z).subst t hd).freeVarSet ∪ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
Tactic:
have s1 : (Var.freeVarSet hd ∪ Finset.biUnion (List.toFinset tl) Var.freeVarSet) \ {free_ z} = (Var.freeVarSet hd \ {free_ z}) ∪ ((Finset.biUnion (List.toFinset tl) Var.freeVarSet) \ {free_ z})
Proof state after:
case s1
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
⊢ (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}

z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
s1 :
  (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}
⊢ (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} ⊆
    ((free_ z).subst t hd).freeVarSet ∪ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
case s1
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
⊢ (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}

z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
s1 :
  (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}
⊢ (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} ⊆
    ((free_ z).subst t hd).freeVarSet ∪ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
Tactic:
exact Finset.union_sdiff_distrib (Var.freeVarSet hd) (Finset.biUnion (List.toFinset tl) Var.freeVarSet) {free_ z}
Proof state after:
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
s1 :
  (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}
⊢ (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} ⊆
    ((free_ z).subst t hd).freeVarSet ∪ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
s1 :
  (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}
⊢ (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} ⊆
    ((free_ z).subst t hd).freeVarSet ∪ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
Tactic:
simp only [s1]
Proof state after:
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
s1 :
  (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}
⊢ hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆
    ((free_ z).subst t hd).freeVarSet ∪ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
X : String
hd : Var
tl : List Var
ih : tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
s1 :
  (hd.freeVarSet ∪ tl.toFinset.biUnion Var.freeVarSet) \ {free_ z} =
    hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z}
⊢ hd.freeVarSet \ {free_ z} ∪ tl.toFinset.biUnion Var.freeVarSet \ {free_ z} ⊆
    ((free_ z).subst t hd).freeVarSet ∪ (List.map ((free_ z).subst t) tl).toFinset.biUnion Var.freeVarSet
Tactic:
exact Finset.union_subset_union (VarSubstFreeVarSet' z t hd) ih
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ phi.not_.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi.not_).freeVarSet
Tactic:
simp only [Formula.subst]
Proof state after:
z : String
t : Var
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ phi.not_.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).not_.freeVarSet
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ phi.not_.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).not_.freeVarSet
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
z : String
t : Var
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
Tactic:
exact phi_ih
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ (phi.imp_ psi).freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t (phi.imp_ psi)).freeVarSet
Tactic:
simp only [Formula.subst]
Proof state after:
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ (phi.imp_ psi).freeVarSet \ {free_ z} ⊆
    ((Formula.subst (free_ z) t phi).imp_ (Formula.subst (free_ z) t psi)).freeVarSet
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ (phi.imp_ psi).freeVarSet \ {free_ z} ⊆
    ((Formula.subst (free_ z) t phi).imp_ (Formula.subst (free_ z) t psi)).freeVarSet
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ (phi.freeVarSet ∪ psi.freeVarSet) \ {free_ z} ⊆
    (Formula.subst (free_ z) t phi).freeVarSet ∪ (Formula.subst (free_ z) t psi).freeVarSet
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ (phi.freeVarSet ∪ psi.freeVarSet) \ {free_ z} ⊆
    (Formula.subst (free_ z) t phi).freeVarSet ∪ (Formula.subst (free_ z) t psi).freeVarSet
Tactic:
apply Finset.diff_union_subset
Proof state after:
case h1
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet

case h2
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
case h1
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
Tactic:
apply phi_ih
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
case h2
z : String
t : Var
phi psi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
psi_ih : psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
⊢ psi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t psi).freeVarSet
Tactic:
apply psi_ih
Proof state after:
no goals
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
x : String
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ (forall_ x phi).freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t (forall_ x phi)).freeVarSet
Tactic:
simp only [Formula.subst]
Proof state after:
z : String
t : Var
x : String
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ (forall_ x phi).freeVarSet \ {free_ z} ⊆ (forall_ x (Formula.subst (free_ z) t phi)).freeVarSet
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
x : String
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ (forall_ x phi).freeVarSet \ {free_ z} ⊆ (forall_ x (Formula.subst (free_ z) t phi)).freeVarSet
Tactic:
simp only [Formula.freeVarSet]
Proof state after:
z : String
t : Var
x : String
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
Theorem: LN.FormulaSubstFreeVarSet'
Proof state before:
z : String
t : Var
x : String
phi : Formula
phi_ih : phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
⊢ phi.freeVarSet \ {free_ z} ⊆ (Formula.subst (free_ z) t phi).freeVarSet
Tactic:
exact phi_ih
Proof state after:
no goals
Theorem: LN.SubOpenVar
Proof state before:
v : Var
σ : String → String
j : ℕ
z : String
h1 : σ z = z
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) v) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) v)
Tactic:
cases v
Proof state after:
case free_
σ : String → String
j : ℕ
z : String
h1 : σ z = z
a✝ : String
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) (free_ a✝)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (free_ a✝))

case bound_
σ : String → String
j : ℕ
z : String
h1 : σ z = z
a✝ : ℕ
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) (bound_ a✝)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ a✝))
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
x : String
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) (free_ x)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (free_ x))
Tactic:
case free_ x =>
  conv =>
    lhs
    simp only [Var.open]
    simp only [Var.substFun]
    simp only [str_fun_to_var_fun]
Proof state after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
x : String
⊢ free_ (σ x) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (free_ x))
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) (bound_ i)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
case bound_ i =>
  conv =>
    lhs
    simp only [Var.open]
  split_ifs
  case pos c1 =>
    simp only [Var.substFun]
    simp only [Var.open]
    simp only [if_pos c1]
  case pos c1 c2 =>
    simp only [Var.substFun]
    simp only [str_fun_to_var_fun]
    simp only [Var.open]
    simp only [if_neg c1]
    simp only [if_pos c2]
    simp only [h1]
  case neg c1 c2 =>
    simp only [Var.substFun]
    simp only [Var.open]
    simp only [if_neg c1]
    simp only [if_neg c2]
Proof state after:
no goals
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
x : String
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) (free_ x)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (free_ x))
Tactic:
conv =>
  lhs
  simp only [Var.open]
  simp only [Var.substFun]
  simp only [str_fun_to_var_fun]
Proof state after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
x : String
⊢ free_ (σ x) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (free_ x))
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
⊢ Var.substFun (str_fun_to_var_fun σ) (Var.open j (free_ z) (bound_ i)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
conv =>
  lhs
  simp only [Var.open]
Proof state after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
⊢ Var.substFun (str_fun_to_var_fun σ) (if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
⊢ Var.substFun (str_fun_to_var_fun σ) (if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
split_ifs
Proof state after:
case pos
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
h✝ : i < j
⊢ Var.substFun (str_fun_to_var_fun σ) (bound_ i) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))

case pos
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
h✝¹ : ¬i < j
h✝ : i = j
⊢ Var.substFun (str_fun_to_var_fun σ) (free_ z) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))

case neg
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
h✝¹ : ¬i < j
h✝ : ¬i = j
⊢ Var.substFun (str_fun_to_var_fun σ) (bound_ (i - 1)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : i < j
⊢ Var.substFun (str_fun_to_var_fun σ) (bound_ i) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
case pos c1 =>
  simp only [Var.substFun]
  simp only [Var.open]
  simp only [if_pos c1]
Proof state after:
no goals
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ Var.substFun (str_fun_to_var_fun σ) (free_ z) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
case pos c1 c2 =>
  simp only [Var.substFun]
  simp only [str_fun_to_var_fun]
  simp only [Var.open]
  simp only [if_neg c1]
  simp only [if_pos c2]
  simp only [h1]
Proof state after:
no goals
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ Var.substFun (str_fun_to_var_fun σ) (bound_ (i - 1)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
case neg c1 c2 =>
  simp only [Var.substFun]
  simp only [Var.open]
  simp only [if_neg c1]
  simp only [if_neg c2]
Proof state after:
no goals
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : i < j
⊢ Var.substFun (str_fun_to_var_fun σ) (bound_ i) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
simp only [Var.substFun]
Proof state after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : i < j
⊢ bound_ i = Var.open j (free_ z) (bound_ i)
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : i < j
⊢ bound_ i = Var.open j (free_ z) (bound_ i)
Tactic:
simp only [Var.open]
Proof state after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : i < j
⊢ bound_ i = if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : i < j
⊢ bound_ i = if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)
Tactic:
simp only [if_pos c1]
Proof state after:
no goals
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ Var.substFun (str_fun_to_var_fun σ) (free_ z) = Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
simp only [Var.substFun]
Proof state after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ str_fun_to_var_fun σ (free_ z) = Var.open j (free_ z) (bound_ i)
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ str_fun_to_var_fun σ (free_ z) = Var.open j (free_ z) (bound_ i)
Tactic:
simp only [str_fun_to_var_fun]
Proof state after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ free_ (σ z) = Var.open j (free_ z) (bound_ i)
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ free_ (σ z) = Var.open j (free_ z) (bound_ i)
Tactic:
simp only [Var.open]
Proof state after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ free_ (σ z) = if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ free_ (σ z) = if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)
Tactic:
simp only [if_neg c1]
Proof state after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ free_ (σ z) = if i = j then free_ z else bound_ (i - 1)
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ free_ (σ z) = if i = j then free_ z else bound_ (i - 1)
Tactic:
simp only [if_pos c2]
Proof state after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ free_ (σ z) = free_ z
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : i = j
⊢ free_ (σ z) = free_ z
Tactic:
simp only [h1]
Proof state after:
no goals
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ Var.substFun (str_fun_to_var_fun σ) (bound_ (i - 1)) =
    Var.open j (free_ z) (Var.substFun (str_fun_to_var_fun σ) (bound_ i))
Tactic:
simp only [Var.substFun]
Proof state after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ bound_ (i - 1) = Var.open j (free_ z) (bound_ i)
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ bound_ (i - 1) = Var.open j (free_ z) (bound_ i)
Tactic:
simp only [Var.open]
Proof state after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ bound_ (i - 1) = if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ bound_ (i - 1) = if i < j then bound_ i else if i = j then free_ z else bound_ (i - 1)
Tactic:
simp only [if_neg c1]
Proof state after:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ bound_ (i - 1) = if i = j then free_ z else bound_ (i - 1)
Theorem: LN.SubOpenVar
Proof state before:
σ : String → String
j : ℕ
z : String
h1 : σ z = z
i : ℕ
c1 : ¬i < j
c2 : ¬i = j
⊢ bound_ (i - 1) = if i = j then free_ z else bound_ (i - 1)
Tactic:
simp only [if_neg c2]
Proof state after:
no goals
Theorem: LN.ShiftVarOpenList
Proof state before:
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d = shift D V d ∘ Var.openList (j + 1) (List.map free_ zs)
Tactic:
funext v
Proof state after:
case h
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
v : Var
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d v = (shift D V d ∘ Var.openList (j + 1) (List.map free_ zs)) v