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

State before:
α : Type u_1
inst✝ : DecidableEq α
𝓓 𝓓₁ 𝓓₂ : DeductionParameter α
h : 𝓓₁.rules = 𝓓₂.rules
⊢ ((𝓓₁ ⊔ 𝓓₂) h).rules = 𝓓₂.rules
Tactic:
cases 𝓓₂
State after:
case mk
α : Type u_1
inst✝ : DecidableEq α
𝓓 𝓓₁ : DeductionParameter α
axiomSet✝ : AxiomSet α
rules✝ : DeductionParameterRules
h : 𝓓₁.rules = { axiomSet := axiomSet✝, rules := rules✝ }.rules
⊢ ((𝓓₁ ⊔ { axiomSet := axiomSet✝, rules := rules✝ }) h).rules = { axiomSet := axiomSet✝, rules := rules✝ }.rules

State before:
case mk
α : Type u_1
inst✝ : DecidableEq α
𝓓 𝓓₁ : DeductionParameter α
axiomSet✝ : AxiomSet α
rules✝ : DeductionParameterRules
h : 𝓓₁.rules = { axiomSet := axiomSet✝, rules := rules✝ }.rules
⊢ ((𝓓₁ ⊔ { axiomSet := axiomSet✝, rules := rules✝ }) h).rules = { axiomSet := axiomSet✝, rules := rules✝ }.rules
Tactic:
exact h
State after:
no goals