internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
⊢ V x = V y ↔ V' (σ' x) = V' (σ' y)
Tactic:
congr! 1
Proof state after:
case a.h.e'_2
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
⊢ V x = V' (σ' x)

case a.h.e'_3
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
⊢ V y = V' (σ' y)
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
case a.h.e'_2
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
⊢ V x = V' (σ' x)
Tactic:
apply h2
Proof state after:
case a.h.e'_2.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
⊢ x ∈ binders ∨ σ' x ∉ binders
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
case a.h.e'_2.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
⊢ x ∈ binders ∨ σ' x ∉ binders
Tactic:
by_cases c1 : x ∈ binders
Proof state after:
case pos
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : x ∈ binders
⊢ x ∈ binders ∨ σ' x ∉ binders

case neg
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : x ∉ binders
⊢ x ∈ binders ∨ σ' x ∉ binders
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : x ∈ binders
⊢ x ∈ binders ∨ σ' x ∉ binders
Tactic:
left
Proof state after:
case pos.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : x ∈ binders
⊢ x ∈ binders
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
case pos.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : x ∈ binders
⊢ x ∈ binders
Tactic:
exact c1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : x ∉ binders
⊢ x ∈ binders ∨ σ' x ∉ binders
Tactic:
right
Proof state after:
case neg.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : x ∉ binders
⊢ σ' x ∉ binders
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
case neg.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : x ∉ binders
⊢ σ' x ∉ binders
Tactic:
simp only [h3 x c1]
Proof state after:
case neg.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : x ∉ binders
⊢ σ x ∉ binders
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
case neg.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : x ∉ binders
⊢ σ x ∉ binders
Tactic:
exact h1_left c1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
case a.h.e'_3
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
⊢ V y = V' (σ' y)
Tactic:
apply h2
Proof state after:
case a.h.e'_3.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
⊢ y ∈ binders ∨ σ' y ∉ binders
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
case a.h.e'_3.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
⊢ y ∈ binders ∨ σ' y ∉ binders
Tactic:
by_cases c1 : y ∈ binders
Proof state after:
case pos
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : y ∈ binders
⊢ y ∈ binders ∨ σ' y ∉ binders

case neg
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : y ∉ binders
⊢ y ∈ binders ∨ σ' y ∉ binders
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : y ∈ binders
⊢ y ∈ binders ∨ σ' y ∉ binders
Tactic:
left
Proof state after:
case pos.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : y ∈ binders
⊢ y ∈ binders
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
case pos.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : y ∈ binders
⊢ y ∈ binders
Tactic:
exact c1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : y ∉ binders
⊢ y ∈ binders ∨ σ' y ∉ binders
Tactic:
right
Proof state after:
case neg.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : y ∉ binders
⊢ σ' y ∉ binders
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
case neg.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : y ∉ binders
⊢ σ' y ∉ binders
Tactic:
simp only [h3 y c1]
Proof state after:
case neg.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : y ∉ binders
⊢ σ y ∉ binders
Theorem: FOL.NV.Sub.Var.All.Rec.substitution_theorem_aux
Proof state before:
case neg.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (σ σ' : VarName → VarName) (binders : Finset VarName) (F : Formula),
    admitsAux σ binders F →
      (∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)) →
        (∀ v ∈ binders, v = σ' v) →
          (∀ v ∉ binders, σ' v = σ v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ (fastReplaceFree σ' F))
x y : VarName
V V' : VarAssignment D
σ σ' : VarName → VarName
binders : Finset VarName
h2 : ∀ (v : VarName), v ∈ binders ∨ σ' v ∉ binders → V v = V' (σ' v)
h2' : ∀ v ∈ binders, v = σ' v
h3 : ∀ v ∉ binders, σ' v = σ v
h1_left : x ∉ binders → σ x ∉ binders
h1_right : y ∉ binders → σ y ∉ binders
c1 : y ∉ binders
⊢ σ y ∉ binders
Tactic:
exact h1_right c1
Proof state after:
no goals