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

State before:
Γ : Ctx
Δ : Th
⊢ Γ ⊆ ↑Δ → ▲Γ ⊆ ↑Δ
Tactic:
intros h₁ f h₂
State after:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f : Form
h₂ : f ∈ ▲Γ
⊢ f ∈ ↑Δ

State before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f : Form
h₂ : f ∈ ▲Γ
⊢ f ∈ ↑Δ
Tactic:
have ⟨prf⟩ := h₂
State after:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f : Form
h₂ : f ∈ ▲Γ
prf : BProof Γ f
⊢ f ∈ ↑Δ

State before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f : Form
h₂ : f ∈ ▲Γ
prf : BProof Γ f
⊢ f ∈ ↑Δ
Tactic:
induction prf
State after:
case ax
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p✝ : Form
h✝ : p✝ ∈ Γ
h₂ : p✝ ∈ ▲Γ
⊢ p✝ ∈ ↑Δ

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

case adj
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
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
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p : Form
ih : p ∈ Γ
h₂ : p ∈ ▲Γ
⊢ p ∈ ↑Δ
Tactic:
case ax p ih => exact h₁ ih
State after:
no goals

State before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BTheorem (p⊃q)
ih : p ∈ ▲Γ → p ∈ ↑Δ
h₂ : q ∈ ▲Γ
⊢ q ∈ ↑Δ
Tactic:
case mp p q prf₁ prf₂ ih => 
  have l₁ := ih ⟨prf₁⟩
  have ⟨prf₃⟩ := Δ.property.mp l₁
  exact Δ.property.mpr ⟨BProof.mp prf₃ prf₂⟩
State after:
no goals

State before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
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 l₁ := ih₁ ⟨prf₁⟩
  have l₂ := ih₂ ⟨prf₂⟩
  have ⟨prf₃⟩ := Δ.property.mp l₁
  have ⟨prf₄⟩ := Δ.property.mp l₂
  exact Δ.property.mpr ⟨BProof.adj prf₃ prf₄⟩
State after:
no goals

State before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p : Form
ih : p ∈ Γ
h₂ : p ∈ ▲Γ
⊢ p ∈ ↑Δ
Tactic:
exact h₁ ih
State after:
no goals

State before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BTheorem (p⊃q)
ih : p ∈ ▲Γ → p ∈ ↑Δ
h₂ : q ∈ ▲Γ
⊢ q ∈ ↑Δ
Tactic:
have l₁ := ih ⟨prf₁⟩
State after:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BTheorem (p⊃q)
ih : p ∈ ▲Γ → p ∈ ↑Δ
h₂ : q ∈ ▲Γ
l₁ : p ∈ ↑Δ
⊢ q ∈ ↑Δ

State before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BTheorem (p⊃q)
ih : p ∈ ▲Γ → p ∈ ↑Δ
h₂ : q ∈ ▲Γ
l₁ : p ∈ ↑Δ
⊢ q ∈ ↑Δ
Tactic:
have ⟨prf₃⟩ := Δ.property.mp l₁
State after:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BTheorem (p⊃q)
ih : p ∈ ▲Γ → p ∈ ↑Δ
h₂ : q ∈ ▲Γ
l₁ : p ∈ ↑Δ
prf₃ : BProof (↑Δ) p
⊢ q ∈ ↑Δ

State before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BTheorem (p⊃q)
ih : p ∈ ▲Γ → p ∈ ↑Δ
h₂ : q ∈ ▲Γ
l₁ : p ∈ ↑Δ
prf₃ : BProof (↑Δ) p
⊢ q ∈ ↑Δ
Tactic:
exact Δ.property.mpr ⟨BProof.mp prf₃ prf₂⟩
State after:
no goals

State before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
⊢ p&q ∈ ↑Δ
Tactic:
have l₁ := ih₁ ⟨prf₁⟩
State after:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
l₁ : p ∈ ↑Δ
⊢ p&q ∈ ↑Δ

State before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
l₁ : p ∈ ↑Δ
⊢ p&q ∈ ↑Δ
Tactic:
have l₂ := ih₂ ⟨prf₂⟩
State after:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
l₁ : p ∈ ↑Δ
l₂ : q ∈ ↑Δ
⊢ p&q ∈ ↑Δ

State before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
l₁ : p ∈ ↑Δ
l₂ : q ∈ ↑Δ
⊢ p&q ∈ ↑Δ
Tactic:
have ⟨prf₃⟩ := Δ.property.mp l₁
State after:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
l₁ : p ∈ ↑Δ
l₂ : q ∈ ↑Δ
prf₃ : BProof (↑Δ) p
⊢ p&q ∈ ↑Δ

State before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
l₁ : p ∈ ↑Δ
l₂ : q ∈ ↑Δ
prf₃ : BProof (↑Δ) p
⊢ p&q ∈ ↑Δ
Tactic:
have ⟨prf₄⟩ := Δ.property.mp l₂
State after:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
l₁ : p ∈ ↑Δ
l₂ : q ∈ ↑Δ
prf₃ : BProof (↑Δ) p
prf₄ : BProof (↑Δ) q
⊢ p&q ∈ ↑Δ

State before:
Γ : Ctx
Δ : Th
h₁ : Γ ⊆ ↑Δ
f p q : Form
prf₁ : BProof Γ p
prf₂ : BProof Γ q
ih₁ : p ∈ ▲Γ → p ∈ ↑Δ
ih₂ : q ∈ ▲Γ → q ∈ ↑Δ
h₂ : p&q ∈ ▲Γ
l₁ : p ∈ ↑Δ
l₂ : q ∈ ↑Δ
prf₃ : BProof (↑Δ) p
prf₄ : BProof (↑Δ) q
⊢ p&q ∈ ↑Δ
Tactic:
exact Δ.property.mpr ⟨BProof.adj prf₃ prf₄⟩
State after:
no goals