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

State before:
l : List Form
f g : Form
⊢ BProof { h | h = f ∨ h ∈ l } g → BProof {Form.conjoinList f l} g
Tactic:
intros prf₁
State after:
l : List Form
f g : Form
prf₁ : BProof { h | h = f ∨ h ∈ l } g
⊢ BProof {Form.conjoinList f l} g

State before:
l : List Form
f g : Form
prf₁ : BProof { h | h = f ∨ h ∈ l } g
⊢ BProof {Form.conjoinList f l} g
Tactic:
induction prf₁
State after:
case ax
l : List Form
f g p✝ : Form
h✝ : p✝ ∈ { h | h = f ∨ h ∈ l }
⊢ BProof {Form.conjoinList f l} p✝

case mp
l : List Form
f g p✝ q✝ : Form
h₁✝ : BProof { h | h = f ∨ h ∈ l } p✝
h₂✝ : BTheorem (p✝⊃q✝)
h₁_ih✝ : BProof {Form.conjoinList f l} p✝
⊢ BProof {Form.conjoinList f l} q✝

case adj
l : List Form
f g p✝ q✝ : Form
h₁✝ : BProof { h | h = f ∨ h ∈ l } p✝
h₂✝ : BProof { h | h = f ∨ h ∈ l } q✝
h₁_ih✝ : BProof {Form.conjoinList f l} p✝
h₂_ih✝ : BProof {Form.conjoinList f l} q✝
⊢ BProof {Form.conjoinList f l} (p✝&q✝)

State before:
l : List Form
f g p : Form
h₁ : p ∈ { h | h = f ∨ h ∈ l }
⊢ BProof {Form.conjoinList f l} p
Tactic:
case ax p h₁ => exact BProof.proveFromList $ List.mem_cons.mpr h₁
State after:
no goals

State before:
l : List Form
f g p q : Form
h₁✝ : BProof { h | h = f ∨ h ∈ l } p
prf₂ : BTheorem (p⊃q)
ih : BProof {Form.conjoinList f l} p
⊢ BProof {Form.conjoinList f l} q
Tactic:
case mp p q _ prf₂ ih => exact BProof.mp ih prf₂
State after:
no goals

State before:
l : List Form
f g p q : Form
h₁✝ : BProof { h | h = f ∨ h ∈ l } p
h₂✝ : BProof { h | h = f ∨ h ∈ l } q
prf₁ : BProof {Form.conjoinList f l} p
prf₂ : BProof {Form.conjoinList f l} q
⊢ BProof {Form.conjoinList f l} (p&q)
Tactic:
case adj p q _ _ prf₁ prf₂  => exact BProof.adj prf₁ prf₂
State after:
no goals

State before:
l : List Form
f g p : Form
h₁ : p ∈ { h | h = f ∨ h ∈ l }
⊢ BProof {Form.conjoinList f l} p
Tactic:
exact BProof.proveFromList $ List.mem_cons.mpr h₁
State after:
no goals

State before:
l : List Form
f g p q : Form
h₁✝ : BProof { h | h = f ∨ h ∈ l } p
prf₂ : BTheorem (p⊃q)
ih : BProof {Form.conjoinList f l} p
⊢ BProof {Form.conjoinList f l} q
Tactic:
exact BProof.mp ih prf₂
State after:
no goals

State before:
l : List Form
f g p q : Form
h₁✝ : BProof { h | h = f ∨ h ∈ l } p
h₂✝ : BProof { h | h = f ∨ h ∈ l } q
prf₁ : BProof {Form.conjoinList f l} p
prf₂ : BProof {Form.conjoinList f l} q
⊢ BProof {Form.conjoinList f l} (p&q)
Tactic:
exact BProof.adj prf₁ prf₂
State after:
no goals