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

State before:
F : Formula
Δ : Set Formula
h1 : IsDeduct Δ F
⊢ ∀ (Γ : Set Formula), IsDeduct (Δ ∪ Γ) F
Tactic:
intro Γ
State after:
F : Formula
Δ : Set Formula
h1 : IsDeduct Δ F
Γ : Set Formula
⊢ IsDeduct (Δ ∪ Γ) F

State before:
F : Formula
Δ : Set Formula
h1 : IsDeduct Δ F
Γ : Set Formula
⊢ IsDeduct (Δ ∪ Γ) F
Tactic:
induction h1
State after:
case axiom_
F : Formula
Δ Γ : Set Formula
phi✝ : Formula
a✝ : IsAxiom phi✝
⊢ IsDeduct (Δ ∪ Γ) phi✝

case assume_
F : Formula
Δ Γ : Set Formula
phi✝ : Formula
a✝ : phi✝ ∈ Δ
⊢ IsDeduct (Δ ∪ Γ) phi✝

case mp_
F : Formula
Δ Γ : Set Formula
phi✝ psi✝ : Formula
a✝¹ : IsDeduct Δ (phi✝.imp_ psi✝)
a✝ : IsDeduct Δ phi✝
a_ih✝¹ : IsDeduct (Δ ∪ Γ) (phi✝.imp_ psi✝)
a_ih✝ : IsDeduct (Δ ∪ Γ) phi✝
⊢ IsDeduct (Δ ∪ Γ) psi✝

State before:
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct (Δ ∪ Γ) h1_phi
Tactic:
case axiom_ h1_phi h1_1 =>
  apply IsDeduct.axiom_
  exact h1_1
State after:
no goals

State before:
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct (Δ ∪ Γ) h1_phi
Tactic:
case assume_ h1_phi h1_1 =>
  apply IsDeduct.assume_
  simp
  left
  exact h1_1
State after:
no goals

State before:
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsDeduct (Δ ∪ Γ) h1_phi
Tactic:
apply IsDeduct.axiom_
State after:
case a
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom h1_phi

State before:
case a
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : IsAxiom h1_phi
⊢ IsAxiom h1_phi
Tactic:
exact h1_1
State after:
no goals

State before:
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ IsDeduct (Δ ∪ Γ) h1_phi
Tactic:
apply IsDeduct.assume_
State after:
case a
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ ∪ Γ

State before:
case a
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ ∪ Γ
Tactic:
simp
State after:
case a
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ ∨ h1_phi ∈ Γ

State before:
case a
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ ∨ h1_phi ∈ Γ
Tactic:
left
State after:
case a.h
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ

State before:
case a.h
F : Formula
Δ Γ : Set Formula
h1_phi : Formula
h1_1 : h1_phi ∈ Δ
⊢ h1_phi ∈ Δ
Tactic:
exact h1_1
State after:
no goals

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

case a
F : Formula
Δ Γ : Set Formula
h1_phi h1_psi : Formula
a✝¹ : IsDeduct Δ (h1_phi.imp_ h1_psi)
a✝ : IsDeduct Δ h1_phi
h1_ih_1 : IsDeduct (Δ ∪ Γ) (h1_phi.imp_ h1_psi)
h1_ih_2 : IsDeduct (Δ ∪ Γ) h1_phi
⊢ IsDeduct (Δ ∪ Γ) h1_phi

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

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