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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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