Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.subset_axiomset (Logic/Modal/Standard/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
⊢ Ax(L) ⊆ Ω.theory
Tactic:
intro p hp
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ p : Formula α
hp : p ∈ Ax(L)
⊢ p ∈ Ω.theory

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ p : Formula α
hp : p ∈ Ax(L)
⊢ p ∈ Ω.theory
Tactic:
apply membership_iff.mpr
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ p : Formula α
hp : p ∈ Ax(L)
⊢ Ω.theory *⊢[L]! p

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ p : Formula α
hp : p ∈ Ax(L)
⊢ Ω.theory *⊢[L]! p
Tactic:
apply Context.of!
State after:
case b
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ p : Formula α
hp : p ∈ Ax(L)
⊢ L ⊢! p

State before:
case b
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ p : Formula α
hp : p ∈ Ax(L)
⊢ L ⊢! p
Tactic:
exact ⟨Deduction.maxm (by aesop)⟩
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p✝ p : Formula α
hp : p ∈ Ax(L)
⊢ p ∈ Ax(L)
Tactic:
aesop
State after:
no goals