Theorem: FOL.NV.T_14_3 (FOL/NV/Margaris/Prop.lean)

State before:
P Q : Formula
Δ : Set Formula
h1 : IsDeduct (Δ ∪ {P}) Q
⊢ IsDeduct Δ (P.imp_ Q)
Tactic:
induction h1
State after:
case axiom_
P Q : Formula
Δ : Set Formula
phi✝ : Formula
a✝ : IsAxiom phi✝
⊢ IsDeduct Δ (P.imp_ phi✝)

case assume_
P Q : Formula
Δ : Set Formula
phi✝ : Formula
a✝ : phi✝ ∈ Δ ∪ {P}
⊢ IsDeduct Δ (P.imp_ phi✝)

case mp_
P Q : Formula
Δ : Set Formula
phi✝ psi✝ : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (phi✝.imp_ psi✝)
a✝ : IsDeduct (Δ ∪ {P}) phi✝
a_ih✝¹ : IsDeduct Δ (P.imp_ (phi✝.imp_ psi✝))
a_ih✝ : IsDeduct Δ (P.imp_ phi✝)
⊢ IsDeduct Δ (P.imp_ psi✝)

State before:
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ (P.imp_ h1_phi)
Tactic:
apply IsDeduct.mp_ h1_phi
State after:
case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ (h1_phi.imp_ (P.imp_ h1_phi))

case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ h1_phi

State before:
case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ (h1_phi.imp_ (P.imp_ h1_phi))
Tactic:
apply IsDeduct.axiom_
State after:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom (h1_phi.imp_ (P.imp_ h1_phi))

State before:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom (h1_phi.imp_ (P.imp_ h1_phi))
Tactic:
exact IsAxiom.prop_1_ h1_phi P
State after:
no goals

State before:
case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct Δ h1_phi
Tactic:
apply IsDeduct.axiom_
State after:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom h1_phi

State before:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom h1_phi
Tactic:
exact h1_1
State after:
no goals

State before:
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ ∪ {P}
⊢ IsDeduct Δ (P.imp_ h1_phi)
Tactic:
simp at h1_1
State after:
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi = P ∨ h1_phi ∈ Δ
⊢ IsDeduct Δ (P.imp_ h1_phi)

State before:
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi = P ∨ h1_phi ∈ Δ
⊢ IsDeduct Δ (P.imp_ h1_phi)
Tactic:
cases h1_1
State after:
case inl
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h✝ : h1_phi = P
⊢ IsDeduct Δ (P.imp_ h1_phi)

case inr
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h✝ : h1_phi ∈ Δ
⊢ IsDeduct Δ (P.imp_ h1_phi)

State before:
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi = P
⊢ IsDeduct Δ (P.imp_ h1_phi)
Tactic:
case inl h1_1 =>
  subst h1_1
  apply proof_imp_deduct
  exact prop_id h1_phi
State after:
no goals

State before:
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi = P
⊢ IsDeduct Δ (P.imp_ h1_phi)
Tactic:
subst h1_1
State after:
Q : Formula
Δ : Set Formula
h1_phi : Formula
⊢ IsDeduct Δ (h1_phi.imp_ h1_phi)

State before:
Q : Formula
Δ : Set Formula
h1_phi : Formula
⊢ IsDeduct Δ (h1_phi.imp_ h1_phi)
Tactic:
apply proof_imp_deduct
State after:
case h1
Q : Formula
Δ : Set Formula
h1_phi : Formula
⊢ IsProof (h1_phi.imp_ h1_phi)

State before:
case h1
Q : Formula
Δ : Set Formula
h1_phi : Formula
⊢ IsProof (h1_phi.imp_ h1_phi)
Tactic:
exact prop_id h1_phi
State after:
no goals

State before:
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ (P.imp_ h1_phi)
Tactic:
apply IsDeduct.mp_ h1_phi
State after:
case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ (h1_phi.imp_ (P.imp_ h1_phi))

case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ h1_phi

State before:
case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ (h1_phi.imp_ (P.imp_ h1_phi))
Tactic:
apply IsDeduct.axiom_
State after:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsAxiom (h1_phi.imp_ (P.imp_ h1_phi))

State before:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsAxiom (h1_phi.imp_ (P.imp_ h1_phi))
Tactic:
exact IsAxiom.prop_1_ h1_phi P
State after:
no goals

State before:
case a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct Δ h1_phi
Tactic:
apply IsDeduct.assume_
State after:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ

State before:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ
Tactic:
exact h1_1
State after:
no goals

State before:
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ (P.imp_ h1_psi)
Tactic:
apply IsDeduct.mp_ (P.imp_ h1_phi)
State after:
case a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ ((P.imp_ h1_phi).imp_ (P.imp_ h1_psi))

case a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ (P.imp_ h1_phi)

State before:
case a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ ((P.imp_ h1_phi).imp_ (P.imp_ h1_psi))
Tactic:
apply IsDeduct.mp_ (P.imp_ (h1_phi.imp_ h1_psi))
State after:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ ((P.imp_ (h1_phi.imp_ h1_psi)).imp_ ((P.imp_ h1_phi).imp_ (P.imp_ h1_psi)))

case a.a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))

State before:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ ((P.imp_ (h1_phi.imp_ h1_psi)).imp_ ((P.imp_ h1_phi).imp_ (P.imp_ h1_psi)))
Tactic:
apply IsDeduct.axiom_
State after:
case a.a.a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsAxiom ((P.imp_ (h1_phi.imp_ h1_psi)).imp_ ((P.imp_ h1_phi).imp_ (P.imp_ h1_psi)))

State before:
case a.a.a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsAxiom ((P.imp_ (h1_phi.imp_ h1_psi)).imp_ ((P.imp_ h1_phi).imp_ (P.imp_ h1_psi)))
Tactic:
exact IsAxiom.prop_2_ P h1_phi h1_psi
State after:
no goals

State before:
case a.a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
Tactic:
exact h1_ih_1
State after:
no goals

State before:
case a
P Q : Formula
Δ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct (Δ ∪ {P}) (h1_phi.imp_ h1_psi)
a✝ : IsDeduct (Δ ∪ {P}) h1_phi
h1_ih_1 : IsDeduct Δ (P.imp_ (h1_phi.imp_ h1_psi))
h1_ih_2 : IsDeduct Δ (P.imp_ h1_phi)
⊢ IsDeduct Δ (P.imp_ h1_phi)
Tactic:
exact h1_ih_2
State after:
no goals