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

State before:
⊢ ∀ (Γ : Ctx), formalTheory (▲Γ)
Tactic:
unfold formalTheory
State after:
⊢ ∀ (Γ : Ctx) {f : Form}, f ∈ ▲Γ ↔ ▲Γ⊢f

State before:
⊢ ∀ (Γ : Ctx) {f : Form}, f ∈ ▲Γ ↔ ▲Γ⊢f
Tactic:
intros Γ f
State after:
Γ : Ctx
f : Form
⊢ f ∈ ▲Γ ↔ ▲Γ⊢f

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

case mpr
Γ : Ctx
f : Form
⊢ ▲Γ⊢f → f ∈ ▲Γ

State before:
Γ : Ctx
f : Form
⊢ f ∈ ▲Γ → ▲Γ⊢f
Tactic:
case mp => 
   intros h₁
   exact Nonempty.intro $ BProof.ax h₁
State after:
no goals

State before:
Γ : Ctx
f : Form
⊢ ▲Γ⊢f → f ∈ ▲Γ
Tactic:
case mpr =>
  intros h₁  
  have ⟨w⟩ := h₁
  induction w
  case ax => assumption
  case mp P Q prf thm ih => 
    have ⟨prf₂⟩ := ih ⟨prf⟩
    exact ⟨BProof.mp prf₂ thm⟩
  case adj P Q prf₁ prf₂ ih₁ ih₂ => 
    have ⟨prf₃⟩ := ih₁ ⟨prf₁⟩
    have ⟨prf₄⟩ := ih₂ ⟨prf₂⟩
    exact ⟨BProof.adj prf₃ prf₄⟩
State after:
no goals

State before:
Γ : Ctx
f : Form
⊢ f ∈ ▲Γ → ▲Γ⊢f
Tactic:
intros h₁
State after:
Γ : Ctx
f : Form
h₁ : f ∈ ▲Γ
⊢ ▲Γ⊢f

State before:
Γ : Ctx
f : Form
h₁ : f ∈ ▲Γ
⊢ ▲Γ⊢f
Tactic:
exact Nonempty.intro $ BProof.ax h₁
State after:
no goals

State before:
Γ : Ctx
f : Form
⊢ ▲Γ⊢f → f ∈ ▲Γ
Tactic:
intros h₁
State after:
Γ : Ctx
f : Form
h₁ : ▲Γ⊢f
⊢ f ∈ ▲Γ

State before:
Γ : Ctx
f : Form
h₁ : ▲Γ⊢f
⊢ f ∈ ▲Γ
Tactic:
have ⟨w⟩ := h₁
State after:
Γ : Ctx
f : Form
h₁ : ▲Γ⊢f
w : BProof (▲Γ) f
⊢ f ∈ ▲Γ

State before:
Γ : Ctx
f : Form
h₁ : ▲Γ⊢f
w : BProof (▲Γ) f
⊢ f ∈ ▲Γ
Tactic:
induction w
State after:
case ax
Γ : Ctx
f p✝ : Form
h✝ : p✝ ∈ ▲Γ
h₁ : ▲Γ⊢p✝
⊢ p✝ ∈ ▲Γ

case mp
Γ : Ctx
f p✝ q✝ : Form
h₁✝ : BProof (▲Γ) p✝
h₂✝ : BTheorem (p✝⊃q✝)
h₁_ih✝ : ▲Γ⊢p✝ → p✝ ∈ ▲Γ
h₁ : ▲Γ⊢q✝
⊢ q✝ ∈ ▲Γ

case adj
Γ : Ctx
f p✝ q✝ : Form
h₁✝ : BProof (▲Γ) p✝
h₂✝ : BProof (▲Γ) q✝
h₁_ih✝ : ▲Γ⊢p✝ → p✝ ∈ ▲Γ
h₂_ih✝ : ▲Γ⊢q✝ → q✝ ∈ ▲Γ
h₁ : ▲Γ⊢p✝&q✝
⊢ p✝&q✝ ∈ ▲Γ

