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

State before:
α : Type u_1
inst✝² : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
⊢ ((𝓓₁ ⊔ 𝓓₂) ⋯).rules = 𝓓₁.rules
Tactic:
apply union_left_rules
State after:
no goals