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

State before:
α : Type u_1
inst✝ : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
hNec : 𝓓₁.rules ≤ 𝓓₂.rules
hAx : autoParam (Ax(𝓓₁) ⊆ Ax(𝓓₂)) _auto✝
⊢ 𝓓₁ ≤ₛ 𝓓₂
Tactic:
intro p hp
State after:
α : Type u_1
inst✝ : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
hNec : 𝓓₁.rules ≤ 𝓓₂.rules
hAx : autoParam (Ax(𝓓₁) ⊆ Ax(𝓓₂)) _auto✝
p : Formula α
hp : p ∈ System.theory 𝓓₁
⊢ p ∈ System.theory 𝓓₂

State before:
α : Type u_1
inst✝ : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
hNec : 𝓓₁.rules ≤ 𝓓₂.rules
hAx : autoParam (Ax(𝓓₁) ⊆ Ax(𝓓₂)) _auto✝
p : Formula α
hp : p ∈ System.theory 𝓓₁
⊢ p ∈ System.theory 𝓓₂
Tactic:
apply maxm_subset! hNec hAx hp
State after:
no goals