Theorem: BisFormal (Fine/SystemB/Theories.lean)

State before:
⊢ formalTheory BTheory
Tactic:
intros f
State after:
f : Form
⊢ f ∈ BTheory ↔ BTheory⊢f

State before:
f : Form
⊢ f ∈ BTheory ↔ BTheory⊢f
Tactic:
apply Iff.intro
State after:
case mp
f : Form
⊢ f ∈ BTheory → BTheory⊢f

case mpr
f : Form
⊢ BTheory⊢f → f ∈ BTheory

State before:
f P Q : Form
prf₁ : BProof BTheory P
thm₁ : BTheorem (P⊃Q)
ih : BTheory⊢P → P ∈ BTheory
h₁ : BTheory⊢Q
⊢ Q ∈ BTheory
Tactic:
have l₁ := ih ⟨prf₁⟩
State after:
f P Q : Form
prf₁ : BProof BTheory P
thm₁ : BTheorem (P⊃Q)
ih : BTheory⊢P → P ∈ BTheory
h₁ : BTheory⊢Q
l₁ : P ∈ BTheory
⊢ Q ∈ BTheory

State before:
f P Q : Form
prf₁ : BProof BTheory P
thm₁ : BTheorem (P⊃Q)
ih : BTheory⊢P → P ∈ BTheory
h₁ : BTheory⊢Q
l₁ : P ∈ BTheory
⊢ Q ∈ BTheory
Tactic:
have ⟨thm₂⟩ := l₁
State after:
f P Q : Form
prf₁ : BProof BTheory P
thm₁ : BTheorem (P⊃Q)
ih : BTheory⊢P → P ∈ BTheory
h₁ : BTheory⊢Q
l₁ : P ∈ BTheory
thm₂ : BTheorem P
⊢ Q ∈ BTheory

State before:
f P Q : Form
prf₁ : BProof BTheory P
thm₁ : BTheorem (P⊃Q)
ih : BTheory⊢P → P ∈ BTheory
h₁ : BTheory⊢Q
l₁ : P ∈ BTheory
thm₂ : BTheorem P
⊢ Q ∈ BTheory
Tactic:
exact ⟨BTheorem.mp thm₂ thm₁⟩
State after:
no goals

State before:
f P Q : Form
prf₁ : BProof BTheory P
prf₂ : BProof BTheory Q
ih₁ : BTheory⊢P → P ∈ BTheory
ih₂ : BTheory⊢Q → Q ∈ BTheory
h₁ : BTheory⊢P&Q
⊢ P&Q ∈ BTheory
Tactic:
have ⟨l₁⟩ := ih₁ ⟨prf₁⟩
State after:
f P Q : Form
prf₁ : BProof BTheory P
prf₂ : BProof BTheory Q
ih₁ : BTheory⊢P → P ∈ BTheory
ih₂ : BTheory⊢Q → Q ∈ BTheory
h₁ : BTheory⊢P&Q
l₁ : BTheorem P
⊢ P&Q ∈ BTheory

State before:
f P Q : Form
prf₁ : BProof BTheory P
prf₂ : BProof BTheory Q
ih₁ : BTheory⊢P → P ∈ BTheory
ih₂ : BTheory⊢Q → Q ∈ BTheory
h₁ : BTheory⊢P&Q
l₁ : BTheorem P
⊢ P&Q ∈ BTheory
Tactic:
have ⟨l₂⟩ := ih₂ ⟨prf₂⟩
State after:
f P Q : Form
prf₁ : BProof BTheory P
prf₂ : BProof BTheory Q
ih₁ : BTheory⊢P → P ∈ BTheory
ih₂ : BTheory⊢Q → Q ∈ BTheory
h₁ : BTheory⊢P&Q
l₁ : BTheorem P
l₂ : BTheorem Q
⊢ P&Q ∈ BTheory

State before:
f P Q : Form
prf₁ : BProof BTheory P
prf₂ : BProof BTheory Q
ih₁ : BTheory⊢P → P ∈ BTheory
ih₂ : BTheory⊢Q → Q ∈ BTheory
h₁ : BTheory⊢P&Q
l₁ : BTheorem P
l₂ : BTheorem Q
⊢ P&Q ∈ BTheory
Tactic:
exact ⟨BTheorem.adj l₁ l₂⟩
State after:
no goals