Theorem: LO.Propositional.Superintuitionistic.SaturatedConsistentTableau.mem₁_of_provable (Logic/Propositional/Superintuitionistic/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p : Formula α
⊢ 𝓓 ⊢! p → p ∈ t.tableau.1
Tactic:
intro h
State after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p : Formula α
h : 𝓓 ⊢! p
⊢ p ∈ t.tableau.1

State before:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Encodable α
t✝ t t₁ t₂ : SCT 𝓓
p : Formula α
h : 𝓓 ⊢! p
⊢ p ∈ t.tableau.1
Tactic:
exact mdp₁ mem₁_verum $ dhyp! h
State after:
no goals