internlm/Lean-Github huggingface dataset:
Theorem: Finset.mem_image_update
Proof state before:
case right
α : Type
inst✝ : DecidableEq α
x y : α
f : α → α
S : Finset α
h1 : ¬y = x
h2 : y ∈ S
⊢ (if y = x then x else f y) = f y
Tactic:
simp only [if_neg h1]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ✝ : VarName → VarName
binders✝ : Finset VarName
V V' : VarAssignment D
h2 : ∀ v ∈ binders✝, V v = V' (σ✝ v)
h3 : ∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)
h4 : ∀ v ∈ binders✝, v = σ✝ v
⊢ Holds D I V E false_ ↔ Holds D I V' E false_
Tactic:
case true_ | false_ =>
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
phi phi' : Formula
a✝ : IsSubAux σ' binders' phi phi'
ih_2 :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders', V v = V' (σ' v)) →
      (∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)) →
        (∀ v ∈ binders', v = σ' v) → (Holds D I V E phi ↔ Holds D I V' E phi')
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ Holds D I V E phi.not_ ↔ Holds D I V' E phi'.not_
Tactic:
case not_ σ' binders' phi phi' _ ih_2 =>
  simp only [Holds]
  congr! 1
  exact ih_2 V V' h2 h3 h4
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ Holds D I V E (pred_var_ X' xs') ↔ Holds D I V' E (pred_var_ X' (List.map σ' xs'))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ I.pred_var_ X' (List.map V xs') ↔ I.pred_var_ X' (List.map V' (List.map σ' xs'))
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ I.pred_var_ X' (List.map V xs') ↔ I.pred_var_ X' (List.map V' (List.map σ' xs'))
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ I.pred_var_ X' (List.map V xs') ↔ I.pred_var_ X' (List.map (V' ∘ σ') xs')
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ I.pred_var_ X' (List.map V xs') ↔ I.pred_var_ X' (List.map (V' ∘ σ') xs')
Tactic:
congr! 1
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ List.map V xs' = List.map (V' ∘ σ') xs'
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ List.map V xs' = List.map (V' ∘ σ') xs'
Tactic:
simp only [List.map_eq_map_iff]
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ ∀ x ∈ xs', V x = (V' ∘ σ') x
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ ∀ x ∈ xs', V x = (V' ∘ σ') x
Tactic:
intro x a1
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
x : VarName
a1 : x ∈ xs'
⊢ V x = (V' ∘ σ') x
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
x : VarName
a1 : x ∈ xs'
⊢ V x = (V' ∘ σ') x
Tactic:
simp
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
x : VarName
a1 : x ∈ xs'
⊢ V x = V' (σ' x)
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
x : VarName
a1 : x ∈ xs'
⊢ V x = V' (σ' x)
Tactic:
by_cases c1 : x ∈ binders'
Proof state after:
case pos
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
x : VarName
a1 : x ∈ xs'
c1 : x ∈ binders'
⊢ V x = V' (σ' x)

case neg
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
x : VarName
a1 : x ∈ xs'
c1 : x ∉ binders'
⊢ V x = V' (σ' x)
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
x : VarName
a1 : x ∈ xs'
c1 : x ∈ binders'
⊢ V x = V' (σ' x)
Tactic:
exact h2 x c1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
x : VarName
a1 : x ∈ xs'
c1 : x ∉ binders'
⊢ V x = V' (σ' x)
Tactic:
apply h3
Proof state after:
case neg.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
x : VarName
a1 : x ∈ xs'
c1 : x ∉ binders'
⊢ σ' x ∉ binders'
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case neg.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : PredName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
x : VarName
a1 : x ∈ xs'
c1 : x ∉ binders'
⊢ σ' x ∉ binders'
Tactic:
exact ih_1 x a1 c1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ Holds D I V E (eq_ x y) ↔ Holds D I V' E (eq_ (σ' x) (σ' y))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ V x = V y ↔ V' (σ' x) = V' (σ' y)
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ V x = V y ↔ V' (σ' x) = V' (σ' y)
Tactic:
congr! 1
Proof state after:
case a.h.e'_2
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ V x = V' (σ' x)

case a.h.e'_3
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ V y = V' (σ' y)
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case a.h.e'_2
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ V x = V' (σ' x)
Tactic:
by_cases c1 : x ∈ binders'
Proof state after:
case pos
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : x ∈ binders'
⊢ V x = V' (σ' x)

case neg
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : x ∉ binders'
⊢ V x = V' (σ' x)
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : x ∈ binders'
⊢ V x = V' (σ' x)
Tactic:
exact h2 x c1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : x ∉ binders'
⊢ V x = V' (σ' x)
Tactic:
apply h3
Proof state after:
case neg.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : x ∉ binders'
⊢ σ' x ∉ binders'
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case neg.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : x ∉ binders'
⊢ σ' x ∉ binders'
Tactic:
apply ih_1
Proof state after:
case neg.a.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : x ∉ binders'
⊢ x = x ∨ x = y

case neg.a.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : x ∉ binders'
⊢ x ∉ binders'
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case neg.a.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : x ∉ binders'
⊢ x = x ∨ x = y
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case neg.a.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : x ∉ binders'
⊢ x ∉ binders'
Tactic:
exact c1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case a.h.e'_3
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
⊢ V y = V' (σ' y)
Tactic:
by_cases c1 : y ∈ binders'
Proof state after:
case pos
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : y ∈ binders'
⊢ V y = V' (σ' y)

case neg
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : y ∉ binders'
⊢ V y = V' (σ' y)
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : y ∈ binders'
⊢ V y = V' (σ' y)
Tactic:
exact h2 y c1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : y ∉ binders'
⊢ V y = V' (σ' y)
Tactic:
apply h3
Proof state after:
case neg.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : y ∉ binders'
⊢ σ' y ∉ binders'
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case neg.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : y ∉ binders'
⊢ σ' y ∉ binders'
Tactic:
apply ih_1
Proof state after:
case neg.a.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : y ∉ binders'
⊢ y = x ∨ y = y

case neg.a.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : y ∉ binders'
⊢ y ∉ binders'
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case neg.a.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : y ∉ binders'
⊢ y = x ∨ y = y
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
case neg.a.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
x y : VarName
ih_1 : ∀ (v : VarName), v = x ∨ v = y → v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
c1 : y ∉ binders'
⊢ y ∉ binders'
Tactic:
exact c1
Proof state after:
no goals