Theorem: FOL.NV.T_21_1 (FOL/NV/Margaris/Fol.lean)

State before:
x y : VarName
⊢ IsProof (forall_ x (forall_ y ((eq_ x y).imp_ (eq_ y x))))
Tactic:
apply generalization
State after:
case h1
x y : VarName
⊢ IsDeduct ∅ (forall_ y ((eq_ x y).imp_ (eq_ y x)))

case h2
x y : VarName
⊢ ∀ H ∈ ∅, ¬isFreeIn x H

State before:
case h1
x y : VarName
⊢ IsDeduct ∅ (forall_ y ((eq_ x y).imp_ (eq_ y x)))
Tactic:
apply generalization
State after:
case h1.h1
x y : VarName
⊢ IsDeduct ∅ ((eq_ x y).imp_ (eq_ y x))

case h1.h2
x y : VarName
⊢ ∀ H ∈ ∅, ¬isFreeIn y H

State before:
case h1.h1
x y : VarName
⊢ IsDeduct ∅ ((eq_ x y).imp_ (eq_ y x))
Tactic:
apply IsDeduct.mp_ (eq_ y y)
State after:
case h1.h1.a
x y : VarName
⊢ IsDeduct ∅ ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x)))

case h1.h1.a
x y : VarName
⊢ IsDeduct ∅ (eq_ y y)

State before:
case h1.h1.a
x y : VarName
⊢ IsDeduct ∅ ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x)))
Tactic:
apply IsDeduct.mp_ (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))
State after:
case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅
    ((((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y))).imp_ ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x))))

case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅ (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))

State before:
case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅
    ((((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y))).imp_ ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x))))
Tactic:
simp only [def_iff_]
State after:
case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅
    ((((eq_ y y).and_ (eq_ x y)).imp_ (((eq_ y x).imp_ (eq_ y y)).and_ ((eq_ y y).imp_ (eq_ y x)))).imp_
      ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x))))

State before:
case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅
    ((((eq_ y y).and_ (eq_ x y)).imp_ (((eq_ y x).imp_ (eq_ y y)).and_ ((eq_ y y).imp_ (eq_ y x)))).imp_
      ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x))))
Tactic:
simp only [def_and_]
State after:
case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅
    ((((eq_ y y).imp_ (eq_ x y).not_).not_.imp_
          (((eq_ y x).imp_ (eq_ y y)).imp_ ((eq_ y y).imp_ (eq_ y x)).not_).not_).imp_
      ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x))))

State before:
case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅
    ((((eq_ y y).imp_ (eq_ x y).not_).not_.imp_
          (((eq_ y x).imp_ (eq_ y y)).imp_ ((eq_ y y).imp_ (eq_ y x)).not_).not_).imp_
      ((eq_ y y).imp_ ((eq_ x y).imp_ (eq_ y x))))
Tactic:
SC
State after:
no goals

State before:
case h1.h1.a.a
x y : VarName
⊢ IsDeduct ∅ (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))
Tactic:
apply specId y
State after:
case h1.h1.a.a.h1
x y : VarName
⊢ IsDeduct ∅ (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y))))

State before:
case h1.h1.a.a.h1
x y : VarName
⊢ IsDeduct ∅ (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y))))
Tactic:
apply specId y
State after:
case h1.h1.a.a.h1.h1
x y : VarName
⊢ IsDeduct ∅ (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))))

State before:
case h1.h1.a.a.h1.h1
x y : VarName
⊢ IsDeduct ∅ (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))))
Tactic:
apply specId x
State after:
case h1.h1.a.a.h1.h1.h1
x y : VarName
⊢ IsDeduct ∅ (forall_ x (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y))))))

State before:
case h1.h1.a.a.h1.h1.h1
x y : VarName
⊢ IsDeduct ∅ (forall_ x (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y))))))
Tactic:
apply specId y
State after:
case h1.h1.a.a.h1.h1.h1.h1
x y : VarName
⊢ IsDeduct ∅
    (forall_ y (forall_ x (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))))))

State before:
case h1.h1.a.a.h1.h1.h1.h1
x y : VarName
⊢ IsDeduct ∅
    (forall_ y (forall_ x (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))))))
Tactic:
apply IsDeduct.axiom_
State after:
case h1.h1.a.a.h1.h1.h1.h1.a
x y : VarName
⊢ IsAxiom (forall_ y (forall_ x (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))))))

State before:
case h1.h1.a.a.h1.h1.h1.h1.a
x y : VarName
⊢ IsAxiom (forall_ y (forall_ x (forall_ y (forall_ y (((eq_ y y).and_ (eq_ x y)).imp_ ((eq_ y x).iff_ (eq_ y y)))))))
Tactic:
exact IsAxiom.eq_2_eq_ y x y y
State after:
no goals

State before:
case h1.h1.a
x y : VarName
⊢ IsDeduct ∅ (eq_ y y)
Tactic:
apply specId y
State after:
case h1.h1.a.h1
x y : VarName
⊢ IsDeduct ∅ (forall_ y (eq_ y y))

State before:
case h1.h1.a.h1
x y : VarName
⊢ IsDeduct ∅ (forall_ y (eq_ y y))
Tactic:
apply IsDeduct.axiom_
State after:
case h1.h1.a.h1.a
x y : VarName
⊢ IsAxiom (forall_ y (eq_ y y))

State before:
case h1.h1.a.h1.a
x y : VarName
⊢ IsAxiom (forall_ y (eq_ y y))
Tactic:
exact IsAxiom.eq_1_ y
State after:
no goals

State before:
case h1.h2
x y : VarName
⊢ ∀ H ∈ ∅, ¬isFreeIn y H
Tactic:
intro H a1
State after:
case h1.h2
x y : VarName
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn y H

State before:
case h1.h2
x y : VarName
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn y H
Tactic:
simp at a1
State after:
no goals

State before:
case h2
x y : VarName
⊢ ∀ H ∈ ∅, ¬isFreeIn x H
Tactic:
intro H a1
State after:
case h2
x y : VarName
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn x H

State before:
case h2
x y : VarName
H : Formula
a1 : H ∈ ∅
⊢ ¬isFreeIn x H
Tactic:
simp at a1
State after:
no goals