Theorem: FOL.NV.Sub.Var.One.Rec.admits_iff_fastAdmits (FOL/NV/Sub/Var/One/Rec/Admits.lean)

State before:
F : Formula
v u : VarName
⊢ admits v u F ↔ fastAdmits v u F
Tactic:
simp only [admits]
State after:
F : Formula
v u : VarName
⊢ admitsAux v u ∅ F ↔ fastAdmits v u F

State before:
F : Formula
v u : VarName
⊢ admitsAux v u ∅ F ↔ fastAdmits v u F
Tactic:
simp only [fastAdmits]
State after:
F : Formula
v u : VarName
⊢ admitsAux v u ∅ F ↔ fastAdmitsAux v u ∅ F

State before:
F : Formula
v u : VarName
⊢ admitsAux v u ∅ F ↔ fastAdmitsAux v u ∅ F
Tactic:
constructor
State after:
case mp
F : Formula
v u : VarName
⊢ admitsAux v u ∅ F → fastAdmitsAux v u ∅ F

case mpr
F : Formula
v u : VarName
⊢ fastAdmitsAux v u ∅ F → admitsAux v u ∅ F

State before:
case mp
F : Formula
v u : VarName
⊢ admitsAux v u ∅ F → fastAdmitsAux v u ∅ F
Tactic:
apply admitsAux_imp_fastAdmitsAux
State after:
case mp.h1
F : Formula
v u : VarName
⊢ v ∉ ∅

State before:
case mp.h1
F : Formula
v u : VarName
⊢ v ∉ ∅
Tactic:
simp
State after:
no goals

State before:
case mpr
F : Formula
v u : VarName
⊢ fastAdmitsAux v u ∅ F → admitsAux v u ∅ F
Tactic:
exact fastAdmitsAux_imp_admitsAux F v u ∅
State after:
no goals