Theorem: Pos.mul_le_mul (Extra/Pos/Lemmas.lean)

State before:
x₁ y₁ x₂ y₂ : Pos
⊢ x₁ ≤ y₁ → x₂ ≤ y₂ → x₁ * x₂ ≤ y₁ * y₂
Tactic:
by_toNat
State after:
x₁ y₁ x₂ y₂ : Pos
⊢ y₁.toNat ≥ x₁.toNat → y₂.toNat ≥ x₂.toNat → y₁.toNat * y₂.toNat ≥ x₁.toNat * x₂.toNat

State before:
x₁ y₁ x₂ y₂ : Pos
⊢ y₁.toNat ≥ x₁.toNat → y₂.toNat ≥ x₂.toNat → y₁.toNat * y₂.toNat ≥ x₁.toNat * x₂.toNat
Tactic:
exact Nat.mul_le_mul
State after:
no goals