Theorem: BProof.compactness (Fine/SystemB/Hilbert.lean)

State before:
Γ : Ctx
f : Form
⊢ BProof Γ f → (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) f
Tactic:
intros prf₁
State after:
Γ : Ctx
f : Form
prf₁ : BProof Γ f
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) f

State before:
Γ : Ctx
f : Form
prf₁ : BProof Γ f
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) f
Tactic:
induction prf₁
State after:
case ax
Γ : Ctx
f p✝ : Form
h✝ : p✝ ∈ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) p✝

case mp
Γ : Ctx
f p✝ q✝ : Form
h₁✝ : BProof Γ p✝
h₂✝ : BTheorem (p✝⊃q✝)
h₁_ih✝ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) p✝
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) q✝

case adj
Γ : Ctx
f p✝ q✝ : Form
h₁✝ : BProof Γ p✝
h₂✝ : BProof Γ q✝
h₁_ih✝ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) p✝
h₂_ih✝ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) q✝
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (p✝&q✝)

State before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Tactic:
case ax g h₁ => 
  let Gsing : Finset Form := {g} 
  have l₁ : g ∈ {g} := Finset.mem_singleton.mpr rfl
  have l₂ : Gsing = ({g} : Ctx) := Finset.coe_singleton g
  have l₃ : ↑Gsing ⊆ Γ := by
    intros g' h₂
    rw [l₂] at h₂
    rw [h₂]
    assumption
  have prf₂ : BProof ↑{g} g := by
    rw [←l₂]
    apply ax l₁
  rw [←l₂] at prf₂
  exact ⟨Gsing, l₃, prf₂⟩
State after:
no goals

State before:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂ : BTheorem (P⊃Q)
ih : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
Tactic:
case mp P Q _ h₂ ih => 
  have ⟨fin, h₁, prf⟩ := ih
  exact ⟨fin, h₁, mp prf h₂⟩
State after:
no goals

State before:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
case adj P Q _ _ ih₁ ih₂ => 
  have ⟨fin₁, h₁, prf₁⟩ := ih₁
  have ⟨fin₂, h₂, prf₂⟩ := ih₂
  have prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P := BProof.monotone (Set.subset_union_left ↑fin₁ ↑fin₂) prf₁
  have prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q := BProof.monotone (Set.subset_union_right ↑fin₁ ↑fin₂) prf₂
  have prf₅ := adj prf₃ prf₄
  have l₁ : ↑(fin₁ ∪ fin₂) ⊆ Γ := by
    intros f h₃
    rw [Finset.coe_union] at h₃
    cases h₃
    case inl h₄ => exact h₁ h₄
    case inr h₄ => exact h₂ h₄
  rw [←Finset.coe_union] at prf₅
  exact ⟨↑(fin₁ ∪ fin₂), l₁, prf₅⟩
State after:
no goals

State before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Tactic:
let Gsing : Finset Form := {g}
State after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g

State before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Tactic:
have l₁ : g ∈ {g} := Finset.mem_singleton.mpr rfl
State after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g

State before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Tactic:
have l₂ : Gsing = ({g} : Ctx) := Finset.coe_singleton g
State after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g

State before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Tactic:
have l₃ : ↑Gsing ⊆ Γ := by
  intros g' h₂
  rw [l₂] at h₂
  rw [h₂]
  assumption
State after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g

State before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Tactic:
have prf₂ : BProof ↑{g} g := by
  rw [←l₂]
  apply ax l₁
State after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
prf₂ : BProof {g} g
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g

State before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
prf₂ : BProof {g} g
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Tactic:
rw [←l₂] at prf₂
State after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
prf₂ : BProof (↑Gsing) g
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g

State before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
prf₂ : BProof (↑Gsing) g
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) g
Tactic:
exact ⟨Gsing, l₃, prf₂⟩
State after:
no goals

State before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
⊢ ↑Gsing ⊆ Γ
Tactic:
intros g' h₂
State after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
g' : Form
h₂ : g' ∈ ↑Gsing
⊢ g' ∈ Γ

State before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
g' : Form
h₂ : g' ∈ ↑Gsing
⊢ g' ∈ Γ
Tactic:
rw [l₂] at h₂
State after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
g' : Form
h₂ : g' ∈ {g}
⊢ g' ∈ Γ

State before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
g' : Form
h₂ : g' ∈ {g}
⊢ g' ∈ Γ
Tactic:
rw [h₂]
State after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
g' : Form
h₂ : g' ∈ {g}
⊢ g ∈ Γ

State before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
g' : Form
h₂ : g' ∈ {g}
⊢ g ∈ Γ
Tactic:
assumption
State after:
no goals

State before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
⊢ BProof {g} g
Tactic:
rw [←l₂]
State after:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
⊢ BProof (↑Gsing) g