State before:
Γ : Ctx
f p✝ : Form
h✝ : p✝ ∈ ▲Γ
h₁ : ▲Γ⊢p✝
⊢ p✝ ∈ ▲Γ
Tactic:
case ax => assumption
State after:
no goals

State before:
Γ : Ctx
f P Q : Form
prf : BProof (▲Γ) P
thm : BTheorem (P⊃Q)
ih : ▲Γ⊢P → P ∈ ▲Γ
h₁ : ▲Γ⊢Q
⊢ Q ∈ ▲Γ
Tactic:
case mp P Q prf thm ih => 
  have ⟨prf₂⟩ := ih ⟨prf⟩
  exact ⟨BProof.mp prf₂ thm⟩
State after:
no goals

State before:
Γ : Ctx
f P Q : Form
prf₁ : BProof (▲Γ) P
prf₂ : BProof (▲Γ) Q
ih₁ : ▲Γ⊢P → P ∈ ▲Γ
ih₂ : ▲Γ⊢Q → Q ∈ ▲Γ
h₁ : ▲Γ⊢P&Q
⊢ P&Q ∈ ▲Γ
Tactic:
case adj P Q prf₁ prf₂ ih₁ ih₂ => 
  have ⟨prf₃⟩ := ih₁ ⟨prf₁⟩
  have ⟨prf₄⟩ := ih₂ ⟨prf₂⟩
  exact ⟨BProof.adj prf₃ prf₄⟩
State after:
no goals

State before:
Γ : Ctx
f p✝ : Form
h✝ : p✝ ∈ ▲Γ
h₁ : ▲Γ⊢p✝
⊢ p✝ ∈ ▲Γ
Tactic:
assumption
State after:
no goals

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

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

State before:
Γ : Ctx
f P Q : Form
prf₁ : BProof (▲Γ) P
prf₂ : BProof (▲Γ) Q
ih₁ : ▲Γ⊢P → P ∈ ▲Γ
ih₂ : ▲Γ⊢Q → Q ∈ ▲Γ
h₁ : ▲Γ⊢P&Q
⊢ P&Q ∈ ▲Γ
Tactic:
have ⟨prf₃⟩ := ih₁ ⟨prf₁⟩
State after:
Γ : Ctx
f P Q : Form
prf₁ : BProof (▲Γ) P
prf₂ : BProof (▲Γ) Q
ih₁ : ▲Γ⊢P → P ∈ ▲Γ
ih₂ : ▲Γ⊢Q → Q ∈ ▲Γ
h₁ : ▲Γ⊢P&Q
prf₃ : BProof Γ P
⊢ P&Q ∈ ▲Γ

State before:
Γ : Ctx
f P Q : Form
prf₁ : BProof (▲Γ) P
prf₂ : BProof (▲Γ) Q
ih₁ : ▲Γ⊢P → P ∈ ▲Γ
ih₂ : ▲Γ⊢Q → Q ∈ ▲Γ
h₁ : ▲Γ⊢P&Q
prf₃ : BProof Γ P
⊢ P&Q ∈ ▲Γ
Tactic:
have ⟨prf₄⟩ := ih₂ ⟨prf₂⟩
State after:
Γ : Ctx
f P Q : Form
prf₁ : BProof (▲Γ) P
prf₂ : BProof (▲Γ) Q
ih₁ : ▲Γ⊢P → P ∈ ▲Γ
ih₂ : ▲Γ⊢Q → Q ∈ ▲Γ
h₁ : ▲Γ⊢P&Q
prf₃ : BProof Γ P
prf₄ : BProof Γ Q
⊢ P&Q ∈ ▲Γ

State before:
Γ : Ctx
f P Q : Form
prf₁ : BProof (▲Γ) P
prf₂ : BProof (▲Γ) Q
ih₁ : ▲Γ⊢P → P ∈ ▲Γ
ih₂ : ▲Γ⊢Q → Q ∈ ▲Γ
h₁ : ▲Γ⊢P&Q
prf₃ : BProof Γ P
prf₄ : BProof Γ Q
⊢ P&Q ∈ ▲Γ
Tactic:
exact ⟨BProof.adj prf₃ prf₄⟩
State after:
no goals