Theorem: ClassicalPropositionalLogic.ProvableFrom.insert (GlimpseOfLean/Solutions/Topics/ClassicalPropositionalLogic.lean)

State before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Insert.insert B Γ ⊢ A
Tactic:
apply weakening h
State after:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Γ ⊆ Insert.insert B Γ

State before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Γ ⊆ Insert.insert B Γ
Tactic:
exact subset_insert B Γ
State after:
no goals