internlm/Lean-Github huggingface dataset:
Theorem: EpsilonNFA.eval_from_iff
Proof state before:
case eps.refl
α σ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq σ
M : EpsilonNFA α σ
a : α
as : List α
IH : ∀ (S : List σ), (∃ s ∈ M.eval_from S as, s ∈ M.accepting_state_list) ↔ ∃ s ∈ S, M.toAbstract.eval s as
S : List σ
s : σ
l : List α
start_state✝ stop_state✝ : σ
h2 : M.toAbstract.epsilon start_state✝ stop_state✝
h1 : M.toAbstract.eval stop_state✝ (a :: as)
ih :
  a :: as = a :: as →
    ∃ s₁ s₂, M.toAbstract.EpsilonClosure stop_state✝ s₂ ∧ M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as
s₁ s₂ : σ
h3 : M.toAbstract.EpsilonClosure stop_state✝ s₂
h4 : M.toAbstract.symbol s₂ a s₁
h5 : M.toAbstract.eval s₁ as
⊢ ∃ s₁ s₂, M.toAbstract.EpsilonClosure start_state✝ s₂ ∧ M.toAbstract.symbol s₂ a s₁ ∧ M.toAbstract.eval s₁ as
Tactic:
exact ⟨_, _, .head h2 h3, h4, h5⟩
Proof state after:
no goals
Theorem: EpsilonNFA.accepts_iff
Proof state before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
input : List α
⊢ e.accepts input ↔ e.toAbstract.accepts input
Tactic:
simp [accepts, eval]
Proof state after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
input : List α
⊢ (∃ s ∈ e.eval_from e.starting_state_list input, s ∈ e.accepting_state_list) ↔ e.toAbstract.accepts input
Theorem: EpsilonNFA.accepts_iff
Proof state before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
input : List α
⊢ (∃ s ∈ e.eval_from e.starting_state_list input, s ∈ e.accepting_state_list) ↔ e.toAbstract.accepts input
Tactic:
rw [EpsilonNFA.eval_from_iff]
Proof state after:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
input : List α
⊢ (∃ s ∈ e.starting_state_list, e.toAbstract.eval s input) ↔ e.toAbstract.accepts input
Theorem: EpsilonNFA.accepts_iff
Proof state before:
α : Type
inst✝¹ : DecidableEq α
σ : Type
inst✝ : DecidableEq σ
e : EpsilonNFA α σ
input : List α
⊢ (∃ s ∈ e.starting_state_list, e.toAbstract.eval s input) ↔ e.toAbstract.accepts input
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_id
Proof state before:
F : Formula
⊢ fastReplaceFree id F = F
Tactic:
induction F
Proof state after:
case pred_const_
a✝¹ : PredName
a✝ : List VarName
⊢ fastReplaceFree id (pred_const_ a✝¹ a✝) = pred_const_ a✝¹ a✝

case pred_var_
a✝¹ : PredName
a✝ : List VarName
⊢ fastReplaceFree id (pred_var_ a✝¹ a✝) = pred_var_ a✝¹ a✝

case eq_
a✝¹ a✝ : VarName
⊢ fastReplaceFree id (eq_ a✝¹ a✝) = eq_ a✝¹ a✝

case true_

⊢ fastReplaceFree id true_ = true_

case false_

⊢ fastReplaceFree id false_ = false_

case not_
a✝ : Formula
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ fastReplaceFree id a✝.not_ = a✝.not_

case imp_
a✝¹ a✝ : Formula
a_ih✝¹ : fastReplaceFree id a✝¹ = a✝¹
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ fastReplaceFree id (a✝¹.imp_ a✝) = a✝¹.imp_ a✝

case and_
a✝¹ a✝ : Formula
a_ih✝¹ : fastReplaceFree id a✝¹ = a✝¹
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ fastReplaceFree id (a✝¹.and_ a✝) = a✝¹.and_ a✝

case or_
a✝¹ a✝ : Formula
a_ih✝¹ : fastReplaceFree id a✝¹ = a✝¹
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ fastReplaceFree id (a✝¹.or_ a✝) = a✝¹.or_ a✝

case iff_
a✝¹ a✝ : Formula
a_ih✝¹ : fastReplaceFree id a✝¹ = a✝¹
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ fastReplaceFree id (a✝¹.iff_ a✝) = a✝¹.iff_ a✝

case forall_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ fastReplaceFree id (forall_ a✝¹ a✝) = forall_ a✝¹ a✝

case exists_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ fastReplaceFree id (exists_ a✝¹ a✝) = exists_ a✝¹ a✝

