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

State before:
α : Type u_1
inst✝ : DecidableEq α
R₁ R₂ : DeductionParameterRules
h : autoParam (R₁ ≤ R₂) _auto✝
hNec : R₁.nec = true
⊢ R₂.nec = true
Tactic:
apply h.1
State after:
α : Type u_1
inst✝ : DecidableEq α
R₁ R₂ : DeductionParameterRules
h : autoParam (R₁ ≤ R₂) _auto✝
hNec : R₁.nec = true
⊢ R₁.nec = true

State before:
α : Type u_1
inst✝ : DecidableEq α
R₁ R₂ : DeductionParameterRules
h : autoParam (R₁ ≤ R₂) _auto✝
hNec : R₁.nec = true
⊢ R₁.nec = true
Tactic:
assumption
State after:
no goals