Theorem: LO.Modal.Standard.DeductionParameter.union_left_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 : { axiomSet := axiomSet✝, rules := 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 : { axiomSet := axiomSet✝, rules := rules✝ }.rules = 𝓓₂.rules
⊢ (({ axiomSet := axiomSet✝, rules := rules✝ } ⊔ 𝓓₂) h).rules = { axiomSet := axiomSet✝, rules := rules✝ }.rules
Tactic:
rfl
State after:
no goals