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

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

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