case def_
a✝¹ : DefName
a✝ : List VarName
⊢ fastReplaceFree id (def_ a✝¹ a✝) = def_ a✝¹ a✝
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_id
Proof state before:
case pred_const_
a✝¹ : PredName
a✝ : List VarName
⊢ fastReplaceFree id (pred_const_ a✝¹ a✝) = pred_const_ a✝¹ a✝

case pred_var_
a✝¹ : PredName
a✝ : List VarName
⊢ fastReplaceFree id (pred_var_ a✝¹ a✝) = pred_var_ a✝¹ a✝

case eq_
a✝¹ a✝ : VarName
⊢ fastReplaceFree id (eq_ a✝¹ a✝) = eq_ a✝¹ a✝

case true_

⊢ fastReplaceFree id true_ = true_

case false_

⊢ fastReplaceFree id false_ = false_

case not_
a✝ : Formula
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ fastReplaceFree id a✝.not_ = a✝.not_

case imp_
a✝¹ a✝ : Formula
a_ih✝¹ : fastReplaceFree id a✝¹ = a✝¹
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ fastReplaceFree id (a✝¹.imp_ a✝) = a✝¹.imp_ a✝

case and_
a✝¹ a✝ : Formula
a_ih✝¹ : fastReplaceFree id a✝¹ = a✝¹
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ fastReplaceFree id (a✝¹.and_ a✝) = a✝¹.and_ a✝

case or_
a✝¹ a✝ : Formula
a_ih✝¹ : fastReplaceFree id a✝¹ = a✝¹
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ fastReplaceFree id (a✝¹.or_ a✝) = a✝¹.or_ a✝

case iff_
a✝¹ a✝ : Formula
a_ih✝¹ : fastReplaceFree id a✝¹ = a✝¹
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ fastReplaceFree id (a✝¹.iff_ a✝) = a✝¹.iff_ a✝

case forall_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ fastReplaceFree id (forall_ a✝¹ a✝) = forall_ a✝¹ a✝

case exists_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ fastReplaceFree id (exists_ a✝¹ a✝) = exists_ a✝¹ a✝

case def_
a✝¹ : DefName
a✝ : List VarName
⊢ fastReplaceFree id (def_ a✝¹ a✝) = def_ a✝¹ a✝
Tactic:
all_goals
  simp only [fastReplaceFree]
Proof state after:
case pred_const_
a✝¹ : PredName
a✝ : List VarName
⊢ pred_const_ a✝¹ (List.map id a✝) = pred_const_ a✝¹ a✝

case pred_var_
a✝¹ : PredName
a✝ : List VarName
⊢ pred_var_ a✝¹ (List.map id a✝) = pred_var_ a✝¹ a✝

case eq_
a✝¹ a✝ : VarName
⊢ eq_ (id a✝¹) (id a✝) = eq_ a✝¹ a✝

case not_
a✝ : Formula
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ (fastReplaceFree id a✝).not_ = a✝.not_

case imp_
a✝¹ a✝ : Formula
a_ih✝¹ : fastReplaceFree id a✝¹ = a✝¹
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ (fastReplaceFree id a✝¹).imp_ (fastReplaceFree id a✝) = a✝¹.imp_ a✝

case and_
a✝¹ a✝ : Formula
a_ih✝¹ : fastReplaceFree id a✝¹ = a✝¹
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ (fastReplaceFree id a✝¹).and_ (fastReplaceFree id a✝) = a✝¹.and_ a✝

case or_
a✝¹ a✝ : Formula
a_ih✝¹ : fastReplaceFree id a✝¹ = a✝¹
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ (fastReplaceFree id a✝¹).or_ (fastReplaceFree id a✝) = a✝¹.or_ a✝

case iff_
a✝¹ a✝ : Formula
a_ih✝¹ : fastReplaceFree id a✝¹ = a✝¹
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ (fastReplaceFree id a✝¹).iff_ (fastReplaceFree id a✝) = a✝¹.iff_ a✝

case forall_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ forall_ a✝¹ (fastReplaceFree (Function.updateITE id a✝¹ a✝¹) a✝) = forall_ a✝¹ a✝

case exists_
a✝¹ : VarName
a✝ : Formula
a_ih✝ : fastReplaceFree id a✝ = a✝
⊢ exists_ a✝¹ (fastReplaceFree (Function.updateITE id a✝¹ a✝¹) a✝) = exists_ a✝¹ a✝

case def_
a✝¹ : DefName
a✝ : List VarName
⊢ def_ a✝¹ (List.map id a✝) = def_ a✝¹ a✝
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_id
Proof state before:
X : DefName
xs : List VarName
⊢ def_ X (List.map id xs) = def_ X xs
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  congr!
  simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_id
