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

State before:
f g h : Form
⊢ f ∈ ▲{g} ∧ f ∈ ▲{h} → f ∈ ▲{g¦h}
Tactic:
intros h₁
State after:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
⊢ f ∈ ▲{g¦h}

State before:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
⊢ f ∈ ▲{g¦h}
Tactic:
have ⟨⟨prf₁⟩,⟨prf₂⟩⟩ := h₁
State after:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
⊢ f ∈ ▲{g¦h}

State before:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
⊢ f ∈ ▲{g¦h}
Tactic:
have l₁ := prf₁.toTheorem
State after:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
l₁ : BTheorem (g⊃f)
⊢ f ∈ ▲{g¦h}

State before:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
l₁ : BTheorem (g⊃f)
⊢ f ∈ ▲{g¦h}
Tactic:
have l₂ := prf₂.toTheorem
State after:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
l₁ : BTheorem (g⊃f)
l₂ : BTheorem (h⊃f)
⊢ f ∈ ▲{g¦h}

State before:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
l₁ : BTheorem (g⊃f)
l₂ : BTheorem (h⊃f)
⊢ f ∈ ▲{g¦h}
Tactic:
have l₃ := (BTheorem.mp (BTheorem.adj l₁ l₂) BTheorem.orE)
State after:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
l₁ : BTheorem (g⊃f)
l₂ : BTheorem (h⊃f)
l₃ : BTheorem (g¦h⊃f)
⊢ f ∈ ▲{g¦h}

State before:
f g h : Form
h₁ : f ∈ ▲{g} ∧ f ∈ ▲{h}
prf₁ : BProof {g} f
prf₂ : BProof {h} f
l₁ : BTheorem (g⊃f)
l₂ : BTheorem (h⊃f)
l₃ : BTheorem (g¦h⊃f)
⊢ f ∈ ▲{g¦h}
Tactic:
exact ⟨l₃.toProof⟩
State after:
no goals