Theorem: LO.Modal.Standard.normal_reducible_subset (Logic/Modal/Standard/Deduction.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hSubset : Ax(𝓓₁) ⊆ Ax(𝓓₂)
⊢ 𝓓₁ ≤ₛ 𝓓₂
Tactic:
apply normal_reducible
State after:
case hMaxm
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hSubset : Ax(𝓓₁) ⊆ Ax(𝓓₂)
⊢ ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p

State before:
case hMaxm
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hSubset : Ax(𝓓₁) ⊆ Ax(𝓓₂)
⊢ ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
Tactic:
intro p hp
State after:
case hMaxm
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hSubset : Ax(𝓓₁) ⊆ Ax(𝓓₂)
p : Formula α
hp : p ∈ Ax(𝓓₁)
⊢ 𝓓₂ ⊢! p

State before:
case hMaxm
α : Type u_1
inst✝² : DecidableEq α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hSubset : Ax(𝓓₁) ⊆ Ax(𝓓₂)
p : Formula α
hp : p ∈ Ax(𝓓₁)
⊢ 𝓓₂ ⊢! p
Tactic:
exact ⟨Deduction.maxm $ hSubset hp⟩
State after:
no goals