Proof state before:
x y : VarName
⊢ eq_ (id x) (id y) = eq_ x y
Tactic:
case eq_ x y =>
  congr!
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_id
Proof state before:
phi : Formula
phi_ih : fastReplaceFree id phi = phi
⊢ (fastReplaceFree id phi).not_ = phi.not_
Tactic:
case not_ phi phi_ih =>
  congr!
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_id
Proof state before:
phi psi : Formula
phi_ih : fastReplaceFree id phi = phi
psi_ih : fastReplaceFree id psi = psi
⊢ (fastReplaceFree id phi).iff_ (fastReplaceFree id psi) = phi.iff_ psi
Tactic:
case
    imp_ phi psi phi_ih psi_ih
  | and_ phi psi phi_ih psi_ih
  | or_ phi psi phi_ih psi_ih
  | iff_ phi psi phi_ih psi_ih =>
  congr!
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_id
Proof state before:
x : VarName
phi : Formula
phi_ih : fastReplaceFree id phi = phi
⊢ exists_ x (fastReplaceFree (Function.updateITE id x x) phi) = exists_ x phi
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  congr!
  simp only [Function.updateITE_id]
  exact phi_ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_id
Proof state before:
case def_
a✝¹ : DefName
a✝ : List VarName
⊢ fastReplaceFree id (def_ a✝¹ a✝) = def_ a✝¹ a✝
Tactic:
simp only [fastReplaceFree]
Proof state after:
case def_
a✝¹ : DefName
a✝ : List VarName
⊢ def_ a✝¹ (List.map id a✝) = def_ a✝¹ a✝
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_id
Proof state before:
X : DefName
xs : List VarName
⊢ def_ X (List.map id xs) = def_ X xs
Tactic:
congr!
Proof state after:
case h.e'_2
X : DefName
xs : List VarName
⊢ List.map id xs = xs
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_id
Proof state before:
case h.e'_2
X : DefName
xs : List VarName
⊢ List.map id xs = xs
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_id
Proof state before:
x y : VarName
⊢ eq_ (id x) (id y) = eq_ x y
Tactic:
congr!
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_id
Proof state before:
phi : Formula
phi_ih : fastReplaceFree id phi = phi
⊢ (fastReplaceFree id phi).not_ = phi.not_
Tactic:
congr!
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_id
Proof state before:
phi psi : Formula
phi_ih : fastReplaceFree id phi = phi
psi_ih : fastReplaceFree id psi = psi
⊢ (fastReplaceFree id phi).iff_ (fastReplaceFree id psi) = phi.iff_ psi
Tactic:
congr!
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_id
Proof state before:
x : VarName
phi : Formula
phi_ih : fastReplaceFree id phi = phi
⊢ exists_ x (fastReplaceFree (Function.updateITE id x x) phi) = exists_ x phi
Tactic:
congr!
Proof state after:
case h.e'_2
x : VarName
phi : Formula
phi_ih : fastReplaceFree id phi = phi
⊢ fastReplaceFree (Function.updateITE id x x) phi = phi
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_id
Proof state before:
case h.e'_2
x : VarName
phi : Formula
phi_ih : fastReplaceFree id phi = phi
⊢ fastReplaceFree (Function.updateITE id x x) phi = phi
Tactic:
simp only [Function.updateITE_id]
Proof state after:
case h.e'_2
x : VarName
phi : Formula
phi_ih : fastReplaceFree id phi = phi
⊢ fastReplaceFree id phi = phi
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_id
Proof state before:
case h.e'_2
x : VarName
phi : Formula
phi_ih : fastReplaceFree id phi = phi
⊢ fastReplaceFree id phi = phi
Tactic:
exact phi_ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
X : DefName
xs : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ xs, σ v = σ' v
⊢ def_ X (List.map σ xs) = def_ X (List.map σ' xs)
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  congr! 1
  simp only [List.map_eq_map_iff]
  exact h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi → σ v = σ' v
⊢ (fastReplaceFree σ phi).not_ = (fastReplaceFree σ' phi).not_
Tactic:
case not_ phi phi_ih =>
  congr! 1
  exact phi_ih σ σ' h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
x : VarName
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → σ v = σ' v
⊢ exists_ x (fastReplaceFree (Function.updateITE σ x x) phi) =
    exists_ x (fastReplaceFree (Function.updateITE σ' x x) phi)
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  congr! 1
  apply phi_ih
  intro v a1
  simp only [Function.updateITE]
  split_ifs
  case _ c1 =>
    rfl
  case _ c1 =>
    apply h1
    tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
case def_
a✝¹ : DefName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (def_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (def_ a✝¹ a✝) = fastReplaceFree σ' (def_ a✝¹ a✝)
Tactic:
simp only [isFreeIn] at h1
Proof state after:
case def_
a✝¹ : DefName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ a✝, σ v = σ' v
⊢ fastReplaceFree σ (def_ a✝¹ a✝) = fastReplaceFree σ' (def_ a✝¹ a✝)
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
case def_
a✝¹ : DefName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ a✝, σ v = σ' v
⊢ fastReplaceFree σ (def_ a✝¹ a✝) = fastReplaceFree σ' (def_ a✝¹ a✝)
Tactic:
simp only [fastReplaceFree]
Proof state after:
case def_
a✝¹ : DefName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ a✝, σ v = σ' v
⊢ def_ a✝¹ (List.map σ a✝) = def_ a✝¹ (List.map σ' a✝)
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
X : DefName
xs : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ xs, σ v = σ' v
⊢ def_ X (List.map σ xs) = def_ X (List.map σ' xs)
Tactic:
congr! 1
Proof state after:
case h.e'_2
X : DefName
xs : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ xs, σ v = σ' v
⊢ List.map σ xs = List.map σ' xs
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
case h.e'_2
X : DefName
xs : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ xs, σ v = σ' v
⊢ List.map σ xs = List.map σ' xs
Tactic:
simp only [List.map_eq_map_iff]
Proof state after:
case h.e'_2
X : DefName
xs : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ xs, σ v = σ' v
⊢ ∀ x ∈ xs, σ x = σ' x
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
case h.e'_2
X : DefName
xs : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ xs, σ v = σ' v
⊢ ∀ x ∈ xs, σ x = σ' x
Tactic:
exact h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ eq_ (σ x) (σ y) = eq_ (σ' x) (σ' y)
Tactic:
congr! 1
Proof state after:
case h.e'_1
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ σ x = σ' x

case h.e'_2
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ σ y = σ' y
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
case h.e'_1
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ σ x = σ' x
Tactic:
apply h1
Proof state after:
case h.e'_1.a
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ x = x ∨ x = y
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
case h.e'_1.a
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ x = x ∨ x = y
Tactic:
left
Proof state after:
case h.e'_1.a.h
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ x = x
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
case h.e'_1.a.h
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ x = x
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
case h.e'_2
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ σ y = σ' y
Tactic:
apply h1
Proof state after:
case h.e'_2.a
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ y = x ∨ y = y
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
case h.e'_2.a
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ y = x ∨ y = y
Tactic:
right
Proof state after:
case h.e'_2.a.h
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ y = y
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
case h.e'_2.a.h
x y : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = x ∨ v = y → σ v = σ' v
⊢ y = y
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi → σ v = σ' v
⊢ (fastReplaceFree σ phi).not_ = (fastReplaceFree σ' phi).not_
Tactic:
congr! 1
Proof state after:
case h.e'_1
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi → σ v = σ' v
⊢ fastReplaceFree σ phi = fastReplaceFree σ' phi
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
case h.e'_1
phi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi → σ v = σ' v
⊢ fastReplaceFree σ phi = fastReplaceFree σ' phi
Tactic:
exact phi_ih σ σ' h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
⊢ (fastReplaceFree σ phi).iff_ (fastReplaceFree σ psi) = (fastReplaceFree σ' phi).iff_ (fastReplaceFree σ' psi)
Tactic:
congr! 1
Proof state after:
case h.e'_1
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
⊢ fastReplaceFree σ phi = fastReplaceFree σ' phi

case h.e'_2
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
⊢ fastReplaceFree σ psi = fastReplaceFree σ' psi
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
case h.e'_1
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
⊢ fastReplaceFree σ phi = fastReplaceFree σ' phi
Tactic:
apply phi_ih
Proof state after:
case h.e'_1.h1
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
⊢ ∀ (v : VarName), isFreeIn v phi → σ v = σ' v
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
case h.e'_1.h1
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
⊢ ∀ (v : VarName), isFreeIn v phi → σ v = σ' v
Tactic:
intro v a1
Proof state after:
case h.e'_1.h1
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
⊢ σ v = σ' v
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
case h.e'_1.h1
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
⊢ σ v = σ' v
Tactic:
apply h1
Proof state after:
case h.e'_1.h1.a
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
⊢ isFreeIn v phi ∨ isFreeIn v psi
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
case h.e'_1.h1.a
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
⊢ isFreeIn v phi ∨ isFreeIn v psi
Tactic:
left
Proof state after:
case h.e'_1.h1.a.h
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
⊢ isFreeIn v phi
Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
case h.e'_1.h1.a.h
phi psi : Formula
phi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v phi → σ v = σ' v) → fastReplaceFree σ phi = fastReplaceFree σ' phi
psi_ih :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v psi → σ v = σ' v) → fastReplaceFree σ psi = fastReplaceFree σ' psi
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → σ v = σ' v
v : VarName
a1 : isFreeIn v phi
⊢ isFreeIn v phi
Tactic:
exact a1
Proof state after:
no goals