Theorem: IntuitionisticPropositionalLogic.deduction_theorem (GlimpseOfLean/Solutions/Topics/IntuitionisticPropositionalLogic.lean)

State before:
H : Type ?u.36610
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ insert (A ⇒ B) Γ ⊢ B
Tactic:
apply impE (ax $ mem_insert _ _)
State after:
H : Type ?u.36610
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ insert (A ⇒ B) Γ ⊢ A

State before:
H : Type ?u.36610
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ insert (A ⇒ B) Γ ⊢ A
Tactic:
exact h.insert
State after:
no goals