Theorem: ClassicalPropositionalLogic.Provable.mp (GlimpseOfLean/Solutions/Topics/ClassicalPropositionalLogic.lean)

State before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ Γ ⊢ B
Tactic:
apply impE _ h2
State after:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ Γ ⊢ A ⇒ B

State before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ Γ ⊢ A ⇒ B
Tactic:
apply weakening h1
State after:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ ∅ ⊆ Γ

State before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h1 : Provable (A ⇒ B)
h2 : Γ ⊢ A
⊢ ∅ ⊆ Γ
Tactic:
exact empty_subset Γ
State after:
no goals