State before:
Γ : Ctx
f g : Form
h₁ : g ∈ Γ
Gsing : Finset Form := {g}
l₁ : g ∈ {g}
l₂ : ↑Gsing = {g}
l₃ : ↑Gsing ⊆ Γ
⊢ BProof (↑Gsing) g
Tactic:
apply ax l₁
State after:
no goals

State before:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂ : BTheorem (P⊃Q)
ih : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
Tactic:
have ⟨fin, h₁, prf⟩ := ih
State after:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂ : BTheorem (P⊃Q)
ih : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
fin : Finset Form
h₁ : ↑fin ⊆ Γ
prf : BProof (↑fin) P
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q

State before:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂ : BTheorem (P⊃Q)
ih : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
fin : Finset Form
h₁ : ↑fin ⊆ Γ
prf : BProof (↑fin) P
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
Tactic:
exact ⟨fin, h₁, mp prf h₂⟩
State after:
no goals

State before:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
have ⟨fin₁, h₁, prf₁⟩ := ih₁
State after:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)

State before:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
have ⟨fin₂, h₂, prf₂⟩ := ih₂
State after:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)

State before:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
have prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P := BProof.monotone (Set.subset_union_left ↑fin₁ ↑fin₂) prf₁
State after:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)

State before:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
have prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q := BProof.monotone (Set.subset_union_right ↑fin₁ ↑fin₂) prf₂
State after:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)

State before:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
have prf₅ := adj prf₃ prf₄
State after:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)

State before:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
have l₁ : ↑(fin₁ ∪ fin₂) ⊆ Γ := by
  intros f h₃
  rw [Finset.coe_union] at h₃
  cases h₃
  case inl h₄ => exact h₁ h₄
  case inr h₄ => exact h₂ h₄
State after:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
l₁ : ↑(fin₁ ∪ fin₂) ⊆ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)

State before:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
l₁ : ↑(fin₁ ∪ fin₂) ⊆ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
rw [←Finset.coe_union] at prf₅
State after:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅✝ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
prf₅ : BProof (↑(fin₁ ∪ fin₂)) (P&Q)
l₁ : ↑(fin₁ ∪ fin₂) ⊆ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)

State before:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅✝ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
prf₅ : BProof (↑(fin₁ ∪ fin₂)) (P&Q)
l₁ : ↑(fin₁ ∪ fin₂) ⊆ Γ
⊢ (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) (P&Q)
Tactic:
exact ⟨↑(fin₁ ∪ fin₂), l₁, prf₅⟩
State after:
no goals

State before:
Γ : Ctx
f P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
⊢ ↑(fin₁ ∪ fin₂) ⊆ Γ
Tactic:
intros f h₃
State after:
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h₃ : f ∈ ↑(fin₁ ∪ fin₂)
⊢ f ∈ Γ

State before:
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h₃ : f ∈ ↑(fin₁ ∪ fin₂)
⊢ f ∈ Γ
Tactic:
rw [Finset.coe_union] at h₃
State after:
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h₃ : f ∈ ↑fin₁ ∪ ↑fin₂
⊢ f ∈ Γ

State before:
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h₃ : f ∈ ↑fin₁ ∪ ↑fin₂
⊢ f ∈ Γ
Tactic:
cases h₃
State after:
case inl
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h✝ : f ∈ ↑fin₁
⊢ f ∈ Γ

case inr
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h✝ : f ∈ ↑fin₂
⊢ f ∈ Γ

State before:
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h₄ : f ∈ ↑fin₁
⊢ f ∈ Γ
Tactic:
case inl h₄ => exact h₁ h₄
State after:
no goals

State before:
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h₄ : f ∈ ↑fin₂
⊢ f ∈ Γ
Tactic:
case inr h₄ => exact h₂ h₄
State after:
no goals

State before:
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h₄ : f ∈ ↑fin₁
⊢ f ∈ Γ
Tactic:
exact h₁ h₄
State after:
no goals

State before:
Γ : Ctx
f✝ P Q : Form
h₁✝ : BProof Γ P
h₂✝ : BProof Γ Q
ih₁ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) P
ih₂ : (s : Finset Form) × (_ : ↑s ⊆ Γ) ×' BProof (↑s) Q
fin₁ : Finset Form
h₁ : ↑fin₁ ⊆ Γ
prf₁ : BProof (↑fin₁) P
fin₂ : Finset Form
h₂ : ↑fin₂ ⊆ Γ
prf₂ : BProof (↑fin₂) Q
prf₃ : BProof (↑fin₁ ∪ ↑fin₂) P
prf₄ : BProof (↑fin₁ ∪ ↑fin₂) Q
prf₅ : BProof (↑fin₁ ∪ ↑fin₂) (P&Q)
f : Form
h₄ : f ∈ ↑fin₂
⊢ f ∈ Γ
Tactic:
exact h₂ h₄
State after:
no goals